--- a/Quot/Examples/FSet.thy	Tue Dec 08 23:32:54 2009 +0100
+++ b/Quot/Examples/FSet.thy	Wed Dec 09 00:03:18 2009 +0100
@@ -26,44 +26,21 @@
   apply(rule equivp_list_eq)
   done
 
-print_theorems
-
-typ "'a fset"
-thm "Rep_fset"
-thm "ABS_fset_def"
-
 quotient_def 
   EMPTY :: "'a fset"
 where
   "EMPTY \<equiv> ([]::'a list)"
 
-term Nil
-term EMPTY
-thm EMPTY_def
-
 quotient_def 
   INSERT :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 where
   "INSERT \<equiv> op #"
 
-term Cons
-term INSERT
-thm INSERT_def
-
 quotient_def 
   FUNION :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 where
   "FUNION \<equiv> (op @)"
 
-term append
-term FUNION
-thm FUNION_def
-
-thm Quotient_fset
-
-thm QUOT_TYPE_I_fset.thm11
-
-
 fun
   membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infix "memb" 100)
 where
@@ -81,10 +58,6 @@
 where
   "CARD \<equiv> card1"
 
-term card1
-term CARD
-thm CARD_def
-
 (* text {*
  Maybe make_const_def should require a theorem that says that the particular lifted function
  respects the relation. With it such a definition would be impossible:
@@ -148,29 +121,16 @@
 where
   "IN \<equiv> membship"
 
-term membship
-term IN
-thm IN_def
-
-term fold1
 quotient_def 
   FOLD :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a"
 where
   "FOLD \<equiv> fold1"
 
-term fold1
-term fold
-thm fold_def
-
 quotient_def 
   fmap::"('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
 where
   "fmap \<equiv> map"
 
-term map
-term fmap
-thm fmap_def
-
 lemma memb_rsp:
   fixes z
   assumes a: "x \<approx> y"
@@ -290,58 +250,46 @@
   shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
 by (auto intro: list_eq.intros)
 
-print_quotients
-
-ML {* val qty = @{typ "'a fset"} *}
-ML {* val rsp_thms =
-  @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp} *}
 
 lemma "IN x EMPTY = False"
-apply(tactic {* procedure_tac @{context} @{thm m1} 1 *})
-apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} 1 *})
-apply(tactic {* clean_tac @{context} 1*})
+apply(lifting m1)
 done
 
 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)"
-by (tactic {* lift_tac @{context} @{thm m2} 1 *})
+by (lifting m2)
 
 lemma "INSERT a (INSERT a x) = INSERT a x"
-apply (tactic {* lift_tac @{context} @{thm list_eq.intros(4)} 1 *})
+apply (lifting list_eq.intros(4))
 done
 
 lemma "x = xa \<Longrightarrow> INSERT a x = INSERT a xa"
-apply (tactic {* lift_tac @{context} @{thm list_eq.intros(5)} 1 *})
+apply (lifting list_eq.intros(5))
 done
 
 lemma "CARD x = Suc n \<Longrightarrow> (\<exists>a b. \<not> IN a b & x = INSERT a b)"
-apply (tactic {* lift_tac @{context} @{thm card1_suc} 1 *})
+apply (lifting card1_suc)
 done
 
 lemma "(\<not> IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))"
-apply (tactic {* lift_tac @{context} @{thm not_mem_card1} 1 *})
+apply (lifting not_mem_card1)
 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 @{context} @{thm fold1.simps(2)} 1 *})
+apply(lifting fold1.simps(2))
 done
 
 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
-apply (tactic {* lift_tac @{context} @{thm map_append} 1 *})
+apply (lifting map_append)
 done
 
 lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"
-apply (tactic {* lift_tac @{context} @{thm append_assoc} 1 *})
+apply (lifting append_assoc)
 done
 
 
 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
-apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
-apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})
-apply(tactic {* regularize_tac @{context} 1 *})
-apply(injection)
-apply(tactic {* clean_tac @{context} 1 *})
+apply(lifting list.induct)
 done
 
 lemma list_induct_part:
@@ -355,20 +303,19 @@
   done
 
 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 @{context} @{thm list_induct_part} 1 *})
+apply (lifting list_induct_part)
 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 @{context} @{thm list_induct_part} 1 *})
+apply (lifting list_induct_part)
 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 @{context} @{thm list_induct_part} 1 *})
+apply (lifting list_induct_part)
 done
 
 quotient fset2 = "'a list" / "list_eq"
-  apply(rule equivp_list_eq)
-  done
+  by (rule equivp_list_eq)
 
 quotient_def
   EMPTY2 :: "'a fset2"
@@ -381,11 +328,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 @{context} @{thm list_induct_part} 1 *})
+apply (lifting list_induct_part)
 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 @{context} @{thm list_induct_part} 1 *})
+apply (lifting list_induct_part)
 done
 
 quotient_def
@@ -412,22 +359,24 @@
   sorry
 
 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"
-apply (tactic {* lift_tac @{context} @{thm list.recs(2)} 1 *})
+apply (lifting list.recs(2))
 done
 
 lemma "fset_case (f1::'t) f2 (INSERT a xa) = f2 a xa"
-apply (tactic {* lift_tac @{context} @{thm list.cases(2)} 1 *})
+apply (lifting list.cases(2))
 done
 
 lemma ttt: "((op @) x ((op #) e [])) = (((op #) e x))"
 sorry
+
 lemma "(FUNION x (INSERT e EMPTY)) = ((INSERT e x))"
-apply (tactic {* lift_tac @{context} @{thm ttt} 1 *})
+apply (lifting ttt)
 done
 
 lemma ttt2: "(\<lambda>e. ((op @) x ((op #) e []))) = (\<lambda>e. ((op #) e x))"
 sorry
 
+(* PROBLEM *)
 lemma "(\<lambda>e. (FUNION x (INSERT e EMPTY))) = (\<lambda>e. (INSERT e x))"
 apply(lifting ttt2)
 apply(regularize)
@@ -459,30 +408,11 @@
 lemma hard: "(\<lambda>P. \<lambda>Q. P (Q (x::'a list))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a list)))"
 sorry
 
+(* PROBLEM *)
 lemma hard_lift: "(\<lambda>P. \<lambda>Q. P (Q (x::'a fset))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a fset)))"
 apply(lifting_setup hard)
 defer
 apply(injection)
-apply(subst babs_prs)
-apply(tactic {* quotient_tac @{context} 1 *})
-apply(tactic {* quotient_tac @{context} 1 *})
-apply(subst babs_prs)
-apply(tactic {* quotient_tac @{context} 1 *})
-apply(tactic {* quotient_tac @{context} 1 *})
-apply(subst babs_prs)
-apply(tactic {* quotient_tac @{context} 1 *})
-apply(tactic {* quotient_tac @{context} 1 *})
-apply(subst babs_prs)
-apply(tactic {* quotient_tac @{context} 1 *})
-apply(tactic {* quotient_tac @{context} 1 *})
-apply(subst all_prs)
-apply(tactic {* quotient_tac @{context} 1 *})
-apply(tactic {* lambda_prs_tac @{context} 1 *})
-apply(subst fun_map.simps)
-apply(tactic {* lambda_prs_tac @{context} 1 *})
-apply(subst fun_map.simps)
-apply(subst fun_map.simps)
-apply(tactic {* lambda_prs_tac @{context} 1 *})
 apply(cleaning)
 sorry