--- 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