--- a/Quot/quotient_tacs.ML Wed Jan 13 00:46:31 2010 +0100
+++ b/Quot/quotient_tacs.ML Wed Jan 13 09:19:20 2010 +0100
@@ -1,13 +1,13 @@
signature QUOTIENT_TACS =
sig
- val regularize_tac: Proof.context -> int -> tactic
- val injection_tac: Proof.context -> int -> tactic
- val all_injection_tac: Proof.context -> int -> tactic
- val clean_tac: Proof.context -> int -> tactic
- val procedure_tac: Proof.context -> thm -> int -> tactic
- val lift_tac: Proof.context -> thm -> int -> tactic
- val quotient_tac: Proof.context -> int -> tactic
- val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic
+ val regularize_tac: Proof.context -> int -> tactic
+ val injection_tac: Proof.context -> int -> tactic
+ val all_injection_tac: Proof.context -> int -> tactic
+ val clean_tac: Proof.context -> int -> tactic
+ val procedure_tac: Proof.context -> thm -> int -> tactic
+ val lift_tac: Proof.context -> thm -> int -> tactic
+ val quotient_tac: Proof.context -> int -> tactic
+ val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic
end;
structure Quotient_Tacs: QUOTIENT_TACS =
@@ -16,7 +16,8 @@
open Quotient_Info;
open Quotient_Term;
-(* various helper fuctions *)
+
+(** various helper fuctions **)
(* Since HOL_basic_ss is too "big" for us, we *)
(* need to set up our own minimal simpset. *)
@@ -48,14 +49,14 @@
end
-(*********************)
-(* Regularize Tactic *)
-(*********************)
+
+(*** Regularize Tactic ***)
-(* solvers for equivp and quotient assumptions *)
+(** solvers for equivp and quotient assumptions **)
+
(* FIXME / TODO: should this SOLVES' the goal, like with quotient_tac? *)
(* FIXME / TODO: none of te examples break if added *)
-fun equiv_tac ctxt =
+fun equiv_tac ctxt =
REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt))
fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
@@ -63,13 +64,14 @@
(* FIXME / TODO: test whether DETERM makes any runtime-difference *)
(* FIXME / TODO: reason: the tactic might back-track over the two alternatives in FIRST' *)
-fun quotient_tac ctxt = SOLVES'
+fun quotient_tac ctxt = SOLVES'
(REPEAT_ALL_NEW (FIRST'
[rtac @{thm identity_quotient},
resolve_tac (quotient_rules_get ctxt)]))
fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
-val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
+val quotient_solver =
+ Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
fun solve_quotient_assm ctxt thm =
case Seq.pull (quotient_tac ctxt 1 thm) of
@@ -86,7 +88,7 @@
fun get_match_inst thy pat trm =
let
val univ = Unify.matchers thy [(pat, trm)]
- val SOME (env, _) = Seq.pull univ (* raises BIND, if no unifier *)
+ val SOME (env, _) = Seq.pull univ (* raises BIND, if no unifier *)
val tenv = Vartab.dest (Envir.term_env env)
val tyenv = Vartab.dest (Envir.type_env env)
in
@@ -130,27 +132,22 @@
| _ => NONE
end
-(* 0. preliminary simplification step according to *)
-(* thm ball_reg_eqv bex_reg_eqv babs_reg_eqv *)
-(* ball_reg_eqv_range bex_reg_eqv_range *)
-(* *)
-(* 1. eliminating simple Ball/Bex instances *)
-(* thm ball_reg_right bex_reg_left *)
-(* *)
-(* 2. monos *)
-(* *)
-(* 3. commutation rules for ball and bex *)
-(* thm ball_all_comm bex_ex_comm *)
-(* *)
-(* 4. then rel-equalities, which need to be *)
-(* instantiated with the followig theorem *)
-(* to avoid loops: *)
-(* thm eq_imp_rel *)
-(* *)
-(* 5. then simplification like 0 *)
-(* *)
-(* finally jump back to 1 *)
+(*
+0. preliminary simplification step according to
+ ball_reg_eqv bex_reg_eqv babs_reg_eqv ball_reg_eqv_range bex_reg_eqv_range
+
+1. eliminating simple Ball/Bex instances (ball_reg_right bex_reg_left)
+
+2. monos
+3. commutation rules for ball and bex (ball_all_comm bex_ex_comm)
+
+4. then rel-equalities, which need to be instantiated with 'eq_imp_rel'
+ to avoid loops
+
+5. then simplification like 0
+
+finally jump back to 1 *)
fun regularize_tac ctxt =
let
val thy = ProofContext.theory_of ctxt
@@ -158,7 +155,7 @@
val bex_pat = @{term "Bex (Respects (R1 ===> R2)) P"}
val simproc = Simplifier.simproc_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc))
val simpset = (mk_minimal_ss ctxt)
- addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp} @ (id_simps_get ctxt)
+ addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
addsimprocs [simproc]
addSolver equiv_solver addSolver quotient_solver
val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt)
@@ -173,12 +170,11 @@
end
-(********************)
-(* Injection Tactic *)
-(********************)
+
+(*** Injection Tactic ***)
-(* Looks for Quot_True assumtions, and in case its parameter *)
-(* is an application, it returns the function and the argument. *)
+(* Looks for Quot_True assumtions, and in case its parameter
+ is an application, it returns the function and the argument. *)
fun find_qt_asm asms =
let
fun find_fun trm =
@@ -232,9 +228,9 @@
val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl
-(* We apply apply_rsp only in case if the type needs lifting. *)
-(* This is the case if the type of the data in the Quot_True *)
-(* assumption is different from the corresponding type in the goal. *)
+(* We apply apply_rsp only in case if the type needs lifting.
+ This is the case if the type of the data in the Quot_True
+ assumption is different from the corresponding type in the goal. *)
val apply_rsp_tac =
Subgoal.FOCUS (fn {concl, asms, context,...} =>
let
@@ -243,17 +239,18 @@
in
case (bare_concl, qt_asm) of
(R2 $ (f $ x) $ (g $ y), SOME (qt_fun, qt_arg)) =>
- if (fastype_of qt_fun) = (fastype_of f)
- then no_tac
- else
+ if (fastype_of qt_fun) = (fastype_of f)
+ then no_tac
+ else
let
val ty_x = fastype_of x
val ty_b = fastype_of qt_arg
- val ty_f = range_type (fastype_of f)
+ val ty_f = range_type (fastype_of f)
val thy = ProofContext.theory_of context
val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f]
val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];
- val inst_thm = Drule.instantiate' ty_inst ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp}
+ val inst_thm = Drule.instantiate' ty_inst
+ ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp}
in
(rtac inst_thm THEN' quotient_tac context) 1
end
@@ -281,44 +278,45 @@
(* TODO: Again, can one specify more concretely *)
(* TODO: in terms of R when no_tac should be returned? *)
-fun rep_abs_rsp_tac ctxt =
+fun rep_abs_rsp_tac ctxt =
SUBGOAL (fn (goal, i) =>
- case (bare_concl goal) of
- (rel $ _ $ (rep $ (abs $ _))) =>
- (let
- val thy = ProofContext.theory_of ctxt;
- val (ty_a, ty_b) = dest_fun_type (fastype_of abs);
- val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
- val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep];
- val inst_thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp}
- in
- (rtac inst_thm THEN' quotient_tac ctxt) i
- end
- handle THM _ => no_tac | TYPE _ => no_tac) (* TODO: same here *)
+ case (try bare_concl goal) of
+ SOME (rel $ _ $ (rep $ (abs $ _))) =>
+ let
+ val thy = ProofContext.theory_of ctxt;
+ val (ty_a, ty_b) = dest_fun_type (fastype_of abs);
+ val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
+ in
+ case try (map (SOME o (cterm_of thy))) [rel, abs, rep] of
+ SOME t_inst =>
+ (case try (Drule.instantiate' ty_inst t_inst) @{thm rep_abs_rsp} of
+ SOME inst_thm => (rtac inst_thm THEN' quotient_tac ctxt) i
+ | NONE => no_tac)
+ | NONE => no_tac
+ end
| _ => no_tac)
-(* FIXME / TODO needs to be adapted *)
(*
-To prove that the regularised theorem implies the abs/rep injected,
+To prove that the regularised theorem implies the abs/rep injected,
we try:
- 1) theorems 'trans2' from the appropriate Quot_Type
- 2) remove lambdas from both sides: lambda_rsp_tac
- 3) remove Ball/Bex from the right hand side
- 4) use user-supplied RSP theorems
- 5) remove rep_abs from the right side
- 6) reflexivity of equality
- 7) split applications of lifted type (apply_rsp)
- 8) split applications of non-lifted type (cong_tac)
- 9) apply extentionality
- A) reflexivity of the relation
- B) assumption
+ The deterministic part:
+ -) remove lambdas from both sides
+ -) prove Ball/Bex/Babs equalities using ball_rsp, bex_rsp, babs_rsp
+ -) prove Ball/Bex relations unfolding fun_rel_id
+ -) reflexivity of equality
+ -) prove equality of relations using equals_rsp
+ -) use user-supplied RSP theorems
+ -) solve 'relation of relations' goals using quot_rel_rsp
+ -) remove rep_abs from the right side
(Lambdas under respects may have left us some assumptions)
- C) proving obvious higher order equalities by simplifying fun_rel
- (not sure if it is still needed?)
- D) unfolding lambda on one side
- E) simplifying (= ===> =) for simpler respectfulness
+ Then in order:
+ -) split applications of lifted type (apply_rsp)
+ -) split applications of non-lifted type (cong_tac)
+ -) apply extentionality
+ -) assumption
+ -) reflexivity of the relation
*)
@@ -382,7 +380,7 @@
FIRST' [
injection_match_tac ctxt,
- (* R (t $ ...) (t' $ ...) ----> apply_rsp provided type of t needs lifting *)
+ (* R (t $ ...) (t' $ ...) ----> apply_rsp provided type of t needs lifting *)
apply_rsp_tac ctxt THEN'
RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
@@ -390,13 +388,13 @@
(* merge with previous tactic *)
Cong_Tac.cong_tac @{thm cong} THEN'
RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
-
+
(* (op =) (%x...) (%y...) ----> (op =) (...) (...) *)
rtac @{thm ext} THEN' quot_true_tac ctxt unlam,
-
+
(* resolving with R x y assumptions *)
atac,
-
+
(* reflexivity of the basic relations *)
(* R ... ... *)
resolve_tac rel_refl]
@@ -405,24 +403,21 @@
let
val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt)
in
- simp_tac ((mk_minimal_ss ctxt) addsimps (id_simps_get ctxt)) (* HACK? *)
- THEN' injection_step_tac ctxt rel_refl
+ injection_step_tac ctxt rel_refl
end
fun all_injection_tac ctxt =
REPEAT_ALL_NEW (injection_tac ctxt)
-(***************************)
-(* Cleaning of the Theorem *)
-(***************************)
-(* expands all fun_maps, except in front of the bound *)
-(* variables listed in xs *)
+(** Cleaning of the Theorem **)
+
+(* expands all fun_maps, except in front of the bound variables listed in xs *)
fun fun_map_simple_conv xs ctrm =
case (term_of ctrm) of
((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) =>
- if (member (op=) xs h)
+ if (member (op=) xs h)
then Conv.all_conv ctrm
else Conv.rewr_conv @{thm fun_map.simps[THEN eq_reflection]} ctrm
| _ => Conv.all_conv ctrm
@@ -461,58 +456,52 @@
(f, Abs ("x", T, mk_abs u 0 g))
end
-(* Simplifies a redex using the 'lambda_prs' theorem. *)
-(* First instantiates the types and known subterms. *)
-(* Then solves the quotient assumptions to get Rep2 and Abs1 *)
-(* Finally instantiates the function f using make_inst *)
-(* If Rep2 is an identity then the pattern is simpler and *)
-(* make_inst_id is used *)
+(* Simplifies a redex using the 'lambda_prs' theorem.
+ First instantiates the types and known subterms.
+ Then solves the quotient assumptions to get Rep2 and Abs1
+ Finally instantiates the function f using make_inst
+ If Rep2 is an identity then the pattern is simpler and
+ make_inst_id is used *)
fun lambda_prs_simple_conv ctxt ctrm =
case (term_of ctrm) of
- (Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _) =>
- (let
- val thy = ProofContext.theory_of ctxt
- val (ty_b, ty_a) = dest_fun_type (fastype_of r1)
- val (ty_c, ty_d) = dest_fun_type (fastype_of a2)
- val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]
- val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
- val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
- val te = solve_quotient_assm ctxt (solve_quotient_assm ctxt lpi)
- val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te
- val (insp, inst) =
- if ty_c = ty_d
- then make_inst_id (term_of (Thm.lhs_of ts)) (term_of ctrm)
- else make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm)
- val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
- in
- Conv.rewr_conv ti ctrm
- end
- handle _ => Conv.all_conv ctrm) (* TODO: another catch all - can this be improved? *)
+ (Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _) =>
+ let
+ val thy = ProofContext.theory_of ctxt
+ val (ty_b, ty_a) = dest_fun_type (fastype_of r1)
+ val (ty_c, ty_d) = dest_fun_type (fastype_of a2)
+ val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]
+ val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
+ val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
+ val te = solve_quotient_assm ctxt (solve_quotient_assm ctxt lpi)
+ val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te
+ val (insp, inst) =
+ if ty_c = ty_d
+ then make_inst_id (term_of (Thm.lhs_of ts)) (term_of ctrm)
+ else make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm)
+ val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
+ in
+ Conv.rewr_conv ti ctrm
+ end
| _ => Conv.all_conv ctrm
-
fun lambda_prs_conv ctxt = More_Conv.top_conv lambda_prs_simple_conv ctxt
fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)
-(* 1. folding of definitions and preservation lemmas; *)
-(* and simplification with *)
-(* thm babs_prs all_prs ex_prs *)
-(* *)
-(* 2. unfolding of ---> in front of everything, except *)
-(* bound variables (this prevents lambda_prs from *)
-(* becoming stuck) *)
-(* thm fun_map.simps *)
-(* *)
-(* 3. simplification with *)
-(* thm lambda_prs *)
-(* *)
-(* 4. simplification with *)
-(* thm Quotient_abs_rep Quotient_rel_rep id_simps *)
-(* *)
-(* 5. test for refl *)
+(* Cleaning consists of:
+ 1. folding of definitions and preservation lemmas;
+ and simplification with babs_prs all_prs ex_prs
-fun clean_tac_aux lthy =
+ 2. unfolding of ---> in front of everything, except
+ bound variables
+ (this prevents lambda_prs from becoming stuck)
+
+ 3. simplification with lambda_prs
+
+ 4. simplification with Quotient_abs_rep Quotient_rel_rep id_simps
+
+ 5. test for refl *)
+fun clean_tac lthy =
let
(* FIXME/TODO produce defs with lthy, like prs and ids *)
val thy = ProofContext.theory_of lthy;
@@ -520,24 +509,22 @@
(* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *)
val prs = prs_rules_get lthy
val ids = id_simps_get lthy
-
+
fun mk_simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
val ss1 = mk_simps (defs @ prs @ @{thms babs_prs all_prs ex_prs})
- val ss2 = mk_simps (@{thms Quotient_abs_rep Quotient_rel_rep} @ ids)
+ val ss2 = mk_simps (@{thms Quotient_abs_rep Quotient_rel_rep} @ ids)
in
EVERY' [simp_tac ss1,
fun_map_tac lthy,
lambda_prs_tac lthy,
simp_tac ss2,
- TRY o rtac refl]
+ TRY o rtac refl]
end
-fun clean_tac lthy = REPEAT o CHANGED o (clean_tac_aux lthy) (* HACK?? *)
-(****************************************************)
-(* Tactic for Generalising Free Variables in a Goal *)
-(****************************************************)
+(** Tactic for Generalising Free Variables in a Goal **)
+
fun inst_spec ctrm =
Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}
@@ -552,39 +539,38 @@
HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop
fun gen_frees_tac ctxt =
- SUBGOAL (fn (concl, i) =>
- let
- val thy = ProofContext.theory_of ctxt
- val vrs = Term.add_frees concl []
- val cvrs = map (cterm_of thy o Free) vrs
- val concl' = apply_under_Trueprop (all_list vrs) concl
- val goal = Logic.mk_implies (concl', concl)
- val rule = Goal.prove ctxt [] [] goal
- (K (EVERY1 [inst_spec_tac (rev cvrs), atac]))
- in
- rtac rule i
- end)
+ SUBGOAL (fn (concl, i) =>
+ let
+ val thy = ProofContext.theory_of ctxt
+ val vrs = Term.add_frees concl []
+ val cvrs = map (cterm_of thy o Free) vrs
+ val concl' = apply_under_Trueprop (all_list vrs) concl
+ val goal = Logic.mk_implies (concl', concl)
+ val rule = Goal.prove ctxt [] [] goal
+ (K (EVERY1 [inst_spec_tac (rev cvrs), atac]))
+ in
+ rtac rule i
+ end)
-(**********************************************)
-(* The General Shape of the Lifting Procedure *)
-(**********************************************)
+
+(** The General Shape of the Lifting Procedure **)
-(* - A is the original raw theorem *)
-(* - B is the regularized theorem *)
-(* - C is the rep/abs injected version of B *)
-(* - D is the lifted theorem *)
-(* *)
-(* - 1st prem is the regularization step *)
-(* - 2nd prem is the rep/abs injection step *)
-(* - 3rd prem is the cleaning part *)
-(* *)
-(* the Quot_True premise in 2nd records the lifted theorem *)
+
+(* - A is the original raw theorem
+ - B is the regularized theorem
+ - C is the rep/abs injected version of B
+ - D is the lifted theorem
-val lifting_procedure_thm =
- @{lemma "[|A;
- A --> B;
- Quot_True D ==> B = C;
- C = D|] ==> D"
+ - 1st prem is the regularization step
+ - 2nd prem is the rep/abs injection step
+ - 3rd prem is the cleaning part
+
+ the Quot_True premise in 2nd records the lifted theorem *)
+val lifting_procedure_thm =
+ @{lemma "[|A;
+ A --> B;
+ Quot_True D ==> B = C;
+ C = D|] ==> D"
by (simp add: Quot_True_def)}
fun lift_match_error ctxt str rtrm qtrm =
@@ -592,20 +578,20 @@
val rtrm_str = Syntax.string_of_term ctxt rtrm
val qtrm_str = Syntax.string_of_term ctxt qtrm
val msg = cat_lines [enclose "[" "]" str, "The quotient theorem", qtrm_str,
- "", "does not match with original theorem", rtrm_str]
+ "", "does not match with original theorem", rtrm_str]
in
error msg
end
-
+
fun procedure_inst ctxt rtrm qtrm =
let
val thy = ProofContext.theory_of ctxt
val rtrm' = HOLogic.dest_Trueprop rtrm
val qtrm' = HOLogic.dest_Trueprop qtrm
val reg_goal = regularize_trm_chk ctxt (rtrm', qtrm')
- handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm
+ handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm
val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm')
- handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm
+ handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm
in
Drule.instantiate' []
[SOME (cterm_of thy rtrm'),
--- a/Quot/quotient_term.ML Wed Jan 13 00:46:31 2010 +0100
+++ b/Quot/quotient_term.ML Wed Jan 13 09:19:20 2010 +0100
@@ -1,20 +1,20 @@
signature QUOTIENT_TERM =
sig
- exception LIFT_MATCH of string
-
- datatype flag = absF | repF
-
- val absrep_fun: flag -> Proof.context -> (typ * typ) -> term
- val absrep_fun_chk: flag -> Proof.context -> (typ * typ) -> term
+ exception LIFT_MATCH of string
+
+ datatype flag = absF | repF
+
+ val absrep_fun: flag -> Proof.context -> typ * typ -> term
+ val absrep_fun_chk: flag -> Proof.context -> typ * typ -> term
- val equiv_relation: Proof.context -> (typ * typ) -> term
- val equiv_relation_chk: Proof.context -> (typ * typ) -> term
+ val equiv_relation: Proof.context -> typ * typ -> term
+ val equiv_relation_chk: Proof.context -> typ * typ -> term
- val regularize_trm: Proof.context -> (term * term) -> term
- val regularize_trm_chk: Proof.context -> (term * term) -> term
-
- val inj_repabs_trm: Proof.context -> (term * term) -> term
- val inj_repabs_trm_chk: Proof.context -> (term * term) -> term
+ val regularize_trm: Proof.context -> term * term -> term
+ val regularize_trm_chk: Proof.context -> term * term -> term
+
+ val inj_repabs_trm: Proof.context -> term * term -> term
+ val inj_repabs_trm_chk: Proof.context -> term * term -> term
end;
structure Quotient_Term: QUOTIENT_TERM =
@@ -52,7 +52,7 @@
fun get_mapfun ctxt s =
let
val thy = ProofContext.theory_of ctxt
- val exc = LIFT_MATCH ("No map function for type " ^ (quote s) ^ " found.")
+ val exc = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
val mapfun = #mapfun (maps_lookup thy s) handle NotFound => raise exc
in
Const (mapfun, dummyT)
@@ -89,7 +89,7 @@
fun get_rty_qty ctxt s =
let
val thy = ProofContext.theory_of ctxt
- val exc = LIFT_MATCH ("No quotient type " ^ (quote s) ^ " found.")
+ val exc = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
val qdata = (quotdata_lookup thy s) handle NotFound => raise exc
in
(#rtyp qdata, #qtyp qdata)
@@ -351,14 +351,14 @@
A = B ----> R A B
- or
+ or
A = B ----> (R ===> R) A B
-
+
for more complicated types of A and B
*)
-
+
val mk_babs = Const (@{const_name Babs}, dummyT)
val mk_ball = Const (@{const_name Ball}, dummyT)
val mk_bex = Const (@{const_name Bex}, dummyT)
@@ -375,9 +375,9 @@
| _ => f (trm1, trm2)
(* the major type of All and Ex quantifiers *)
-fun qnt_typ ty = domain_type (domain_type ty)
+fun qnt_typ ty = domain_type (domain_type ty)
-(* produces a regularized version of rtrm
+(* produces a regularized version of rtrm
- the result might contain dummyTs
@@ -487,15 +487,14 @@
|> Syntax.check_term ctxt
-(*********************)
-(* Rep/Abs Injection *)
-(*********************)
+
+(*** Rep/Abs Injection ***)
(*
Injection of Rep/Abs means:
- For abstractions
-:
+ For abstractions:
+
* If the type of the abstraction needs lifting, then we add Rep/Abs
around the abstraction; otherwise we leave it unchanged.
@@ -532,9 +531,8 @@
end
-(* bound variables need to be treated properly, *)
-(* as the type of subterms needs to be calculated *)
-
+(* bound variables need to be treated properly,
+ as the type of subterms needs to be calculated *)
fun inj_repabs_trm ctxt (rtrm, qtrm) =
case (rtrm, qtrm) of
(Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>