# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259747795 -3600
# Node ID 24799397a3ce628309e55ff95ec82de0ea7ebb5e
# Parent  b0e57277661257dd7e3765645fef467be0451fa0
The conversion approach works.

diff -r b0e572776612 -r 24799397a3ce FSet.thy
--- a/FSet.thy	Wed Dec 02 10:30:20 2009 +0100
+++ b/FSet.thy	Wed Dec 02 10:56:35 2009 +0100
@@ -309,40 +309,6 @@
 apply(tactic {* clean_tac @{context} [quot] defs 1*})
 done
 
-lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b"
-by (simp add: QUOT_TRUE_def)
-
-ML {*
-fun quot_true_tac' ctxt fnctn =
-  CSUBGOAL (fn (cgl, i) =>
-  let
-    val gl = term_of cgl;
-    val thy = ProofContext.theory_of ctxt;
-    fun find_fun trm =
-      case trm of
-        (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true
-      | _ => false
-  in
-    case find_first find_fun (Logic.strip_assums_hyp gl) of
-      SOME (asm as (_ $ (_ $ x))) =>
-        let
-          val thm' = Thm.lift_rule cgl @{thm QUOT_TRUE_imp}
-          val _ = tracing (Syntax.string_of_term @{context} (prop_of (thm')))
-          val ps = Logic.strip_params (Thm.concl_of thm');
-          val fx = fnctn x;
-          val (_ $ (_ $ fx')) = Logic.strip_assums_concl (prop_of thm');
-            val insts = [(fx', fx)]
-            |> map (fn (t, u) => (cterm_of thy (Term.head_of t), cterm_of thy (Term.list_abs (ps, u))));
-          val thm_i = Drule.cterm_instantiate insts thm'
-          val thm_j = Thm.forall_elim_vars 0 thm_i
-        in
-          dtac thm_j i
-        end
-    | NONE => error "quot_true_tac!"
-    | _ => error "quot_true_tac!!"
-  end)
-*}
-
 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)"
 by (tactic {* lift_tac_fset @{context} @{thm m2} 1 *})
 
@@ -362,8 +328,6 @@
 apply (tactic {* lift_tac_fset @{context} @{thm not_mem_card1} 1 *})
 done
 
-ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *}
-
 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_fset @{context} @{thm fold1.simps(2)} 1 *})
@@ -379,91 +343,43 @@
 
 lemma cheat: "P" sorry
 
+ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *}
 ML {* fun inj_repabs_tac_fset' lthy = inj_repabs_tac' lthy rty [quot] [rel_refl] [trans2] *}
 
-ML {*
-fun quot_true_conv1 ctxt fnctn ctrm =
-  case (term_of ctrm) of
-    (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ x)) =>
-    let
-      val _ = tracing "A";
-      val fx = fnctn x;
-      val thy = ProofContext.theory_of ctxt;
-      val cx = cterm_of thy x;
-      val cfx = cterm_of thy fx;
-      val cxt = ctyp_of thy (fastype_of x);
-      val cfxt = ctyp_of thy (fastype_of fx);
-      val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QUOT_TRUE_imp}
-      val _ = tracing (Syntax.string_of_term @{context} (prop_of thm));
-    in
-      Conv.rewr_conv thm ctrm
-    end
-*}
-
-ML {*
-fun quot_true_conv ctxt fnctn ctrm =
-  case (term_of ctrm) of
-    (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) =>
-      quot_true_conv1 ctxt fnctn ctrm
-  | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm
-  | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm
-  | _ => Conv.all_conv ctrm
-*}
-
-ML CONVERSION
-ML {*
-fun quot_true_tac ctxt fnctn = CONVERSION (
-  fn ctrm => 
-    let
-      val _ = tracing "B";
-      val t = quot_true_conv ctxt fnctn ctrm;
-      val _ = tracing "C";
-    in
-      t
-    end)
-*}
-
 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} [rel_eqv] 1 *})
 prefer 2
 apply(tactic {* clean_tac @{context} [quot] defs 1 *})
