# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1311039005 -3600
# Node ID c62e268304200289d85c5339bf39f17857f377ac
# Parent  b95a2065aa10f0b3b9222a3fd90044b4ced0d9af
preliminary version of automatically generation the eqvt-lemmas for functions defined with nominal_primrec

diff -r b95a2065aa10 -r c62e26830420 Nominal/Ex/Classical.thy
--- a/Nominal/Ex/Classical.thy	Tue Jul 19 01:40:36 2011 +0100
+++ b/Nominal/Ex/Classical.thy	Tue Jul 19 02:30:05 2011 +0100
@@ -382,17 +382,8 @@
 termination (eqvt)
   by lexicographic_order
 
-lemma crename_name_eqvt[eqvt]:
-  shows "p \<bullet> (M[d\<turnstile>c>e]) = (p \<bullet> M)[(p \<bullet> d)\<turnstile>c>(p \<bullet> e)]"
-apply(nominal_induct M avoiding: d e rule: trm.strong_induct)
-apply(auto)
-done
+thm crename.eqvt nrename.eqvt
 
-lemma nrename_name_eqvt[eqvt]:
-  shows "p \<bullet> (M[x\<turnstile>n>y]) = (p \<bullet> M)[(p \<bullet> x)\<turnstile>n>(p \<bullet> y)]"
-apply(nominal_induct M avoiding: x y rule: trm.strong_induct)
-apply(auto)
-done
 
 nominal_primrec 
   substn :: "trm \<Rightarrow> name   \<Rightarrow> coname \<Rightarrow> trm \<Rightarrow> trm" ("_{_:=<_>._}" [100,100,100,100] 100) 
diff -r b95a2065aa10 -r c62e26830420 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Tue Jul 19 01:40:36 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Tue Jul 19 02:30:05 2011 +0100
@@ -45,18 +45,10 @@
 
 termination (eqvt) by lexicographic_order
 
-ML {*
-Item_Net.content (Nominal_Function_Common.get_function @{context})
-*}
-
 thm is_app_def
+thm is_app.eqvt
 
-
-lemma [eqvt]:
-  shows "(p \<bullet> (is_app t)) = is_app (p \<bullet> t)"
-apply(induct t rule: lam.induct)
-apply(simp_all add: permute_bool_def)
-done
+thm eqvts
 
 nominal_primrec 
   rator :: "lam \<Rightarrow> lam option"
@@ -74,12 +66,6 @@
 
 termination (eqvt) by lexicographic_order
 
-lemma [eqvt]:
-  shows "(p \<bullet> (rator t)) = rator (p \<bullet> t)"
-apply(induct t rule: lam.induct)
-apply(simp_all)
-done
-
 nominal_primrec 
   rand :: "lam \<Rightarrow> lam option"
 where
@@ -96,12 +82,6 @@
 
 termination (eqvt) by lexicographic_order
 
-lemma [eqvt]:
-  shows "(p \<bullet> (rand t)) = rand (p \<bullet> t)"
-apply(induct t rule: lam.induct)
-apply(simp_all)
-done
-
 nominal_primrec 
   is_eta_nf :: "lam \<Rightarrow> bool"
 where
@@ -162,11 +142,6 @@
 apply(rule refl)
 done
 
-thm inl_eqvt
-thm var_pos_def
-
-thm fun_eq_iff
-
 termination (eqvt) by lexicographic_order
 
 lemma var_pos1:
@@ -315,9 +290,7 @@
 termination (eqvt)
   by lexicographic_order
 
-lemma subst_eqvt[eqvt]:
-  shows "(p \<bullet> t[x ::= s]) = (p \<bullet> t)[(p \<bullet> x) ::= (p \<bullet> s)]"
-by (induct t x s rule: subst.induct) (simp_all)
+thm subst.eqvt
 
 lemma forget:
   shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"
diff -r b95a2065aa10 -r c62e26830420 Nominal/Ex/LetRec.thy
--- a/Nominal/Ex/LetRec.thy	Tue Jul 19 01:40:36 2011 +0100
+++ b/Nominal/Ex/LetRec.thy	Tue Jul 19 02:30:05 2011 +0100
@@ -59,19 +59,10 @@
   apply (simp add: permute_fun_def)
   done
 
-ML {*
-let
-  val [t1, t2] = Item_Net.content (Nominal_Function_Common.get_function @{context})
-in
-  (#eqvts (snd t1),
-   #eqvts (snd t2))
-end
-*}
+termination (eqvt) by lexicographic_order
 
+thm height_trm_height_bp.eqvt
 
-thm height_trm_def height_bp_def
-
-termination (eqvt) by lexicographic_order
 
 end
 
diff -r b95a2065aa10 -r c62e26830420 Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Tue Jul 19 01:40:36 2011 +0100
+++ b/Nominal/Ex/TypeSchemes.thy	Tue Jul 19 02:30:05 2011 +0100
@@ -325,9 +325,6 @@
 termination (eqvt)
   by lexicographic_order
 
-lemma subst_eqvt[eqvt]:
-  shows "(p \<bullet> subst2 \<theta> T) = subst2 (p \<bullet> \<theta>) (p \<bullet> T)"
-  by (induct \<theta> T rule: subst2.induct) (simp_all add: lookup2_eqvt)
 
 lemma supp_fun_app2_eqvt:
   assumes e: "eqvt f"
diff -r b95a2065aa10 -r c62e26830420 Nominal/nominal_mutual.ML
--- a/Nominal/nominal_mutual.ML	Tue Jul 19 01:40:36 2011 +0100
+++ b/Nominal/nominal_mutual.ML	Tue Jul 19 02:30:05 2011 +0100
@@ -214,6 +214,8 @@
         val ctrm2 = f_def
           |> cprop_of
           |> Thm.dest_equals_lhs
+        val _ = tracing ("ctrm1:\n" ^ @{make_string} ctrm1)
+        val _ = tracing ("ctrm2:\n" ^ @{make_string} ctrm2)
       in
         eqvt_thm
 	|> Thm.instantiate (Thm.match (ctrm1, ctrm2))