# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259688168 -3600
# Node ID fc16faef5dfae2a18fd5909b47e830d60ef068b9
# Parent  6d077eac6ad77ce65ec0af636d2302779ed8fcfb
Transformation of QUOT_TRUE assumption by any given function

diff -r 6d077eac6ad7 -r fc16faef5dfa FSet.thy
--- a/FSet.thy	Tue Dec 01 16:27:42 2009 +0100
+++ b/FSet.thy	Tue Dec 01 18:22:48 2009 +0100
@@ -360,6 +360,13 @@
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 prefer 2
 apply(tactic {* clean_tac @{context} [quot] defs 1 *})
+apply(rule_tac a="\<forall>(P\<Colon>'a fset \<Rightarrow> bool) l\<Colon>'a fset. P EMPTY \<longrightarrow> (\<forall>(a\<Colon>'a) x\<Colon>'a fset. P x \<longrightarrow> P (INSERT a x)) \<longrightarrow> P l" in QUOT_TRUE_i)
+
+apply (drule QT_all)
+apply (drule_tac x = "x" in QT_lam)
+apply (drule QT_all)
+apply (drule_tac x = "y" in QT_lam)
+apply (tactic {* quot_true_tac @{context} (fst o strip_comb) 1 *})
 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 = (===>) *) 
diff -r 6d077eac6ad7 -r fc16faef5dfa QuotMain.thy
--- a/QuotMain.thy	Tue Dec 01 16:27:42 2009 +0100
+++ b/QuotMain.thy	Tue Dec 01 18:22:48 2009 +0100
@@ -722,6 +722,7 @@
   ct |> term_of |> HOLogic.dest_Trueprop
 *}
 
+(* TODO: check if it still works with first_order_match *)
 ML {*
 fun instantiate_tac thm = 
   Subgoal.FOCUS (fn {concl, ...} =>
@@ -847,6 +848,38 @@
 apply(simp_all add: QUOT_TRUE_def)
 done
 
+lemma QUOT_TRUE_i: "(QUOT_TRUE a \<Longrightarrow> P) \<Longrightarrow> P"
+by (simp add: QUOT_TRUE_def)
+
+lemma QUOT_TRUE_imp: "QUOT_TRUE a \<Longrightarrow> QUOT_TRUE b"
+by (simp add: QUOT_TRUE_def)
+
+ML {*
+fun quot_true_tac ctxt fnctn =
+  SUBGOAL (fn (gl, _) =>
+  let
+    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_imp_prems gl) of
+      SOME (_ $ (_ $ x)) =>
+        let
+          val fx = fnctn x;
+          val ctrm1 = cterm_of thy x;
+          val cty1 = ctyp_of thy (fastype_of x);
+          val ctrm2 = cterm_of thy fx;
+          val cty2 = ctyp_of thy (fastype_of fx);
+          val thm = Drule.instantiate' [SOME cty1, SOME cty2] [SOME ctrm1, SOME ctrm2] @{thm QUOT_TRUE_imp}
+        in
+          dtac thm 1
+        end
+    | NONE => error "quot_true_tac!"
+    | _ => error "quot_true_tac!!"
+  end)
+*}
 
 ML {*
 fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 =
@@ -1155,4 +1188,3 @@
 
 end
 
-