nominal2: comparison QuotMain.thy

equal deleted inserted replaced

-:5d06e1dba69a
+:1a0f0b758071
 (* version with explicit qtrm             *)
 (******************************************)
 (******************************************)
 ML {*
+(* builds the relation for respects *)
 fun mk_resp_arg lthy (rty, qty) =
 let
 val thy = ProofContext.theory_of lthy
 in
 case (rty, qty) of
 in
 list_comb (Const (#relfun map_info, dummyT), args)
 end
 else let
 val SOME qinfo = quotdata_lookup_thy thy s'
+(* FIXME: check in this case that the rty and qty *)
+(* FIXME: correspond to each other *)
 in
 #rel qinfo
 end
 | _ => HOLogic.eq_const dummyT
+(* FIXME: do the types correspond to each other? *)
 end
 *}
 ML {*
 val mk_babs = Const (@{const_name "Babs"}, dummyT)
 raise LIFT_MATCH (space_implode " " msg)
 end
 *}
 ML {*
-(* applies f to the subterm of an abstractions, otherwise to the given term *)
+(* - applies f to the subterm of an abstraction,   *)
-(* abstracted variables do not have to be treated specially *)
+(*   otherwise to the given term,                  *)
+(* - used by REGUKARIZE, therefore abstracted      *)
+(*   variables do not have to be treated specially *)
 fun apply_subt f trm1 trm2 =
 case (trm1, trm2) of
 (Abs (x, T, t), Abs (x', T', t')) => Abs (x, T, f t t')
 | _ => f trm1 trm2
+(* the major type of All and Ex quantifiers *)
 fun qnt_typ ty = domain_type (domain_type ty)
 *}
 (*
-Regularizing an rterm means:
+Regularizing an rtrm means:
-- Quantifiers over a type that needs lifting are replaced by
+- quantifiers over a type that needs lifting are replaced by
 bounded quantifiers, for example:
-\<forall>x. P     \<Longrightarrow>     \<forall>x\<in>(Respects R). P
+\<forall>x. P     \<Longrightarrow>     \<forall>x \<in> (Respects R). P  /  All (Respects R) P
-- Abstractions over a type that needs lifting are replaced
+the relation R is given by the rty and qty;
+- abstractions over a type that needs lifting are replaced
 by bounded abstractions:
 \<lambda>x. P     \<Longrightarrow>     Ball (Respects R) (\<lambda>x. P)
-- Equalities over the type being lifted are replaced by
+- equalities over the type being lifted are replaced by
-appropriate relations:
+corresponding relations:
 A = B     \<Longrightarrow>     A \<approx> B
-Example with more complicated types of A, B:
+example with more complicated types of A, B:
 A = B     \<Longrightarrow>     (op = \<Longrightarrow> op \<approx>) A B
 *)
 ML {*
+(* produces a regularized version of rtm      *)
+(* - the result is still not completely typed *)
+(* - does not need any special treatment of   *)
+(*   bound variables                          *)
 fun REGULARIZE_trm lthy rtrm qtrm =
 case (rtrm, qtrm) of
 (Abs (x, ty, t), Abs (x', ty', t')) =>
 let
 val subtrm = REGULARIZE_trm lthy t t'
 end
 | (t1 $ t2, t1' $ t2') =>
 (REGULARIZE_trm lthy t1 t1') $ (REGULARIZE_trm lthy t2 t2')
 | (Free (x, ty), Free (x', ty')) =>
 if x = x'
-then rtrm
+then rtrm     (* FIXME: check whether types corresponds *)
 else trm_lift_error lthy rtrm qtrm
 | (Bound i, Bound i') =>
 if i = i'
 then rtrm
 else trm_lift_error lthy rtrm qtrm
 | _ => trm_lift_error lthy rtrm qtrm
 *}
 ML {*
 fun mk_REGULARIZE_goal lthy rtrm qtrm =
-Logic.mk_implies (rtrm, REGULARIZE_trm lthy rtrm qtrm |> Syntax.check_term lthy)
+Logic.mk_implies (rtrm, Syntax.check_term lthy (REGULARIZE_trm lthy rtrm qtrm))
 *}
 (*
 To prove that the old theorem implies the new one, we first
 atomize it and then try:
 - Reflexivity of the relation
 - Assumption
 - Elimnating quantifiers on both sides of toplevel implication
 - Simplifying implications on both sides of toplevel implication
 - Ball (Respects ?E) ?P = All ?P
 apply(rule a)
 apply(rule b)
 done
 ML {*
+(* FIXME: get_rid of rel_refl rel_eqv *)
 fun REGULARIZE_tac lthy rel_refl rel_eqv =
 (REPEAT1 o FIRST1)
 [rtac rel_refl,
 atac,
 rtac @{thm universal_twice},
 (* For a = b \<longrightarrow> a \<approx> b *)
 rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl,
 rtac @{thm RIGHT_RES_FORALL_REGULAR}]
 *}
-(* same version including debugging information *)
+(* version of REGULARIZE_tac including debugging information *)
 ML {*
 fun my_print_tac ctxt s thm =
 let
 val prems_str = prems_of thm
 |> map (Syntax.string_of_term ctxt)
 fun DT ctxt s tac = EVERY' [tac, K (my_print_tac ctxt ("after " ^ s))]
 *}
 ML {*
-(* FIXME: change rel_refl rel_eqv *)
 fun REGULARIZE_tac' lthy rel_refl rel_eqv =
 (REPEAT1 o FIRST1)
 [(K (print_tac "start")) THEN' (K no_tac),
 DT lthy "1" (rtac rel_refl),
 DT lthy "2" atac,
 ML {*
 fun REGULARIZE_prove rtrm qtrm rel_eqv rel_refl lthy =
 let
 val goal = mk_REGULARIZE_goal lthy rtrm qtrm
-val cthm = Goal.prove lthy [] [] goal
+in
+Goal.prove lthy [] [] goal
 (fn {context, ...} => REGULARIZE_tac' context rel_refl rel_eqv)
-in
-cthm
 end
 *}
 end

changeset 330	1a0f0b758071
parent 326	e755a5da14c8
child 334	5a7024be9083