# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269450153 -3600
# Node ID 8b4595cb552418f8b702f92a5d22e1b6ef8f0176
# Parent  b6656b707a8db65625318ecbbddf8a49bd91aaf0
Further in the strong induction proof.

diff -r b6656b707a8d -r 8b4595cb5524 Nominal/ExCoreHaskell.thy
--- a/Nominal/ExCoreHaskell.thy	Wed Mar 24 16:06:31 2010 +0100
+++ b/Nominal/ExCoreHaskell.thy	Wed Mar 24 18:02:33 2010 +0100
@@ -88,11 +88,99 @@
 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.supp(1-9,11,13,15)
 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.fv[simplified fv_supp]
 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.perm
+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
 
 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)
 
+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}) *})
+apply (simp_all add: eq_iff fresh_star_union)
+apply (subst supp_perm_eq)
+apply (simp_all add: fv_supp)
+done
+
+lemma fv_alpha2: "fv_bv_tvck x \<sharp>* pa \<Longrightarrow> alpha_bv_tvck (pa \<bullet> x) x"
+apply (induct x rule: inducts(12))
+apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
+apply (simp_all add: eq_iff fresh_star_union)
+apply (subst supp_perm_eq)
+apply (simp_all add: fv_supp)
+done
+
+lemma fv_alpha3: "fv_bv_vt x \<sharp>* pa \<Longrightarrow> alpha_bv_vt (pa \<bullet> x) x"
+apply (induct x rule: inducts(10))
+apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
+apply (simp_all add: eq_iff fresh_star_union)
+apply (subst supp_perm_eq)
+apply (simp_all add: fv_supp)
+done
+
+lemma fv_alpha: "fv_bv x \<sharp>* pa \<Longrightarrow> alpha_bv (pa \<bullet> x) x"
+apply (induct x rule: inducts(9))
+apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
+apply (simp_all add: eq_iff fresh_star_union)
+apply (simp add: fv_alpha1 fv_alpha2 fv_alpha3)
+apply (simp add: eqvts)
+done
+
+lemma fin1: "finite (fv_bv_tvtk x)"
+apply (induct x rule: inducts(11))
+apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
+apply (simp_all add: fv_supp finite_supp)
+done
+
+lemma fin2: "finite (fv_bv_tvck x)"
+apply (induct x rule: inducts(12))
+apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
+apply (simp_all add: fv_supp finite_supp)
+done
+
+lemma fin3: "finite (fv_bv_vt x)"
+apply (induct x rule: inducts(10))
+apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
+apply (simp_all add: fv_supp finite_supp)
+done
+
+lemma fin_fv_bv: "finite (fv_bv x)"
+apply (induct x rule: inducts(9))
+apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
+apply (simp add: fin1 fin2 fin3)
+done
+
+lemma finb1: "finite (bv_tvtk x)"
+apply (induct x rule: inducts(11))
+apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
+apply (simp_all add: fv_supp finite_supp)
+done
+
+lemma finb2: "finite (bv_tvck x)"
+apply (induct x rule: inducts(12))
+apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
+apply (simp_all add: fv_supp finite_supp)
+done
+
+lemma finb3: "finite (bv_vt x)"
+apply (induct x rule: inducts(10))
+apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
+apply (simp_all add: fv_supp finite_supp)
+done
+
+lemma fin_bv: "finite (bv x)"
+apply (induct x rule: inducts(9))
+apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
+apply (simp add: finb1 finb2 finb3)
+done
+
+lemma "bv x \<sharp>* fv_bv x"
+apply (induct x rule: inducts(9))
+apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
+apply (simp)
+oops
+
 lemma 
   assumes a01: "\<And>b. P1 b KStar"
   and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)"
@@ -152,10 +240,10 @@
          P2 (b :: 'b :: pt) ckind \<and>
          P3 (c :: 'c :: {pt,fs}) ty \<and>
          P4 (d :: 'd :: pt) ty_lst \<and>
-         P5 (e :: 'e :: pt) co \<and>
+         P5 (e :: 'e :: {pt,fs}) co \<and>
          P6 (f :: 'f :: pt) co_lst \<and>
          P7 (g :: 'g :: pt) trm \<and>
-         P8 (h :: 'h :: pt) assoc_lst \<and>
+         P8 (h :: 'h :: {pt,fs}) assoc_lst \<and>
          P9 (i :: 'i :: pt) pat \<and>
          P10 (j :: 'j :: pt) vt_lst \<and>
          P11 (k :: 'k :: pt) tvtk_lst \<and>
@@ -165,53 +253,142 @@
     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})) *})
-    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> c \<and> supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> ty)) \<sharp>* pa)")
-    prefer 2
+
+(* GOAL1 *)
+    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> c \<and>
+                       supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> ty)) \<sharp>* pa)")
+    apply clarify
+    apply (simp only: perm)
+    apply(rule_tac t="TAll (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> ty)"
+               and s="TAll (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> ty)" 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> ty) - {atom (pa \<bullet> p \<bullet> tvar)}"
+                and s="pa \<bullet> (p \<bullet> supp ty - {p \<bullet> atom tvar})" 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 a08)
+    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
+
+(* GOAL2 *)
+    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> e \<and>
+                       supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> co)) \<sharp>* pa)")
     apply clarify
     apply (simp only: perm)
-    apply(rule_tac t="TAll (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> ty)" and s="TAll (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> ty)" in subst)
-    apply (simp only: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.eq_iff)
+    apply(rule_tac t="CAll (p \<bullet> tvar) (p \<bullet> ckind) (p \<bullet> co)"
+               and s="CAll (pa \<bullet> p \<bullet> tvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> co)" in subst)
+    apply (simp only: eq_iff)
     apply (rule_tac x="-pa" in exI)
-    apply (simp add: alphas)
-    prefer 2
-    apply (rule a08)
-    apply simp
-    apply(rotate_tac 1)
-    apply(erule_tac x="(pa + p)" in allE)
-    apply simp
-    apply (simp add: eqvts eqvts_raw)
-    apply (simp add: eqvts eqvts_raw supp_Abs)
+    apply (simp add: alphas eqvts eqvts_raw supp_Abs fv_supp)
+    apply (rule_tac t="supp (pa \<bullet> p \<bullet> co) - {atom (pa \<bullet> p \<bullet> tvar)}"
+                and s="pa \<bullet> (p \<bullet> supp co - {p \<bullet> atom tvar})" in subst)
+    apply (simp add: eqvts)
+    apply (simp add: eqvts[symmetric])
     apply (rule conjI)
-    apply (simp add: eqvts[symmetric])
-    apply (simp add: fv_supp)
-    apply (rule_tac t="pa \<bullet> p \<bullet> supp ty - {pa \<bullet> p \<bullet> atom tvar}"
-                and s="pa \<bullet> (p \<bullet> supp ty - {p \<bullet> atom tvar})" in subst)
-    apply (simp add: eqvts)
     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 (simp add: fv_supp)
-    apply (simp add: eqvts[symmetric])
-    apply (rule_tac t="pa \<bullet> p \<bullet> supp ty - {pa \<bullet> p \<bullet> atom tvar}"
-                and s="pa \<bullet> (p \<bullet> supp ty - {p \<bullet> atom tvar})" in subst)
-    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 a15)
+    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
+
+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)")
+    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 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 (simp add: eqvts)
+    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 conjI)
+    apply (simp add: eqvts[symmetric])
+    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 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: 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 (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)
     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>