--- a/Nominal-General/nominal_library.ML	Thu Aug 12 21:29:35 2010 +0800
+++ b/Nominal-General/nominal_library.ML	Sat Aug 14 16:54:41 2010 +0800
@@ -55,6 +55,9 @@
   (* transformations of premises in inductions *)
   val transform_prem1: Proof.context -> string list -> thm -> thm
   val transform_prem2: Proof.context -> string list -> thm -> thm
+
+  (* transformation into the object logic *)
+  val atomize: thm -> thm
 end
 
 
@@ -256,6 +259,9 @@
   map_thm ctxt (split_conj2 names) (etac conjunct2 1) thm
 
 
+(* transformes a theorem into one of the object logic *)
+val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars
+
 
 end (* structure *)
 

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

--- a/Nominal/NewParser.thy	Thu Aug 12 21:29:35 2010 +0800
+++ b/Nominal/NewParser.thy	Sat Aug 14 16:54:41 2010 +0800
@@ -438,15 +438,19 @@
     then raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy6 
     else raise TEST lthy6
   
-  (* auxiliary lemmas for respectfulness proofs *)
-  val raw_funs_rsp = raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs 
+  (* respectfulness proofs *)
+  val raw_funs_rsp_aux = raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs 
     raw_bns raw_fv_bns alpha_induct (raw_bn_eqs @ raw_fv_defs) lthy6
+  val raw_funs_rsp = map mk_funs_rsp raw_funs_rsp_aux
 
   val raw_size_rsp = raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct 
     (raw_size_thms @ raw_size_eqvt) lthy6
+    |> map mk_funs_rsp
 
   val raw_constrs_rsp = raw_constrs_rsp all_raw_constrs alpha_trms alpha_intros
-    (alpha_bn_imp_thms @ raw_funs_rsp) lthy6 
+    (alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy6 
+
+  val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt
 
   (* defining the quotient type *)
   val _ = warning "Declaring the quotient types"
@@ -508,13 +512,10 @@
      ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) 
      ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms)
      ||>> Local_Theory.note ((@{binding "funs_rsp"}, []), raw_funs_rsp)
-     ||>> Local_Theory.note ((@{binding "size_eqvt"}, []), raw_size_eqvt)
-     ||>> Local_Theory.note ((@{binding "size_simps"}, []), raw_size_thms)
      ||>> Local_Theory.note ((@{binding "size_rsp"}, []), raw_size_rsp)
      ||>> Local_Theory.note ((@{binding "constrs_rsp"}, []), raw_constrs_rsp)
-     ||>> Local_Theory.note ((@{binding "alpha_sym_thms"}, []), alpha_sym_thms)
-     ||>> Local_Theory.note ((@{binding "alpha_trans_thms"}, []), alpha_trans_thms)
-  
+     ||>> Local_Theory.note ((@{binding "permute_rsp"}, []), alpha_permute_rsp)
+
   val _ = 
     if get_STEPS lthy > 17
     then true else raise TEST lthy8'

--- a/Nominal/nominal_dt_alpha.ML	Thu Aug 12 21:29:35 2010 +0800
+++ b/Nominal/nominal_dt_alpha.ML	Sat Aug 14 16:54:41 2010 +0800
@@ -30,7 +30,8 @@
   val raw_size_rsp_aux: term list -> thm -> thm list -> Proof.context -> thm list
   val raw_constrs_rsp: term list -> term list -> thm list -> thm list -> Proof.context -> thm list
 
-  val resolve_fun_rel: thm -> thm
+  val mk_funs_rsp: thm -> thm
+  val mk_alpha_permute_rsp: thm -> thm 
 end
 
 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA =
@@ -559,21 +560,21 @@
 
 (** proves the equivp predicate for all alphas **)
 
-val equivp_intro = 
-  @{lemma "[|!x. R x x; !x y. R x y --> R y x; !x y. R x y --> (!z. R y z --> R x z)|] ==> equivp R"
-    by (rule equivpI, unfold reflp_def symp_def transp_def, blast+)}
+val transp_def' =
+  @{lemma "transp R == !x y. R x y --> (!z. R y z --> R x z)" 
+    by (rule eq_reflection, auto simp add: transp_def)}
 
 fun raw_prove_equivp alphas refl symm trans ctxt = 
 let
-  val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars
-  val refl' = map atomize refl
-  val symm' = map atomize symm
-  val trans' = map atomize trans
+  val refl' = map (fold_rule @{thms reflp_def} o atomize) refl
+  val symm' = map (fold_rule @{thms symp_def} o atomize) symm
+  val trans' = map (fold_rule [transp_def'] o atomize) trans
+
   fun prep_goal t = 
     HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t) 
 in    
   Goal.prove_multi ctxt [] [] (map prep_goal alphas)
-  (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (rtac equivp_intro THEN' 
+  (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (rtac @{thm equivpI} THEN' 
      RANGE [resolve_tac refl', resolve_tac symm', resolve_tac trans']))))
 end
 
@@ -613,10 +614,11 @@
 let
   val arg_ty = domain_type o fastype_of 
   val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms
+  fun mk_eq' t x y = HOLogic.mk_eq (t $ x, t $ y)
 
-  val prop1 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => HOLogic.mk_eq (t $ x, t $ y))) fvs
-  val prop2 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => HOLogic.mk_eq (t $ x, t $ y))) bns
-  val prop3 = map2 (fn t1 => fn t2 => (t1, fn (x, y) => HOLogic.mk_eq (t2 $ x, t2 $ y))) alpha_bn_trms fv_bns
+  val prop1 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) fvs
+  val prop2 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) (bns @ fv_bns)
+  val prop3 = map2 (fn t1 => fn t2 => (t1, fn (x, y) => mk_eq' t2 x y)) alpha_bn_trms fv_bns
   
   val ss = HOL_ss addsimps (simps @ @{thms alphas prod_fv.simps set.simps append.simps} 
     @ @{thms Un_assoc Un_insert_left Un_empty_right Un_empty_left}) 
@@ -690,17 +692,28 @@
 end
 
 
-(* resolve with @{thm fun_relI} *)
+(* transformation of the natural rsp-lemmas into the standard form *)
+
+val fun_rsp = @{lemma
+  "(!x y. R x y --> f x = f y) ==> (R ===> (op =)) f f" by simp}
+
+fun mk_funs_rsp thm = 
+ thm
+ |> atomize
+ |> single
+ |> curry (op OF) fun_rsp
 
-fun resolve_fun_rel thm =
-let 
-  val fun_rel = @{thm fun_relI}
-  val thm' = forall_intr_vars thm
-  val cinsts = Thm.match (cprem_of fun_rel 1, cprop_of thm')
-  val fun_rel' = Thm.instantiate cinsts fun_rel
-in
-  thm' COMP fun_rel'
-end 
+
+val permute_rsp = @{lemma 
+  "(!x y p. R x y --> R (permute p x) (permute p y)) 
+     ==> ((op =) ===> R ===> R) permute permute"  by simp}
+
+fun mk_alpha_permute_rsp thm = 
+ thm
+ |> atomize
+ |> single
+ |> curry (op OF) permute_rsp
+
 
 
 end (* structure *)