# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259911196 -3600
# Node ID d62b6517a0ab82619fd70c24827f9bda64f89002
# Parent  fac6069d8e80215ebc2d4eab0c63a1eb9d605af4# Parent  f7569f994195690747801e89e2546f1f96b6f6bf
merge

diff -r f7569f994195 -r d62b6517a0ab FSet.thy
--- a/FSet.thy	Thu Dec 03 19:06:14 2009 +0100
+++ b/FSet.thy	Fri Dec 04 08:19:56 2009 +0100
@@ -135,9 +135,6 @@
        if (a memb A) then (fold1 f g z A) else (f (g a) (fold1 f g z A))
      ) else z)"
 
-(* fold1_def is not usable, but: *)
-thm fold1.simps
-
 lemma fs1_strong_cases:
   fixes X :: "'a list"
   shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a memb Y) \<and> (X \<approx> a # Y)))"
@@ -408,86 +405,7 @@
 thm quotient_thm
 
 lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
-apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
-apply(tactic {* procedure_tac @{context} @{thm list_induct_part} 1 *})
-apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
-prefer 2
-apply(tactic {* clean_tac @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* APPLY_RSP_TAC @{context} 1*})
-thm quotient_thm
-apply(rule quotient_thm(3))
-apply(rule quotient_thm)
-apply(rule quotient_thm)
-apply(rule quotient_thm)
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* APPLY_RSP_TAC @{context} 1*})
-thm quotient_thm
-apply(rule quotient_thm(3))
-apply(rule quotient_thm)
-apply(rule quotient_thm)
-apply(rule quotient_thm)
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* APPLY_RSP_TAC @{context} 1*})
-thm quotient_thm
-apply(rule quotient_thm(3))
-apply(rule quotient_thm)
-apply(rule quotient_thm)
-apply(rule quotient_thm)
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* APPLY_RSP_TAC @{context} 1*})
-thm quotient_thm
-apply(rule quotient_thm(3))
-apply(rule quotient_thm)
-apply(rule quotient_thm)
-apply(rule quotient_thm)
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1 *})
-(* apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) *)
+apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
 done
 
 lemma "P (x :: 'a fset) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
@@ -548,7 +466,7 @@
   sorry
 
 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *}
-ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv]  *}
+ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *}
 
 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"
 apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *})
diff -r f7569f994195 -r d62b6517a0ab LamEx.thy
--- a/LamEx.thy	Thu Dec 03 19:06:14 2009 +0100
+++ b/LamEx.thy	Fri Dec 04 08:19:56 2009 +0100
@@ -128,7 +128,7 @@
 unfolding fresh_def supp_def
 sorry
 
-lemma perm_rsp[quot_rsp]:
+lemma perm_rsp[quotient_rsp]:
   "(op = ===> alpha ===> alpha) op \<bullet> op \<bullet>"
   apply(auto)
   (* this is propably true if some type conditions are imposed ;o) *)
@@ -140,14 +140,14 @@
   (* this is probably only true if some type conditions are imposed *)
   sorry
 
-lemma rVar_rsp[quot_rsp]:
+lemma rVar_rsp[quotient_rsp]:
   "(op = ===> alpha) rVar rVar"
 by (auto intro:a1)
 
-lemma rApp_rsp[quot_rsp]: "(alpha ===> alpha ===> alpha) rApp rApp"
+lemma rApp_rsp[quotient_rsp]: "(alpha ===> alpha ===> alpha) rApp rApp"
 by (auto intro:a2)
 
-lemma rLam_rsp[quot_rsp]: "(op = ===> alpha ===> alpha) rLam rLam"
+lemma rLam_rsp[quotient_rsp]: "(op = ===> alpha ===> alpha) rLam rLam"
   apply(auto)
   apply(rule a3)
   apply(rule_tac t="[(x,x)]\<bullet>y" and s="y" in subst)
@@ -160,7 +160,7 @@
   apply(simp add: abs_fresh)
   done
 
-lemma rfv_rsp[quot_rsp]: "(alpha ===> op =) rfv rfv"
+lemma rfv_rsp[quotient_rsp]: "(alpha ===> op =) rfv rfv"
   sorry
 
 lemma rvar_inject: "rVar a \<approx> rVar b = (a = b)"
@@ -174,7 +174,7 @@
 
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 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] [quot] *}
+ML {* fun lift_tac_lam lthy t = lift_tac lthy t [rel_eqv] *}
 
 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 *})
diff -r f7569f994195 -r d62b6517a0ab QuotMain.thy
--- a/QuotMain.thy	Thu Dec 03 19:06:14 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 08:19:56 2009 +0100
@@ -958,7 +958,7 @@
 
     (* (op =) ===> (op =)  \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *)
     (* global simplification *)
-    NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))])
+    NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ] eq_reflection[OF LIST_REL_EQ]})))])
 *}
 
 ML {*