# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1256802394 -3600
# Node ID 811f17de4031e765ae413a392a296222368737f1
# Parent  fcff14e578d33cbfccd655db57d8d8f20e675407
Lifting of the 3 lemmas in LamEx

diff -r fcff14e578d3 -r 811f17de4031 LamEx.thy
--- a/LamEx.thy	Thu Oct 29 08:06:49 2009 +0100
+++ b/LamEx.thy	Thu Oct 29 08:46:34 2009 +0100
@@ -56,19 +56,19 @@
 thm perm_lam_def
 
 (* lemmas that need to lift *)
-lemma
+lemma pi_var_com:
   fixes pi::"'x prm"
-  shows "(pi\<bullet>Var a) = Var (pi\<bullet>a)"
+  shows "(pi\<bullet>rVar a) \<approx> rVar (pi\<bullet>a)"
   sorry
 
-lemma
+lemma pi_app_com:
   fixes pi::"'x prm"
-  shows "(pi\<bullet>App t1 t2) = App (pi\<bullet>t1) (pi\<bullet>t2)"
+  shows "(pi\<bullet>rApp t1 t2) \<approx> rApp (pi\<bullet>t1) (pi\<bullet>t2)"
   sorry
 
-lemma
+lemma pi_lam_com:
   fixes pi::"'x prm"
-  shows "(pi\<bullet>Lam a t) = Lam (pi\<bullet>a) (pi\<bullet>t)"
+  shows "(pi\<bullet>rLam a t) \<approx> rLam (pi\<bullet>a) (pi\<bullet>t)"
   sorry
 
 lemma real_alpha:
@@ -82,17 +82,30 @@
 
 (* Construction Site code *)
 
-lemma perm_rsp: "op = ===> alpha ===> alpha op \<bullet> op \<bullet>"
+lemma perm_rsp: "(op = ===> alpha ===> alpha) op \<bullet> op \<bullet>"
   apply(auto)
   (* this is propably true if some type conditions are imposed ;o) *)
   sorry
 
-lemma fresh_rsp: "op = ===> (alpha ===> op =) fresh fresh" 
+lemma fresh_rsp: "(op = ===> alpha ===> op =) fresh fresh" 
   apply(auto)
   (* this is probably only true if some type conditions are imposed *)
   sorry
 
-lemma rLam_rsp: "op = ===> (alpha ===> alpha) rLam rLam"
+lemma rVar_rsp: "(op = ===> alpha) rVar rVar"
+  apply(auto)
+  apply(rule a1)
+  apply(simp)
+  done
+
+lemma rApp_rsp: "(alpha ===> alpha ===> alpha) rApp rApp"
+  apply(auto)
+  apply(rule a2)
+  apply (assumption)
+  apply (assumption)
+  done
+
+lemma rLam_rsp: "(op = ===> alpha ===> alpha) rLam rLam"
   apply(auto)
   apply(rule a3)
   apply(rule_tac t="[(x,x)]\<bullet>y" and s="y" in subst)
@@ -105,8 +118,8 @@
   apply(simp add: abs_fresh)
   done
 
-ML {* val defs = @{thms Var_def App_def Lam_def} *}
-ML {* val consts = [@{const_name "rVar"}, @{const_name "rApp"}, @{const_name "rLam"}]; *}
+ML {* val defs = @{thms Var_def App_def Lam_def perm_lam_def} *}
+ML {* val consts = [@{const_name "rVar"}, @{const_name "rApp"}, @{const_name "rLam"}, @{const_name "perm"}]; *}
 
 ML {* val rty = @{typ "rlam"} *}
 ML {* val qty = @{typ "lam"} *}
@@ -114,28 +127,12 @@
 ML {* val rel_eqv = (#equiv_thm o hd) (quotdata_lookup @{context}) *}
 ML {* val rel_refl = @{thm EQUIV_REFL} OF [rel_eqv] *}
 ML {* val quot = @{thm QUOTIENT_lam} *}
-ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rLam_rsp} @ @{thms ho_all_prs ho_ex_prs} *}
+ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp} @ @{thms ho_all_prs ho_ex_prs} *}
 ML {* val trans2 = @{thm QUOT_TYPE_I_lam.R_trans2} *}
 ML {* val reps_same = @{thm QUOT_TYPE_I_lam.REPS_same} *}
 
-ML {*
-fun lift_thm_lam lthy t =
-  lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t
-*}
-ML {* lift_thm_lam @{context} @{thm a3} *}
-
-local_setup {*
-  old_make_const_def @{binding lperm} @{term "perm :: ('a \<times> 'a) list \<Rightarrow> rlam \<Rightarrow> rlam"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd
-*}
-
-ML {* val consts = @{const_name perm} :: consts *}
-ML {* val defs = @{thms lperm_def} @ defs *}
-ML {*
-fun lift_thm_lam lthy t =
-  lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t
-*}
-ML {* val t_b = lift_thm_lam @{context} @{thm a3} *}
-ML {* val rr = @{thm eq_reflection} OF [hd (rev (add_lower_defs @{context} @{thms lperm_def}))] *}
+ML {* add_lower_defs @{context} @{thms perm_lam_def} *}
+ML {* val rr = @{thm eq_reflection} OF [hd (rev (add_lower_defs @{context} @{thms perm_lam_def}))] *}
 lemma prod_fun_id: "prod_fun id id = id"
   apply (simp add: prod_fun_def)
 done
@@ -143,10 +140,18 @@
   apply (induct x)
   apply (simp_all add: map.simps)
 done
+ML {* val rrr = repeat_eqsubst_thm @{context} @{thms prod_fun_id map_id} rr *}
+ML {*
+fun lift_thm_lam lthy t =
+  lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t
+*}
+ML {* val t1 = Toplevel.program (fn () => lift_thm_lam @{context} @{thm pi_var_com}) *}
+ML {* val t2 = eqsubst_thm @{context} [rrr] (atomize_thm t1) *}
+ML {* ObjectLogic.rulify t2 *}
+ML {* val t1 = Toplevel.program (fn () => lift_thm_lam @{context} @{thm pi_app_com}) *}
+ML {* val t2 = repeat_eqsubst_thm @{context} [rrr] (atomize_thm t1) *}
+ML {* ObjectLogic.rulify t2 *}
+ML {* val t1 = Toplevel.program (fn () => lift_thm_lam @{context} @{thm pi_lam_com}) *}
+ML {* val t2 = repeat_eqsubst_thm @{context} [rrr] (atomize_thm t1) *}
+ML {* ObjectLogic.rulify t2 *}
 
-ML {* val rrr = repeat_eqsubst_thm @{context} @{thms prod_fun_id map_id} rr *}
-ML {* val t_b' = eqsubst_thm @{context} [rrr] (atomize_thm t_b) *}
-ML {* ObjectLogic.rulify t_b' *}
-
-ML {* val t_u = MetaSimplifier.rewrite_rule @{thms fresh_def supp_def} @{thm a3} *}
-ML {* Toplevel.program (fn () => lift_thm_lam @{context} t_u) *} (* Is not ture *)