# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269515078 -3600
# Node ID 733bac87d5bffd5281f99d60dd16ae8ec56b7949
# Parent  bde8da26093edbd199b4887c463979efef3c7008
Solved all boring subgoals, and looking at properly defning permute_bv

diff -r bde8da26093e -r 733bac87d5bf Nominal/ExCoreHaskell.thy
--- 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