# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259078453 -3600
# Node ID c5c49d240cdeca36b9df281701aa8c3a41adb1f4
# Parent  d444389fe3f9ce8a89ef56cecaa05161e7e098f1
Conversion

diff -r d444389fe3f9 -r c5c49d240cde FSet.thy
--- a/FSet.thy	Tue Nov 24 16:20:34 2009 +0100
+++ b/FSet.thy	Tue Nov 24 17:00:53 2009 +0100
@@ -337,42 +337,64 @@
 apply (tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})
 done
 
-(*
 ML {*
-fun lambda_prs_conv ctxt ctrm =
+
+fun lambda_prs_conv ctxt quot ctrm =
   case (Thm.term_of ctrm) of
-    (@{term "op --->"} $ x $ y) $ (Abs (_, T, x)) =>
+    (Const (@{const_name "fun_map"}, _) $ y $ z) $ (Abs (_, T, x)) =>
       let
+        val _ = tracing "AAA";
         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
+        val lpi = Drule.instantiate' inst [] @{thm LAMBDA_PRS};
+        val tac =
+          (compose_tac (false, lpi, 2)) THEN_ALL_NEW
+          (quotient_tac quot);
+        val gc = Drule.strip_imp_concl (cprop_of lpi);
+        val t = Goal.prove_internal [] gc (fn _ => tac 1)
+        val _ = tracing (Syntax.string_of_term @{context} (prop_of t))
+      in
+        Conv.rewr_conv (eq_reflection OF [t]) ctrm
+      end
+  | _ $ _ => Conv.comb_conv (lambda_prs_conv ctxt quot) ctrm
+  | Abs _ => Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt ctrm
   | _ => Conv.all_conv ctrm
 *}
 
+ML {*
+  lambda_prs_conv @{context} quot
+*}
 
 ML {*
-fun lambda_prs_tac ctxt = CSUBGOAL (fn (goal, i) =>
+fun lambda_prs_tac ctxt quot = 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)
+       (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv
+          Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i)
 *}
-*)
+
+ML {*
+lambda_prs_conv @{context} quot 
+@{cterm "((ABS_fset ---> id) ---> id) (\<lambda>x\<Colon>'a list \<Rightarrow> bool. id ((f ((REP_fset ---> id) x) ((REP_fset ---> id) x))))"}
+*}
 
-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
+ML {*
+@{cterm "((ABS_fset ---> id) ---> id)
+          (\<lambda>P.
+              All ((REP_fset ---> id)
+                    (\<lambda>list.
+                        (ABS_fset ---> id) ((REP_fset ---> id) P) (REP_fset (ABS_fset [])) \<longrightarrow>
+                        (\<forall>a. All ((REP_fset ---> id)
+                                      (\<lambda>list.
+                                          (ABS_fset ---> id) ((REP_fset ---> id) P) (REP_fset (ABS_fset list)) \<longrightarrow>
+                                          (ABS_fset ---> id) ((REP_fset ---> id) P)
+                                           (REP_fset (ABS_fset (a # REP_fset (ABS_fset list))))))) \<longrightarrow>
+                        (ABS_fset ---> id) ((REP_fset ---> id) P) (REP_fset (ABS_fset list)))))"}
+
+*}
 
 
 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
@@ -380,6 +402,8 @@
 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 *})
 
@@ -392,6 +416,19 @@
 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"} *}
 
+
+
+
+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 "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"
 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *})
 done