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.
only one of the fcb precondistions are needed (probably the same with the perm-conditions)
authorChristian Urban <urbanc@in.tum.de>
Sun, 26 Jun 2011 21:42:07 +0100
changeset 2903 e26c6c728b9e
parent 2902 9c3f6a4d95d4
child 2904 eb322a392461
child 2905 9448945a1e60
only one of the fcb precondistions are needed (probably the same with the perm-conditions)
Nominal/Ex/Classical.thy file | annotate | diff | comparison | revisions 
--- a/Nominal/Ex/Classical.thy	Sun Jun 26 17:55:22 2011 +0100
+++ b/Nominal/Ex/Classical.thy	Sun Jun 26 21:42:07 2011 +0100
@@ -52,12 +52,24 @@
     and c::"'c::fs"
   assumes e: "(Abs_lst [atom a] T) = (Abs_lst [atom b] S)"
   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"
   shows "f a T c = f b S c"
 proof -
+  have fcb2: "atom b \<sharp> f b S c"
+    using e[symmetric]
+    apply(simp add: Abs_eq_iff2)
+    apply(erule exE)
+    apply(simp add: alphas)
+    apply(rule_tac p="p" in permute_boolE)
+    apply(simp add: fresh_eqvt)
+    apply(subst perm2)
+    using fresh
+    apply(auto simp add: fresh_star_def)[1]
+    apply(simp add: atom_eqvt)
+    apply(rule fcb1)
+    done
   have fin1: "finite (supp (f a T c))"
     apply(rule_tac S="supp (a, T, c)" in supports_finite)
     apply(simp add: supports_def)
@@ -133,7 +145,20 @@
   finally show ?thesis by simp
 qed
 
-
+(*
+lemma Abs_lst_fcb2:
+  fixes as bs :: "atom list"
+    and x y :: "'b :: fs"
+    and c::"'c::fs"
+  assumes e: "(Abs_lst as x) = (Abs_lst bs y)"
+  and fcb1: "(set as) \<sharp>* f as x c"
+  and fcb2: "(set bs) \<sharp>* f bs y c"
+  and fresh1: "set as \<sharp>* c"
+  and fresh2: "set bs \<sharp>* c"
+  and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c"
+  and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c"
+  shows "f as x c = f bs y c"
+*)
 
 nominal_primrec 
   crename :: "trm \<Rightarrow> coname \<Rightarrow> coname \<Rightarrow> trm"  ("_[_\<turnstile>c>_]" [100,100,100] 100) 
@@ -169,14 +194,12 @@
   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)
@@ -185,7 +208,6 @@
   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,7 +216,6 @@
   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)
@@ -204,7 +225,6 @@
   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)
@@ -215,7 +235,6 @@
   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)
@@ -224,14 +243,12 @@
   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)
@@ -240,7 +257,6 @@
   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)
@@ -251,7 +267,6 @@
   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)
@@ -263,7 +278,6 @@
   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)
@@ -274,7 +288,6 @@
   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)
@@ -287,7 +300,6 @@
   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)
@@ -297,7 +309,6 @@
   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