# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259082798 -3600
# Node ID 09e28d4c19aa13f541f18dba84297001c226f799
# Parent  577539640a47133ed315f2a61593729ee43e61d5
Lambda & SOLVED' for new quotient_tac

diff -r 577539640a47 -r 09e28d4c19aa LamEx.thy
--- a/LamEx.thy	Tue Nov 24 17:35:31 2009 +0100
+++ b/LamEx.thy	Tue Nov 24 18:13:18 2009 +0100
@@ -189,27 +189,69 @@
   @{thms ho_all_prs ho_ex_prs} *}
 
 ML {* fun lift_thm_lam lthy t = lift_thm lthy qty "lam" rsp_thms defs t *}
+ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
+ML {* val consts = lookup_quot_consts defs *}
+ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *}
+ML {* fun lift_tac_lam lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs *}
 
-ML {* val pi_var = lift_thm_lam @{context} @{thm pi_var_com} *}
+lemma "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)"
+apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *})
+done
+
 ML {* val pi_app = lift_thm_lam @{context} @{thm pi_app_com} *}
+lemma "(pi\<Colon>('x \<times> 'x) list) \<bullet> App (x\<Colon>lam) (xa\<Colon>lam) = App (pi \<bullet> x) (pi \<bullet> xa)"
+apply (tactic {* lift_tac_lam @{context} @{thm pi_app_com} 1 *})
+done
 ML {* val pi_lam = lift_thm_lam @{context} @{thm pi_lam_com} *}
+lemma "(pi\<Colon>('x \<times> 'x) list) \<bullet> Lam (a\<Colon>name) (x\<Colon>lam) = Lam (pi \<bullet> a) (pi \<bullet> x)"
+apply (tactic {* lift_tac_lam @{context} @{thm pi_lam_com} 1 *})
+done
 
 ML {* val fv_var = lift_thm_lam @{context} @{thm rfv_var} *}
+lemma "\<forall>a. fv (Var (a\<Colon>name)) = {a}"
+apply (tactic {* lift_tac_lam @{context} @{thm rfv_var} 1 *})
+done
 ML {* val fv_app = lift_thm_lam @{context} @{thm rfv_app} *}
+lemma "fv (App (x\<Colon>lam) (xa\<Colon>lam)) = fv x \<union> fv xa"
+(*apply (tactic {* lift_tac_lam @{context} @{thm rfv_app} 1 *})*)
+sorry
 ML {* val fv_lam = lift_thm_lam @{context} @{thm rfv_lam} *}
+lemma "fv (Lam (a\<Colon>name) (x\<Colon>lam)) = fv x - {a}"
+(*apply (tactic {* lift_tac_lam @{context} @{thm rfv_lam} 1 *})*)
+sorry
 
 ML {* val a1 = lift_thm_lam @{context} @{thm a1} *}
+lemma "(a\<Colon>name) = (b\<Colon>name) \<Longrightarrow> Var a = Var b"
+apply (tactic {* lift_tac_lam @{context} @{thm a1} 1 *})
+done
 ML {* val a2 = lift_thm_lam @{context} @{thm a2} *}
+lemma "\<lbrakk>(x\<Colon>lam) = (xa\<Colon>lam); (xb\<Colon>lam) = (xc\<Colon>lam)\<rbrakk> \<Longrightarrow> App x xb = App xa xc"
+apply (tactic {* lift_tac_lam @{context} @{thm a2} 1 *})
+done
 ML {* val a3 = lift_thm_lam @{context} @{thm a3} *}
-
-thm a2
-ML {* val t_a = atomize_thm @{thm a2} *}
-ML {* val t_r = regularize t_a @{typ rlam} @{term alpha} @{thm alpha_EQUIV} @{thm alpha_refl} @{context} *}
+lemma "\<lbrakk>(x\<Colon>lam) = [(a\<Colon>name, b\<Colon>name)] \<bullet> (xa\<Colon>lam); a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> Lam a x = Lam b xa"
+(*apply (tactic {* lift_tac_lam @{context} @{thm a3} 1 *})*)
+sorry
 
 ML {* val alpha_cases = lift_thm_lam @{context} @{thm alpha.cases} *}
+lemma "\<lbrakk>(x\<Colon>lam) = (xa\<Colon>lam); \<And>(a\<Colon>name) b\<Colon>name. \<lbrakk>x = Var a; xa = Var b; a = b\<rbrakk> \<Longrightarrow> P\<Colon>bool;
+     \<And>(x\<Colon>lam) (xa\<Colon>lam) (xb\<Colon>lam) xc\<Colon>lam. \<lbrakk>x = App x xb; xa = App xa xc; x = xa; xb = xc\<rbrakk> \<Longrightarrow> P;
+     \<And>(x\<Colon>lam) (a\<Colon>name) (b\<Colon>name) xa\<Colon>lam. \<lbrakk>x = Lam a x; xa = Lam b xa; x = [(a, b)] \<bullet> xa; a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> P\<rbrakk>
+    \<Longrightarrow> P"
+(* apply (tactic {* lift_tac_lam @{context} @{thm alpha.cases} 1 *}) *)
+sorry
 ML {* val alpha_induct = lift_thm_lam @{context} @{thm alpha.induct} *}
+lemma "\<lbrakk>(qx\<Colon>lam) = (qxa\<Colon>lam); \<And>(a\<Colon>name) b\<Colon>name. a = b \<Longrightarrow> (qxb\<Colon>lam \<Rightarrow> lam \<Rightarrow> bool) (Var a) (Var b);
+     \<And>(x\<Colon>lam) (xa\<Colon>lam) (xb\<Colon>lam) xc\<Colon>lam. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc);
+     \<And>(x\<Colon>lam) (a\<Colon>name) (b\<Colon>name) xa\<Colon>lam.
+        \<lbrakk>x = [(a, b)] \<bullet> xa; qxb x ([(a, b)] \<bullet> xa); a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> qxb (Lam a x) (Lam b xa)\<rbrakk>
+    \<Longrightarrow> qxb qx qxa"
+(* apply (tactic {* lift_tac_lam @{context} @{thm alpha.induct} 1 *}) *)
+sorry
 
-ML {* val var_inject = lift_thm_lam @{context} @{thm rvar_inject} *}
+lemma "(Var a = Var b) = (a = b)"
+apply (tactic {* lift_tac_lam @{context} @{thm rvar_inject} 1 *})
+done
 
 local_setup {*
   Quotient.note (@{binding "pi_var"}, pi_var) #> snd #>
diff -r 577539640a47 -r 09e28d4c19aa QuotMain.thy
--- a/QuotMain.thy	Tue Nov 24 17:35:31 2009 +0100
+++ b/QuotMain.thy	Tue Nov 24 18:13:18 2009 +0100
@@ -841,8 +841,8 @@
     bex_rsp_tac ctxt,
     FIRST' (map rtac rsp_thms),
     rtac refl,
-    (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
-    (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
+    (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thm)])),
+    (APPLY_RSP_TAC rty ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thm), SOLVES' (quotient_tac quot_thm)])),
     Cong_Tac.cong_tac @{thm cong},
     rtac @{thm ext},
     rtac reflex_thm,