# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260370742 -3600
# Node ID 546ba31fbb830151a8b6df68ee36b2a8c82055b4
# Parent  0dd10a900cae549236765ae44811568ebc304134# Parent  37de94a84dbc0f92be4dd47c79890388c9df6383
merge

diff -r 0dd10a900cae -r 546ba31fbb83 Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Wed Dec 09 15:57:47 2009 +0100
+++ b/Quot/Examples/FSet.thy	Wed Dec 09 15:59:02 2009 +0100
@@ -373,10 +373,10 @@
 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)
@@ -389,6 +389,7 @@
 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 *}) *)
 sorry
@@ -396,9 +397,10 @@
 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 hard)
+apply(regularize)
+apply(auto)
 sorry
 
 end
diff -r 0dd10a900cae -r 546ba31fbb83 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Wed Dec 09 15:57:47 2009 +0100
+++ b/Quot/QuotMain.thy	Wed Dec 09 15:59:02 2009 +0100
@@ -928,6 +928,25 @@
 
 section {* Cleaning of the Theorem *}
 
+ML {*
+fun fun_map_simple_conv xs ctxt ctrm =
+  case (term_of ctrm) of
+    ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) =>
+        if (member (op=) xs h) 
+        then Conv.all_conv ctrm
+        else Conv.rewr_conv @{thm fun_map.simps[THEN eq_reflection]} ctrm 
+  | _ => Conv.all_conv ctrm
+
+fun fun_map_conv xs ctxt ctrm =
+  case (term_of ctrm) of
+      _ $ _ => (Conv.comb_conv (fun_map_conv xs ctxt) then_conv
+                fun_map_simple_conv xs ctxt) ctrm
+    | Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm
+    | _ => Conv.all_conv ctrm
+
+fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt)
+*}
+
 (* Since the patterns for the lhs are different; there are 3 different make-insts *)
 (* 1: does  ? \<rightarrow> id *)
 (* 2: does id \<rightarrow> ? *)
@@ -963,21 +982,6 @@
 *}
 
 ML {*
-fun make_inst3 lhs t =
-  let
-    val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;
-    val _ $ (Abs (_, _, (_ $ g))) = t;
-    fun mk_abs i t =
-      if incr_boundvars i u aconv t then Bound i
-      else (case t of
-        t1 $ t2 => mk_abs i t1 $ mk_abs i t2
-      | Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t')
-      | Bound j => if i = j then error "make_inst" else t
-      | _ => t);
-  in (f, Abs ("x", T, mk_abs 0 g)) end;
-*}
-
-ML {*
 fun lambda_prs_simple_conv ctxt ctrm =
   case (term_of ctrm) of
    ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) =>
@@ -1005,7 +1009,7 @@
            Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
          end handle _ => (* TODO handle only Bind | Error "make_inst" *)
          let
-           val (insp, inst) = make_inst3 (term_of (Thm.lhs_of te)) (term_of ctrm)
+           val (insp, inst) = make_inst2 (term_of (Thm.lhs_of te)) (term_of ctrm)
            val td = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) te
          in
            MetaSimplifier.rewrite_rule (id_simps_get ctxt) td
@@ -1032,30 +1036,17 @@
 fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)
 *}
 
-(* 1. conversion (is not a pattern) *)
-thm lambda_prs
-(* 2. folding of definitions: (rep ---> abs) oldConst == newconst *)
-(*    prservation lemma                                           *)
-(*    and simplification with                                     *)
-thm all_prs ex_prs 
+(* 1. folding of definitions and preservation lemmas;  *)
+(*    and simplification with                          *)
+thm babs_prs all_prs ex_prs 
+(* 2. unfolding of ---> in front of everything, except *)
+(*    bound variables                                  *)
+thm fun_map.simps
 (* 3. simplification with *)
-thm fun_map.simps Quotient_abs_rep Quotient_rel_rep id_simps 
-(* 4. Test for refl *)
-
-ML {*
-fun fun_map_conv xs ctxt ctrm =
-  case (term_of ctrm) of
-    ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) =>
-        (Conv.binop_conv (fun_map_conv xs ctxt) then_conv
-        (if (member (op=) xs h) 
-         then Conv.all_conv 
-         else Conv.rewr_conv @{thm fun_map.simps[THEN eq_reflection]})) ctrm
-    | _ $ _ => Conv.comb_conv (fun_map_conv xs ctxt) ctrm
-    | Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm
-    | _ => Conv.all_conv ctrm
-
-fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt)
-*}
+thm lambda_prs
+(* 4. simplification with *)
+thm Quotient_abs_rep Quotient_rel_rep id_simps 
+(* 5. Test for refl *)
 
 ML {*
 fun clean_tac lthy =
@@ -1063,12 +1054,13 @@
     val thy = ProofContext.theory_of lthy;
     val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
       (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *)
+    
     val thms1 = defs @ (prs_rules_get lthy) @ @{thms babs_prs all_prs ex_prs}
-    val thms2 = @{thms Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy)
+    val thms2 = @{thms Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy) 
     fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
   in
     EVERY' [simp_tac (simps thms1),
-            TRY o REPEAT_ALL_NEW (CHANGED o (fun_map_tac lthy)),
+            fun_map_tac lthy,
             lambda_prs_tac lthy,
             simp_tac (simps thms2),
             TRY o rtac refl]