230 text {* tyRel takes a type and builds a relation that a quantifier over this

   231   type needs to respect. *}

   232 ML {*

   233 fun tyRel ty rty rel lthy =

   234   if Sign.typ_instance (ProofContext.theory_of lthy) (ty, rty)

   235   then rel

   236   else (case ty of

   237           Type (s, tys) =>

   238             let

   239               val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys;

   240               val ty_out = ty --> ty --> @{typ bool};

   241               val tys_out = tys_rel ---> ty_out;

   242             in

   243             (case (maps_lookup (ProofContext.theory_of lthy) s) of

   244                SOME (info) => list_comb (Const (#relfun info, tys_out),

   245                               map (fn ty => tyRel ty rty rel lthy) tys)

   246              | NONE  => HOLogic.eq_const ty

   247             )

   248             end

   249         | _ => HOLogic.eq_const ty)

   250 *}

   251 

   252 (* 

   253 ML {* cterm_of @{theory} 

   254   (tyRel @{typ "'a \<Rightarrow> 'a list \<Rightarrow> 't \<Rightarrow> 't"} (Logic.varifyT @{typ "'a list"}) 

   255          @{term "f::('a list \<Rightarrow> 'a list \<Rightarrow> bool)"} @{context}) 

   256 *} 

   257 *)

   258 

   276 ML {*

   277 fun mk_babs ty ty' = Const (@{const_name "Babs"}, [ty' --> @{typ bool}, ty] ---> ty)

   278 fun mk_ball ty = Const (@{const_name "Ball"}, [ty, ty] ---> @{typ bool})

   279 fun mk_bex ty = Const (@{const_name "Bex"}, [ty, ty] ---> @{typ bool})

   280 fun mk_resp ty = Const (@{const_name Respects}, [[ty, ty] ---> @{typ bool}, ty] ---> @{typ bool})

   281 *}

   282 

   283 (* applies f to the subterm of an abstractions, otherwise to the given term *)

   284 ML {*

   285 fun apply_subt f trm =

   286   case trm of

   287     Abs (x, T, t) => 

   288        let 

   289          val (x', t') = Term.dest_abs (x, T, t)

   290        in

   291          Term.absfree (x', T, f t') 

   292        end

   293   | _ => f trm

   294 *}

   295 

   296 (* FIXME: if there are more than one quotient, then you have to look up the relation *)

   297 ML {*

   298 fun my_reg lthy rel rty trm =

   299   case trm of

   300     Abs (x, T, t) =>

   301        if (needs_lift rty T) then

   302          let

   303             val rrel = tyRel T rty rel lthy

   304          in

   305            (mk_babs (fastype_of trm) T) $ (mk_resp T $ rrel) $ (apply_subt (my_reg lthy rel rty) trm)

   306          end

   307        else

   308          Abs(x, T, (apply_subt (my_reg lthy rel rty) t))

   309   | Const (@{const_name "All"}, ty) $ (t as Abs (x, T, _)) =>

   310        let

   311           val ty1 = domain_type ty

   312           val ty2 = domain_type ty1

   313           val rrel = tyRel T rty rel lthy

   314        in

   315          if (needs_lift rty T) then

   316            (mk_ball ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t)

   317          else

   318            Const (@{const_name "All"}, ty) $ apply_subt (my_reg lthy rel rty) t

   319        end

   320   | Const (@{const_name "Ex"}, ty) $ (t as Abs (x, T, _)) =>

   321        let

   322           val ty1 = domain_type ty

   323           val ty2 = domain_type ty1

   324           val rrel = tyRel T rty rel lthy

   325        in

   326          if (needs_lift rty T) then

   327            (mk_bex ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t)

   328          else

   329            Const (@{const_name "Ex"}, ty) $ apply_subt (my_reg lthy rel rty) t

   330        end

   331   | Const (@{const_name "op ="}, ty) $ t =>

   332       if needs_lift rty (fastype_of t) then

   333         (tyRel (fastype_of t) rty rel lthy) $ t   (* FIXME: t should be regularised too *)

   334       else Const (@{const_name "op ="}, ty) $ (my_reg lthy rel rty t)

   335   | t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2)

   336   | _ => trm

   337 *}

   338 

   339 (* For polymorphic types we need to find the type of the Relation term. *)

   340 (* TODO: we assume that the relation is a Constant. Is this always true? *)

   341 ML {*

   342 fun my_reg_inst lthy rel rty trm =

   343   case rel of

   344     Const (n, _) => Syntax.check_term lthy

   345       (my_reg lthy (Const (n, dummyT)) (Logic.varifyT rty) trm)

   346 *}

   347 

   348 (*

   349 ML {*

   350   val r = Free ("R", dummyT);

   351   val t = (my_reg_inst @{context} r @{typ "'a list"} @{term "\<forall>(x::'b list). P x"});

   352   val t2 = Syntax.check_term @{context} t;

   353   cterm_of @{theory} t2

   354 *}

   355 *)

   356 

   357 text {* Assumes that the given theorem is atomized *}

   358 ML {*

   359   fun build_regularize_goal thm rty rel lthy =

   360      Logic.mk_implies

   361        ((prop_of thm),

   362        (my_reg_inst lthy rel rty (prop_of thm)))

   363 *}

   375 

   376 ML {*

   377 fun regularize thm rty rel rel_eqv rel_refl lthy =

   378   let

   379     val goal = build_regularize_goal thm rty rel lthy;

   380     fun tac ctxt =

   381       (ObjectLogic.full_atomize_tac) THEN'

   382       REPEAT_ALL_NEW (FIRST' [

   383         rtac rel_refl,

   384         atac,

   385         rtac @{thm universal_twice},

   386         (rtac @{thm impI} THEN' atac),

   387         rtac @{thm implication_twice},

   388         EqSubst.eqsubst_tac ctxt [0]

   389           [(@{thm equiv_res_forall} OF [rel_eqv]),

   390            (@{thm equiv_res_exists} OF [rel_eqv])],

   391         (* For a = b \<longrightarrow> a \<approx> b *)

   392         (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),

   393         (rtac @{thm RIGHT_RES_FORALL_REGULAR})

   394       ]);

   395     val cthm = Goal.prove lthy [] [] goal

   396       (fn {context, ...} => tac context 1);

   397   in

   398     cthm OF [thm]

   399   end

   400 *}

   476 (*consts Rl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"

   477 axioms Rl_eq: "EQUIV Rl"

   478 

   479 quotient ql = "'a list" / "Rl"

   480   by (rule Rl_eq)

   481 ML {*

   482   ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "'a list"}) (Logic.varifyT @{typ "'a ql"}) @{typ "nat list \<Rightarrow> (nat \<times> nat) list"});

   483   ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "nat \<times> nat"}) (Logic.varifyT @{typ "int"}) @{typ "nat list \<Rightarrow> (nat \<times> nat) list"})

   484 *}

   485 *)

   538 

   539 (* returns all subterms where two types differ *)

   540 fun diff (T, S) Ds =

   541   case (T, S) of

   542     (TVar v, TVar u) => if v = u then Ds else (T, S)::Ds 

   543   | (TFree x, TFree y) => if x = y then Ds else (T, S)::Ds

   544   | (Type (a, Ts), Type (b, Us)) => 

   545       if a = b then diffs (Ts, Us) Ds else (T, S)::Ds

   546   | _ => (T, S)::Ds

   547 and diffs (T::Ts, U::Us) Ds = diffs (Ts, Us) (diff (T, U) Ds)

   548   | diffs ([], []) Ds = Ds

   549   | diffs _ _ = error "Unequal length of type arguments"

   550 

   610 

   611 ML {*

   612 fun build_repabs_term lthy thm consts rty qty =

   613   let

   614     (* TODO: The rty and qty stored in the quotient_info should

   615        be varified, so this will soon not be needed *)

   616     val rty = Logic.varifyT rty;

   617     val qty = Logic.varifyT qty;

   618 

   619   fun mk_abs tm =

   620     let

   621       val ty = fastype_of tm

   622     in Syntax.check_term lthy ((get_fun_OLD absF (rty, qty) lthy ty) $ tm) end

   623   fun mk_repabs tm =

   624     let

   625       val ty = fastype_of tm

   626     in Syntax.check_term lthy ((get_fun_OLD repF (rty, qty) lthy ty) $ (mk_abs tm)) end

   627 

   628     fun is_lifted_const (Const (x, _)) = member (op =) consts x

   629       | is_lifted_const _ = false;

   630 

   631     fun build_aux lthy tm =

   632       case tm of

   633         Abs (a as (_, vty, _)) =>

   634           let

   635             val (vs, t) = Term.dest_abs a;

   636             val v = Free(vs, vty);

   637             val t' = lambda v (build_aux lthy t)

   638           in

   639             if (not (needs_lift rty (fastype_of tm))) then t'

   640             else mk_repabs (

   641               if not (needs_lift rty vty) then t'

   642               else

   643                 let

   644                   val v' = mk_repabs v;

   645                   (* TODO: I believe 'beta' is not needed any more *)

   646                   val t1 = (* Envir.beta_norm *) (t' $ v')

   647                 in

   648                   lambda v t1

   649                 end)

   650           end

   651       | x =>

   652         case Term.strip_comb tm of

   653           (Const(@{const_name Respects}, _), _) => tm

   654         | (opp, tms0) =>

   655           let

   656             val tms = map (build_aux lthy) tms0

   657             val ty = fastype_of tm

   658           in

   659             if (is_lifted_const opp andalso needs_lift rty ty) then

   660             mk_repabs (list_comb (opp, tms))

   661             else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then

   662               mk_repabs (list_comb (opp, tms))

   663             else if tms = [] then opp

   664             else list_comb(opp, tms)

   665           end

   666   in

   667     repeat_eqsubst_prop lthy @{thms id_def_sym}

   668       (build_aux lthy (Thm.prop_of thm))

   669   end

   670 *}

   671 

   672 text {* Builds provable goals for regularized theorems *}

   673 ML {*

   674 fun build_repabs_goal ctxt thm cons rty qty =

   675   Logic.mk_equals ((Thm.prop_of thm), (build_repabs_term ctxt thm cons rty qty))

   676 *}

   804 ML {*

   805 fun repabs lthy thm consts rty qty quot_thm reflex_thm trans_thm rsp_thms =

   806   let

   807     val rt = build_repabs_term lthy thm consts rty qty;

   808     val rg = Logic.mk_equals ((Thm.prop_of thm), rt);

   809     fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN'

   810       (REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms));

   811     val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1);

   812   in

   813     @{thm Pure.equal_elim_rule1} OF [cthm, thm]

   814   end

   815 *}

   816 

   855 *}

   856 

   857 (* TODO: Check if it behaves properly with varifyed rty *)

   858 ML {*

   859 fun findabs_all rty tm =

   860   case tm of

   861     Abs(_, T, b) =>

   862       let

   863         val b' = subst_bound ((Free ("x", T)), b);

   864         val tys = findabs_all rty b'

   865         val ty = fastype_of tm

   866       in if needs_lift rty ty then (ty :: tys) else tys

   867       end

   868   | f $ a => (findabs_all rty f) @ (findabs_all rty a)

   869   | _ => [];

   870 fun findabs rty tm = distinct (op =) (findabs_all rty tm)

   885 (* Currently useful only for LAMBDA_PRS *)

   886 ML {*

   887 fun make_simp_prs_thm lthy quot_thm thm typ =

   888   let

   889     val (_, [lty, rty]) = dest_Type typ;

   890     val thy = ProofContext.theory_of lthy;

   891     val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty)

   892     val inst = [SOME lcty, NONE, SOME rcty];

   893     val lpi = Drule.instantiate' inst [] thm;

   894     val tac =

   895       (compose_tac (false, lpi, 2)) THEN_ALL_NEW

   896       (quotient_tac quot_thm);

   897     val gc = Drule.strip_imp_concl (cprop_of lpi);

   898     val t = Goal.prove_internal [] gc (fn _ => tac 1)

   899   in

   900     MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t

   901   end

   902 *}

   903 

   904 ML {*

   905 fun findallex_all rty qty tm =

   906   case tm of

   907     Const (@{const_name All}, T) $ (s as (Abs(_, _, b))) =>

   908       let

   909         val (tya, tye) = findallex_all rty qty s

   910       in if needs_lift rty T then

   911         ((T :: tya), tye)

   912       else (tya, tye) end

   913   | Const (@{const_name Ex}, T) $ (s as (Abs(_, _, b))) =>

   914       let

   915         val (tya, tye) = findallex_all rty qty s

   916       in if needs_lift rty T then

   917         (tya, (T :: tye))

   918       else (tya, tye) end

   919   | Abs(_, T, b) =>

   920       findallex_all rty qty (subst_bound ((Free ("x", T)), b))

   921   | f $ a =>

   922       let

   923         val (a1, e1) = findallex_all rty qty f;

   924         val (a2, e2) = findallex_all rty qty a;

   925       in (a1 @ a2, e1 @ e2) end

   926   | _ => ([], []);

   927 *}

   928 

   929 ML {*

   930 fun findallex lthy rty qty tm =

   931   let

   932     val (a, e) = findallex_all rty qty tm;

   933     val (ad, ed) = (map domain_type a, map domain_type e);

   934     val (au, eu) = (distinct (op =) ad, distinct (op =) ed);

   935     val (rty, qty) = (Logic.varifyT rty, Logic.varifyT qty)

   936   in

   937     (map (exchange_ty lthy rty qty) au, map (exchange_ty lthy rty qty) eu)

   938   end

   939 *}

   940 

   941 ML {*

   942 fun make_allex_prs_thm lthy quot_thm thm typ =

   943   let

   944     val (_, [lty, rty]) = dest_Type typ;

   945     val thy = ProofContext.theory_of lthy;

   946     val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty)

   947     val inst = [NONE, SOME lcty];

   948     val lpi = Drule.instantiate' inst [] thm;

   949     val tac =

   950       (compose_tac (false, lpi, 1)) THEN_ALL_NEW

   951       (quotient_tac quot_thm);

   952     val gc = Drule.strip_imp_concl (cprop_of lpi);

   953     val t = Goal.prove_internal [] gc (fn _ => tac 1)

   954     val t_noid = MetaSimplifier.rewrite_rule

   955       [@{thm eq_reflection} OF @{thms id_apply}] t;

   956     val t_sym = @{thm "HOL.sym"} OF [t_noid];

   957     val t_eq = @{thm "eq_reflection"} OF [t_sym]

   958   in

   959     t_eq

   960   end

   961 *}

  1038 ML {*

  1039 fun lift_thm lthy qty qty_name rsp_thms defs rthm = 

  1040 let

  1041   val _ = tracing ("raw theorem:\n" ^ Syntax.string_of_term lthy (prop_of rthm))

  1042 

  1043   val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty;

  1044   val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name;

  1045   val consts = lookup_quot_consts defs;

  1046   val t_a = atomize_thm rthm;

  1047 

  1048   val _ = tracing ("raw atomized theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_a))

  1049 

  1050   val t_r = regularize t_a rty rel rel_eqv rel_refl lthy;

  1051 

  1052   val _ = tracing ("regularised theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_r))

  1053 

  1054   val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms;

  1055 

  1056   val _ = tracing ("rep/abs injected theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_t))

  1057 

  1058   val (alls, exs) = findallex lthy rty qty (prop_of t_a);

  1059   val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls

  1060   val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs

  1061   val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t

  1062 

  1063   val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_a))

  1064 

  1065   val abs = findabs rty (prop_of t_a);

  1066   val aps = findaps rty (prop_of t_a);

  1067   val app_prs_thms = map (applic_prs lthy rty qty absrep) aps;

  1068   val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs;

  1069   val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a;

  1070   

  1071   val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_l))

  1072 

  1073   val defs_sym = flat (map (add_lower_defs lthy) defs);

  1074   val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym;

  1075   val t_id = simp_ids lthy t_l;

  1076 

  1077   val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_id))

  1078 

  1079   val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id;

  1080 

  1081   val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_d0))

  1082 

  1083   val t_d = repeat_eqsubst_thm lthy defs_sym t_d0;

  1084 

  1085   val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_d))

  1086 

  1087   val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;

  1088 

  1089   val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_r))

  1090 

  1091   val t_rv = ObjectLogic.rulify t_r

  1092 

  1093   val _ = tracing ("lifted theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_rv))

  1094 in

  1095   Thm.varifyT t_rv

  1096 end

  1097 *}

  1098 

  1099 ML {*

  1100 fun lift_thm_note qty qty_name rsp_thms defs thm name lthy =

  1101   let

  1102     val lifted_thm = lift_thm lthy qty qty_name rsp_thms defs thm;

  1103     val (_, lthy2) = note (name, lifted_thm) lthy;

  1104   in

  1105     lthy2

  1106   end

  1107 *}

  1464 fun regularize_goal lthy thm rel_eqv rel_refl qtrm =

  1465   let

  1466     val reg_trm = mk_REGULARIZE_goal lthy (prop_of thm) qtrm;

  1467     fun tac lthy = regularize_tac lthy rel_eqv rel_refl;

  1468     val cthm = Goal.prove lthy [] [] reg_trm

  1469       (fn {context, ...} => tac context 1);

  1470   in

  1471     cthm OF [thm]

  1472   end

  1473 *}

  1474 

  1475 ML {*

  1476 fun repabs_goal lthy thm rty quot_thm reflex_thm trans_thm rsp_thms qtrm =

  1477   let

  1478     val rg = Syntax.check_term lthy (mk_inj_REPABS_goal lthy ((prop_of thm), qtrm));

  1479     fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN'

  1480       (REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms));

  1481     val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1);

  1482   in

  1483     @{thm Pure.equal_elim_rule1} OF [cthm, thm]

  1484   end

  1485 *}

  1486 

  1487 ML {*

  1488 fun lift_thm_goal lthy qty qty_name rsp_thms defs rthm goal =

  1489 let

  1490   val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty;

  1491   val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name;

  1492   val t_a = atomize_thm rthm;

  1493   val goal_a = atomize_goal (ProofContext.theory_of lthy) goal;

  1494   val t_r = regularize_goal lthy t_a rel_eqv rel_refl goal_a;

  1495   val t_t = repabs_goal lthy t_r rty quot rel_refl trans2 rsp_thms goal_a;

  1496   val (alls, exs) = findallex lthy rty qty (prop_of t_a);

  1497   val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls

  1498   val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs

  1499   val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t

  1500   val abs = findabs rty (prop_of t_a);

  1501   val aps = findaps rty (prop_of t_a);

  1502   val app_prs_thms = map (applic_prs lthy rty qty absrep) aps;

  1503   val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs;

  1504   val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a;

  1505   val defs_sym = flat (map (add_lower_defs lthy) defs);

  1506   val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym;

  1507   val t_id = simp_ids lthy t_l;

  1508   val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id;

  1509   val t_d = repeat_eqsubst_thm lthy defs_sym t_d0;

  1510   val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;

  1511   val t_rv = ObjectLogic.rulify t_r

  1512 in

  1513   Thm.varifyT t_rv

  1514 end

  1515 *}

  1516 

  1517 ML {*

  1518 fun lift_thm_goal_note lthy qty qty_name rsp_thms defs thm name goal =

  1519   let

  1520     val lifted_thm = lift_thm_goal lthy qty qty_name rsp_thms defs thm goal;

  1521     val (_, lthy2) = note (name, lifted_thm) lthy;

  1522   in

  1523     lthy2

  1524   end

  1525 *}

  1526 

  1527 ML {*