347 fun matches_typ (ty, ty') =

   348   case (ty, ty') of

   349     (_, TVar _) => true

   350   | (TFree x, TFree x') => x = x'

   351   | (Type (s, tys), Type (s', tys')) => 

   352        s = s' andalso 

   353        if (length tys = length tys') 

   354        then (List.all matches_typ (tys ~~ tys')) 

   355        else false

   356   | _ => false

   357 *}

   358 ML {*

   359 fun matches_term (trm, trm') = 

   360    case (trm, trm') of 

   361      (_, Var _) => true

   362    | (Const (s, ty), Const (s', ty')) => s = s' andalso matches_typ (ty, ty')

   363    | (Free (x, ty), Free (x', ty')) => x = x' andalso matches_typ (ty, ty')

   364    | (Bound i, Bound j) => i = j

   365    | (Abs (_, T, t), Abs (_, T', t')) => matches_typ (T, T') andalso matches_term (t, t')

   366    | (t $ s, t' $ s') => matches_term (t, t') andalso matches_term (s, s') 

   367    | _ => false

   368 *}

   369 

   370 ML {*

   760 (* Not used anymore *)

   761 (* FIXME/TODO: do not handle everything *)

   762 ML {*

   763 fun instantiate_tac thm = 

   764   Subgoal.FOCUS (fn {concl, ...} =>

   765   let

   766     val pat = Drule.strip_imp_concl (cprop_of thm)

   767     val insts = Thm.first_order_match (pat, concl)

   768   in

   769     rtac (Drule.instantiate insts thm) 1

   770   end

   771   handle _ => no_tac)

   772 *}

   773 

   852 

   855 *}

   856 

   857 (*

   858 To prove that the regularised theorem implies the abs/rep injected, 

   859 we try:

   860 

   861  1) theorems 'trans2' from the appropriate QUOT_TYPE

   862  2) remove lambdas from both sides: lambda_rsp_tac

   863  3) remove Ball/Bex from the right hand side

   864  4) use user-supplied RSP theorems

   865  5) remove rep_abs from the right side

   866  6) reflexivity of equality

   867  7) split applications of lifted type (apply_rsp)

   868  8) split applications of non-lifted type (cong_tac)

   869  9) apply extentionality

   870  A) reflexivity of the relation

   871  B) assumption

   872     (Lambdas under respects may have left us some assumptions)

   873  C) proving obvious higher order equalities by simplifying fun_rel

   874     (not sure if it is still needed?)

   875  D) unfolding lambda on one side

   876  E) simplifying (= ===> =) for simpler respectfulness

   877 

   878 *)

   879 

   880 lemma quot_true_dests:

   881   shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P"

   882   and   QT_ex:  "QUOT_TRUE (Ex P) \<Longrightarrow> QUOT_TRUE P"

   883   and   QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE  (P x))"

   884   and   QT_ext: "(\<And>x. QUOT_TRUE (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (QUOT_TRUE a \<Longrightarrow> f = g)"

   885 apply(simp_all add: QUOT_TRUE_def ext)

   886 done

   887 

   888 lemma QUOT_TRUE_i: "(QUOT_TRUE (a :: bool) \<Longrightarrow> P) \<Longrightarrow> P"

   889 by (simp add: QUOT_TRUE_def)

   890 

   891 lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b"

   892 by (simp add: QUOT_TRUE_def)

   893 

   894 ML {*

   895 fun quot_true_conv1 ctxt fnctn ctrm =

   896   case (term_of ctrm) of

   897     (Const (@{const_name QUOT_TRUE}, _) $ x) =>

   898     let

   899       val fx = fnctn x;

   900       val thy = ProofContext.theory_of ctxt;

   901       val cx = cterm_of thy x;

   902       val cfx = cterm_of thy fx;

   903       val cxt = ctyp_of thy (fastype_of x);

   904       val cfxt = ctyp_of thy (fastype_of fx);

   905       val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QUOT_TRUE_imp}

   906     in

   907       Conv.rewr_conv thm ctrm

   908     end

   909 *}

   910 

   911 ML {*

   912 fun quot_true_conv ctxt fnctn ctrm =

   913   case (term_of ctrm) of

   914     (Const (@{const_name QUOT_TRUE}, _) $ _) =>

   915       quot_true_conv1 ctxt fnctn ctrm

   916   | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm

   917   | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm

   918   | _ => Conv.all_conv ctrm

   919 *}

   920 

   921 ML {*

   922 fun quot_true_tac ctxt fnctn = CONVERSION

   923     ((Conv.params_conv ~1 (fn ctxt =>

   924        (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt)

   925 *}

   926 

   927 ML {* fun dest_comb (f $ a) = (f, a) *}

   928 ML {* fun dest_bcomb ((_ $ l) $ r) = (l, r) *}

   929 (* TODO: Can this be done easier? *)

   930 ML {*

   931 fun unlam t =

   932   case t of

   933     (Abs a) => snd (Term.dest_abs a)

   934   | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0)))

   935 *}

   936 

   937 ML {*

   938 fun dest_fun_type (Type("fun", [T, S])) = (T, S)

   939   | dest_fun_type _ = error "dest_fun_type"

   940 *}

   941 

   942 ML {*

   943 val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl

  1037 

  1038