Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Simplified and finised eqvt proofs for t1 and t5
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Wed, 24 Feb 2010 18:38:49 +0100
changeset 1255 ab8ed83d0188
parent 1254 2a878d7d631f
child 1256 6c938f84880c
Simplified and finised eqvt proofs for t1 and t5
Quot/Nominal/Abs.thy file | annotate | diff | comparison | revisions
Quot/Nominal/Terms.thy file | annotate | diff | comparison | revisions 
--- a/Quot/Nominal/Abs.thy	Wed Feb 24 17:42:52 2010 +0100
+++ b/Quot/Nominal/Abs.thy	Wed Feb 24 18:38:49 2010 +0100
@@ -113,11 +113,12 @@
   apply(simp)
   done
 
-lemma alpha_gen_atom_eqvt:
-  assumes a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)"
-  and     b: "\<exists>pia. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia ({atom b}, s)"
-  shows  "\<exists>pia. ({atom (pi \<bullet> a)}, pi \<bullet> t) \<approx>gen R f pia ({atom (pi \<bullet> b)}, pi \<bullet> s)"
-  using b 
+lemma alpha_gen_compose_eqvt:
+  assumes b: "\<exists>pia. (g d, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia (g e, s)"
+  and     c: "\<And>y. pi \<bullet> (g y) = g (pi \<bullet> y)"
+  and     a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)"
+  shows  "\<exists>pia. (g (pi \<bullet> d), pi \<bullet> t) \<approx>gen R f pia (g (pi \<bullet> e), pi \<bullet> s)"
+  using b
   apply -
   apply(erule exE)
   apply(rule_tac x="pi \<bullet> pia" in exI)
@@ -125,10 +126,10 @@
   apply(erule conjE)+
   apply(rule conjI)
   apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
-  apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt)
+  apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric])
   apply(rule conjI)
   apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
-  apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt)
+  apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric])
   apply(subst permute_eqvt[symmetric])
   apply(simp)
   done
--- a/Quot/Nominal/Terms.thy	Wed Feb 24 17:42:52 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 24 18:38:49 2010 +0100
@@ -65,14 +65,14 @@
 lemma bv1_eqvt[eqvt]:
   shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)"
   apply (induct x)
-  apply (simp_all add: atom_eqvt eqvts)
+  apply (simp_all add: eqvts atom_eqvt)
   done
 
 lemma fv_rtrm1_eqvt[eqvt]:
     "(pi\<bullet>fv_rtrm1 t) = fv_rtrm1 (pi\<bullet>t)"
     "(pi\<bullet>fv_bp b) = fv_bp (pi\<bullet>b)"
   apply (induct t and b)
-  apply (simp_all add: insert_eqvt atom_eqvt empty_eqvt union_eqvt Diff_eqvt bv1_eqvt)
+  apply (simp_all add: eqvts atom_eqvt)
   done
 
 lemma alpha1_eqvt:
@@ -80,40 +80,12 @@
   "alpha_bp a b \<Longrightarrow> alpha_bp (pi \<bullet> a) (pi \<bullet> b)"
   apply (induct t s and a b rule: alpha_rtrm1_alpha_bp.inducts)
   apply (simp_all add:eqvts alpha1_inj)
-  apply (erule exE)
-  apply (rule_tac x="pi \<bullet> pia" in exI)
-  apply (simp add: alpha_gen)
-  apply(erule conjE)+
-  apply(rule conjI)
-  apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
-  apply(simp add: atom_eqvt Diff_eqvt insert_eqvt empty_eqvt fv_rtrm1_eqvt)
-  apply(rule conjI)
-  apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
-  apply(simp add: atom_eqvt Diff_eqvt fv_rtrm1_eqvt insert_eqvt empty_eqvt)
-  apply(simp add: permute_eqvt[symmetric])
-  apply (erule exE)
-  apply (erule exE)
-  apply (rule conjI)
-  apply (rule_tac x="pi \<bullet> pia" in exI)
-  apply (simp add: alpha_gen)
-  apply(erule conjE)+
-  apply(rule conjI)
-  apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
-  apply(simp add: fv_rtrm1_eqvt Diff_eqvt bv1_eqvt)
-  apply(rule conjI)
-  apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
-  apply(simp add: atom_eqvt fv_rtrm1_eqvt Diff_eqvt bv1_eqvt)
-  apply(simp add: permute_eqvt[symmetric])
-  apply (rule_tac x="pi \<bullet> piaa" in exI)
-  apply (simp add: alpha_gen)
-  apply(erule conjE)+
-  apply(rule conjI)
-  apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
-  apply(simp add: fv_rtrm1_eqvt Diff_eqvt bv1_eqvt)
-  apply(rule conjI)
-  apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
-  apply(simp add: atom_eqvt fv_rtrm1_eqvt Diff_eqvt bv1_eqvt)
-  apply(simp add: permute_eqvt[symmetric])
+  apply (tactic {* 
+    ALLGOALS (
+      TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW
+      (etac @{thm alpha_gen_compose_eqvt})
+    ) *})
+  apply (simp_all only: eqvts atom_eqvt)
   done
 
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []),
@@ -453,45 +425,30 @@
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases} ctxt)) ctxt)) *}
 thm alpha5_inj
 
-lemma rbv5_eqvt:
+lemma rbv5_eqvt[eqvt]:
   "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)"
-sorry
+  apply (induct x)
+  apply (simp_all add: eqvts atom_eqvt)
+  done
 
-lemma fv_rtrm5_eqvt:
+lemma fv_rtrm5_rlts_eqvt[eqvt]:
   "pi \<bullet> (fv_rtrm5 x) = fv_rtrm5 (pi \<bullet> x)"
-sorry
-
-lemma fv_rlts_eqvt:
-  "pi \<bullet> (fv_rlts x) = fv_rlts (pi \<bullet> x)"
-sorry
+  "pi \<bullet> (fv_rlts l) = fv_rlts (pi \<bullet> l)"
+  apply (induct x and l)
+  apply (simp_all add: eqvts atom_eqvt)
+  done
 
 lemma alpha5_eqvt:
   "xa \<approx>5 y \<Longrightarrow> (x \<bullet> xa) \<approx>5 (x \<bullet> y)"
   "xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)"
-  apply(induct rule: alpha_rtrm5_alpha_rlts.inducts)
+  apply (induct rule: alpha_rtrm5_alpha_rlts.inducts)
   apply (simp_all add: alpha5_inj)
-  apply (erule exE)+
-  apply(unfold alpha_gen)
-  apply (erule conjE)+
-  apply (rule conjI)
-  apply (rule_tac x="x \<bullet> pi" in exI)
-  apply (rule conjI)
-  apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1])
-  apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt)
-  apply(rule conjI)
-  apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1])
-  apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt)
-  apply (subst permute_eqvt[symmetric])
-  apply (simp)
-  apply (rule_tac x="x \<bullet> pia" in exI)
-  apply (rule conjI)
-  apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1])
-  apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt)
-  apply(rule conjI)
-  apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1])
-  apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt)
-  apply (subst permute_eqvt[symmetric])
-  apply (simp)
+  apply (tactic {* 
+    ALLGOALS (
+      TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW
+      (etac @{thm alpha_gen_compose_eqvt})
+    ) *})
+  apply (simp_all only: eqvts atom_eqvt)
   done
 
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_equivp}, []),
nominal2