Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Ex/Classical.thy
changeset 2902 9c3f6a4d95d4
parent 2901 754aa24006c8
child 2903 e26c6c728b9e 
--- a/Nominal/Ex/Classical.thy	Sat Jun 25 22:51:43 2011 +0100
+++ b/Nominal/Ex/Classical.thy	Sun Jun 26 17:55:22 2011 +0100
@@ -29,7 +29,7 @@
      ("OrL '(_')._ '(_')._ _" [100,100,100,100,100] 100)
 | ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name"       bind c in t1, bind n in t2
      ("ImpL <_>._ '(_')._ _" [100,100,100,100,100] 100)
-| ImpR c::"coname" n::"name" t::"trm" "coname"                bind n c in t
+| ImpR n::"name" c::"coname" t::"trm" "coname"                bind n c in t
      ("ImpR '(_').<_>._ _" [100,100,100,100] 100)
 
 thm trm.distinct
@@ -51,7 +51,8 @@
     and S T :: "'b :: fs"
     and c::"'c::fs"
   assumes e: "(Abs_lst [atom a] T) = (Abs_lst [atom b] S)"
-  and fcb: "\<And>a T. atom a \<sharp> f a T c"
+  and fcb1: "atom a \<sharp> f a T c"
+  and fcb2: "atom b \<sharp> f b S c"
   and fresh: "{atom a, atom b} \<sharp>* c"
   and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a T c) = f (p \<bullet> a) (p \<bullet> T) c"
   and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f b S c) = f (p \<bullet> b) (p \<bullet> S) c"
@@ -102,7 +103,7 @@
     unfolding flip_def
     apply(rule sym)
     apply(rule swap_fresh_fresh)
-    using fcb[where a="a"] 
+    using fcb1 
     apply(simp)
     using fr
     apply(simp add: fresh_Pair)
@@ -124,7 +125,7 @@
     done
   also have "... = f b S c"   
     apply(rule flip_fresh_fresh)
-    using fcb[where a="b"] 
+    using fcb2
     apply(simp)
     using fr
     apply(simp add: fresh_Pair)
@@ -133,10 +134,6 @@
 qed
 
 
-lemma swap_at_base_sort: 
-  "sort_of (atom a) \<noteq> sort_of (atom x) \<Longrightarrow> sort_of (atom b) \<noteq> sort_of (atom x) 
-  \<Longrightarrow> (atom a \<rightleftharpoons> atom b) \<bullet> x = x"
-  by (rule swap_fresh_fresh) (simp_all add: fresh_at_base(1))
 
 nominal_primrec 
   crename :: "trm \<Rightarrow> coname \<Rightarrow> coname \<Rightarrow> trm"  ("_[_\<turnstile>c>_]" [100,100,100] 100) 
@@ -172,12 +169,14 @@
   apply(elim conjE)
   apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
+  apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(elim conjE)
   apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
+  apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
@@ -186,6 +185,7 @@
   apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
+  apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
@@ -194,6 +194,7 @@
   apply(elim conjE)
   apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
+  apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
@@ -203,6 +204,7 @@
   apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
+  apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
@@ -213,6 +215,7 @@
   apply(subgoal_tac "eqvt_at crename_sumC (Na, da, ea)")
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
+  apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
@@ -221,12 +224,14 @@
   apply(elim conjE)
   apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
+  apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(elim conjE)
   apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
+  apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
@@ -235,6 +240,7 @@
   apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
+  apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
@@ -245,6 +251,7 @@
   apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
+  apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
@@ -256,6 +263,7 @@
   apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
+  apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
@@ -266,6 +274,7 @@
   apply(subgoal_tac "eqvt_at crename_sumC (Na, da, ea)")
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
+  apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
@@ -278,6 +287,7 @@
   apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
+  apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
@@ -287,6 +297,7 @@
   apply(subgoal_tac "eqvt_at crename_sumC (Na, da, ea)")
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
+  apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
nominal2