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/CPS/CPS3_DanvyFilinski.thy
changeset 3186 425b4c406d80
parent 3089 9bcf02a6eea9
child 3187 b3d97424b130 
--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Sat Jun 09 19:48:19 2012 +0100
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Mon Jun 11 14:02:57 2012 +0100
@@ -42,208 +42,7 @@
   apply (rule contra_subsetD[OF supp_fun_app])
   back
   apply (simp add: supp_fun_eqvt lt.supp supp_at_base)
---"-"
-  apply (rule arg_cong)
-  back
-  apply simp
-  apply (thin_tac "eqvt ka")
-  apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh)
-  apply (subgoal_tac "Lam c (CPS1_CPS2_sumC (Inr (M, c~))) = Lam a (CPS1_CPS2_sumC (Inr (M, a~)))")
-  prefer 2
-  apply (simp add: Abs1_eq_iff')
-  apply (case_tac "c = a")
-  apply simp_all[2]
-  apply rule
-  apply (simp add: eqvt_at_def)
-  apply (simp add: swap_fresh_fresh fresh_Pair_elim)
-  apply (erule fresh_eqvt_at)
-  apply (simp add: supp_Inr finite_supp)
-  apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
-  apply (subgoal_tac "Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Lam a (CPS1_CPS2_sumC (Inr (Ma, a~)))")
-  prefer 2
-  apply (simp add: Abs1_eq_iff')
-  apply (case_tac "ca = a")
-  apply simp_all[2]
-  apply rule
-  apply (simp add: eqvt_at_def)
-  apply (simp add: swap_fresh_fresh fresh_Pair_elim)
-  apply (erule fresh_eqvt_at)
-  apply (simp add: supp_Inr finite_supp)
-  apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
-  apply (simp only: )
-  apply (erule Abs_lst1_fcb)
-  apply (simp add: Abs_fresh_iff)
-  apply (drule sym)
-  apply (simp only:)
-  apply (simp add: Abs_fresh_iff lt.fresh)
-  apply clarify
-  apply (erule fresh_eqvt_at)
-  apply (simp add: supp_Inr finite_supp)
-  apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
-  apply (drule sym)
-  apply (drule sym)
-  apply (drule sym)
-  apply (simp only:)
-  apply (thin_tac "Lam a (CPS1_CPS2_sumC (Inr (M, a~))) = Lam c (CPS1_CPS2_sumC (Inr (M, c~)))")
-  apply (thin_tac "Lam a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~)))")
-  apply (thin_tac "atom a \<sharp> (c, ca, x, xa, M, Ma)")
-  apply (simp add: fresh_Pair_elim)
-  apply (subst iffD1[OF meta_eq_to_obj_eq[OF eqvt_at_def]])
-  back
-  back
-  back
-  apply assumption
-  apply (simp add: Abs1_eq_iff' fresh_Pair_elim fresh_at_base swap_fresh_fresh lt.fresh)
-  apply (case_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> c = ca")
-  apply simp_all[3]
-  apply rule
-  apply (case_tac "c = xa")
-  apply simp_all[2]
-  apply (rotate_tac 1)
-  apply (drule_tac q="(atom ca \<rightleftharpoons> atom x)" in eqvt_at_perm)
-  apply (simp add: swap_fresh_fresh)
-  apply (simp add: eqvt_at_def swap_fresh_fresh)
-  apply (thin_tac "eqvt_at CPS1_CPS2_sumC (Inr (M, c~))")
-  apply (simp add: eqvt_at_def)
-  apply (drule_tac x="(atom ca \<rightleftharpoons> atom c)" in spec)
-  apply simp
-  apply (metis (no_types) atom_eq_iff fresh_permute_iff permute_swap_cancel swap_atom_simps(3) swap_fresh_fresh)
-  apply (case_tac "c = xa")
-  apply simp
-  apply (subgoal_tac "((ca \<leftrightarrow> x) \<bullet> (atom x)) \<sharp> (ca \<leftrightarrow> x) \<bullet> CPS1_CPS2_sumC (Inr (Ma, ca~))")
-  apply (simp add: atom_eqvt eqvt_at_def)
-  apply (simp add: flip_fresh_fresh)
-  apply (subst fresh_permute_iff)
-  apply (erule fresh_eqvt_at)
-  apply (simp add: supp_Inr finite_supp)
-  apply (simp add: fresh_Inr lt.fresh fresh_at_base fresh_Pair)
-  apply simp
-  apply clarify
-  apply (subgoal_tac "atom ca \<sharp> (atom x \<rightleftharpoons> atom xa) \<bullet> CPS1_CPS2_sumC (Inr (M, c~))")
-  apply (simp add: eqvt_at_def)
-  apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> atom ca \<sharp> CPS1_CPS2_sumC (Inr (M, c~))")
-  apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2)
-  apply (erule fresh_eqvt_at)
-  apply (simp add: finite_supp supp_Inr)
-  apply (simp add: fresh_Inr fresh_Pair lt.fresh)
-  apply rule
-  apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2)
-  apply (simp add: fresh_def supp_at_base)
-  apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3))
---"-"
-  apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh)
-  apply (subgoal_tac "Lam c (CPS1_CPS2_sumC (Inr (M, c~))) = Lam a (CPS1_CPS2_sumC (Inr (M, a~)))")
-  prefer 2
-  apply (simp add: Abs1_eq_iff')
-  apply (case_tac "c = a")
-  apply simp_all[2]
-  apply rule
-  apply (simp add: eqvt_at_def)
-  apply (simp add: swap_fresh_fresh fresh_Pair_elim)
-  apply (erule fresh_eqvt_at)
-  apply (simp add: supp_Inr finite_supp)
-  apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
-  apply (subgoal_tac "Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Lam a (CPS1_CPS2_sumC (Inr (Ma, a~)))")
-  prefer 2
-  apply (simp add: Abs1_eq_iff')
-  apply (case_tac "ca = a")
-  apply simp_all[2]
-  apply rule
-  apply (simp add: eqvt_at_def)
-  apply (simp add: swap_fresh_fresh fresh_Pair_elim)
-  apply (erule fresh_eqvt_at)
-  apply (simp add: supp_Inr finite_supp)
-  apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
-  apply (simp only: )
-  apply (erule Abs_lst1_fcb)
-  apply (simp add: Abs_fresh_iff)
-  apply (drule sym)
-  apply (simp only:)
-  apply (simp add: Abs_fresh_iff lt.fresh)
-  apply clarify
-  apply (erule fresh_eqvt_at)
-  apply (simp add: supp_Inr finite_supp) (* TODO put sum of fs into fs typeclass *)
-  apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
-  apply (drule sym)
-  apply (drule sym)
-  apply (drule sym)
-  apply (simp only:)
-  apply (thin_tac "Lam a (CPS1_CPS2_sumC (Inr (M, a~))) = Lam c (CPS1_CPS2_sumC (Inr (M, c~)))")
-  apply (thin_tac "Lam a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~)))")
-  apply (thin_tac "atom a \<sharp> (c, ca, x, xa, M, Ma)")
-  apply (simp add: fresh_Pair_elim)
-  apply (subst iffD1[OF meta_eq_to_obj_eq[OF eqvt_at_def]])
-  back
-  back
-  back
-  apply assumption
-  apply (simp add: Abs1_eq_iff' fresh_Pair_elim fresh_at_base swap_fresh_fresh lt.fresh)
-  apply (case_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> c = ca")
-  apply simp_all[3]
-  apply rule
-  apply (case_tac "c = xa")
-  apply simp_all[2]
-  apply (rotate_tac 1)
-  apply (drule_tac q="(atom ca \<rightleftharpoons> atom x)" in eqvt_at_perm)
-  apply (simp add: swap_fresh_fresh)
-  apply (simp add: eqvt_at_def swap_fresh_fresh)
-  apply (thin_tac "eqvt_at CPS1_CPS2_sumC (Inr (M, c~))")
-  apply (simp add: eqvt_at_def)
-  apply (drule_tac x="(atom ca \<rightleftharpoons> atom c)" in spec)
-  apply simp
-  apply (metis (no_types) atom_eq_iff fresh_permute_iff permute_swap_cancel swap_atom_simps(3) swap_fresh_fresh)
-  apply (case_tac "c = xa")
-  apply simp
-  apply (subgoal_tac "((ca \<leftrightarrow> x) \<bullet> (atom x)) \<sharp> (ca \<leftrightarrow> x) \<bullet> CPS1_CPS2_sumC (Inr (Ma, ca~))")
-  apply (simp add: atom_eqvt eqvt_at_def)
-  apply (simp add: flip_fresh_fresh)
-  apply (subst fresh_permute_iff)
-  apply (erule fresh_eqvt_at)
-  apply (simp add: supp_Inr finite_supp)
-  apply (simp add: fresh_Inr lt.fresh fresh_at_base fresh_Pair)
-  apply simp
-  apply clarify
-  apply (subgoal_tac "atom ca \<sharp> (atom x \<rightleftharpoons> atom xa) \<bullet> CPS1_CPS2_sumC (Inr (M, c~))")
-  apply (simp add: eqvt_at_def)
-  apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> atom ca \<sharp> CPS1_CPS2_sumC (Inr (M, c~))")
-  apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2)
-  apply (erule fresh_eqvt_at)
-  apply (simp add: finite_supp supp_Inr)
-  apply (simp add: fresh_Inr fresh_Pair lt.fresh)
-  apply rule
-  apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2)
-  apply (simp add: fresh_def supp_at_base)
-  apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3))
-  done
-
-termination (eqvt)
-  by lexicographic_order
-
-definition psi:: "lt => lt"
-  where [simp]: "psi V == V*(\<lambda>x. x)"
-
-section {* Simple consequence of CPS *}
-
-lemma [simp]: "eqvt (\<lambda>x\<Colon>lt. x)"
-  by (simp add: eqvt_def eqvt_bound eqvt_lambda)
-
-lemma value_eq1 : "isValue V \<Longrightarrow> eqvt k \<Longrightarrow> V*k = k (psi V)"
-  apply (cases V rule: lt.exhaust)
-  apply simp_all
-  apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)
-  apply simp
-  done
-
-lemma value_eq2 : "isValue V \<Longrightarrow> V^K = K $ (psi V)"
-  apply (cases V rule: lt.exhaust)
-  apply simp_all
-  apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)
-  apply simp
-  done
-
-lemma value_eq3' : "~isValue M \<Longrightarrow> eqvt k \<Longrightarrow> M*k = (M^(Lam n (k (Var n))))"
-  by (cases M rule: lt.exhaust) auto
-
+oops
 
 
 end
nominal2