1 theory QuotMain

     2 imports QuotScript QuotList QuotProd Prove

     3 uses ("quotient_info.ML")

     4      ("quotient.ML")

     5      ("quotient_def.ML")

     6 begin

     7 

     8 

     9 locale QUOT_TYPE =

    10   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"

    11   and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"

    12   and   Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"

    13   assumes equivp: "equivp R"

    14   and     rep_prop: "\<And>y. \<exists>x. Rep y = R x"

    15   and     rep_inverse: "\<And>x. Abs (Rep x) = x"

    16   and     abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)"

    17   and     rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"

    18 begin

    19 

    20 definition

    21   ABS::"'a \<Rightarrow> 'b"

    22 where

    23   "ABS x \<equiv> Abs (R x)"

    24 

    25 definition

    26   REP::"'b \<Rightarrow> 'a"

    27 where

    28   "REP a = Eps (Rep a)"

    29 

    30 lemma lem9:

    31   shows "R (Eps (R x)) = R x"

    32 proof -

    33   have a: "R x x" using equivp by (simp add: equivp_reflp_symp_transp reflp_def)

    34   then have "R x (Eps (R x))" by (rule someI)

    35   then show "R (Eps (R x)) = R x"

    36     using equivp unfolding equivp_def by simp

    37 qed

    38 

    39 theorem thm10:

    40   shows "ABS (REP a) \<equiv> a"

    41   apply  (rule eq_reflection)

    42   unfolding ABS_def REP_def

    43 proof -

    44   from rep_prop

    45   obtain x where eq: "Rep a = R x" by auto

    46   have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp

    47   also have "\<dots> = Abs (R x)" using lem9 by simp

    48   also have "\<dots> = Abs (Rep a)" using eq by simp

    49   also have "\<dots> = a" using rep_inverse by simp

    50   finally

    51   show "Abs (R (Eps (Rep a))) = a" by simp

    52 qed

    53 

    54 lemma REP_refl:

    55   shows "R (REP a) (REP a)"

    56 unfolding REP_def

    57 by (simp add: equivp[simplified equivp_def])

    58 

    59 lemma lem7:

    60   shows "(R x = R y) = (Abs (R x) = Abs (R y))"

    61 apply(rule iffI)

    62 apply(simp)

    63 apply(drule rep_inject[THEN iffD2])

    64 apply(simp add: abs_inverse)

    65 done

    66 

    67 theorem thm11:

    68   shows "R r r' = (ABS r = ABS r')"

    69 unfolding ABS_def

    70 by (simp only: equivp[simplified equivp_def] lem7)

    71 

    72 

    73 lemma REP_ABS_rsp:

    74   shows "R f (REP (ABS g)) = R f g"

    75   and   "R (REP (ABS g)) f = R g f"

    76 by (simp_all add: thm10 thm11)

    77 

    78 lemma Quotient:

    79   "Quotient R ABS REP"

    80 apply(unfold Quotient_def)

    81 apply(simp add: thm10)

    82 apply(simp add: REP_refl)

    83 apply(subst thm11[symmetric])

    84 apply(simp add: equivp[simplified equivp_def])

    85 done

    86 

    87 lemma R_trans:

    88   assumes ab: "R a b"

    89   and     bc: "R b c"

    90   shows "R a c"

    91 proof -

    92   have tr: "transp R" using equivp equivp_reflp_symp_transp[of R] by simp

    93   moreover have ab: "R a b" by fact

    94   moreover have bc: "R b c" by fact

    95   ultimately show "R a c" unfolding transp_def by blast

    96 qed

    97 

    98 lemma R_sym:

    99   assumes ab: "R a b"

   100   shows "R b a"

   101 proof -

   102   have re: "symp R" using equivp equivp_reflp_symp_transp[of R] by simp

   103   then show "R b a" using ab unfolding symp_def by blast

   104 qed

   105 

   106 lemma R_trans2:

   107   assumes ac: "R a c"

   108   and     bd: "R b d"

   109   shows "R a b = R c d"

   110 using ac bd

   111 by (blast intro: R_trans R_sym)

   112 

   113 lemma REPS_same:

   114   shows "R (REP a) (REP b) \<equiv> (a = b)"

   115 proof -

   116   have "R (REP a) (REP b) = (a = b)"

   117   proof

   118     assume as: "R (REP a) (REP b)"

   119     from rep_prop

   120     obtain x y

   121       where eqs: "Rep a = R x" "Rep b = R y" by blast

   122     from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp

   123     then have "R x (Eps (R y))" using lem9 by simp

   124     then have "R (Eps (R y)) x" using R_sym by blast

   125     then have "R y x" using lem9 by simp

   126     then have "R x y" using R_sym by blast

   127     then have "ABS x = ABS y" using thm11 by simp

   128     then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp

   129     then show "a = b" using rep_inverse by simp

   130   next

   131     assume ab: "a = b"

   132     have "reflp R" using equivp equivp_reflp_symp_transp[of R] by simp

   133     then show "R (REP a) (REP b)" unfolding reflp_def using ab by auto

   134   qed

   135   then show "R (REP a) (REP b) \<equiv> (a = b)" by simp

   136 qed

   137 

   138 end

   139 

   140 section {* type definition for the quotient type *}

   141 

   142 (* the auxiliary data for the quotient types *)

   143 use "quotient_info.ML"

   144 

   145 declare [[map list = (map, list_rel)]]

   146 declare [[map * = (prod_fun, prod_rel)]]

   147 declare [[map "fun" = (fun_map, fun_rel)]]

   148 

   149 (* identity quotient is not here as it has to be applied first *)

   150 lemmas [quotient_thm] =

   151   fun_quotient list_quotient prod_quotient

   152 

   153 lemmas [quotient_rsp] =

   154   quot_rel_rsp nil_rsp cons_rsp foldl_rsp pair_rsp

   155 

   156 (* fun_map is not here since equivp is not true *)

   157 (* TODO: option, ... *)

   158 lemmas [quotient_equiv] =

   159   identity_equivp list_equivp prod_equivp

   160 

   161 

   162 ML {* maps_lookup @{theory} "List.list" *}

   163 ML {* maps_lookup @{theory} "*" *}

   164 ML {* maps_lookup @{theory} "fun" *}

   165 

   166 

   167 (* definition of the quotient types *)

   168 (* FIXME: should be called quotient_typ.ML *)

   169 use "quotient.ML"

   170 

   171 

   172 (* lifting of constants *)

   173 use "quotient_def.ML"

   174 

   175 section {* Simset setup *}

   176 

   177 (* since HOL_basic_ss is too "big", we need to set up *)

   178 (* our own minimal simpset                            *)

   179 ML {*

   180 fun  mk_minimal_ss ctxt =

   181   Simplifier.context ctxt empty_ss

   182     setsubgoaler asm_simp_tac

   183     setmksimps (mksimps [])

   184 *}

   185 

   186 section {* atomize *}

   187 

   188 lemma atomize_eqv[atomize]:

   189   shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"

   190 proof

   191   assume "A \<equiv> B"

   192   then show "Trueprop A \<equiv> Trueprop B" by unfold

   193 next

   194   assume *: "Trueprop A \<equiv> Trueprop B"

   195   have "A = B"

   196   proof (cases A)

   197     case True

   198     have "A" by fact

   199     then show "A = B" using * by simp

   200   next

   201     case False

   202     have "\<not>A" by fact

   203     then show "A = B" using * by auto

   204   qed

   205   then show "A \<equiv> B" by (rule eq_reflection)

   206 qed

   207 

   208 ML {*

   209 fun atomize_thm thm =

   210 let

   211   val thm' = Thm.freezeT (forall_intr_vars thm)

   212   val thm'' = ObjectLogic.atomize (cprop_of thm')

   213 in

   214   @{thm equal_elim_rule1} OF [thm'', thm']

   215 end

   216 *}

   217 

   218 section {* infrastructure about id *}

   219 

   220 lemma prod_fun_id: "prod_fun id id \<equiv> id"

   221   by (rule eq_reflection) (simp add: prod_fun_def)

   222 

   223 lemma map_id: "map id \<equiv> id"

   224   apply (rule eq_reflection)

   225   apply (rule ext)

   226   apply (rule_tac list="x" in list.induct)

   227   apply (simp_all)

   228   done

   229 

   230 lemmas id_simps =

   231   fun_map_id[THEN eq_reflection]

   232   id_apply[THEN eq_reflection]

   233   id_def[THEN eq_reflection,symmetric]

   234   prod_fun_id map_id

   235 

   236 ML {*

   237 fun simp_ids thm =

   238   MetaSimplifier.rewrite_rule @{thms id_simps} thm

   239 *}

   240 

   241 section {* Debugging infrastructure for testing tactics *}

   242 

   243 ML {*

   244 fun my_print_tac ctxt s i thm =

   245 let

   246   val prem_str = nth (prems_of thm) (i - 1)

   247                  |> Syntax.string_of_term ctxt

   248                  handle Subscript => "no subgoal"

   249   val _ = tracing (s ^ "\n" ^ prem_str)

   250 in

   251   Seq.single thm

   252 end *}

   253 

   254 ML {*

   255 fun DT ctxt s tac i thm =

   256 let

   257   val before_goal = nth (prems_of thm) (i - 1)

   258                     |> Syntax.string_of_term ctxt

   259   val before_msg = ["before: " ^ s, before_goal, "after: " ^ s]

   260                    |> cat_lines

   261 in 

   262   EVERY [tac i, my_print_tac ctxt before_msg i] thm

   263 end

   264 

   265 fun NDT ctxt s tac thm = tac thm  

   266 *}

   267 

   268 section {* Matching of terms and types *}

   269 

   270 ML {*

   271 fun matches_typ (ty, ty') =

   272   case (ty, ty') of

   273     (_, TVar _) => true

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

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

   276        s = s' andalso 

   277        if (length tys = length tys') 

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

   279        else false

   280   | _ => false

   281 *}

   282 

   283 ML {*

   284 fun matches_term (trm, trm') = 

   285    case (trm, trm') of 

   286      (_, Var _) => true

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

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

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

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

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

   292    | _ => false

   293 *}

   294 

   295 section {* Infrastructure for collecting theorems for starting the lifting *}

   296 

   297 ML {*

   298 fun lookup_quot_data lthy qty =

   299   let

   300     val qty_name = fst (dest_Type qty)

   301     val SOME quotdata = quotdata_lookup lthy qty_name

   302     (* TODO: Should no longer be needed *)

   303     val rty = Logic.unvarifyT (#rtyp quotdata)

   304     val rel = #rel quotdata

   305     val rel_eqv = #equiv_thm quotdata

   306     val rel_refl = @{thm equivp_reflp} OF [rel_eqv]

   307   in

   308     (rty, rel, rel_refl, rel_eqv)

   309   end

   310 *}

   311 

   312 ML {*

   313 fun lookup_quot_thms lthy qty_name =

   314   let

   315     val thy = ProofContext.theory_of lthy;

   316     val trans2 = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".R_trans2")

   317     val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same")

   318     val absrep = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".thm10")

   319     val quot = PureThy.get_thm thy ("Quotient_" ^ qty_name)

   320   in

   321     (trans2, reps_same, absrep, quot)

   322   end

   323 *}

   324 

   325 section {* Regularization *} 

   326 

   327 (*

   328 Regularizing an rtrm means:

   329  - quantifiers over a type that needs lifting are replaced by

   330    bounded quantifiers, for example:

   331       \<forall>x. P     \<Longrightarrow>     \<forall>x \<in> (Respects R). P  /  All (Respects R) P

   332 

   333    the relation R is given by the rty and qty;

   334  

   335  - abstractions over a type that needs lifting are replaced

   336    by bounded abstractions:

   337       \<lambda>x. P     \<Longrightarrow>     Ball (Respects R) (\<lambda>x. P)

   338 

   339  - equalities over the type being lifted are replaced by

   340    corresponding relations:

   341       A = B     \<Longrightarrow>     A \<approx> B

   342 

   343    example with more complicated types of A, B:

   344       A = B     \<Longrightarrow>     (op = \<Longrightarrow> op \<approx>) A B

   345 *)

   346 

   347 ML {*

   348 (* builds the relation that is the argument of respects *)

   349 fun mk_resp_arg lthy (rty, qty) =

   350 let

   351   val thy = ProofContext.theory_of lthy

   352 in  

   353   if rty = qty

   354   then HOLogic.eq_const rty

   355   else

   356     case (rty, qty) of

   357       (Type (s, tys), Type (s', tys')) =>

   358        if s = s' 

   359        then let

   360               val SOME map_info = maps_lookup thy s

   361               val args = map (mk_resp_arg lthy) (tys ~~ tys')

   362             in

   363               list_comb (Const (#relfun map_info, dummyT), args) 

   364             end  

   365        else let  

   366               val SOME qinfo = quotdata_lookup_thy thy s'

   367               (* FIXME: check in this case that the rty and qty *)

   368               (* FIXME: correspond to each other *)

   369               val (s, _) = dest_Const (#rel qinfo)

   370               (* FIXME: the relation should only be the string        *)

   371               (* FIXME: and the type needs to be calculated as below; *)

   372               (* FIXME: maybe one should actually have a term         *)

   373               (* FIXME: and one needs to force it to have this type   *)

   374             in

   375               Const (s, rty --> rty --> @{typ bool})

   376             end

   377       | _ => HOLogic.eq_const dummyT 

   378              (* FIXME: check that the types correspond to each other? *)

   379 end

   380 *}

   381 

   382 ML {*

   383 val mk_babs = Const (@{const_name Babs}, dummyT)

   384 val mk_ball = Const (@{const_name Ball}, dummyT)

   385 val mk_bex  = Const (@{const_name Bex}, dummyT)

   386 val mk_resp = Const (@{const_name Respects}, dummyT)

   387 *}

   388 

   389 ML {*

   390 (* - applies f to the subterm of an abstraction,   *)

   391 (*   otherwise to the given term,                  *)

   392 (* - used by regularize, therefore abstracted      *)

   393 (*   variables do not have to be treated specially *)

   394 

   395 fun apply_subt f trm1 trm2 =

   396   case (trm1, trm2) of

   397     (Abs (x, T, t), Abs (x', T', t')) => Abs (x, T, f t t')

   398   | _ => f trm1 trm2

   399 

   400 (* the major type of All and Ex quantifiers *)

   401 fun qnt_typ ty = domain_type (domain_type ty)  

   402 *}

   403 

   404 ML {*

   405 (* produces a regularized version of rtm      *)

   406 (* - the result is still not completely typed *)

   407 (* - does not need any special treatment of   *)

   408 (*   bound variables                          *)

   409 

   410 fun regularize_trm lthy rtrm qtrm =

   411   case (rtrm, qtrm) of

   412     (Abs (x, ty, t), Abs (x', ty', t')) =>

   413        let

   414          val subtrm = Abs(x, ty, regularize_trm lthy t t')

   415        in

   416          if ty = ty'

   417          then subtrm

   418          else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm

   419        end

   420 

   421   | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>

   422        let

   423          val subtrm = apply_subt (regularize_trm lthy) t t'

   424        in

   425          if ty = ty'

   426          then Const (@{const_name "All"}, ty) $ subtrm

   427          else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm

   428        end

   429 

   430   | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>

   431        let

   432          val subtrm = apply_subt (regularize_trm lthy) t t'

   433        in

   434          if ty = ty'

   435          then Const (@{const_name "Ex"}, ty) $ subtrm

   436          else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm

   437        end

   438 

   439   | (* equalities need to be replaced by appropriate equivalence relations *) 

   440     (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) =>

   441          if ty = ty'

   442          then rtrm

   443          else mk_resp_arg lthy (domain_type ty, domain_type ty') 

   444 

   445   | (* in this case we check whether the given equivalence relation is correct *) 

   446     (rel, Const (@{const_name "op ="}, ty')) =>

   447        let 

   448          val exc = LIFT_MATCH "regularise (relation mismatch)"

   449          val rel_ty = (fastype_of rel) handle TERM _ => raise exc 

   450          val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty') 

   451        in 

   452          if rel' = rel

   453          then rtrm

   454          else raise exc

   455        end  

   456   | (_, Const (s, _)) =>

   457        let 

   458          fun same_name (Const (s, _)) (Const (s', _)) = (s = s')

   459            | same_name _ _ = false

   460        in

   461          if same_name rtrm qtrm 

   462          then rtrm 

   463          else 

   464            let 

   465              fun exc1 s = LIFT_MATCH ("regularize (constant " ^ s ^ " not found)")

   466              val exc2   = LIFT_MATCH ("regularize (constant mismatch)")

   467              val thy = ProofContext.theory_of lthy

   468              val rtrm' = (#rconst (qconsts_lookup thy s)) handle NotFound => raise (exc1 s) 

   469            in 

   470              if matches_term (rtrm, rtrm')

   471              then rtrm

   472              else raise exc2

   473            end

   474        end 

   475 

   476   | (t1 $ t2, t1' $ t2') =>

   477        (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2')

   478 

   479   | (Free (x, ty), Free (x', ty')) => 

   480        (* this case cannot arrise as we start with two fully atomized terms *)

   481        raise (LIFT_MATCH "regularize (frees)")

   482 

   483   | (Bound i, Bound i') =>

   484        if i = i' 

   485        then rtrm 

   486        else raise (LIFT_MATCH "regularize (bounds mismatch)")

   487 

   488   | (rt, qt) =>

   489        raise (LIFT_MATCH "regularize (default)")

   490 *}

   491 

   492 ML {*

   493 fun equiv_tac ctxt =

   494   REPEAT_ALL_NEW (FIRST' 

   495     [resolve_tac (equiv_rules_get ctxt)])

   496 *}

   497 

   498 ML {*

   499 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)

   500 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac

   501 *}

   502 

   503 ML {*

   504 fun prep_trm thy (x, (T, t)) =

   505   (cterm_of thy (Var (x, T)), cterm_of thy t)

   506 

   507 fun prep_ty thy (x, (S, ty)) =

   508   (ctyp_of thy (TVar (x, S)), ctyp_of thy ty)

   509 *}

   510 

   511 ML {*

   512 fun matching_prs thy pat trm =

   513 let

   514   val univ = Unify.matchers thy [(pat, trm)]

   515   val SOME (env, _) = Seq.pull univ

   516   val tenv = Vartab.dest (Envir.term_env env)

   517   val tyenv = Vartab.dest (Envir.type_env env)

   518 in

   519   (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)

   520 end

   521 *}

   522 

   523 ML {*

   524 fun calculate_instance ctxt thm redex R1 R2 =

   525 let

   526   val thy = ProofContext.theory_of ctxt

   527   val goal = Const (@{const_name "equivp"}, dummyT) $ R2  

   528              |> Syntax.check_term ctxt

   529              |> HOLogic.mk_Trueprop 

   530   val eqv_prem = Goal.prove ctxt [] [] goal (fn {context,...} => equiv_tac context 1)

   531   val thm = (@{thm eq_reflection} OF [thm OF [eqv_prem]])

   532   val R1c = cterm_of thy R1

   533   val thmi = Drule.instantiate' [] [SOME R1c] thm

   534   val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) redex

   535   val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi)

   536 in

   537   SOME thm2

   538 end

   539 handle _ => NONE

   540 (* FIXME/TODO: what is the place where the exception can be raised: matching_prs? *)

   541 *}

   542 

   543 ML {*

   544 fun ball_bex_range_simproc ss redex =

   545 let

   546   val ctxt = Simplifier.the_context ss

   547 in 

   548  case redex of

   549     (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $ 

   550       (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>

   551         calculate_instance ctxt @{thm ball_reg_eqv_range} redex R1 R2

   552   | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $ 

   553       (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>  

   554         calculate_instance ctxt @{thm bex_reg_eqv_range} redex R1 R2

   555   | _ => NONE

   556 end

   557 *}

   558 

   559 lemma eq_imp_rel: 

   560   shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"

   561 by (simp add: equivp_reflp)

   562 

   563 (* FIXME/TODO: How does regularizing work? *)

   564 (* FIXME/TODO: needs to be adapted

   565 

   566 To prove that the raw theorem implies the regularised one, 

   567 we try in order:

   568 

   569  - Reflexivity of the relation

   570  - Assumption

   571  - Elimnating quantifiers on both sides of toplevel implication

   572  - Simplifying implications on both sides of toplevel implication

   573  - Ball (Respects ?E) ?P = All ?P

   574  - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q

   575 

   576 *)

   577 ML {*

   578 fun regularize_tac ctxt =

   579 let

   580   val thy = ProofContext.theory_of ctxt

   581   val pat_ball = @{term "Ball (Respects (R1 ===> R2)) P"}

   582   val pat_bex  = @{term "Bex (Respects (R1 ===> R2)) P"}

   583   val simproc = Simplifier.simproc_i thy "" [pat_ball, pat_bex] (K (ball_bex_range_simproc))

   584   val simpset = (mk_minimal_ss ctxt) 

   585                        addsimps @{thms ball_reg_eqv bex_reg_eqv}

   586                        addsimprocs [simproc] addSolver equiv_solver

   587   (* TODO: Make sure that there are no list_rel, pair_rel etc involved *)

   588   val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt)

   589 in

   590   ObjectLogic.full_atomize_tac THEN'

   591   simp_tac simpset THEN'

   592   REPEAT_ALL_NEW (FIRST' [

   593     rtac @{thm ball_reg_right},

   594     rtac @{thm bex_reg_left},

   595     resolve_tac (Inductive.get_monos ctxt),

   596     rtac @{thm ball_all_comm},

   597     rtac @{thm bex_ex_comm},

   598     resolve_tac eq_eqvs,

   599     simp_tac simpset])

   600 end

   601 *}

   602 

   603 section {* Injections of rep and abses *}

   604 

   605 (*

   606 Injecting repabs means:

   607 

   608   For abstractions:

   609   * If the type of the abstraction doesn't need lifting we recurse.

   610   * If it does we add RepAbs around the whole term and check if the

   611     variable needs lifting.

   612     * If it doesn't then we recurse

   613     * If it does we recurse and put 'RepAbs' around all occurences

   614       of the variable in the obtained subterm. This in combination

   615       with the RepAbs above will let us change the type of the

   616       abstraction with rewriting.

   617   For applications:

   618   * If the term is 'Respects' applied to anything we leave it unchanged

   619   * If the term needs lifting and the head is a constant that we know

   620     how to lift, we put a RepAbs and recurse

   621   * If the term needs lifting and the head is a free applied to subterms

   622     (if it is not applied we treated it in Abs branch) then we

   623     put RepAbs and recurse

   624   * Otherwise just recurse.

   625 *)

   626 

   627 ML {*

   628 fun mk_repabs lthy (T, T') trm = 

   629   Quotient_Def.get_fun repF lthy (T, T') 

   630     $ (Quotient_Def.get_fun absF lthy (T, T') $ trm)

   631 *}

   632 

   633 ML {*

   634 (* bound variables need to be treated properly,    *)

   635 (* as the type of subterms need to be calculated   *)

   636 (* in the abstraction case                         *)

   637 

   638 fun inj_repabs_trm lthy (rtrm, qtrm) =

   639  case (rtrm, qtrm) of

   640     (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>

   641        Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm lthy (t, t'))

   642 

   643   | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>

   644        Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t'))

   645 

   646   | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) =>

   647        Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t'))

   648 

   649   | (Abs (x, T, t), Abs (x', T', t')) =>

   650       let

   651         val rty = fastype_of rtrm

   652         val qty = fastype_of qtrm

   653         val (y, s) = Term.dest_abs (x, T, t)

   654         val (_, s') = Term.dest_abs (x', T', t')

   655         val yvar = Free (y, T)

   656         val result = Term.lambda_name (y, yvar) (inj_repabs_trm lthy (s, s'))

   657       in

   658         if rty = qty 

   659         then result

   660         else mk_repabs lthy (rty, qty) result

   661       end

   662 

   663   | (t $ s, t' $ s') =>  

   664        (inj_repabs_trm lthy (t, t')) $ (inj_repabs_trm lthy (s, s'))

   665 

   666   | (Free (_, T), Free (_, T')) => 

   667         if T = T' 

   668         then rtrm 

   669         else mk_repabs lthy (T, T') rtrm

   670 

   671   | (_, Const (@{const_name "op ="}, _)) => rtrm

   672 

   673     (* FIXME: check here that rtrm is the corresponding definition for the const *)

   674   | (_, Const (_, T')) =>

   675       let

   676         val rty = fastype_of rtrm

   677       in 

   678         if rty = T'                    

   679         then rtrm

   680         else mk_repabs lthy (rty, T') rtrm

   681       end   

   682   

   683   | _ => raise (LIFT_MATCH "injection")

   684 *}

   685 

   686 section {* RepAbs Injection Tactic *}

   687 

   688 ML {*

   689 fun quotient_tac ctxt =

   690   REPEAT_ALL_NEW (FIRST'

   691     [rtac @{thm identity_quotient},

   692      resolve_tac (quotient_rules_get ctxt)])

   693 *}

   694 

   695 (* solver for the simplifier *)

   696 ML {*

   697 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)

   698 val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac

   699 *}

   700 

   701 ML {*

   702 fun solve_quotient_assums ctxt thm =

   703   let val gl = hd (Drule.strip_imp_prems (cprop_of thm)) in

   704   thm OF [Goal.prove_internal [] gl (fn _ => quotient_tac ctxt 1)]

   705   end

   706   handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing"

   707 *}

   708 

   709 (* Not used *)

   710 (* It proves the Quotient assumptions by calling quotient_tac *)

   711 ML {*

   712 fun solve_quotient_assum i ctxt thm =

   713   let

   714     val tac =

   715       (compose_tac (false, thm, i)) THEN_ALL_NEW

   716       (quotient_tac ctxt);

   717     val gc = Drule.strip_imp_concl (cprop_of thm);

   718   in

   719     Goal.prove_internal [] gc (fn _ => tac 1)

   720   end

   721   handle _ => error "solve_quotient_assum"

   722 *}

   723 

   724 definition

   725   "QUOT_TRUE x \<equiv> True"

   726 

   727 ML {*

   728 fun find_qt_asm asms =

   729   let

   730     fun find_fun trm =

   731       case trm of

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

   733       | _ => false

   734   in

   735     case find_first find_fun asms of

   736       SOME (_ $ (_ $ (f $ a))) => (f, a)

   737     | SOME _ => error "find_qt_asm: no pair"

   738     | NONE => error "find_qt_asm: no assumption"

   739   end

   740 *}

   741 

   742 (*

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

   744 we try:

   745 

   746  1) theorems 'trans2' from the appropriate QUOT_TYPE

   747  2) remove lambdas from both sides: lambda_rsp_tac

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

   749  4) use user-supplied RSP theorems

   750  5) remove rep_abs from the right side

   751  6) reflexivity of equality

   752  7) split applications of lifted type (apply_rsp)

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

   754  9) apply extentionality

   755  A) reflexivity of the relation

   756  B) assumption

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

   758  C) proving obvious higher order equalities by simplifying fun_rel

   759     (not sure if it is still needed?)

   760  D) unfolding lambda on one side

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

   762 

   763 *)

   764 

   765 lemma quot_true_dests:

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

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

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

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

   770 apply(simp_all add: QUOT_TRUE_def ext)

   771 done

   772 

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

   774 by (simp add: QUOT_TRUE_def)

   775 

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

   777 by (simp add: QUOT_TRUE_def)

   778 

   779 ML {*

   780 fun quot_true_conv1 ctxt fnctn ctrm =

   781   case (term_of ctrm) of

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

   783     let

   784       val fx = fnctn x;

   785       val thy = ProofContext.theory_of ctxt;

   786       val cx = cterm_of thy x;

   787       val cfx = cterm_of thy fx;

   788       val cxt = ctyp_of thy (fastype_of x);

   789       val cfxt = ctyp_of thy (fastype_of fx);

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

   791     in

   792       Conv.rewr_conv thm ctrm

   793     end

   794 *}

   795 

   796 ML {*

   797 fun quot_true_conv ctxt fnctn ctrm =

   798   case (term_of ctrm) of

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

   800       quot_true_conv1 ctxt fnctn ctrm

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

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

   803   | _ => Conv.all_conv ctrm

   804 *}

   805 

   806 ML {*

   807 fun quot_true_tac ctxt fnctn = CONVERSION

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

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

   810 *}

   811 

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

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

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

   815 ML {*

   816 fun unlam t =

   817   case t of

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

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

   820 *}

   821 

   822 ML {*

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

   824   | dest_fun_type _ = error "dest_fun_type"

   825 *}

   826 

   827 ML {*

   828 val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl

   829 *}

   830 

   831 ML {*

   832 val apply_rsp_tac =

   833   Subgoal.FOCUS (fn {concl, asms, context,...} =>

   834     case ((HOLogic.dest_Trueprop (term_of concl))) of

   835       ((R2 $ (f $ x) $ (g $ y))) =>

   836         (let

   837           val (asmf, asma) = find_qt_asm (map term_of asms);

   838         in

   839           if (fastype_of asmf) = (fastype_of f) then no_tac else let

   840             val ty_a = fastype_of x;

   841             val ty_b = fastype_of asma;

   842             val ty_c = range_type (type_of f);

   843             val thy = ProofContext.theory_of context;

   844             val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c];

   845             val thm = Drule.instantiate' ty_inst [] @{thm apply_rsp}

   846             val te = solve_quotient_assums context thm

   847             val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];

   848             val thm = Drule.instantiate' [] t_inst te

   849           in

   850             compose_tac (false, thm, 2) 1

   851           end

   852         end

   853         handle ERROR "find_qt_asm: no pair" => no_tac)

   854     | _ => no_tac)

   855 *}

   856 ML {*

   857 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)

   858 *}

   859 

   860 ML {*

   861 fun rep_abs_rsp_tac ctxt =

   862   SUBGOAL (fn (goal, i) =>

   863     case (bare_concl goal) of 

   864       (rel $ _ $ (rep $ (abs $ _))) =>

   865         (let

   866            val thy = ProofContext.theory_of ctxt;

   867            val (ty_a, ty_b) = dest_fun_type (fastype_of abs);

   868            val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];

   869            val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep];

   870            val thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp}

   871            val te = solve_quotient_assums ctxt thm

   872          in

   873            rtac te i

   874          end

   875          handle _ => no_tac)

   876     | _ => no_tac)

   877 *}

   878 

   879 ML {*

   880 fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) =>

   881 (case (bare_concl goal) of

   882     (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)

   883   ((Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _))

   884       => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam

   885 

   886     (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)

   887 | (Const (@{const_name "op ="},_) $

   888     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $

   889     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))

   890       => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}

   891 

   892     (* (R1 ===> op =) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Ball\<dots>x) = (Ball\<dots>y) *)

   893 | (Const (@{const_name fun_rel}, _) $ _ $ _) $

   894     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $

   895     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)

   896       => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam

   897 

   898     (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)

   899 | Const (@{const_name "op ="},_) $

   900     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $

   901     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)

   902       => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}

   903 

   904     (* (R1 ===> op =) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Bex\<dots>x) = (Bex\<dots>y) *)

   905 | (Const (@{const_name fun_rel}, _) $ _ $ _) $

   906     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $

   907     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)

   908       => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam

   909 

   910 | (_ $

   911     (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $

   912     (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))

   913       => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt]

   914 

   915     (* reflexivity of operators arising from Cong_tac *)

   916 | Const (@{const_name "op ="},_) $ _ $ _ 

   917       => rtac @{thm refl} ORELSE'

   918           (resolve_tac trans2 THEN' RANGE [

   919             quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])

   920 

   921 (* TODO: These patterns should should be somehow combined and generalized... *)

   922 | (Const (@{const_name fun_rel}, _) $ _ $ _) $

   923     (Const (@{const_name fun_rel}, _) $ _ $ _) $

   924     (Const (@{const_name fun_rel}, _) $ _ $ _)

   925     => rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt

   926 

   927 | (Const (@{const_name fun_rel}, _) $ _ $ _) $

   928     (Const (@{const_name prod_rel}, _) $ _ $ _) $

   929     (Const (@{const_name prod_rel}, _) $ _ $ _)

   930     => rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt

   931 

   932    (* respectfulness of constants; in particular of a simple relation *)

   933 | _ $ (Const _) $ (Const _)  (* fun_rel, list_rel, etc but not equality *)

   934     => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt

   935 

   936     (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)

   937     (* observe ---> *)

   938 | _ $ _ $ _ 

   939     => rep_abs_rsp_tac ctxt

   940 

   941 | _ => error "inj_repabs_tac not a relation"

   942 ) i)

   943 *}

   944 

   945 ML {*

   946 fun inj_repabs_tac ctxt rel_refl trans2 =

   947   (FIRST' [

   948     inj_repabs_tac_match ctxt trans2,

   949     (* R (t $ \<dots>) (t' $ \<dots>) ----> apply_rsp   provided type of t needs lifting *)

   950     NDT ctxt "A" (apply_rsp_tac ctxt THEN'

   951                 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),

   952     (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong   provided type of t does not need lifting *)

   953     (* merge with previous tactic *)

   954     NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN'

   955                 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),

   956     (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *)

   957     NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam),

   958     (* resolving with R x y assumptions *)

   959     NDT ctxt "E" (atac),

   960     (* reflexivity of the basic relations *)

   961     (* R \<dots> \<dots> *)

   962     NDT ctxt "D" (resolve_tac rel_refl)

   963     ])

   964 *}

   965 

   966 ML {*

   967 fun all_inj_repabs_tac ctxt rel_refl trans2 =

   968   REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2)

   969 *}

   970 

   971 section {* Cleaning of the theorem *}

   972 

   973 ML {*

   974 fun make_inst lhs t =

   975   let

   976     val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;

   977     val _ $ (Abs (_, _, g)) = t;

   978     fun mk_abs i t =

   979       if incr_boundvars i u aconv t then Bound i

   980       else (case t of

   981         t1 $ t2 => mk_abs i t1 $ mk_abs i t2

   982       | Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t')

   983       | Bound j => if i = j then error "make_inst" else t

   984       | _ => t);

   985   in (f, Abs ("x", T, mk_abs 0 g)) end;

   986 *}

   987 

   988 ML {*

   989 fun lambda_prs_simple_conv ctxt ctrm =

   990   case (term_of ctrm) of

   991    ((Const (@{const_name fun_map}, _) $ r1 $ (a2 as (Const (s,_)))) $ (Abs _)) =>

   992      let

   993        val thy = ProofContext.theory_of ctxt

   994        val (ty_b, ty_a) = dest_fun_type (fastype_of r1)

   995        val (ty_c, ty_d) = dest_fun_type (fastype_of a2)

   996        val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]

   997        val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]

   998        val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs}

   999        val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)]

  1000        val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te

  1001        val _ = tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te)));

  1002        val tl = Thm.lhs_of ts

  1003        val (insp, inst) = make_inst (term_of tl) (term_of ctrm)

  1004        val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts

  1005        val _ = if not (s = @{const_name "id"}) then

  1006                   (tracing "lambda_prs";

  1007                    tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm)));

  1008                    tracing ("lpi rule:\n" ^ (Syntax.string_of_term ctxt (prop_of lpi)));

  1009                    tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te)));

  1010                    tracing ("ts rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ts)));

  1011                    tracing ("instantiated rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti))))

  1012                else ()

  1013      in

  1014        Conv.rewr_conv ti ctrm

  1015      end

  1016   | _ => Conv.all_conv ctrm

  1017 *}

  1018 

  1019 ML {*

  1020 val lambda_prs_conv =

  1021   More_Conv.top_conv lambda_prs_simple_conv

  1022 

  1023 fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)

  1024 *}

  1025 

  1026 (*

  1027  Cleaning the theorem consists of three rewriting steps.

  1028  The first two need to be done before fun_map is unfolded

  1029 

  1030  1) lambda_prs:

  1031      (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))  ---->  f

  1032 

  1033     Implemented as conversion since it is not a pattern.

  1034 

  1035  2) all_prs (the same for exists):

  1036      Ball (Respects R) ((abs ---> id) f)  ---->  All f

  1037 

  1038     Rewriting with definitions from the argument defs

  1039      (rep ---> abs) oldConst ----> newconst

  1040 

  1041  3) Quotient_rel_rep:

  1042       Rel (Rep x) (Rep y)  ---->  x = y

  1043 

  1044     Quotient_abs_rep:

  1045       Abs (Rep x)  ---->  x

  1046 

  1047     id_simps; fun_map.simps

  1048 *)

  1049 

  1050 ML {*

  1051 fun clean_tac lthy =

  1052   let

  1053     val thy = ProofContext.theory_of lthy;

  1054     val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)

  1055       (* FIXME: shouldn't the definitions already be varified? *)

  1056     val thms1 = @{thms all_prs ex_prs} @ defs

  1057     val thms2 = @{thms eq_reflection[OF fun_map.simps]} 

  1058                 @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} 

  1059     fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver

  1060   in

  1061     EVERY' [lambda_prs_tac lthy,

  1062             simp_tac (simps thms1),

  1063             simp_tac (simps thms2),

  1064             TRY o rtac refl]

  1065   end

  1066 *}

  1067 

  1068 section {* Genralisation of free variables in a goal *}

  1069 

  1070 ML {*

  1071 fun inst_spec ctrm =

  1072    Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}

  1073 

  1074 fun inst_spec_tac ctrms =

  1075   EVERY' (map (dtac o inst_spec) ctrms)

  1076 

  1077 fun all_list xs trm = 

  1078   fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm

  1079 

  1080 fun apply_under_Trueprop f = 

  1081   HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop

  1082 

  1083 fun gen_frees_tac ctxt =

  1084  SUBGOAL (fn (concl, i) =>

  1085   let

  1086     val thy = ProofContext.theory_of ctxt

  1087     val vrs = Term.add_frees concl []

  1088     val cvrs = map (cterm_of thy o Free) vrs

  1089     val concl' = apply_under_Trueprop (all_list vrs) concl

  1090     val goal = Logic.mk_implies (concl', concl)

  1091     val rule = Goal.prove ctxt [] [] goal 

  1092       (K (EVERY1 [inst_spec_tac (rev cvrs), atac]))

  1093   in

  1094     rtac rule i

  1095   end)  

  1096 *}

  1097 

  1098 section {* General outline of the lifting procedure *}

  1099 

  1100 (* - A is the original raw theorem          *)

  1101 (* - B is the regularized theorem           *)

  1102 (* - C is the rep/abs injected version of B *) 

  1103 (* - D is the lifted theorem                *)

  1104 (*                                          *)

  1105 (* - b is the regularization step           *)

  1106 (* - c is the rep/abs injection step        *)

  1107 (* - d is the cleaning part                 *)

  1108 

  1109 lemma lifting_procedure:

  1110   assumes a: "A"

  1111   and     b: "A \<Longrightarrow> B"

  1112   and     c: "B = C"

  1113   and     d: "C = D"

  1114   shows   "D"

  1115   using a b c d

  1116   by simp

  1117 

  1118 ML {*

  1119 fun lift_match_error ctxt fun_str rtrm qtrm =

  1120 let

  1121   val rtrm_str = Syntax.string_of_term ctxt rtrm

  1122   val qtrm_str = Syntax.string_of_term ctxt qtrm

  1123   val msg = [enclose "[" "]" fun_str, "The quotient theorem\n", qtrm_str, 

  1124              "and the lifted theorem\n", rtrm_str, "do not match"]

  1125 in

  1126   error (space_implode " " msg)

  1127 end

  1128 *}

  1129 

  1130 ML {* 

  1131 fun procedure_inst ctxt rtrm qtrm =

  1132 let

  1133   val thy = ProofContext.theory_of ctxt

  1134   val rtrm' = HOLogic.dest_Trueprop rtrm

  1135   val qtrm' = HOLogic.dest_Trueprop qtrm