# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1256834103 -3600
# Node ID e9cc3a3aa5d195b96333cc4d20ffb8456af457ed
# Parent  80f1df49b940f1112b06976141356cb7402760eb
Tried manually lifting real_alpha

diff -r 80f1df49b940 -r e9cc3a3aa5d1 LamEx.thy
--- a/LamEx.thy	Thu Oct 29 13:30:11 2009 +0100
+++ b/LamEx.thy	Thu Oct 29 17:35:03 2009 +0100
@@ -53,6 +53,12 @@
 
 end
 
+(*quotient_def (for lam)
+  abs_fun_lam :: "'x prm \<Rightarrow> lam \<Rightarrow> lam"
+where
+  "perm_lam \<equiv> (perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam)"*)
+
+
 thm perm_lam_def
 
 (* lemmas that need to lift *)
@@ -144,6 +150,8 @@
 ML {* lift_thm_lam @{context} @{thm pi_app_com} *}
 ML {* lift_thm_lam @{context} @{thm pi_lam_com} *}
 
+thm supp_def
+
 fun
   option_map::"('a \<Rightarrow> 'b) \<Rightarrow> ('a noption) \<Rightarrow> ('b noption)"
 where
@@ -207,7 +215,6 @@
 lemma quotient_cheat: "QUOTIENT op = (option_map ABS_lam) (option_map REP_lam)"
 sorry
 
-
 ML {* val rsp_thms = @{thms abs_fun_rsp OPT_QUOTIENT eq_rsp2 quotient_cheat perm_rsp_eq fresh_rsp_eq} @ rsp_thms *}
 ML {*
 fun lift_thm_lam lthy t =
@@ -216,21 +223,85 @@
 
 thm a3
 ML {* Toplevel.program (fn () => lift_thm_lam @{context} @{thm a3}) *}
-ML {* val t_u = MetaSimplifier.rewrite_rule @{thms fresh_def supp_def} @{thm a3} *}
-ML {* Toplevel.program (fn () => lift_thm_lam @{context} t_u) *}
+thm a3
+ML {* val t_u1 = eqsubst_thm @{context} @{thms abs_fresh(1)} (atomize_thm @{thm a3}) *}
+ML {* val t_u = MetaSimplifier.rewrite_rule @{thms fresh_def supp_def} t_u1 *}
 
-ML t_u
 ML {* val t_a = atomize_thm t_u *}
 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *}
-ML {* val t = (fst o Thm.dest_comb o snd o Thm.dest_comb) (cprop_of t_u) *}
-ML {* val t = (snd o Thm.dest_comb o snd o Thm.dest_comb) t *}
-ML {* val t = (snd o Thm.dest_comb o snd o Thm.dest_comb) t *}
-ML {* val t = (snd o (Thm.dest_abs NONE) o snd o Thm.dest_comb) t *}
-ML {* val t = (snd o Thm.dest_comb o snd o Thm.dest_comb) t *}
-ML {* val t = (snd o (Thm.dest_abs NONE) o snd o Thm.dest_comb) t *}
-ML {* val t = (fst o Thm.dest_comb o snd o Thm.dest_comb) t *}
-ML {* term_of t *}
-term "[b].(s::rlam)"
-thm abs_fun_def
-ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *}
+ML {* fun r_mk_comb_tac_lam ctxt =
+  r_mk_comb_tac ctxt rty quot rel_refl trans2 rsp_thms
+*}
+
+instance lam :: fs_name
+apply(intro_classes)
+sorry
 
+prove asdf: {* Logic.mk_implies (concl_of t_r, (@{term "Trueprop (\<forall>t\<Colon>rlam\<in>Respects
+          alpha.
+         \<forall>(a\<Colon>name) b\<Colon>name.
+            \<forall>s\<Colon>rlam\<in>Respects
+                alpha.
+               t \<approx> ([(a,
+                 b)] \<bullet> s) \<longrightarrow>
+               a = b \<or>
+               a
+               \<notin> {a\<Colon>name.
+                infinite
+                 {b\<Colon>name. Not
+                  (([(a, b)] \<bullet>
+                  s) \<approx>
+                  s)}} \<longrightarrow>
+               rLam a
+                t \<approx> rLam
+                 b s)"})) *}
+apply (tactic {* full_simp_tac ((Simplifier.context @{context} HOL_ss) addsimps
+        [(@{thm equiv_res_forall} OF [rel_eqv]),
+         (@{thm equiv_res_exists} OF [rel_eqv])]) 1 *})
+apply (rule allI)
+apply (drule_tac x="t" in spec)
+apply (rule allI)
+apply (drule_tac x="a" in spec)
+apply (rule allI)
+apply (drule_tac x="b" in spec)
+apply (rule allI)
+apply (drule_tac x="s" in spec)
+apply (rule impI)
+apply (drule_tac mp)
+apply (simp)
+apply (simp)
+apply (rule impI)
+apply (rule a3)
+apply (simp)
+apply (simp add: abs_fresh(1))
+apply (case_tac "a = b")
+apply (simp)
+apply (simp)
+apply (auto)
+apply (unfold fresh_def)
+apply (unfold supp_def)
+apply (simp)
+prefer 2
+apply (simp)
+sorry
+
+ML {* val abs = findabs rty (prop_of t_a) *}
+ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *}
+ML {* val t_defs_sym = add_lower_defs @{context} defs *}
+
+ML {* val t_r' = @{thm asdf} OF [t_r] *}
+ML {* val t_t = repabs @{context} t_r' consts rty qty quot rel_refl trans2 rsp_thms *}
+ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *}
+ML {* val t_a = simp_allex_prs @{context} quot t_l *}
+ML {* val t_d = repeat_eqsubst_thm @{context} t_defs_sym t_a *}
+ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *}
+ML {* val tt = MetaSimplifier.rewrite_rule [symmetric @{thm supp_def}, symmetric @{thm fresh_def}] t_r *}
+ML {* val rr = @{thm sym} OF @{thms abs_fresh(1)} *}
+ML {* val ttt = eqsubst_thm @{context} [rr] tt *}
+ML {* ObjectLogic.rulify ttt *}
+
+lemma
+  assumes a: "a \<notin> {a\<Colon>name. infinite {b\<Colon>name. \<not> ([(a, b)] \<bullet> s) \<approx> s}}"
+  shows "a \<notin> {a\<Colon>name. infinite {b\<Colon>name. [(a, b)] \<bullet> s \<noteq> s}}"
+  using a apply simp
+  sorry (* Not true... *)