# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260313398 -3600
# Node ID 02fd9de9d45e2ac67390b006ff4c6adad97b7633
# Parent  fdccdc52c68a7de82937bf168600d0321f5fc2c0
tuned the examples and flagged the problematic cleaning lemmas in FSet

diff -r fdccdc52c68a -r 02fd9de9d45e Quot/Examples/FSet.thy
--- 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
 
diff -r fdccdc52c68a -r 02fd9de9d45e Quot/Examples/IntEx2.thy
--- a/Quot/Examples/IntEx2.thy	Tue Dec 08 23:32:54 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Wed Dec 09 00:03:18 2009 +0100
@@ -105,8 +105,6 @@
 
 end
 
-thm add_assoc
-
 lemma plus_raw_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_raw plus_raw"
 by auto
@@ -171,42 +169,33 @@
   fix i j k :: int
   show "(i + j) + k = i + (j + k)"
     unfolding add_int_def
-    apply(tactic {* lift_tac @{context} @{thm plus_assoc_raw} 1 *})
-    done
+    by (lifting plus_assoc_raw)
   show "i + j = j + i" 
     unfolding add_int_def
-    apply(tactic {* lift_tac @{context} @{thm plus_sym_raw} 1 *})
-    done
+    by (lifting plus_sym_raw)
   show "0 + i = (i::int)"
     unfolding add_int_def Zero_int_def 
-    apply(tactic {* lift_tac @{context} @{thm plus_zero_raw} 1 *})
-    done
+    by (lifting plus_zero_raw)
   show "- i + i = 0"
     unfolding add_int_def minus_int_def Zero_int_def 
-    apply(tactic {* lift_tac @{context} @{thm plus_minus_zero_raw} 1 *})
-    done
+    by (lifting plus_minus_zero_raw)
   show "i - j = i + - j"
     by (simp add: diff_int_def)
   show "(i * j) * k = i * (j * k)"
     unfolding mult_int_def 
-    apply(tactic {* lift_tac @{context} @{thm mult_assoc_raw} 1 *})
-    done
+    by (lifting mult_assoc_raw)
   show "i * j = j * i"
     unfolding mult_int_def 
-    apply(tactic {* lift_tac @{context} @{thm mult_sym_raw} 1 *})
-    done
+    by (lifting mult_sym_raw)
   show "1 * i = i"
     unfolding mult_int_def One_int_def
-    apply(tactic {* lift_tac @{context} @{thm mult_one_raw} 1 *})
-    done
+    by (lifting mult_one_raw)
   show "(i + j) * k = i * k + j * k"
     unfolding mult_int_def add_int_def
-    apply(tactic {* lift_tac @{context} @{thm mult_plus_comm_raw} 1 *})
-    done
+    by (lifting mult_plus_comm_raw)
   show "0 \<noteq> (1::int)"
     unfolding Zero_int_def One_int_def
-    apply(tactic {* lift_tac @{context} @{thm one_zero_distinct} 1 *})
-    done
+    by (lifting one_zero_distinct)
 qed
 
 term of_nat
@@ -242,22 +231,18 @@
   fix i j k :: int
   show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
     unfolding le_int_def
-    apply(tactic {* lift_tac @{context} @{thm le_antisym_raw} 1 *})
-    done
+    by (lifting le_antisym_raw)
   show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
     by (auto simp add: less_int_def dest: antisym) 
   show "i \<le> i"
     unfolding le_int_def
-    apply(tactic {* lift_tac @{context} @{thm le_refl_raw} 1 *})
-    done
+    by (lifting le_refl_raw)
   show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
     unfolding le_int_def
-    apply(tactic {* lift_tac @{context} @{thm le_trans_raw} 1 *})
-    done
+    by (lifting le_trans_raw)
   show "i \<le> j \<or> j \<le> i"
     unfolding le_int_def
-    apply(tactic {* lift_tac @{context} @{thm le_cases_raw} 1 *})
-    done
+    by (lifting le_cases_raw)
 qed
 
 instantiation int :: distrib_lattice
@@ -285,8 +270,7 @@
   fix i j k :: int
   show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
     unfolding le_int_def add_int_def
-    apply(tactic {* lift_tac @{context} @{thm le_plus_raw} 1 *})
-    done
+    by (lifting le_plus_raw)
 qed
 
 lemma test:
@@ -303,8 +287,7 @@
   fix i j k :: int
   show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
     unfolding mult_int_def le_int_def less_int_def Zero_int_def
-    apply(tactic {* lift_tac @{context} @{thm test} 1 *})
-    done
+    by (lifting test)
   show "\<bar>i\<bar> = (if i < 0 then -i else i)"
     by (simp only: zabs_def)
   show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
diff -r fdccdc52c68a -r 02fd9de9d45e Quot/Examples/LFex.thy
--- a/Quot/Examples/LFex.thy	Tue Dec 08 23:32:54 2009 +0100
+++ b/Quot/Examples/LFex.thy	Wed Dec 09 00:03:18 2009 +0100
@@ -252,12 +252,10 @@
          ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> 
          ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)"
 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11
-apply - 
-apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *})
-apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} 1 *})
+apply(lifting akind_aty_atrm.induct)
+(* FIXME: with overloaded definitions *)
 apply(fold perm_kind_def perm_ty_def perm_trm_def)
-apply(tactic {* clean_tac @{context} 1 *})
+apply(cleaning)
 (*
 Profiling:
 ML_prf {* fun ith i =  (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *}
@@ -292,7 +290,7 @@
   \<And>trm1 trm2. \<lbrakk>R trm1; R trm2\<rbrakk> \<Longrightarrow> R (APP trm1 trm2);
   \<And>ty name trm. \<lbrakk>Q ty; R trm\<rbrakk> \<Longrightarrow> R (LAM ty name trm)\<rbrakk>
   \<Longrightarrow> P mkind \<and> Q mty \<and> R mtrm"
-apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} 1 *})
+apply(lifting kind_ty_trm.induct)
 done
 
 end