-apply (tactic {* quot_true_tac @{context} (fst o dest_comb) 1 *}) apply(assumption)
-
 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 3 *) (* Ball-Ball *)
 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)
-apply (tactic {* quot_true_tac @{context} (unlam) 1 *}) apply(assumption)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)
 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 3 *) (* Ball-Ball *)
 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)
-apply (drule QT_lam)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
-apply (tactic {* quot_true_tac' @{context} (fst o dest_comb) 1 *})
-apply (assumption)
-apply (assumption)
-apply (tactic {* quot_true_tac @{context} (fst o strip_comb) 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* D *) (* reflexivity of basic relations *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* C *) (* = and extensionality *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) 
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* D *) (* reflexivity of basic relations *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* C *) (* = and extensionality *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 3 *) (* Ball-Ball *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) 
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *)
 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
diff -r b0e572776612 -r 24799397a3ce QuotMain.thy
--- a/QuotMain.thy	Wed Dec 02 10:30:20 2009 +0100
+++ b/QuotMain.thy	Wed Dec 02 10:56:35 2009 +0100
@@ -900,39 +900,42 @@
 lemma QUOT_TRUE_i: "(QUOT_TRUE (a :: bool) \<Longrightarrow> P) \<Longrightarrow> P"
 by (simp add: QUOT_TRUE_def)
 
-lemma QUOT_TRUE_imp: "QUOT_TRUE a"
+lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b"
 by (simp add: QUOT_TRUE_def)
 
 ML {*
-fun quot_true_tac ctxt fnctn =
-  CSUBGOAL (fn (cgl, i) =>
-  let
-    val gl = term_of cgl;
-    val thy = ProofContext.theory_of ctxt;
-    fun find_fun trm =
-      case trm of
-        (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true
-      | _ => false
-  in
-    case find_first find_fun (Logic.strip_assums_hyp gl) of
-      SOME (_ $ (_ $ x)) =>
-        let
-          val thm' = Thm.lift_rule cgl @{thm QUOT_TRUE_imp}
-          val ps = Logic.strip_params (Thm.concl_of thm');
-          val fx = fnctn x;
-          val (_ $ (_ $ fx')) = Logic.strip_assums_concl (prop_of thm');
-            val insts = [(fx', fx)]
-            |> map (fn (t, u) => (cterm_of thy (Term.head_of t), cterm_of thy (Term.list_abs (ps, u))));
-          val thm_i = Drule.cterm_instantiate insts thm'
-          val thm_j = Thm.forall_elim_vars 1 thm_i
-        in
-          dtac thm_j i
-        end
-    | NONE => error "quot_true_tac!"
-    | _ => error "quot_true_tac!!"
-  end)
+fun quot_true_conv1 ctxt fnctn ctrm =
+  case (term_of ctrm) of
+    (Const (@{const_name QUOT_TRUE}, _) $ x) =>
+    let
+      val fx = fnctn x;
+      val thy = ProofContext.theory_of ctxt;
+      val cx = cterm_of thy x;
+      val cfx = cterm_of thy fx;
+      val cxt = ctyp_of thy (fastype_of x);
+      val cfxt = ctyp_of thy (fastype_of fx);
+      val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QUOT_TRUE_imp}
+    in
+      Conv.rewr_conv thm ctrm
+    end
 *}
 
+ML {*
+fun quot_true_conv ctxt fnctn ctrm =
+  case (term_of ctrm) of
+    (Const (@{const_name QUOT_TRUE}, _) $ _) =>
+      quot_true_conv1 ctxt fnctn ctrm
+  | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm
+  | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm
+  | _ => Conv.all_conv ctrm
+*}
+
+ML {*
+fun quot_true_tac ctxt fnctn = CSUBGOAL (fn (goal, i) =>
+  CONVERSION
+    (Conv.params_conv ~1 (fn ctxt =>
+       (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn))) ctxt) i)
+*}
 
 ML {* fun dest_comb (f $ a) = (f, a) *}
 ML {* fun dest_bcomb ((_ $ l) $ r) = (l, r) *}