# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260274136 -3600
# Node ID 28e9c770a082ec7533c161342c57d81462403828
# Parent  5d6a2b5fb222442be41ee891e756cf58d15afbab
Finished the proof of ttt2 and found bug in regularize when trying ttt3.

diff -r 5d6a2b5fb222 -r 28e9c770a082 Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Tue Dec 08 13:01:23 2009 +0100
+++ b/Quot/Examples/FSet.thy	Tue Dec 08 13:08:56 2009 +0100
@@ -296,10 +296,6 @@
 ML {* val rsp_thms =
   @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp} *}
 
-ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
-ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *}
-ML {* fun lift_tac_fset lthy t = lift_tac lthy t *}
-
 lemma "IN x EMPTY = False"
 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *})
 apply(tactic {* regularize_tac @{context} 1 *})
@@ -308,35 +304,35 @@
 done
 
 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)"
-by (tactic {* lift_tac_fset @{context} @{thm m2} 1 *})
+by (tactic {* lift_tac @{context} @{thm m2} 1 *})
 
 lemma "INSERT a (INSERT a x) = INSERT a x"
-apply (tactic {* lift_tac_fset @{context} @{thm list_eq.intros(4)} 1 *})
+apply (tactic {* lift_tac @{context} @{thm list_eq.intros(4)} 1 *})
 done
 
 lemma "x = xa \<Longrightarrow> INSERT a x = INSERT a xa"
-apply (tactic {* lift_tac_fset @{context} @{thm list_eq.intros(5)} 1 *})
+apply (tactic {* lift_tac @{context} @{thm list_eq.intros(5)} 1 *})
 done
 
 lemma "CARD x = Suc n \<Longrightarrow> (\<exists>a b. \<not> IN a b & x = INSERT a b)"
-apply (tactic {* lift_tac_fset @{context} @{thm card1_suc} 1 *})
+apply (tactic {* lift_tac @{context} @{thm card1_suc} 1 *})
 done
 
 lemma "(\<not> IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))"
-apply (tactic {* lift_tac_fset @{context} @{thm not_mem_card1} 1 *})
+apply (tactic {* lift_tac @{context} @{thm not_mem_card1} 1 *})
 done
 
 lemma "FOLD f g (z::'b) (INSERT a x) =
   (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)"
-apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})
+apply(tactic {* lift_tac @{context} @{thm fold1.simps(2)} 1 *})
 done
 
 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
-apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *})
+apply (tactic {* lift_tac @{context} @{thm map_append} 1 *})
 done
 
 lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"
-apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *})
+apply (tactic {* lift_tac @{context} @{thm append_assoc} 1 *})
 done
 
 
@@ -359,19 +355,18 @@
   apply (assumption)
   done
 
-ML {* quot *}
 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 {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
+apply (tactic {* lift_tac @{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"
-apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
+apply (tactic {* lift_tac @{context} @{thm list_induct_part} 1 *})
 done
 
 lemma "P (x :: 'a fset) ([] :: 'c list) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (e # t)) \<Longrightarrow> P x l"
-apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
+apply (tactic {* lift_tac @{context} @{thm list_induct_part} 1 *})
 done
 
 quotient fset2 = "'a list" / "list_eq"
@@ -389,11 +384,11 @@
   "INSERT2 \<equiv> op #"
 
 lemma "P (x :: 'a fset2) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
-apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
+apply (tactic {* lift_tac @{context} @{thm list_induct_part} 1 *})
 done
 
 lemma "P (x :: 'a fset) (EMPTY2 :: 'c fset2) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT2 e t)) \<Longrightarrow> P x l"
-apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
+apply (tactic {* lift_tac @{context} @{thm list_induct_part} 1 *})
 done
 
 quotient_def
@@ -420,11 +415,11 @@
   sorry
 
 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 *})
+apply (tactic {* lift_tac @{context} @{thm list.recs(2)} 1 *})
 done
 
 lemma "fset_case (f1::'t) f2 (INSERT a xa) = f2 a xa"
-apply (tactic {* lift_tac_fset @{context} @{thm list.cases(2)} 1 *})
+apply (tactic {* lift_tac @{context} @{thm list.cases(2)} 1 *})
 done
 
 lemma ttt: "((op @) x ((op #) e [])) = (((op #) e x))"
@@ -440,15 +435,18 @@
 apply (tactic {* procedure_tac @{context} @{thm ttt2} 1 *})
 apply(tactic {* regularize_tac @{context} 1 *})
 defer
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac_fset @{context}) 1*})
-(* apply(tactic {* clean_tac @{context} 1 *}) *)
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
+apply(tactic {* clean_tac @{context} 1 *})
+thm lambda_prs[OF identity_quotient Quotient_fset]
+thm lambda_prs[OF identity_quotient Quotient_fset, simplified]
+apply(simp only: lambda_prs[OF identity_quotient Quotient_fset,simplified])
 sorry
 
 lemma ttt3: "(\<lambda>x. ((op @) x ((op #) e []))) = (\<lambda>x. ((op #) e x))"
 sorry
 
 lemma "(\<lambda>x. (FUNION x (INSERT e EMPTY))) = (\<lambda>x. (INSERT e x))"
-(* apply (tactic {* procedure_tac @{context} @{thm ttt3} 1 *}) *)
+apply (tactic {* procedure_tac @{context} @{thm ttt3} 1 *})
 sorry
 
 end