903 lemma QUOT_TRUE_imp: "QUOT_TRUE a \<Longrightarrow> QUOT_TRUE b"

   903 lemma QUOT_TRUE_imp: "QUOT_TRUE a \<Longrightarrow> QUOT_TRUE b"

   904 by (simp add: QUOT_TRUE_def)

   904 by (simp add: QUOT_TRUE_def)

   905 

   905 

   906 ML {*

   906 ML {*

   907 fun quot_true_tac ctxt fnctn =

   907 fun quot_true_tac ctxt fnctn =

   909   let

   909   let

   910     val thy = ProofContext.theory_of ctxt;

   910     val thy = ProofContext.theory_of ctxt;

   911     fun find_fun trm =

   911     fun find_fun trm =

   912       case trm of

   912       case trm of

   913         (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true

   913         (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true

   921           val cty1 = ctyp_of thy (fastype_of x);

   921           val cty1 = ctyp_of thy (fastype_of x);

   922           val ctrm2 = cterm_of thy fx;

   922           val ctrm2 = cterm_of thy fx;

   923           val cty2 = ctyp_of thy (fastype_of fx);

   923           val cty2 = ctyp_of thy (fastype_of fx);

   924           val thm = Drule.instantiate' [SOME cty1, SOME cty2] [SOME ctrm1, SOME ctrm2] @{thm QUOT_TRUE_imp}

   924           val thm = Drule.instantiate' [SOME cty1, SOME cty2] [SOME ctrm1, SOME ctrm2] @{thm QUOT_TRUE_imp}

   925         in

   925         in

   927         end

   927         end

   928     | NONE => error "quot_true_tac!"

   928     | NONE => error "quot_true_tac!"

   929     | _ => error "quot_true_tac!!"

   929     | _ => error "quot_true_tac!!"

   930   end)

   930   end)

   931 *}

   931 *}