--- a/Nominal/Ex/CoreHaskell.thy	Wed Aug 25 23:16:42 2010 +0800
+++ b/Nominal/Ex/CoreHaskell.thy	Thu Aug 26 02:08:00 2010 +0800
@@ -8,9 +8,10 @@
 atom_decl cvar
 atom_decl tvar
 
-declare [[STEPS = 21]]
+declare [[STEPS = 100]]
 
-nominal_datatype tkind =
+nominal_datatype core_haskell: 
+ tkind =
   KStar
 | KFun "tkind" "tkind"
 and ckind =
@@ -85,31 +86,19 @@
 | "bv_cvs CvsNil = []"
 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"
 
-(* can lift *)
-
-thm distinct
-thm induct
-thm exhaust
-thm fv_defs
-thm bn_defs
-thm perm_simps
-thm eq_iff
-thm fv_bn_eqvt
-thm size_eqvt
-
+(* generated theorems *)
 
-
-
+thm core_haskell.distinct
+thm core_haskell.induct
+thm core_haskell.exhaust
+thm core_haskell.fv_defs
+thm core_haskell.bn_defs
+thm core_haskell.perm_simps
+thm core_haskell.eq_iff
+thm core_haskell.fv_bn_eqvt
+thm core_haskell.size_eqvt
 
-lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15)
-lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp]
-lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm
-lemmas eq_iff=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.eq_iff
-lemmas inducts=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.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_vars_raw_alpha_tvars_raw_alpha_cvars_raw_alpha_bv_raw_alpha_bv_vs_raw_alpha_bv_tvs_raw_alpha_bv_cvs_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_vars_raw_alpha_tvars_raw_alpha_cvars_raw_alpha_bv_raw_alpha_bv_vs_raw_alpha_bv_tvs_raw_alpha_bv_cvs_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)
@@ -397,7 +386,7 @@
     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})) *})
 
-(* GOAL1 *)
+--"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
@@ -435,7 +424,7 @@
     apply (simp only: supp_abs eqvts)
     apply blast
 
-(* GOAL2 *)
+--"GOAL2"
     apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> cvar))) \<sharp> e \<and>
                        supp (Abs (p \<bullet> {atom cvar}) (p \<bullet> co)) \<sharp>* pa)")
     apply clarify
@@ -474,7 +463,7 @@
     apply blast
 
 
-(* GOAL3 a copy-and-paste of Goal2 with consts and variable names changed *)
+--"GOAL3 a copy-and-paste of Goal2 with consts and variable names changed"
     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
@@ -512,7 +501,7 @@
     apply (simp only: supp_abs eqvts)
     apply blast
 
-(* GOAL4 a copy-and-paste *)
+--"GOAL4 a copy-and-paste"
     apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> cvar))) \<sharp> g \<and>
                        supp (Abs (p \<bullet> {atom cvar}) (p \<bullet> trm)) \<sharp>* pa)")
     apply clarify
@@ -551,7 +540,7 @@
     apply blast
 
 
-(* GOAL5 a copy-and-paste *)
+--"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
@@ -590,7 +579,7 @@
     apply blast
 
 
-(* GOAL6 a copy-and-paste *)
+--"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
@@ -629,7 +618,7 @@
     apply (simp only: supp_abs eqvts)
     apply blast
 
-(* MAIN ACons Goal *)
+--"MAIN ACons Goal"
     apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (set (bv (p \<bullet> pat)))) \<sharp>* h \<and>
                        supp (Abs_lst (p \<bullet> (bv pat)) (p \<bullet> trm)) \<sharp>* pa)")
     apply clarify
@@ -655,6 +644,7 @@
   moreover have "P9  i (permute_bv 0 (0 \<bullet> pt))" and "P10 j (permute_bv_vs 0 (0 \<bullet> vars))" and "P11 k (permute_bv_tvs 0 (0 \<bullet> tvars))" and "P12 l (permute_bv_cvs 0 (0 \<bullet> cvars))" using a1 a2 a3 a4 by (blast+)
   ultimately show ?thesis by (simp_all add: permute_bv_zero1 permute_bv_zero2)
 qed
+*)
 
 section {* test about equivariance for alpha *}