--- a/Nominal/ExCoreHaskell.thy Thu Mar 25 11:29:54 2010 +0100
+++ b/Nominal/ExCoreHaskell.thy Thu Mar 25 12:04:38 2010 +0100
@@ -95,6 +95,27 @@
unfolding fresh_star_def Ball_def
by auto (simp_all add: fresh_minus_perm)
+(*primrec
+ permute_bv_raw
+where
+ "permute_bv_raw p (K c l1 l2 l3) = K c (permute_.. l1) ...
+
+(permute_bv p (K (q \<bullet> char) (q \<bullet> tvtk_lst) (q \<bullet> tvck_lst) (q \<bullet> vt_lst)
+*)
+
+consts
+ permute_bv :: "perm \<Rightarrow> pat \<Rightarrow> pat"
+
+lemma ACons_subst:
+ "supp (Abs (bv pat) trm) \<sharp>* q \<Longrightarrow> (ACons pat trm al) = ACons (permute_bv q pat) (q \<bullet> trm) al"
+sorry
+
+lemma perm_bv:
+ "p \<bullet> bv l = bv (permute_bv p l)"
+ sorry
+
+
+
lemma fv_alpha1: "fv_bv_tvtk x \<sharp>* pa \<Longrightarrow> alpha_bv_tvtk (pa \<bullet> x) x"
apply (induct x rule: inducts(11))
apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
@@ -249,7 +270,7 @@
P11 (k :: 'k :: pt) tvtk_lst \<and>
P12 (l :: 'l :: pt) tvck_lst"
proof -
- have a: "(\<forall>p a. P1 a (p \<bullet> tkind)) \<and> (\<forall>p b. P2 b (p \<bullet> ckind)) \<and> (\<forall>p c. P3 c (p \<bullet> ty)) \<and> (\<forall>p d. P4 d (p \<bullet> ty_lst)) \<and> (\<forall>p e. P5 e (p \<bullet> co)) \<and> (\<forall>p f. P6 f (p \<bullet> co_lst)) \<and> (\<forall>p g. P7 g (p \<bullet> trm)) \<and> (\<forall>p h. P8 h (p \<bullet> assoc_lst)) \<and> (\<forall>p i. P9 i (p \<bullet> pat)) \<and> (\<forall>p j. P10 j (p \<bullet> vt_lst)) \<and> (\<forall>p k. P11 k (p \<bullet> tvtk_lst)) \<and> (\<forall>p l. P12 l (p \<bullet> tvck_lst))"
+ have a: "(\<forall>p a. P1 a (p \<bullet> tkind)) \<and> (\<forall>p b. P2 b (p \<bullet> ckind)) \<and> (\<forall>p c. P3 c (p \<bullet> ty)) \<and> (\<forall>p d. P4 d (p \<bullet> ty_lst)) \<and> (\<forall>p e. P5 e (p \<bullet> co)) \<and> (\<forall>p f. P6 f (p \<bullet> co_lst)) \<and> (\<forall>p g. P7 g (p \<bullet> trm)) \<and> (\<forall>p h. P8 h (p \<bullet> assoc_lst)) \<and> (\<forall>p q i. P9 i (permute_bv p (q \<bullet> pat))) \<and> (\<forall>p j. P10 j (p \<bullet> vt_lst)) \<and> (\<forall>p k. P11 k (p \<bullet> tvtk_lst)) \<and> (\<forall>p l. P12 l (p \<bullet> tvck_lst))"
apply (rule tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.induct)
apply (tactic {* ALLGOALS (REPEAT o rtac allI) *})
apply (tactic {* ALLGOALS (TRY o SOLVED' (simp_tac @{simpset} THEN_ALL_NEW resolve_tac @{thms assms} THEN_ALL_NEW asm_full_simp_tac @{simpset})) *})
@@ -375,29 +396,62 @@
apply (simp only: supp_Abs eqvts)
apply blast
-prefer 5
-(* using a38*)
- apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (bv (p \<bullet> pat))) \<sharp>* h \<and>
- supp (Abs (p \<bullet> (bv pat)) (p \<bullet> trm), fv_bv (p \<bullet> pat)) \<sharp>* pa)")
+(* GOAL4 a copy-and-paste *)
+ apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> g \<and>
+ supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> trm)) \<sharp>* pa)")
apply clarify
apply (simp only: perm)
- apply(rule_tac t="ACons (p \<bullet> pat) (p \<bullet> trm) (p \<bullet> assoc_lst)"
- and s="ACons (pa \<bullet> p \<bullet> pat) (pa \<bullet> p \<bullet> trm) (p \<bullet> assoc_lst)" in subst)
- apply (simp only: eq_iff supp_Pair fresh_star_union)
- apply (erule conjE)
+ apply(rule_tac t="LAMC (p \<bullet> tvar) (p \<bullet> ckind) (p \<bullet> trm)"
+ and s="LAMC (pa \<bullet> p \<bullet> tvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> trm)" in subst)
+ apply (simp only: eq_iff)
apply (rule_tac x="-pa" in exI)
apply (simp add: alphas eqvts eqvts_raw supp_Abs fv_supp)
- apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - bv (pa \<bullet> p \<bullet> pat)"
- and s="pa \<bullet> (supp (p \<bullet> trm) - bv (p \<bullet> pat))" in subst)
+ apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> tvar)}"
+ and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom tvar})" in subst)
apply (simp add: eqvts)
+ apply (simp add: eqvts[symmetric])
apply (rule conjI)
- apply (rule fv_alpha)
- apply (rule_tac s="supp (fv_bv (p \<bullet> pat))"
- and t="fv_bv (p \<bullet> pat)" in subst)
- apply (rule supp_finite_atom_set[OF fin_fv_bv])
- apply (assumption)
+ apply (rule supp_perm_eq)
+ apply (simp add: eqvts)
+ apply (subst supp_finite_atom_set)
+ apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
+ apply (simp add: eqvts)
+ apply (simp add: eqvts)
+ apply (subst supp_perm_eq)
+ apply (subst supp_finite_atom_set)
+ apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
+ apply (simp add: eqvts)
+ apply assumption
+ apply (simp add: fresh_star_minus_perm)
+ apply (rule a30)
+ apply simp
+ apply(rotate_tac 1)
+ apply(erule_tac x="(pa + p)" in allE)
+ apply simp
+ apply (simp add: eqvts eqvts_raw)
+ apply (rule at_set_avoiding2_atom)
+ apply (simp add: finite_supp)
+ apply (simp add: finite_supp)
+ apply (simp add: fresh_def)
+ apply (simp only: supp_Abs eqvts)
+ apply blast
+
+
+(* GOAL5 a copy-and-paste *)
+ apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> var))) \<sharp> g \<and>
+ supp (Abs (p \<bullet> {atom var}) (p \<bullet> trm)) \<sharp>* pa)")
+ apply clarify
+ apply (simp only: perm)
+ apply(rule_tac t="Lam (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm)"
+ and s="Lam (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (pa \<bullet> p \<bullet> trm)" in subst)
+ apply (simp only: eq_iff)
+ apply (rule_tac x="-pa" in exI)
+ apply (simp add: alphas eqvts eqvts_raw supp_Abs fv_supp)
+ apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> var)}"
+ and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom var})" in subst)
+ apply (simp add: eqvts)
+ apply (simp add: eqvts[symmetric])
apply (rule conjI)
- apply (simp add: eqvts[symmetric])
apply (rule supp_perm_eq)
apply (simp add: eqvts)
apply (subst supp_finite_atom_set)
@@ -410,25 +464,85 @@
apply (simp add: eqvts)
apply assumption
apply (simp add: fresh_star_minus_perm)
+ apply (rule a32)
+ apply simp
+ apply(rotate_tac 1)
+ apply(erule_tac x="(pa + p)" in allE)
+ apply simp
+ apply (simp add: eqvts eqvts_raw)
+ apply (rule at_set_avoiding2_atom)
+ apply (simp add: finite_supp)
+ apply (simp add: finite_supp)
+ apply (simp add: fresh_def)
+ apply (simp only: supp_Abs eqvts)
+ apply blast
+
+
+(* GOAL6 a copy-and-paste *)
+ apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> var))) \<sharp> g \<and>
+ supp (Abs (p \<bullet> {atom var}) (p \<bullet> trm2)) \<sharp>* pa)")
+ apply clarify
+ apply (simp only: perm)
+ apply(rule_tac t="Let (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (p \<bullet> trm2)"
+ and s="Let (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (pa \<bullet> p \<bullet> trm2)" in subst)
+ apply (simp only: eq_iff)
+ apply (rule_tac x="-pa" in exI)
+ apply (simp add: alphas eqvts eqvts_raw supp_Abs fv_supp)
+ apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm2) - {atom (pa \<bullet> p \<bullet> var)}"
+ and s="pa \<bullet> (p \<bullet> supp trm2 - {p \<bullet> atom var})" in subst)
+ apply (simp add: eqvts)
+ apply (simp add: eqvts[symmetric])
+ apply (rule conjI)
+ apply (rule supp_perm_eq)
+ apply (simp add: eqvts)
+ apply (subst supp_finite_atom_set)
+ apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
+ apply (simp add: eqvts)
+ apply (simp add: eqvts)
+ apply (subst supp_perm_eq)
+ apply (subst supp_finite_atom_set)
+ apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
+ apply (simp add: eqvts)
+ apply assumption
+ apply (simp add: fresh_star_minus_perm)
+ apply (rule a34)
+ apply simp
+ apply simp
+ apply(rotate_tac 2)
+ apply(erule_tac x="(pa + p)" in allE)
+ apply simp
+ apply (simp add: eqvts eqvts_raw)
+ apply (rule at_set_avoiding2_atom)
+ apply (simp add: finite_supp)
+ apply (simp add: finite_supp)
+ apply (simp add: fresh_def)
+ apply (simp only: supp_Abs eqvts)
+ apply blast
+
+(* MAIN ACons Goal *)
+ apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (bv (p \<bullet> pat))) \<sharp>* h \<and>
+ supp (Abs (p \<bullet> (bv pat)) (p \<bullet> trm)) \<sharp>* pa)")
+ apply clarify
+ apply (simp only: perm eqvts)
+ apply (subst ACons_subst)
+ apply assumption
apply (rule a38)
- apply(erule_tac x="(pa + p)" in allE)
apply simp
apply(rotate_tac 1)
apply(erule_tac x="(pa + p)" in allE)
apply simp
apply simp
+ apply (simp add: perm_bv[symmetric])
apply (simp add: eqvts eqvts_raw)
apply (rule at_set_avoiding2)
apply (simp add: fin_bv)
apply (simp add: finite_supp)
- apply (simp add: supp_Pair supp_Abs supp_finite_atom_set[OF fin_fv_bv] fin_fv_bv)
+ apply (simp add: supp_Abs)
apply (rule finite_Diff)
- apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
- apply (simp add: True_eqvt)
- apply (simp add: fresh_star_prod eqvts[symmetric])
- apply (rule conjI)
- apply (simp add: fresh_star_def fresh_def supp_Abs)
- apply (simp add: fresh_star_permute_iff)
+ apply (simp add: finite_supp)
+ apply (simp add: fresh_star_def fresh_def supp_Abs eqvts)
+(* Goal for K *)
+ apply (simp)
sorry
have g1: "P1 a (0 \<bullet> tkind)" using a[THEN conjunct1] by blast
have g2: "P2 b (0 \<bullet> ckind)" using a[THEN conjunct2,THEN conjunct1] by blast