442 ML {*

   442 prove t_r: {* mk_REGULARIZE_goal @{context} (prop_of t_a) (term_of glac) *}

   443 fun apply_subt2 f trm trm2 =

   443 

   444   case (trm, trm2) of

   445     (Abs (x, T, t), Abs (x2, T2, t2)) =>

   446        let

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

   448          val (x2', t2') = Term.dest_abs (x2, T2, t2)

   449          val (s1, s2) = f t' t2';

   450        in

   451          (Term.absfree (x', T, s1),

   452           Term.absfree (x2', T2, s2))

   453        end

   454   | _ => f trm trm2

   455 *}

   456 

   457 (*ML_prf {*

   458 val concl = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ()))))

   459 val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP2})

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

   461 val t = Drule.instantiate insts @{thm APPLY_RSP2}

   462 *}*)

   463 

   464 ML {*

   465 fun tyRel2 lthy ty gty =

   466   if ty = gty then HOLogic.eq_const ty else

   467 

   468   case quotdata_lookup lthy (fst (dest_Type gty)) of

   469     SOME quotdata =>

   470       if Sign.typ_instance (ProofContext.theory_of lthy) (ty, #rtyp quotdata) then

   471         case #rel quotdata of

   472           Const(s, _) => Const(s, dummyT)

   473         | _ => error "tyRel2 fail: relation is not a constant"

   474       else error "tyRel2 fail: a non-lifted type lifted to a lifted type"

   475   | NONE => (case (ty, gty) of

   476       (Type (s, tys), Type (s2, tys2)) =>

   477       if s = s2 andalso length tys = length tys2 then

   478         let

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

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

   481           val tys_out = tys_rel ---> ty_out;

   482         in

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

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

   485                               map2 (tyRel2 lthy) tys tys2)

   486         | NONE  => HOLogic.eq_const ty

   487         )

   488         end

   489       else error "tyRel2 fail: different type structures"

   490     | _ => HOLogic.eq_const ty)

   491 *}

   492 

   493 ML mk_babs

   494 

   495 ML {*

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

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

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

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

   500 *}

   501 

   502 

   503 ML {*

   504 fun my_reg2 lthy trm gtrm =

   505   case (trm, gtrm) of

   506     (Abs (x, T, t), Abs (x2, T2, t2)) =>

   507        if not (T = T2) then

   508          let

   509            val rrel = tyRel2 lthy T T2;

   510            val (s1, s2) = apply_subt2 (my_reg2 lthy) trm gtrm

   511          in

   512            (((mk_babs (fastype_of trm) T) $ (mk_resp T $ rrel) $ s1),

   513            ((mk_babs (fastype_of gtrm) T2) $ (mk_resp T2 $ (HOLogic.eq_const dummyT)) $ s2))

   514          end

   515        else

   516          let

   517            val (s1, s2) = apply_subt2 (my_reg2 lthy) t t2

   518          in

   519            (Abs(x, T, s1), Abs(x2, T2, s2))

   520          end

   521   | (Const (@{const_name "All"}, ty) $ (t as Abs (_, T, _)),

   522      Const (@{const_name "All"}, ty') $ (t2 as Abs (_, T2, _))) =>

   523        if not (T = T2) then

   524          let

   525             val ty1 = domain_type ty;

   526             val ty2 = domain_type ty1;

   527             val ty'1 = domain_type ty';

   528             val ty'2 = domain_type ty'1;

   529             val rrel = tyRel2 lthy T T2;

   530             val (s1, s2) = apply_subt2 (my_reg2 lthy) t t2;

   531          in

   532            (((mk_ball ty1) $ (mk_resp ty2 $ rrel) $ s1),

   533            ((mk_ball ty'1) $ (mk_resp ty'2 $ (HOLogic.eq_const dummyT)) $ s2))

   534          end

   535        else

   536          let

   537            val (s1, s2) = apply_subt2 (my_reg2 lthy) t t2

   538          in

   539            ((Const (@{const_name "All"}, ty) $ s1),

   540            (Const (@{const_name "All"}, ty') $ s2))

   541          end

   542   | (Const (@{const_name "Ex"}, ty) $ (t as Abs (_, T, _)),

   543      Const (@{const_name "Ex"}, ty') $ (t2 as Abs (_, T2, _))) =>

   544        if not (T = T2) then

   545          let

   546             val ty1 = domain_type ty

   547             val ty2 = domain_type ty1

   548             val ty'1 = domain_type ty'

   549             val ty'2 = domain_type ty'1

   550             val rrel = tyRel2 lthy T T2

   551             val (s1, s2) = apply_subt2 (my_reg2 lthy) t t2

   552          in

   553            (((mk_bex ty1) $ (mk_resp ty2 $ rrel) $ s1),

   554            ((mk_bex ty'1) $ (mk_resp ty'2 $ (HOLogic.eq_const dummyT)) $ s2))

   555          end

   556        else

   557          let

   558            val (s1, s2) = apply_subt2 (my_reg2 lthy) t t2

   559          in

   560            ((Const (@{const_name "Ex"}, ty) $ s1),

   561            (Const (@{const_name "Ex"}, ty') $ s2))

   562          end

   563   | (Const (@{const_name "op ="}, T) $ t, (Const (@{const_name "op ="}, T2) $ t2)) =>

   564       let

   565         val (s1, s2) = apply_subt2 (my_reg2 lthy) t t2

   566         val rhs = Const (@{const_name "op ="}, T2) $ s2

   567       in

   568         if not (T = T2) then

   569           ((tyRel2 lthy T T2) $ s1, rhs)

   570         else

   571           (Const (@{const_name "op ="}, T) $ s1, rhs)

   572       end

   573   | (t $ t', t2 $ t2') =>

   574       let

   575         val (s1, s2) = apply_subt2 (my_reg2 lthy) t t2

   576         val (s1', s2') = apply_subt2 (my_reg2 lthy) t' t2'

   577       in

   578         (s1 $ s1', s2 $ s2')

   579       end

   580   | (Const c1, Const c2) => (Const c1, Const c2) (* c2 may be lifted *)

   581   | (Bound i, Bound j) => (* Bounds are replaced, so should never happen? *)

   582       if i = j then (Bound i, Bound j) else error "my_reg2: different Bounds"

   583   | (Free (n, T), Free(n2, T2)) => if n = n2 then (Free (n, T), Free (n2, T2))

   584       else error ("my_ref2: different variables: " ^ n ^ ", " ^ n2)

   585   | _ => error "my_reg2: terms don't agree"

   586 *}

   587 

   588 

   589 ML {* prop_of t_a *}

   590 ML {* term_of glac *}

   591 ML {* val (tta, ttb) = (my_reg2 @{context} (prop_of t_a) (term_of glac)) *}

   592 

   593 (* Does not work. *)

   594 ML {* 

   595   prop_of t_a 

   596   |> Syntax.string_of_term @{context}

   597   |> writeln

   598 *}

   599 

   600 ML {* 

   601   (term_of glac) 

   602   |> Syntax.string_of_term @{context}

   603   |> writeln

   604 *}

   605 

   606 ML {* val tta = REGULARIZE_trm @{context} (prop_of t_a) (term_of glac) *} 

   607 

   608 ML {* val tt = Syntax.check_term @{context} tta *}

   609 

   610 

   611 

   612 prove t_r: {* Logic.mk_implies

   613        ((prop_of t_a), tt) *}

   634 ML {* val ttg = Syntax.check_term @{context} ttb *}

   464 ML {* val ttt = mk_inj_REPABS_goal @{context} (prop_of t_r, term_of glac) *}

   635 

   636 ML {*

   637 fun is_lifted_const h gh = is_Const h andalso is_Const gh andalso not (h = gh)

   638 

   639 fun mkrepabs lthy ty gty t =

   640   let

   641     val qenv = distinct (op=) (diff (gty, ty) [])

   642 (*  val _ = sanity_chk qenv lthy *)

   643     val ty = fastype_of t

   644     val abs = get_fun absF qenv lthy gty $ t

   645     val rep = get_fun repF qenv lthy gty $ abs

   646   in

   647     Syntax.check_term lthy rep

   648   end

   649 *}

   650 

   651 ML {*

   652   cterm_of @{theory} (mkrepabs @{context} @{typ "'a list \<Rightarrow> bool"} @{typ "'a fset \<Rightarrow> bool"} @{term "f :: ('a list \<Rightarrow> bool)"})

   653 *}

   654 

   655 

   656 

   657 ML {*

   658 fun build_repabs_term lthy trm gtrm =

   659   case (trm, gtrm) of

   660     (Abs (a as (_, T, _)), Abs (a2 as (_, T2, _))) =>

   661       let

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

   663         val (_,  g) = Term.dest_abs a2;

   664         val v = Free(vs, T);

   665         val t' = lambda v (build_repabs_term lthy t g);

   666         val ty = fastype_of trm;

   667         val gty = fastype_of gtrm;

   668       in

   669         if (ty = gty) then t' else

   670         mkrepabs lthy ty gty (

   671           if (T = T2) then t' else

   672           lambda v (t' $ (mkrepabs lthy T T2 v))

   673         )

   674       end

   675   | _ =>

   676     case (Term.strip_comb trm, Term.strip_comb gtrm) of

   677       ((Const(@{const_name Respects}, _), _), _) => trm

   678     | ((h, tms), (gh, gtms)) =>

   679       let

   680         val ty = fastype_of trm;

   681         val gty = fastype_of gtrm;

   682         val tms' = map2 (build_repabs_term lthy) tms gtms

   683         val t' = list_comb(h, tms')

   684       in

   685         if ty = gty then t' else

   686         if is_lifted_const h gh then mkrepabs lthy ty gty t' else

   687         if (Term.is_Free h) andalso (length tms > 0) then mkrepabs lthy ty gty t' else t'

   688       end

   689 *}

   690 

   691 ML {* val ttt = build_repabs_term @{context} tt ttg *}

   693 prove t_t: {* Logic.mk_equals ((Thm.prop_of t_r), term_of si) *}

   466 prove t_t: {* term_of si *}