# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259480886 -3600
# Node ID 586e3dc4afdb04ecb2aaba55d56bc05906d379bf
# Parent  2dc708ddb93ab08136724b5492f534b42a413ad1
Added 'TRY' to refl in clean_tac to get as far as possible. Removed unnecessary [quot_rsp] in FSet. Added necessary [quot_rsp] and one lifted thm in LamEx.

diff -r 2dc708ddb93a -r 586e3dc4afdb FSet.thy
--- a/FSet.thy	Sun Nov 29 03:59:18 2009 +0100
+++ b/FSet.thy	Sun Nov 29 08:48:06 2009 +0100
@@ -14,9 +14,7 @@
 
 lemma list_eq_refl:
   shows "xs \<approx> xs"
-  apply (induct xs)
-   apply (auto intro: list_eq.intros)
-  done
+  by (induct xs) (auto intro: list_eq.intros)
 
 lemma equiv_list_eq:
   shows "EQUIV list_eq"
@@ -178,7 +176,7 @@
 
 ML {* val defs = @{thms EMPTY_def IN_def FUNION_def CARD_def INSERT_def fmap_def FOLD_def} *}
 
-lemma memb_rsp[quot_rsp]:
+lemma memb_rsp:
   fixes z
   assumes a: "x \<approx> y"
   shows "(z memb x) = (z memb y)"
@@ -188,7 +186,7 @@
   "(op = ===> (op \<approx> ===> op =)) (op memb) (op memb)"
   by (simp add: memb_rsp)
 
-lemma card1_rsp[quot_rsp]:
+lemma card1_rsp:
   fixes a b :: "'a list"
   assumes e: "a \<approx> b"
   shows "card1 a = card1 b"
@@ -246,7 +244,7 @@
   apply (rule rev_rsp)
   done
 
-lemma append_rsp[quot_rsp]:
+lemma append_rsp:
   assumes a : "l1 \<approx> r1"
   assumes b : "l2 \<approx> r2 "
   shows "(l1 @ l2) \<approx> (r1 @ r2)"
@@ -265,7 +263,7 @@
   "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
   by (simp add: append_rsp)
 
-lemma map_rsp[quot_rsp]:
+lemma map_rsp:
   assumes a: "a \<approx> b"
   shows "map f a \<approx> map f b"
   using a
diff -r 2dc708ddb93a -r 586e3dc4afdb IntEx.thy
--- a/IntEx.thy	Sun Nov 29 03:59:18 2009 +0100
+++ b/IntEx.thy	Sun Nov 29 08:48:06 2009 +0100
@@ -215,6 +215,8 @@
 apply(simp add: map_prs)
 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm ho_tst})) (term_of qtm) *}
+apply(simp only: map_prs)
+apply(tactic {* clean_tac @{context} [quot] defs aps 1 *})
 sorry
 
 (*
diff -r 2dc708ddb93a -r 586e3dc4afdb LamEx.thy
--- a/LamEx.thy	Sun Nov 29 03:59:18 2009 +0100
+++ b/LamEx.thy	Sun Nov 29 08:48:06 2009 +0100
@@ -119,37 +119,35 @@
   shows "(pi\<bullet>rLam a t) \<approx> rLam (pi\<bullet>a) (pi\<bullet>t)"
   sorry
 
+
+
 lemma real_alpha:
-  assumes "t = [(a,b)]\<bullet>s" "a\<sharp>[b].s"
+  assumes a: "t = [(a,b)]\<bullet>s" "a\<sharp>[b].s"
   shows "Lam a t = Lam b s"
+using a
+unfolding fresh_def supp_def
 sorry
 
-lemma perm_rsp: 
+lemma perm_rsp[quot_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 rVar_rsp: "(op = ===> alpha) rVar rVar"
-  apply(auto)
-  apply(rule a1)
-  apply(simp)
-  done
+lemma rVar_rsp[quot_rsp]:
+  "(op = ===> alpha) rVar rVar"
+by (auto intro:a1)
 
-lemma rApp_rsp: "(alpha ===> alpha ===> alpha) rApp rApp"
-  apply(auto)
-  apply(rule a2)
-  apply (assumption)
-  apply (assumption)
-  done
+lemma rApp_rsp[quot_rsp]: "(alpha ===> alpha ===> alpha) rApp rApp"
+by (auto intro:a2)
 
-lemma rLam_rsp: "(op = ===> alpha ===> alpha) rLam rLam"
+lemma rLam_rsp[quot_rsp]: "(op = ===> alpha ===> alpha) rLam rLam"
   apply(auto)
   apply(rule a3)
   apply(rule_tac t="[(x,x)]\<bullet>y" and s="y" in subst)
@@ -162,7 +160,7 @@
   apply(simp add: abs_fresh)
   done
 
-lemma rfv_rsp: "(alpha ===> op =) rfv rfv"
+lemma rfv_rsp[quot_rsp]: "(alpha ===> op =) rfv rfv"
   sorry
 
 lemma rvar_inject: "rVar a \<approx> rVar b = (a = b)"
@@ -179,7 +177,7 @@
 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] rty [quot] rsp_thms defs *}
+ML {* fun lift_tac_lam lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *}
 
 lemma pi_var: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)"
 apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *})
@@ -236,6 +234,11 @@
 apply (tactic {* lift_tac_lam @{context} @{thm rvar_inject} 1 *})
 done
 
+lemma lam_induct:" \<lbrakk>\<And>name. P (Var name); \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2);
+              \<And>name lam. P lam \<Longrightarrow> P (Lam name lam)\<rbrakk> \<Longrightarrow> P lam"
+apply (tactic {* lift_tac_lam @{context} @{thm rlam.induct} 1 *})
+done
+
 lemma var_supp:
   shows "supp (Var a) = ((supp a)::name set)"
   apply(simp add: supp_def)
diff -r 2dc708ddb93a -r 586e3dc4afdb QuotMain.thy
--- a/QuotMain.thy	Sun Nov 29 03:59:18 2009 +0100
+++ b/QuotMain.thy	Sun Nov 29 08:48:06 2009 +0100
@@ -1094,7 +1094,7 @@
             TRY o simp_tac simp_ctxt,
             TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot),
             TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] aps_thms),
-            rtac refl]
+            TRY o rtac refl]
   end
 *}