--- a/Nominal/ExCoreHaskell.thy Thu Mar 25 12:04:38 2010 +0100
+++ b/Nominal/ExCoreHaskell.thy Thu Mar 25 14:24:06 2010 +0100
@@ -91,30 +91,112 @@
lemmas eq_iff=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.eq_iff
lemmas inducts=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.inducts
+lemmas alpha_inducts=alpha_tkind_raw_alpha_ckind_raw_alpha_ty_raw_alpha_ty_lst_raw_alpha_co_raw_alpha_co_lst_raw_alpha_trm_raw_alpha_assoc_lst_raw_alpha_pat_raw_alpha_vt_lst_raw_alpha_tvtk_lst_raw_alpha_tvck_lst_raw_alpha_bv_raw_alpha_bv_vt_raw_alpha_bv_tvtk_raw_alpha_bv_tvck_raw.inducts
+lemmas alpha_intros=alpha_tkind_raw_alpha_ckind_raw_alpha_ty_raw_alpha_ty_lst_raw_alpha_co_raw_alpha_co_lst_raw_alpha_trm_raw_alpha_assoc_lst_raw_alpha_pat_raw_alpha_vt_lst_raw_alpha_tvtk_lst_raw_alpha_tvck_lst_raw_alpha_bv_raw_alpha_bv_vt_raw_alpha_bv_tvtk_raw_alpha_bv_tvck_raw.intros
+
lemma fresh_star_minus_perm: "as \<sharp>* - p = as \<sharp>* (p :: perm)"
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) ...
+primrec permute_bv_vt_raw
+where "permute_bv_vt_raw p VTNil_raw = VTNil_raw"
+| "permute_bv_vt_raw p (VTCons_raw v t l) = VTCons_raw (p \<bullet> v) t (permute_bv_vt_raw p l)"
+primrec permute_bv_tvck_raw
+where "permute_bv_tvck_raw p TVCKNil_raw = TVCKNil_raw"
+| "permute_bv_tvck_raw p (TVCKCons_raw v t l) = TVCKCons_raw (p \<bullet> v) t (permute_bv_tvck_raw p l)"
+primrec permute_bv_tvtk_raw
+where "permute_bv_tvtk_raw p TVTKNil_raw = TVTKNil_raw"
+| "permute_bv_tvtk_raw p (TVTKCons_raw v t l) = TVTKCons_raw (p \<bullet> v) t (permute_bv_tvtk_raw p l)"
+primrec permute_bv_raw
+where "permute_bv_raw p (K_raw c l1 l2 l3) =
+ K_raw c (permute_bv_tvtk_raw p l1) (permute_bv_tvck_raw p l2) (permute_bv_vt_raw p l3)"
+
+quotient_definition "permute_bv_vt :: perm \<Rightarrow> vt_lst \<Rightarrow> vt_lst"
+is "permute_bv_vt_raw"
+quotient_definition "permute_bv_tvck :: perm \<Rightarrow> tvck_lst \<Rightarrow> tvck_lst"
+is "permute_bv_tvck_raw"
+quotient_definition "permute_bv_tvtk :: perm \<Rightarrow> tvtk_lst \<Rightarrow> tvtk_lst"
+is "permute_bv_tvtk_raw"
+quotient_definition "permute_bv :: perm \<Rightarrow> pat \<Rightarrow> pat"
+is "permute_bv_raw"
+
+lemma rsp_pre:
+ "alpha_tvtk_lst_raw d a \<Longrightarrow> alpha_tvtk_lst_raw (permute_bv_tvtk_raw x d) (permute_bv_tvtk_raw x a)"
+ "alpha_tvck_lst_raw e b \<Longrightarrow> alpha_tvck_lst_raw (permute_bv_tvck_raw x e) (permute_bv_tvck_raw x b)"
+ "alpha_vt_lst_raw f c \<Longrightarrow> alpha_vt_lst_raw (permute_bv_vt_raw x f) (permute_bv_vt_raw x c)"
+ apply (erule_tac [!] alpha_inducts)
+ apply simp_all
+ apply (rule_tac [!] alpha_intros)
+ apply simp_all
+ done
-(permute_bv p (K (q \<bullet> char) (q \<bullet> tvtk_lst) (q \<bullet> tvck_lst) (q \<bullet> vt_lst)
-*)
+lemma [quot_respect]:
+ "(op = ===> alpha_pat_raw ===> alpha_pat_raw) permute_bv_raw permute_bv_raw"
+ "(op = ===> alpha_tvtk_lst_raw ===> alpha_tvtk_lst_raw) permute_bv_tvtk_raw permute_bv_tvtk_raw"
+ "(op = ===> alpha_tvck_lst_raw ===> alpha_tvck_lst_raw) permute_bv_tvck_raw permute_bv_tvck_raw"
+ "(op = ===> alpha_vt_lst_raw ===> alpha_vt_lst_raw) permute_bv_vt_raw permute_bv_vt_raw"
+ apply (simp_all add: rsp_pre)
+ apply clarify
+ apply (erule_tac alpha_inducts)
+ apply (simp_all)
+ apply (rule alpha_intros)
+ apply (simp_all add: rsp_pre)
+ done
+
+lemmas permute_bv[simp] = permute_bv_raw.simps[quot_lifted]
+ permute_bv_vt_raw.simps[quot_lifted]
+ permute_bv_tvck_raw.simps[quot_lifted]
+ permute_bv_tvtk_raw.simps[quot_lifted]
-consts
- permute_bv :: "perm \<Rightarrow> pat \<Rightarrow> pat"
+lemma perm_bv1:
+ "p \<bullet> bv_tvck b = bv_tvck (permute_bv_tvck p b)"
+ "p \<bullet> bv_tvtk c = bv_tvtk (permute_bv_tvtk p c)"
+ "p \<bullet> bv_vt d = bv_vt (permute_bv_vt p d)"
+ apply(induct b rule: inducts(12))
+ apply(rule TrueI)
+ apply(simp_all add:permute_bv eqvts)
+ apply(induct c rule: inducts(11))
+ apply(rule TrueI)
+ apply(simp_all add:permute_bv eqvts)
+ apply(induct d rule: inducts(10))
+ apply(rule TrueI)
+ apply(simp_all add:permute_bv eqvts)
+ done
+
+lemma perm_bv2:
+ "p \<bullet> bv l = bv (permute_bv p l)"
+ apply(induct l rule: inducts(9))
+ apply(rule TrueI)
+ apply(simp_all add:permute_bv)
+ apply(simp add: perm_bv1[symmetric])
+ apply(simp add: eqvts)
+ done
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 permute_bv_zero1:
+ "permute_bv_tvck 0 b = b"
+ "permute_bv_tvtk 0 c = c"
+ "permute_bv_vt 0 d = d"
+ apply(induct b rule: inducts(12))
+ apply(rule TrueI)
+ apply(simp_all add:permute_bv eqvts)
+ apply(induct c rule: inducts(11))
+ apply(rule TrueI)
+ apply(simp_all add:permute_bv eqvts)
+ apply(induct d rule: inducts(10))
+ apply(rule TrueI)
+ apply(simp_all add:permute_bv eqvts)
+ done
-
+lemma permute_bv_zero2:
+ "permute_bv 0 a = a"
+ apply(induct a rule: inducts(9))
+ apply(rule TrueI)
+ apply(simp_all add:permute_bv eqvts permute_bv_zero1)
+ done
lemma fv_alpha1: "fv_bv_tvtk x \<sharp>* pa \<Longrightarrow> alpha_bv_tvtk (pa \<bullet> x) x"
apply (induct x rule: inducts(11))
@@ -270,8 +352,8 @@
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 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)
+ have a1: "(\<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 a1:"(\<forall>p q i. P9 i (permute_bv p (q \<bullet> pat)))" and a2:"(\<forall>p q j. P10 j (permute_bv_vt q (p \<bullet> vt_lst)))" and a3:"(\<forall>p q k. P11 k ( permute_bv_tvtk q (p \<bullet> tvtk_lst)))" and a4:"(\<forall>p q l. P12 l (permute_bv_tvck q (p \<bullet> tvck_lst)))"
+ apply (induct rule: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.inducts)
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})) *})
@@ -532,7 +614,7 @@
apply(erule_tac x="(pa + p)" in allE)
apply simp
apply simp
- apply (simp add: perm_bv[symmetric])
+ apply (simp add: perm_bv2[symmetric])
apply (simp add: eqvts eqvts_raw)
apply (rule at_set_avoiding2)
apply (simp add: fin_bv)
@@ -541,16 +623,10 @@
apply (rule finite_Diff)
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
- have g3: "P3 c (0 \<bullet> ty) \<and>
- P4 d (0 \<bullet> ty_lst) \<and> P5 e (0 \<bullet> co) \<and> P6 f (0 \<bullet> co_lst) \<and>
- P7 g (0 \<bullet> trm) \<and> P8 h (0 \<bullet> assoc_lst) \<and> P9 i (0 \<bullet> pat) \<and>
- P10 j (0 \<bullet> vt_lst) \<and> P11 k (0 \<bullet> tvtk_lst) \<and> P12 l (0 \<bullet> tvck_lst)" using a by blast
- show ?thesis using g1 g2 g3 by simp
+ done
+ then have b: "P1 a (0 \<bullet> tkind)" and "P2 b (0 \<bullet> ckind)" "P3 c (0 \<bullet> ty)" and "P4 d (0 \<bullet> ty_lst)" and "P5 e (0 \<bullet> co)" and "P6 f (0 \<bullet> co_lst)" and "P7 g (0 \<bullet> trm)" and "P8 h (0 \<bullet> assoc_lst)" by (blast+)
+ moreover have "P9 i (permute_bv 0 (0 \<bullet> pat))" and "P10 j (permute_bv_vt 0 (0 \<bullet> vt_lst))" and "P11 k (permute_bv_tvtk 0 (0 \<bullet> tvtk_lst))" and "P12 l (permute_bv_tvck 0 (0 \<bullet> tvck_lst))" using a1 a2 a3 a4 by (blast+)
+ ultimately show ?thesis by (simp_all add: permute_bv_zero1 permute_bv_zero2)
qed
end