--- a/Nominal/Ex/SingleLet.thy	Thu Aug 12 21:29:35 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Sat Aug 14 16:54:41 2010 +0800
@@ -21,39 +21,29 @@
 where
   "bn (As x y t) = {atom x}"
 
+(* can lift *)
+thm distinct
+thm trm_raw_assg_raw.inducts
+thm fv_defs
 
 
-thm alpha_sym_thms
-thm alpha_trans_thms
-thm size_eqvt
-thm size_simps
-thm size_rsp
-thm alpha_bn_imps
-thm distinct
+(* cannot lift yet *)
 thm eq_iff
 thm eq_iff_simps
-thm fv_defs
 thm perm_simps
 thm perm_laws
+thm trm_raw_assg_raw.size(9 - 16)
+
+(* rsp lemmas *)
+thm size_rsp
 thm funs_rsp
 thm constrs_rsp
+thm permute_rsp
 
 declare constrs_rsp[quot_respect]
-(* declare funs_rsp[quot_respect] *)
-
-typ trm
-typ assg
-term Var 
-term App
-term Baz
-term bn
-term fv_trm
-term alpha_bn
-
-lemma [quot_respect]:
-  "(op = ===> alpha_trm_raw ===> alpha_trm_raw) permute permute"
-apply(simp)
-sorry
+declare funs_rsp[quot_respect] 
+declare size_rsp[quot_respect]
+declare permute_rsp[quot_respect]
 
 ML {*
   val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct}
@@ -67,29 +57,113 @@
   val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms fv_defs}
 *}
 
-thm perm_defs[no_vars]
+instantiation trm and assg :: size 
+begin
+
+quotient_definition 
+  "size_trm :: trm \<Rightarrow> nat"
+is "size :: trm_raw \<Rightarrow> nat"
+
+quotient_definition 
+  "size_assg :: assg \<Rightarrow> nat"
+is "size :: assg_raw \<Rightarrow> nat"
+
+instance .. 
+
+end 
+
+ML {* 
+  val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.size(9 - 16)}
+*}
+
+
+
+instantiation trm and assg :: pt
+begin
+
+quotient_definition 
+  "permute_trm :: perm => trm => trm" 
+  is "permute :: perm \<Rightarrow> trm_raw \<Rightarrow> trm_raw"
+
+quotient_definition 
+  "permute_assg :: perm => assg => assg" 
+  is "permute :: perm \<Rightarrow> assg_raw \<Rightarrow> assg_raw"
+
+lemma qperm_laws:
+  fixes t::trm and a::assg
+  shows "permute 0 t = t"
+  and   "permute 0 a = a" 
+sorry
+  
+instance
+apply(default)
+sorry
+
+end
+
+
+(*
+lemma [quot_respect]:
+  "(alpha_assg_raw ===> alpha_assg_raw ===> op =) alpha_bn_raw alpha_bn_raw"
+apply(simp)
+sorry
+*)
+
+ML {*
+  val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff[unfolded alphas prod_fv.simps prod_rel.simps prod_alpha_def]}
+*}
+
+ML {*
+  val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff[unfolding alphas]}
+*}
+
+
+(*
+instance trm :: size ..
+instance assg :: size ..
+
+lemma "(size (Var x)) = 0"
+apply(descending)
+apply(rule trm_raw_assg_raw.size(9 - 16))
+apply(simp)
+*)
+
+ML {*
+  val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff[unfolding alphas]}
+*}
+
+section {* NOT *}
+
+
+ML {* 
+  val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.size(9 - 16)}
+*}
+
+
+ML {*
+  val thms_p = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_simps(1)}
+*}
+
+ML {*
+  val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_laws}
+*}
+
+
+ML {*
+  val thms_p = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_simps(1)}
+*}
 
 instance trm :: pt sorry
 instance assg :: pt sorry
 
-lemma b1:
-  "p \<bullet> Var name = Var (p \<bullet> name)"
-  "p \<bullet> App trm1 trm2 = App (p \<bullet> trm1) (p \<bullet> trm2)"
-  "p \<bullet> Lam name trm = Lam (p \<bullet> name) (p \<bullet> trm)"
-  "p \<bullet> Let assg trm = Let (p \<bullet> assg) (p \<bullet> trm)"
-  "p \<bullet> Foo name1 name2 trm1 trm2 trm3 =
-     Foo (p \<bullet> name1) (p \<bullet> name2) (p \<bullet> trm1) (p \<bullet> trm2) (p \<bullet> trm3)"
-  "p \<bullet> Bar name1 name2 trm = Bar (p \<bullet> name1) (p \<bullet> name2) (p \<bullet> trm)"
-  "p \<bullet> Baz name trm1 trm2 = Baz (p \<bullet> name) (p \<bullet> trm1) (p \<bullet> trm2)"
-  "p \<bullet> As name1 name2 trm = As (p \<bullet> name1) (p \<bullet> name2) (p \<bullet> trm)"
-sorry
+
+
 
 
-(*
-ML {*
-  val thms_p = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_defs}
-*}
-*)
+
+
+
+
 
 thm eq_iff[no_vars]