# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259076034 -3600
# Node ID d444389fe3f9ce8a89ef56cecaa05161e7e098f1
# Parent  84621d9942f583cfbdd7455146c5c60ed60833f5
The non-working procedure_tac.

diff -r 84621d9942f5 -r d444389fe3f9 FSet.thy
--- a/FSet.thy	Tue Nov 24 16:10:31 2009 +0100
+++ b/FSet.thy	Tue Nov 24 16:20:34 2009 +0100
@@ -320,11 +320,11 @@
 apply (tactic {* lift_tac_fset @{context} @{thm list_eq.intros(4)} 1 *})
 done
 
-lemma "x = xa \<longrightarrow> INSERT a x = INSERT a xa"
+lemma "x = xa \<Longrightarrow> INSERT a x = INSERT a xa"
 apply (tactic {* lift_tac_fset @{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)"
+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 *})
 done
 
@@ -332,27 +332,83 @@
 apply (tactic {* lift_tac_fset @{context} @{thm not_mem_card1} 1 *})
 done
 
-ML {* atomize_thm @{thm fold1.simps(2)} *}
-(*ML {* lift_thm_g_fset @{context} @{thm fold1.simps(2)} @{term "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)"} *}*)
-
 lemma "\<forall>f g z a x. 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 *})
 done
 
+(*
+ML {*
+fun lambda_prs_conv ctxt ctrm =
+  case (Thm.term_of ctrm) of
+    (@{term "op --->"} $ x $ y) $ (Abs (_, T, x)) =>
+      let
+        val lty = T;
+        val rty = fastype_of x;
+        val thy = ProofContext.theory_of ctxt;
+        val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty)
+        val inst = [SOME lcty, NONE, SOME rcty];
+        val lpi = Drule.instantiate' inst [] thm;
+ 
+      (Conv.all_conv ctrm)
+  | _ $ _ => Conv.comb_conv (lambda_prs_conv ctxt) ctrm
+  | Abs _ => Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt) ctxt ctrm
+  | _ => Conv.all_conv ctrm
+*}
+
+
+ML {*
+fun lambda_prs_tac ctxt = CSUBGOAL (fn (goal, i) =>
+  CONVERSION
+    (Conv.params_conv ~1 (fn ctxt =>
+       (Conv.prems_conv ~1 (lambda_prs_conv ctxt) then_conv
+          Conv.concl_conv ~1 (lambda_prs_conv ctxt))) ctxt) i)
+*}
+*)
+
+thm map_append
+lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
+apply(tactic {* procedure_tac @{thm map_append} @{context} 1 *})
+apply(tactic {* prepare_tac 1 *})
+thm map_append
+apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *})
+done
+
+
+lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
+apply(tactic {* procedure_tac @{thm list.induct} @{context} 1 *})
+apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *})
+apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *})
+apply(tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *})
+thm LAMBDA_PRS
+apply(tactic {* EqSubst.eqsubst_tac @{context} [0] @{thms LAMBDA_PRS} 1 *})
+
+apply(tactic {*  (lambda_prs_tac @{context} quot) 1 *})
+
+apply(tactic {* REPEAT_ALL_NEW (lambda_prs_tac @{context} quot) 1 *})
+
+apply(tactic {* clean_tac @{context} quot defs reps_same 1 *})
+apply (tactic {* lift_tac_fset @{context} @{thm list.induct} 1 *})
+ML {* lift_thm_fset @{context} @{thm list.induct} *}
+ML {* lift_thm_g_fset @{context} @{thm list.induct} @{term "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"} *}
+
+lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"
+apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *})
+done
+
+ML {* atomize_thm @{thm fold1.simps(2)} *}
+(*ML {* lift_thm_g_fset @{context} @{thm fold1.simps(2)} @{term "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)"} *}*)
+
+
+
+ML {* lift_thm_g_fset @{context} @{thm map_append} @{term "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"} *}
+
+
 ML {* cterm_of @{theory} (atomize_goal @{theory} @{term "\<forall>x xa a. x = xa \<Longrightarrow> INSERT a x = INSERT a xa"}) *}
 
-(* Doesn't work with 'a, 'b, but works with 'b, 'a *)
-ML {* lift_thm_g_fset @{context} @{thm fold1.simps(2)} 
-
-ML {* lift_thm_fset @{context} @{thm append_assoc} *}
-ML {* lift_thm_g_fset @{context} @{thm append_assoc} @{term "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"} *}
 
 ML {* lift_thm_fset @{context} @{thm map_append} *}
-ML {* lift_thm_g_fset @{context} @{thm map_append} @{term "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"} *}
-ML {* lift_thm_fset @{context} @{thm list.induct} *}
-ML {* lift_thm_g_fset @{context} @{thm list.induct} @{term "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"} *}