--- a/src/HOL/Tools/Quotient/quotient_def.ML Fri Jan 07 14:58:15 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Fri Jan 07 15:35:00 2011 +0100
@@ -34,75 +34,75 @@
It stores the qconst_info in the qconsts data slot.
- Restriction: At the moment the left- and right-hand
- side of the definition must be a constant.
+ Restriction: At the moment the left- and right-hand
+ side of the definition must be a constant.
*)
-fun error_msg bind str =
-let
- val name = Binding.name_of bind
- val pos = Position.str_of (Binding.pos_of bind)
-in
- error ("Head of quotient_definition " ^
- quote str ^ " differs from declaration " ^ name ^ pos)
-end
+fun error_msg bind str =
+ let
+ val name = Binding.name_of bind
+ val pos = Position.str_of (Binding.pos_of bind)
+ in
+ error ("Head of quotient_definition " ^
+ quote str ^ " differs from declaration " ^ name ^ pos)
+ end
fun quotient_def ((optbind, mx), (attr, (lhs, rhs))) lthy =
-let
- val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
- val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
- val _ = if is_Const rhs then () else warning "The definiens is not a constant"
-
- fun sanity_test NONE _ = true
- | sanity_test (SOME bind) str =
- if Name.of_binding bind = str then true
- else error_msg bind str
+ let
+ val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
+ val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
+ val _ = if is_Const rhs then () else warning "The definiens is not a constant"
- val _ = sanity_test optbind lhs_str
+ fun sanity_test NONE _ = true
+ | sanity_test (SOME bind) str =
+ if Name.of_binding bind = str then true
+ else error_msg bind str
+
+ val _ = sanity_test optbind lhs_str
- val qconst_bname = Binding.name lhs_str
- val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs
- val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)
- val (_, prop') = Local_Defs.cert_def lthy prop
- val (_, newrhs) = Local_Defs.abs_def prop'
+ val qconst_bname = Binding.name lhs_str
+ val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs
+ val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)
+ val (_, prop') = Local_Defs.cert_def lthy prop
+ val (_, newrhs) = Local_Defs.abs_def prop'
- val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy
+ val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy
- (* data storage *)
- val qconst_data = {qconst = trm, rconst = rhs, def = thm}
+ (* data storage *)
+ val qconst_data = {qconst = trm, rconst = rhs, def = thm}
- fun qcinfo phi = transform_qconsts phi qconst_data
- fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi)
- val lthy'' = Local_Theory.declaration true
- (fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy'
-in
- (qconst_data, lthy'')
-end
+ fun qcinfo phi = transform_qconsts phi qconst_data
+ fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi)
+ val lthy'' = Local_Theory.declaration true
+ (fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy'
+ in
+ (qconst_data, lthy'')
+ end
fun quotdef_cmd (decl, (attr, (lhs_str, rhs_str))) lthy =
-let
- val lhs = Syntax.read_term lthy lhs_str
- val rhs = Syntax.read_term lthy rhs_str
- val lthy' = Variable.declare_term lhs lthy
- val lthy'' = Variable.declare_term rhs lthy'
-in
- quotient_def (decl, (attr, (lhs, rhs))) lthy''
-end
+ let
+ val lhs = Syntax.read_term lthy lhs_str
+ val rhs = Syntax.read_term lthy rhs_str
+ val lthy' = Variable.declare_term lhs lthy
+ val lthy'' = Variable.declare_term rhs lthy'
+ in
+ quotient_def (decl, (attr, (lhs, rhs))) lthy''
+ end
(* a wrapper for automatically lifting a raw constant *)
fun lift_raw_const qtys (qconst_name, rconst, mx) ctxt =
-let
- val rty = fastype_of rconst
- val qty = derive_qtyp ctxt qtys rty
- val lhs = Free (qconst_name, qty)
-in
- quotient_def ((NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt
-end
+ let
+ val rty = fastype_of rconst
+ val qty = derive_qtyp ctxt qtys rty
+ val lhs = Free (qconst_name, qty)
+ in
+ quotient_def ((NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt
+ end
(* parser and command *)
val quotdef_decl = (Parse.binding >> SOME) -- Parse.opt_mixfix' --| Parse.$$$ "where"
val quotdef_parser =
- Scan.optional quotdef_decl (NONE, NoSyn) --
+ Scan.optional quotdef_decl (NONE, NoSyn) --
Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| Parse.$$$ "is" -- Parse.term))
val _ =
--- a/src/HOL/Tools/Quotient/quotient_info.ML Fri Jan 07 14:58:15 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Fri Jan 07 15:35:00 2011 +0100
@@ -68,9 +68,9 @@
Symtab.defined (MapsData.get thy) s
fun maps_lookup thy s =
- case (Symtab.lookup (MapsData.get thy) s) of
+ (case Symtab.lookup (MapsData.get thy) s of
SOME map_fun => map_fun
- | NONE => raise NotFound
+ | NONE => raise NotFound)
fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo))
fun maps_update k minfo = ProofContext.background_theory (maps_update_thy k minfo) (* FIXME *)
@@ -80,17 +80,17 @@
(* attribute to be used in declare statements *)
fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) =
-let
- val thy = ProofContext.theory_of ctxt
- val tyname = Sign.intern_type thy tystr
- val mapname = Sign.intern_const thy mapstr
- val relname = Sign.intern_const thy relstr
+ let
+ val thy = ProofContext.theory_of ctxt
+ val tyname = Sign.intern_type thy tystr
+ val mapname = Sign.intern_const thy mapstr
+ val relname = Sign.intern_const thy relstr
- fun sanity_check s = (Const (s, dummyT) |> Syntax.check_term ctxt; ())
- val _ = List.app sanity_check [mapname, relname]
-in
- maps_attribute_aux tyname {mapfun = mapname, relmap = relname}
-end
+ fun sanity_check s = (Const (s, dummyT) |> Syntax.check_term ctxt; ())
+ val _ = List.app sanity_check [mapname, relname]
+ in
+ maps_attribute_aux tyname {mapfun = mapname, relmap = relname}
+ end
val maps_attr_parser =
Args.context -- Scan.lift
@@ -103,20 +103,20 @@
"declaration of map information"))
fun print_mapsinfo ctxt =
-let
- fun prt_map (ty_name, {mapfun, relmap}) =
- Pretty.block (Library.separate (Pretty.brk 2)
- (map Pretty.str
- ["type:", ty_name,
- "map:", mapfun,
- "relation map:", relmap]))
-in
- MapsData.get (ProofContext.theory_of ctxt)
- |> Symtab.dest
- |> map (prt_map)
- |> Pretty.big_list "maps for type constructors:"
- |> Pretty.writeln
-end
+ let
+ fun prt_map (ty_name, {mapfun, relmap}) =
+ Pretty.block (Library.separate (Pretty.brk 2)
+ (map Pretty.str
+ ["type:", ty_name,
+ "map:", mapfun,
+ "relation map:", relmap]))
+ in
+ MapsData.get (ProofContext.theory_of ctxt)
+ |> Symtab.dest
+ |> map (prt_map)
+ |> Pretty.big_list "maps for type constructors:"
+ |> Pretty.writeln
+ end
(* info about quotient types *)
@@ -150,24 +150,24 @@
map snd (Symtab.dest (QuotData.get (ProofContext.theory_of lthy)))
fun print_quotinfo ctxt =
-let
- fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} =
- Pretty.block (Library.separate (Pretty.brk 2)
- [Pretty.str "quotient type:",
- Syntax.pretty_typ ctxt qtyp,
- Pretty.str "raw type:",
- Syntax.pretty_typ ctxt rtyp,
- Pretty.str "relation:",
- Syntax.pretty_term ctxt equiv_rel,
- Pretty.str "equiv. thm:",
- Syntax.pretty_term ctxt (prop_of equiv_thm)])
-in
- QuotData.get (ProofContext.theory_of ctxt)
- |> Symtab.dest
- |> map (prt_quot o snd)
- |> Pretty.big_list "quotients:"
- |> Pretty.writeln
-end
+ let
+ fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} =
+ Pretty.block (Library.separate (Pretty.brk 2)
+ [Pretty.str "quotient type:",
+ Syntax.pretty_typ ctxt qtyp,
+ Pretty.str "raw type:",
+ Syntax.pretty_typ ctxt rtyp,
+ Pretty.str "relation:",
+ Syntax.pretty_term ctxt equiv_rel,
+ Pretty.str "equiv. thm:",
+ Syntax.pretty_term ctxt (prop_of equiv_thm)])
+ in
+ QuotData.get (ProofContext.theory_of ctxt)
+ |> Symtab.dest
+ |> map (prt_quot o snd)
+ |> Pretty.big_list "quotients:"
+ |> Pretty.writeln
+ end
(* info about quotient constants *)
@@ -207,32 +207,32 @@
name = name' andalso Sign.typ_instance thy (qty, qty')
end
in
- case Symtab.lookup (QConstsData.get thy) name of
+ (case Symtab.lookup (QConstsData.get thy) name of
NONE => raise NotFound
| SOME l =>
- (case (find_first matches l) of
- SOME x => x
- | NONE => raise NotFound)
+ (case find_first matches l of
+ SOME x => x
+ | NONE => raise NotFound))
end
fun print_qconstinfo ctxt =
-let
- fun prt_qconst {qconst, rconst, def} =
- Pretty.block (separate (Pretty.brk 1)
- [Syntax.pretty_term ctxt qconst,
- Pretty.str ":=",
- Syntax.pretty_term ctxt rconst,
- Pretty.str "as",
- Syntax.pretty_term ctxt (prop_of def)])
-in
- QConstsData.get (ProofContext.theory_of ctxt)
- |> Symtab.dest
- |> map snd
- |> flat
- |> map prt_qconst
- |> Pretty.big_list "quotient constants:"
- |> Pretty.writeln
-end
+ let
+ fun prt_qconst {qconst, rconst, def} =
+ Pretty.block (separate (Pretty.brk 1)
+ [Syntax.pretty_term ctxt qconst,
+ Pretty.str ":=",
+ Syntax.pretty_term ctxt rconst,
+ Pretty.str "as",
+ Syntax.pretty_term ctxt (prop_of def)])
+ in
+ QConstsData.get (ProofContext.theory_of ctxt)
+ |> Symtab.dest
+ |> map snd
+ |> flat
+ |> map prt_qconst
+ |> Pretty.big_list "quotient constants:"
+ |> Pretty.writeln
+ end
(* equivalence relation theorems *)
structure EquivRules = Named_Thms
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Fri Jan 07 14:58:15 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Fri Jan 07 15:35:00 2011 +0100
@@ -11,10 +11,10 @@
val injection_tac: Proof.context -> int -> tactic
val all_injection_tac: Proof.context -> int -> tactic
val clean_tac: Proof.context -> int -> tactic
-
+
val descend_procedure_tac: Proof.context -> thm list -> int -> tactic
val descend_tac: Proof.context -> thm list -> int -> tactic
-
+
val lift_procedure_tac: Proof.context -> thm list -> thm -> int -> tactic
val lift_tac: Proof.context -> thm list -> thm list -> int -> tactic
@@ -42,12 +42,12 @@
fun OF1 thm1 thm2 = thm2 RS thm1
fun atomize_thm thm =
-let
- val thm' = Thm.legacy_freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? no! *)
- val thm'' = Object_Logic.atomize (cprop_of thm')
-in
- @{thm equal_elim_rule1} OF [thm'', thm']
-end
+ let
+ val thm' = Thm.legacy_freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? no! *)
+ val thm'' = Object_Logic.atomize (cprop_of thm')
+ in
+ @{thm equal_elim_rule1} OF [thm'', thm']
+ end
@@ -83,14 +83,14 @@
(ctyp_of thy (TVar (x, S)), ctyp_of thy ty)
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 *) (* FIXME fragile *)
- val tenv = Vartab.dest (Envir.term_env env)
- val tyenv = Vartab.dest (Envir.type_env env)
-in
- (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
-end
+ let
+ val univ = Unify.matchers thy [(pat, trm)]
+ val SOME (env, _) = Seq.pull univ (* raises Bind, if no unifier *) (* FIXME fragile *)
+ val tenv = Vartab.dest (Envir.term_env env)
+ val tyenv = Vartab.dest (Envir.type_env env)
+ in
+ (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
+ end
(* Calculates the instantiations for the lemmas:
@@ -101,35 +101,35 @@
theorem applies and return NONE if it doesn't.
*)
fun calculate_inst ctxt ball_bex_thm redex R1 R2 =
-let
- val thy = ProofContext.theory_of ctxt
- fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm))
- val ty_inst = map (SOME o ctyp_of thy) [domain_type (fastype_of R2)]
- val trm_inst = map (SOME o cterm_of thy) [R2, R1]
-in
- case try (Drule.instantiate' ty_inst trm_inst) ball_bex_thm of
- NONE => NONE
- | SOME thm' =>
- (case try (get_match_inst thy (get_lhs thm')) redex of
- NONE => NONE
- | SOME inst2 => try (Drule.instantiate inst2) thm')
-end
+ let
+ val thy = ProofContext.theory_of ctxt
+ fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm))
+ val ty_inst = map (SOME o ctyp_of thy) [domain_type (fastype_of R2)]
+ val trm_inst = map (SOME o cterm_of thy) [R2, R1]
+ in
+ (case try (Drule.instantiate' ty_inst trm_inst) ball_bex_thm of
+ NONE => NONE
+ | SOME thm' =>
+ (case try (get_match_inst thy (get_lhs thm')) redex of
+ NONE => NONE
+ | SOME inst2 => try (Drule.instantiate inst2) thm'))
+ end
fun ball_bex_range_simproc ss redex =
-let
- val ctxt = Simplifier.the_context ss
-in
- case redex of
- (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $
- (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
- calculate_inst ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2
+ let
+ val ctxt = Simplifier.the_context ss
+ in
+ case redex of
+ (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $
+ (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
+ calculate_inst ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2
- | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $
- (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
- calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2
+ | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $
+ (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
+ calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2
- | _ => NONE
-end
+ | _ => NONE
+ end
(* Regularize works as follows:
@@ -159,25 +159,27 @@
fun eq_imp_rel_get ctxt = map (OF1 eq_imp_rel) (equiv_rules_get ctxt)
fun regularize_tac ctxt =
-let
- val thy = ProofContext.theory_of ctxt
- val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"}
- val bex_pat = @{term "Bex (Respects (R1 ===> R2)) P"}
- val simproc = Simplifier.simproc_global_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}
- addsimprocs [simproc]
- addSolver equiv_solver addSolver quotient_solver
- val eq_eqvs = eq_imp_rel_get ctxt
-in
- simp_tac simpset THEN'
- REPEAT_ALL_NEW (CHANGED o FIRST'
- [resolve_tac @{thms ball_reg_right bex_reg_left bex1_bexeq_reg},
- resolve_tac (Inductive.get_monos ctxt),
- resolve_tac @{thms ball_all_comm bex_ex_comm},
- resolve_tac eq_eqvs,
- simp_tac simpset])
-end
+ let
+ val thy = ProofContext.theory_of ctxt
+ val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"}
+ val bex_pat = @{term "Bex (Respects (R1 ===> R2)) P"}
+ val simproc =
+ Simplifier.simproc_global_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}
+ addsimprocs [simproc]
+ addSolver equiv_solver addSolver quotient_solver
+ val eq_eqvs = eq_imp_rel_get ctxt
+ in
+ simp_tac simpset THEN'
+ REPEAT_ALL_NEW (CHANGED o FIRST'
+ [resolve_tac @{thms ball_reg_right bex_reg_left bex1_bexeq_reg},
+ resolve_tac (Inductive.get_monos ctxt),
+ resolve_tac @{thms ball_all_comm bex_ex_comm},
+ resolve_tac eq_eqvs,
+ simp_tac simpset])
+ end
@@ -187,52 +189,52 @@
is an application, it returns the function and the argument.
*)
fun find_qt_asm asms =
-let
- fun find_fun trm =
- case trm of
- (Const(@{const_name Trueprop}, _) $ (Const (@{const_name Quot_True}, _) $ _)) => true
- | _ => false
-in
- case find_first find_fun asms of
- SOME (_ $ (_ $ (f $ a))) => SOME (f, a)
- | _ => NONE
-end
+ let
+ fun find_fun trm =
+ (case trm of
+ (Const (@{const_name Trueprop}, _) $ (Const (@{const_name Quot_True}, _) $ _)) => true
+ | _ => false)
+ in
+ (case find_first find_fun asms of
+ SOME (_ $ (_ $ (f $ a))) => SOME (f, a)
+ | _ => NONE)
+ end
fun quot_true_simple_conv ctxt fnctn ctrm =
- case (term_of ctrm) of
+ case term_of ctrm of
(Const (@{const_name Quot_True}, _) $ x) =>
- let
- val fx = fnctn x;
- val thy = ProofContext.theory_of ctxt;
- val cx = cterm_of thy x;
- val cfx = cterm_of thy fx;
- val cxt = ctyp_of thy (fastype_of x);
- val cfxt = ctyp_of thy (fastype_of fx);
- val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QT_imp}
- in
- Conv.rewr_conv thm ctrm
- end
+ let
+ val fx = fnctn x;
+ val thy = ProofContext.theory_of ctxt;
+ val cx = cterm_of thy x;
+ val cfx = cterm_of thy fx;
+ val cxt = ctyp_of thy (fastype_of x);
+ val cfxt = ctyp_of thy (fastype_of fx);
+ val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QT_imp}
+ in
+ Conv.rewr_conv thm ctrm
+ end
fun quot_true_conv ctxt fnctn ctrm =
- case (term_of ctrm) of
+ (case term_of ctrm of
(Const (@{const_name Quot_True}, _) $ _) =>
quot_true_simple_conv ctxt fnctn ctrm
| _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm
| Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm
- | _ => Conv.all_conv ctrm
+ | _ => Conv.all_conv ctrm)
fun quot_true_tac ctxt fnctn =
- CONVERSION
+ CONVERSION
((Conv.params_conv ~1 (fn ctxt =>
- (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt)
+ (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt)
fun dest_comb (f $ a) = (f, a)
fun dest_bcomb ((_ $ l) $ r) = (l, r)
fun unlam t =
- case t of
- (Abs a) => snd (Term.dest_abs a)
- | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0)))
+ (case t of
+ Abs a => snd (Term.dest_abs a)
+ | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0))))
val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl
@@ -242,53 +244,53 @@
*)
val apply_rsp_tac =
Subgoal.FOCUS (fn {concl, asms, context,...} =>
- let
- val bare_concl = HOLogic.dest_Trueprop (term_of concl)
- val qt_asm = find_qt_asm (map term_of asms)
- 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
- let
- val ty_x = fastype_of x
- val ty_b = fastype_of qt_arg
- 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}
- in
- (rtac inst_thm THEN' SOLVED' (quotient_tac context)) 1
- end
- | _ => no_tac
- end)
+ let
+ val bare_concl = HOLogic.dest_Trueprop (term_of concl)
+ val qt_asm = find_qt_asm (map term_of asms)
+ 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
+ let
+ val ty_x = fastype_of x
+ val ty_b = fastype_of qt_arg
+ 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}
+ in
+ (rtac inst_thm THEN' SOLVED' (quotient_tac context)) 1
+ end
+ | _ => no_tac
+ end)
(* Instantiates and applies 'equals_rsp'. Since the theorem is
complex we rely on instantiation to tell us if it applies
*)
fun equals_rsp_tac R ctxt =
-let
- val thy = ProofContext.theory_of ctxt
-in
- case try (cterm_of thy) R of (* There can be loose bounds in R *)
- SOME ctm =>
- let
- val ty = domain_type (fastype_of R)
- in
- case try (Drule.instantiate' [SOME (ctyp_of thy ty)]
- [SOME (cterm_of thy R)]) @{thm equals_rsp} of
- SOME thm => rtac thm THEN' quotient_tac ctxt
- | NONE => K no_tac
- end
- | _ => K no_tac
-end
+ let
+ val thy = ProofContext.theory_of ctxt
+ in
+ case try (cterm_of thy) R of (* There can be loose bounds in R *)
+ SOME ctm =>
+ let
+ val ty = domain_type (fastype_of R)
+ in
+ case try (Drule.instantiate' [SOME (ctyp_of thy ty)]
+ [SOME (cterm_of thy R)]) @{thm equals_rsp} of
+ SOME thm => rtac thm THEN' quotient_tac ctxt
+ | NONE => K no_tac
+ end
+ | _ => K no_tac
+ end
fun rep_abs_rsp_tac ctxt =
SUBGOAL (fn (goal, i) =>
- case (try bare_concl goal) of
+ (case try bare_concl goal of
SOME (rel $ _ $ (rep $ (Bound _ $ _))) => no_tac
| SOME (rel $ _ $ (rep $ (abs $ _))) =>
let
@@ -303,7 +305,7 @@
| NONE => no_tac)
| NONE => no_tac
end
- | _ => no_tac)
+ | _ => no_tac))
@@ -329,67 +331,66 @@
- reflexivity of the relation
*)
fun injection_match_tac ctxt = SUBGOAL (fn (goal, i) =>
-(case (bare_concl goal) of
- (* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *)
- (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)
- => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
+ (case bare_concl goal of
+ (* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *)
+ (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)
+ => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
- (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *)
-| (Const (@{const_name HOL.eq},_) $
- (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
- (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
- => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
+ (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *)
+ | (Const (@{const_name HOL.eq},_) $
+ (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+ (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
+ => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
- (* (R1 ===> op =) (Ball...) (Ball...) ----> [|R1 x y|] ==> (Ball...x) = (Ball...y) *)
-| (Const (@{const_name fun_rel}, _) $ _ $ _) $
- (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
- (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
- => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
+ (* (R1 ===> op =) (Ball...) (Ball...) ----> [|R1 x y|] ==> (Ball...x) = (Ball...y) *)
+ | (Const (@{const_name fun_rel}, _) $ _ $ _) $
+ (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+ (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
+ => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
- (* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *)
-| Const (@{const_name HOL.eq},_) $
- (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
- (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
- => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
+ (* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *)
+ | Const (@{const_name HOL.eq},_) $
+ (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+ (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
+ => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
- (* (R1 ===> op =) (Bex...) (Bex...) ----> [|R1 x y|] ==> (Bex...x) = (Bex...y) *)
-| (Const (@{const_name fun_rel}, _) $ _ $ _) $
- (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
- (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
- => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
+ (* (R1 ===> op =) (Bex...) (Bex...) ----> [|R1 x y|] ==> (Bex...x) = (Bex...y) *)
+ | (Const (@{const_name fun_rel}, _) $ _ $ _) $
+ (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+ (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
+ => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
-| (Const (@{const_name fun_rel}, _) $ _ $ _) $
- (Const(@{const_name Bex1_rel},_) $ _) $ (Const(@{const_name Bex1_rel},_) $ _)
- => rtac @{thm bex1_rel_rsp} THEN' quotient_tac ctxt
+ | (Const (@{const_name fun_rel}, _) $ _ $ _) $
+ (Const(@{const_name Bex1_rel},_) $ _) $ (Const(@{const_name Bex1_rel},_) $ _)
+ => rtac @{thm bex1_rel_rsp} THEN' quotient_tac ctxt
-| (_ $
- (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
- (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
- => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt]
+ | (_ $
+ (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+ (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
+ => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt]
-| Const (@{const_name HOL.eq},_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
- (rtac @{thm refl} ORELSE'
- (equals_rsp_tac R ctxt THEN' RANGE [
- quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]))
+ | Const (@{const_name HOL.eq},_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
+ (rtac @{thm refl} ORELSE'
+ (equals_rsp_tac R ctxt THEN' RANGE [
+ quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]))
- (* reflexivity of operators arising from Cong_tac *)
-| Const (@{const_name HOL.eq},_) $ _ $ _ => rtac @{thm refl}
+ (* reflexivity of operators arising from Cong_tac *)
+ | Const (@{const_name HOL.eq},_) $ _ $ _ => rtac @{thm refl}
- (* respectfulness of constants; in particular of a simple relation *)
-| _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *)
- => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
+ (* respectfulness of constants; in particular of a simple relation *)
+ | _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *)
+ => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
- (* R (...) (Rep (Abs ...)) ----> R (...) (...) *)
- (* observe map_fun *)
-| _ $ _ $ _
- => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt)
- ORELSE' rep_abs_rsp_tac ctxt
+ (* R (...) (Rep (Abs ...)) ----> R (...) (...) *)
+ (* observe map_fun *)
+ | _ $ _ $ _
+ => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt)
+ ORELSE' rep_abs_rsp_tac ctxt
-| _ => K no_tac
-) i)
+ | _ => K no_tac) i)
fun injection_step_tac ctxt rel_refl =
- FIRST' [
+ FIRST' [
injection_match_tac ctxt,
(* R (t $ ...) (t' $ ...) ----> apply_rsp provided type of t needs lifting *)
@@ -412,11 +413,11 @@
resolve_tac rel_refl]
fun injection_tac ctxt =
-let
- val rel_refl = reflp_get ctxt
-in
- injection_step_tac ctxt rel_refl
-end
+ let
+ val rel_refl = reflp_get ctxt
+ in
+ injection_step_tac ctxt rel_refl
+ end
fun all_injection_tac ctxt =
REPEAT_ALL_NEW (injection_tac ctxt)
@@ -427,46 +428,48 @@
(* expands all map_funs, except in front of the (bound) variables listed in xs *)
fun map_fun_simple_conv xs ctrm =
- case (term_of ctrm) of
+ (case term_of ctrm of
((Const (@{const_name "map_fun"}, _) $ _ $ _) $ h $ _) =>
if member (op=) xs h
then Conv.all_conv ctrm
else Conv.rewr_conv @{thm map_fun_apply [THEN eq_reflection]} ctrm
- | _ => Conv.all_conv ctrm
+ | _ => Conv.all_conv ctrm)
fun map_fun_conv xs ctxt ctrm =
- case (term_of ctrm) of
- _ $ _ => (Conv.comb_conv (map_fun_conv xs ctxt) then_conv
- map_fun_simple_conv xs) ctrm
- | Abs _ => Conv.abs_conv (fn (x, ctxt) => map_fun_conv ((term_of x)::xs) ctxt) ctxt ctrm
- | _ => Conv.all_conv ctrm
+ (case term_of ctrm of
+ _ $ _ =>
+ (Conv.comb_conv (map_fun_conv xs ctxt) then_conv
+ map_fun_simple_conv xs) ctrm
+ | Abs _ => Conv.abs_conv (fn (x, ctxt) => map_fun_conv ((term_of x)::xs) ctxt) ctxt ctrm
+ | _ => Conv.all_conv ctrm)
fun map_fun_tac ctxt = CONVERSION (map_fun_conv [] ctxt)
(* custom matching functions *)
fun mk_abs u i t =
- if incr_boundvars i u aconv t then Bound i else
- case t of
- t1 $ t2 => mk_abs u i t1 $ mk_abs u i t2
- | Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t')
- | Bound j => if i = j then error "make_inst" else t
- | _ => t
+ if incr_boundvars i u aconv t then Bound i
+ else
+ case t of
+ t1 $ t2 => mk_abs u i t1 $ mk_abs u i t2
+ | Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t')
+ | Bound j => if i = j then error "make_inst" else t
+ | _ => t
fun make_inst lhs t =
-let
- val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;
- val _ $ (Abs (_, _, (_ $ g))) = t;
-in
- (f, Abs ("x", T, mk_abs u 0 g))
-end
+ let
+ val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;
+ val _ $ (Abs (_, _, (_ $ g))) = t;
+ in
+ (f, Abs ("x", T, mk_abs u 0 g))
+ end
fun make_inst_id lhs t =
-let
- val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
- val _ $ (Abs (_, _, g)) = t;
-in
- (f, Abs ("x", T, mk_abs u 0 g))
-end
+ let
+ val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
+ val _ $ (Abs (_, _, g)) = t;
+ in
+ (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.
@@ -476,7 +479,7 @@
make_inst_id is used
*)
fun lambda_prs_simple_conv ctxt ctrm =
- case (term_of ctrm) of
+ (case term_of ctrm of
(Const (@{const_name map_fun}, _) $ r1 $ a2) $ (Abs _) =>
let
val thy = ProofContext.theory_of ctxt
@@ -495,7 +498,7 @@
in
Conv.rewr_conv thm4 ctrm
end
- | _ => Conv.all_conv ctrm
+ | _ => Conv.all_conv ctrm)
fun lambda_prs_conv ctxt = Conv.top_conv lambda_prs_simple_conv ctxt
fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)
@@ -523,25 +526,26 @@
4. test for refl
*)
fun clean_tac lthy =
-let
- val defs = map (Thm.symmetric o #def) (qconsts_dest lthy)
- val prs = prs_rules_get lthy
- val ids = id_simps_get lthy
- val thms = @{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs
+ let
+ val defs = map (Thm.symmetric o #def) (qconsts_dest lthy)
+ val prs = prs_rules_get lthy
+ val ids = id_simps_get lthy
+ val thms =
+ @{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs
- val ss = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
-in
- EVERY' [map_fun_tac lthy,
- lambda_prs_tac lthy,
- simp_tac ss,
- TRY o rtac refl]
-end
+ val ss = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
+ in
+ EVERY' [map_fun_tac lthy,
+ lambda_prs_tac lthy,
+ simp_tac ss,
+ TRY o rtac refl]
+ end
(* Tactic for Generalising Free Variables in a Goal *)
fun inst_spec ctrm =
- Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}
+ Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}
fun inst_spec_tac ctrms =
EVERY' (map (dtac o inst_spec) ctrms)
@@ -588,31 +592,31 @@
by (simp add: Quot_True_def)}
fun lift_match_error ctxt msg rtrm qtrm =
-let
- val rtrm_str = Syntax.string_of_term ctxt rtrm
- val qtrm_str = Syntax.string_of_term ctxt qtrm
- val msg = cat_lines [enclose "[" "]" msg, "The quotient theorem", qtrm_str,
- "", "does not match with original theorem", rtrm_str]
-in
- error msg
-end
+ let
+ val rtrm_str = Syntax.string_of_term ctxt rtrm
+ val qtrm_str = Syntax.string_of_term ctxt qtrm
+ val msg = cat_lines [enclose "[" "]" msg, "The quotient theorem", qtrm_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 msg => lift_match_error ctxt msg rtrm qtrm
- val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm')
- handle LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
-in
- Drule.instantiate' []
- [SOME (cterm_of thy rtrm'),
- SOME (cterm_of thy reg_goal),
- NONE,
- SOME (cterm_of thy inj_goal)] lifting_procedure_thm
-end
+ 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 msg => lift_match_error ctxt msg rtrm qtrm
+ val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm')
+ handle LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
+ in
+ Drule.instantiate' []
+ [SOME (cterm_of thy rtrm'),
+ SOME (cterm_of thy reg_goal),
+ NONE,
+ SOME (cterm_of thy inj_goal)] lifting_procedure_thm
+ end
(* Since we use Ball and Bex during the lifting and descending,
@@ -625,34 +629,34 @@
(** descending as tactic **)
fun descend_procedure_tac ctxt simps =
-let
- val ss = (mk_minimal_ss ctxt) addsimps (simps @ default_unfolds)
-in
- full_simp_tac ss
- THEN' Object_Logic.full_atomize_tac
- THEN' gen_frees_tac ctxt
- THEN' SUBGOAL (fn (goal, i) =>
- let
- val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt)
- val rtrm = derive_rtrm ctxt qtys goal
- val rule = procedure_inst ctxt rtrm goal
- in
- rtac rule i
- end)
-end
+ let
+ val ss = (mk_minimal_ss ctxt) addsimps (simps @ default_unfolds)
+ in
+ full_simp_tac ss
+ THEN' Object_Logic.full_atomize_tac
+ THEN' gen_frees_tac ctxt
+ THEN' SUBGOAL (fn (goal, i) =>
+ let
+ val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt)
+ val rtrm = derive_rtrm ctxt qtys goal
+ val rule = procedure_inst ctxt rtrm goal
+ in
+ rtac rule i
+ end)
+ end
fun descend_tac ctxt simps =
-let
- val mk_tac_raw =
- descend_procedure_tac ctxt simps
- THEN' RANGE
- [Object_Logic.rulify_tac THEN' (K all_tac),
- regularize_tac ctxt,
- all_injection_tac ctxt,
- clean_tac ctxt]
-in
- Goal.conjunction_tac THEN_ALL_NEW mk_tac_raw
-end
+ let
+ val mk_tac_raw =
+ descend_procedure_tac ctxt simps
+ THEN' RANGE
+ [Object_Logic.rulify_tac THEN' (K all_tac),
+ regularize_tac ctxt,
+ all_injection_tac ctxt,
+ clean_tac ctxt]
+ in
+ Goal.conjunction_tac THEN_ALL_NEW mk_tac_raw
+ end
(** lifting as a tactic **)
@@ -660,29 +664,29 @@
(* the tactic leaves three subgoals to be proved *)
fun lift_procedure_tac ctxt simps rthm =
-let
- val ss = (mk_minimal_ss ctxt) addsimps (simps @ default_unfolds)
-in
- full_simp_tac ss
- THEN' Object_Logic.full_atomize_tac
- THEN' gen_frees_tac ctxt
- THEN' SUBGOAL (fn (goal, i) =>
- let
- (* full_atomize_tac contracts eta redexes,
- so we do it also in the original theorem *)
- val rthm' =
- rthm |> full_simplify ss
- |> Drule.eta_contraction_rule
- |> Thm.forall_intr_frees
- |> atomize_thm
+ let
+ val ss = (mk_minimal_ss ctxt) addsimps (simps @ default_unfolds)
+ in
+ full_simp_tac ss
+ THEN' Object_Logic.full_atomize_tac
+ THEN' gen_frees_tac ctxt
+ THEN' SUBGOAL (fn (goal, i) =>
+ let
+ (* full_atomize_tac contracts eta redexes,
+ so we do it also in the original theorem *)
+ val rthm' =
+ rthm |> full_simplify ss
+ |> Drule.eta_contraction_rule
+ |> Thm.forall_intr_frees
+ |> atomize_thm
- val rule = procedure_inst ctxt (prop_of rthm') goal
- in
- (rtac rule THEN' rtac rthm') i
- end)
-end
+ val rule = procedure_inst ctxt (prop_of rthm') goal
+ in
+ (rtac rule THEN' rtac rthm') i
+ end)
+ end
-fun lift_single_tac ctxt simps rthm =
+fun lift_single_tac ctxt simps rthm =
lift_procedure_tac ctxt simps rthm
THEN' RANGE
[ regularize_tac ctxt,
@@ -690,26 +694,26 @@
clean_tac ctxt ]
fun lift_tac ctxt simps rthms =
- Goal.conjunction_tac
+ Goal.conjunction_tac
THEN' RANGE (map (lift_single_tac ctxt simps) rthms)
(* automated lifting with pre-simplification of the theorems;
for internal usage *)
fun lifted ctxt qtys simps rthm =
-let
- val ((_, [rthm']), ctxt') = Variable.import true [rthm] ctxt
- val goal = derive_qtrm ctxt' qtys (prop_of rthm')
-in
- Goal.prove ctxt' [] [] goal
- (K (HEADGOAL (lift_single_tac ctxt' simps rthm')))
- |> singleton (ProofContext.export ctxt' ctxt)
-end
+ let
+ val ((_, [rthm']), ctxt') = Variable.import true [rthm] ctxt
+ val goal = derive_qtrm ctxt' qtys (prop_of rthm')
+ in
+ Goal.prove ctxt' [] [] goal
+ (K (HEADGOAL (lift_single_tac ctxt' simps rthm')))
+ |> singleton (ProofContext.export ctxt' ctxt)
+ end
(* lifting as an attribute *)
-val lifted_attrib = Thm.rule_attribute (fn context =>
+val lifted_attrib = Thm.rule_attribute (fn context =>
let
val ctxt = Context.proof_of context
val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt)
--- a/src/HOL/Tools/Quotient/quotient_term.ML Fri Jan 07 14:58:15 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Fri Jan 07 15:35:00 2011 +0100
@@ -65,13 +65,13 @@
| RepF => Const (@{const_name comp}, dummyT) $ trm2 $ trm1
fun get_mapfun ctxt s =
-let
- val thy = ProofContext.theory_of ctxt
- val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound =>
- raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
-in
- Const (mapfun, dummyT)
-end
+ let
+ val thy = ProofContext.theory_of ctxt
+ val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound =>
+ raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
+ in
+ Const (mapfun, dummyT)
+ end
(* makes a Free out of a TVar *)
fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT)
@@ -85,74 +85,74 @@
it produces: %a b. prod_map (map a) b
*)
fun mk_mapfun ctxt vs rty =
-let
- val vs' = map mk_Free vs
+ let
+ val vs' = map mk_Free vs
- fun mk_mapfun_aux rty =
- case rty of
- TVar _ => mk_Free rty
- | Type (_, []) => mk_identity rty
- | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys)
- | _ => raise LIFT_MATCH "mk_mapfun (default)"
-in
- fold_rev Term.lambda vs' (mk_mapfun_aux rty)
-end
+ fun mk_mapfun_aux rty =
+ case rty of
+ TVar _ => mk_Free rty
+ | Type (_, []) => mk_identity rty
+ | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys)
+ | _ => raise LIFT_MATCH "mk_mapfun (default)"
+ in
+ fold_rev Term.lambda vs' (mk_mapfun_aux rty)
+ end
(* looks up the (varified) rty and qty for
a quotient definition
*)
fun get_rty_qty ctxt s =
-let
- val thy = ProofContext.theory_of ctxt
- val qdata = quotdata_lookup thy s handle Quotient_Info.NotFound =>
- raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
-in
- (#rtyp qdata, #qtyp qdata)
-end
+ let
+ val thy = ProofContext.theory_of ctxt
+ val qdata = quotdata_lookup thy s handle Quotient_Info.NotFound =>
+ raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
+ in
+ (#rtyp qdata, #qtyp qdata)
+ end
(* takes two type-environments and looks
up in both of them the variable v, which
must be listed in the environment
*)
fun double_lookup rtyenv qtyenv v =
-let
- val v' = fst (dest_TVar v)
-in
- (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v')))
-end
+ let
+ val v' = fst (dest_TVar v)
+ in
+ (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v')))
+ end
(* matches a type pattern with a type *)
fun match ctxt err ty_pat ty =
-let
- val thy = ProofContext.theory_of ctxt
-in
- Sign.typ_match thy (ty_pat, ty) Vartab.empty
- handle Type.TYPE_MATCH => err ctxt ty_pat ty
-end
+ let
+ val thy = ProofContext.theory_of ctxt
+ in
+ Sign.typ_match thy (ty_pat, ty) Vartab.empty
+ handle Type.TYPE_MATCH => err ctxt ty_pat ty
+ end
(* produces the rep or abs constant for a qty *)
fun absrep_const flag ctxt qty_str =
-let
- val qty_name = Long_Name.base_name qty_str
- val qualifier = Long_Name.qualifier qty_str
-in
- case flag of
- AbsF => Const (Long_Name.qualify qualifier ("abs_" ^ qty_name), dummyT)
- | RepF => Const (Long_Name.qualify qualifier ("rep_" ^ qty_name), dummyT)
-end
+ let
+ val qty_name = Long_Name.base_name qty_str
+ val qualifier = Long_Name.qualifier qty_str
+ in
+ case flag of
+ AbsF => Const (Long_Name.qualify qualifier ("abs_" ^ qty_name), dummyT)
+ | RepF => Const (Long_Name.qualify qualifier ("rep_" ^ qty_name), dummyT)
+ end
(* Lets Nitpick represent elements of quotient types as elements of the raw type *)
fun absrep_const_chk flag ctxt qty_str =
Syntax.check_term ctxt (absrep_const flag ctxt qty_str)
fun absrep_match_err ctxt ty_pat ty =
-let
- val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
- val ty_str = Syntax.string_of_typ ctxt ty
-in
- raise LIFT_MATCH (space_implode " "
- ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
-end
+ let
+ val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
+ val ty_str = Syntax.string_of_typ ctxt ty
+ in
+ raise LIFT_MATCH (space_implode " "
+ ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
+ end
(** generation of an aggregate absrep function **)
@@ -213,29 +213,29 @@
| (Type (s, tys), Type (s', tys')) =>
if s = s'
then
- let
- val args = map (absrep_fun flag ctxt) (tys ~~ tys')
- in
- list_comb (get_mapfun ctxt s, args)
- end
+ let
+ val args = map (absrep_fun flag ctxt) (tys ~~ tys')
+ in
+ list_comb (get_mapfun ctxt s, args)
+ end
else
- let
- val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
- val rtyenv = match ctxt absrep_match_err rty_pat rty
- val qtyenv = match ctxt absrep_match_err qty_pat qty
- val args_aux = map (double_lookup rtyenv qtyenv) vs
- val args = map (absrep_fun flag ctxt) args_aux
- in
- if forall is_identity args
- then absrep_const flag ctxt s'
- else
- let
- val map_fun = mk_mapfun ctxt vs rty_pat
- val result = list_comb (map_fun, args)
- in
- mk_fun_compose flag (absrep_const flag ctxt s', result)
- end
- end
+ let
+ val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
+ val rtyenv = match ctxt absrep_match_err rty_pat rty
+ val qtyenv = match ctxt absrep_match_err qty_pat qty
+ val args_aux = map (double_lookup rtyenv qtyenv) vs
+ val args = map (absrep_fun flag ctxt) args_aux
+ in
+ if forall is_identity args
+ then absrep_const flag ctxt s'
+ else
+ let
+ val map_fun = mk_mapfun ctxt vs rty_pat
+ val result = list_comb (map_fun, args)
+ in
+ mk_fun_compose flag (absrep_const flag ctxt s', result)
+ end
+ end
| (TFree x, TFree x') =>
if x = x'
then mk_identity rty
@@ -259,13 +259,13 @@
(* instantiates TVars so that the term is of type ty *)
fun force_typ ctxt trm ty =
-let
- val thy = ProofContext.theory_of ctxt
- val trm_ty = fastype_of trm
- val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty
-in
- map_types (Envir.subst_type ty_inst) trm
-end
+ let
+ val thy = ProofContext.theory_of ctxt
+ val trm_ty = fastype_of trm
+ val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty
+ in
+ map_types (Envir.subst_type ty_inst) trm
+ end
fun is_eq (Const (@{const_name HOL.eq}, _)) = true
| is_eq _ = false
@@ -274,44 +274,44 @@
Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2
fun get_relmap ctxt s =
-let
- val thy = ProofContext.theory_of ctxt
- val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound =>
- raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
-in
- Const (relmap, dummyT)
-end
+ let
+ val thy = ProofContext.theory_of ctxt
+ val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound =>
+ raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
+ in
+ Const (relmap, dummyT)
+ end
fun mk_relmap ctxt vs rty =
-let
- val vs' = map (mk_Free) vs
+ let
+ val vs' = map (mk_Free) vs
- fun mk_relmap_aux rty =
- case rty of
- TVar _ => mk_Free rty
- | Type (_, []) => HOLogic.eq_const rty
- | Type (s, tys) => list_comb (get_relmap ctxt s, map mk_relmap_aux tys)
- | _ => raise LIFT_MATCH ("mk_relmap (default)")
-in
- fold_rev Term.lambda vs' (mk_relmap_aux rty)
-end
+ fun mk_relmap_aux rty =
+ case rty of
+ TVar _ => mk_Free rty
+ | Type (_, []) => HOLogic.eq_const rty
+ | Type (s, tys) => list_comb (get_relmap ctxt s, map mk_relmap_aux tys)
+ | _ => raise LIFT_MATCH ("mk_relmap (default)")
+ in
+ fold_rev Term.lambda vs' (mk_relmap_aux rty)
+ end
fun get_equiv_rel ctxt s =
-let
- val thy = ProofContext.theory_of ctxt
-in
- #equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound =>
- raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
-end
+ let
+ val thy = ProofContext.theory_of ctxt
+ in
+ #equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound =>
+ raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
+ end
fun equiv_match_err ctxt ty_pat ty =
-let
- val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
- val ty_str = Syntax.string_of_typ ctxt ty
-in
- raise LIFT_MATCH (space_implode " "
- ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
-end
+ let
+ val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
+ val ty_str = Syntax.string_of_typ ctxt ty
+ in
+ raise LIFT_MATCH (space_implode " "
+ ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
+ end
(* builds the aggregate equivalence relation
that will be the argument of Respects
@@ -322,34 +322,34 @@
else
case (rty, qty) of
(Type (s, tys), Type (s', tys')) =>
- if s = s'
- then
- let
- val args = map (equiv_relation ctxt) (tys ~~ tys')
- in
- list_comb (get_relmap ctxt s, args)
- end
- else
- let
- val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
- val rtyenv = match ctxt equiv_match_err rty_pat rty
- val qtyenv = match ctxt equiv_match_err qty_pat qty
- val args_aux = map (double_lookup rtyenv qtyenv) vs
- val args = map (equiv_relation ctxt) args_aux
- val eqv_rel = get_equiv_rel ctxt s'
- val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
- in
- if forall is_eq args
- then eqv_rel'
- else
- let
- val rel_map = mk_relmap ctxt vs rty_pat
- val result = list_comb (rel_map, args)
- in
- mk_rel_compose (result, eqv_rel')
- end
- end
- | _ => HOLogic.eq_const rty
+ if s = s'
+ then
+ let
+ val args = map (equiv_relation ctxt) (tys ~~ tys')
+ in
+ list_comb (get_relmap ctxt s, args)
+ end
+ else
+ let
+ val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
+ val rtyenv = match ctxt equiv_match_err rty_pat rty
+ val qtyenv = match ctxt equiv_match_err qty_pat qty
+ val args_aux = map (double_lookup rtyenv qtyenv) vs
+ val args = map (equiv_relation ctxt) args_aux
+ val eqv_rel = get_equiv_rel ctxt s'
+ val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
+ in
+ if forall is_eq args
+ then eqv_rel'
+ else
+ let
+ val rel_map = mk_relmap ctxt vs rty_pat
+ val result = list_comb (rel_map, args)
+ in
+ mk_rel_compose (result, eqv_rel')
+ end
+ end
+ | _ => HOLogic.eq_const rty
fun equiv_relation_chk ctxt (rty, qty) =
equiv_relation ctxt (rty, qty)
@@ -414,14 +414,14 @@
| _ => f (trm1, trm2)
fun term_mismatch str ctxt t1 t2 =
-let
- val t1_str = Syntax.string_of_term ctxt t1
- val t2_str = Syntax.string_of_term ctxt t2
- val t1_ty_str = Syntax.string_of_typ ctxt (fastype_of t1)
- val t2_ty_str = Syntax.string_of_typ ctxt (fastype_of t2)
-in
- raise LIFT_MATCH (cat_lines [str, t1_str ^ "::" ^ t1_ty_str, t2_str ^ "::" ^ t2_ty_str])
-end
+ let
+ val t1_str = Syntax.string_of_term ctxt t1
+ val t2_str = Syntax.string_of_term ctxt t2
+ val t1_ty_str = Syntax.string_of_typ ctxt (fastype_of t1)
+ val t2_ty_str = Syntax.string_of_typ ctxt (fastype_of t2)
+ in
+ raise LIFT_MATCH (cat_lines [str, t1_str ^ "::" ^ t1_ty_str, t2_str ^ "::" ^ t2_ty_str])
+ end
(* the major type of All and Ex quantifiers *)
fun qnt_typ ty = domain_type (domain_type ty)
@@ -429,17 +429,18 @@
(* Checks that two types match, for example:
rty -> rty matches qty -> qty *)
fun matches_typ thy rT qT =
- if rT = qT then true else
- case (rT, qT) of
- (Type (rs, rtys), Type (qs, qtys)) =>
- if rs = qs then
- if length rtys <> length qtys then false else
- forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys)
- else
- (case quotdata_lookup_raw thy qs of
- SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo)
- | NONE => false)
- | _ => false
+ if rT = qT then true
+ else
+ (case (rT, qT) of
+ (Type (rs, rtys), Type (qs, qtys)) =>
+ if rs = qs then
+ if length rtys <> length qtys then false
+ else forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys)
+ else
+ (case quotdata_lookup_raw thy qs of
+ SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo)
+ | NONE => false)
+ | _ => false)
(* produces a regularized version of rtrm
@@ -452,124 +453,124 @@
fun regularize_trm ctxt (rtrm, qtrm) =
case (rtrm, qtrm) of
(Abs (x, ty, t), Abs (_, ty', t')) =>
- let
- val subtrm = Abs(x, ty, regularize_trm ctxt (t, t'))
- in
- if ty = ty' then subtrm
- else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm
- end
+ let
+ val subtrm = Abs(x, ty, regularize_trm ctxt (t, t'))
+ in
+ if ty = ty' then subtrm
+ else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm
+ end
| (Const (@{const_name Babs}, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) =>
- let
- val subtrm = regularize_trm ctxt (t, t')
- val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty')
- in
- if resrel <> needres
- then term_mismatch "regularize (Babs)" ctxt resrel needres
- else mk_babs $ resrel $ subtrm
- end
+ let
+ val subtrm = regularize_trm ctxt (t, t')
+ val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty')
+ in
+ if resrel <> needres
+ then term_mismatch "regularize (Babs)" ctxt resrel needres
+ else mk_babs $ resrel $ subtrm
+ end
| (Const (@{const_name All}, ty) $ t, Const (@{const_name All}, ty') $ t') =>
- let
- val subtrm = apply_subt (regularize_trm ctxt) (t, t')
- in
- if ty = ty' then Const (@{const_name All}, ty) $ subtrm
- else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
- end
+ let
+ val subtrm = apply_subt (regularize_trm ctxt) (t, t')
+ in
+ if ty = ty' then Const (@{const_name All}, ty) $ subtrm
+ else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
+ end
| (Const (@{const_name Ex}, ty) $ t, Const (@{const_name Ex}, ty') $ t') =>
- let
- val subtrm = apply_subt (regularize_trm ctxt) (t, t')
- in
- if ty = ty' then Const (@{const_name Ex}, ty) $ subtrm
- else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
- end
+ let
+ val subtrm = apply_subt (regularize_trm ctxt) (t, t')
+ in
+ if ty = ty' then Const (@{const_name Ex}, ty) $ subtrm
+ else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
+ end
| (Const (@{const_name Ex1}, ty) $ (Abs (_, _,
(Const (@{const_name HOL.conj}, _) $ (Const (@{const_name Set.member}, _) $ _ $
(Const (@{const_name Respects}, _) $ resrel)) $ (t $ _)))),
Const (@{const_name Ex1}, ty') $ t') =>
- let
- val t_ = incr_boundvars (~1) t
- val subtrm = apply_subt (regularize_trm ctxt) (t_, t')
- val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
- in
- if resrel <> needrel
- then term_mismatch "regularize (Bex1)" ctxt resrel needrel
- else mk_bex1_rel $ resrel $ subtrm
- end
+ let
+ val t_ = incr_boundvars (~1) t
+ val subtrm = apply_subt (regularize_trm ctxt) (t_, t')
+ val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
+ in
+ if resrel <> needrel
+ then term_mismatch "regularize (Bex1)" ctxt resrel needrel
+ else mk_bex1_rel $ resrel $ subtrm
+ end
| (Const (@{const_name Ex1}, ty) $ t, Const (@{const_name Ex1}, ty') $ t') =>
- let
- val subtrm = apply_subt (regularize_trm ctxt) (t, t')
- in
- if ty = ty' then Const (@{const_name Ex1}, ty) $ subtrm
- else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
- end
+ let
+ val subtrm = apply_subt (regularize_trm ctxt) (t, t')
+ in
+ if ty = ty' then Const (@{const_name Ex1}, ty) $ subtrm
+ else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
+ end
| (Const (@{const_name Ball}, ty) $ (Const (@{const_name Respects}, _) $ resrel) $ t,
Const (@{const_name All}, ty') $ t') =>
- let
- val subtrm = apply_subt (regularize_trm ctxt) (t, t')
- val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
- in
- if resrel <> needrel
- then term_mismatch "regularize (Ball)" ctxt resrel needrel
- else mk_ball $ (mk_resp $ resrel) $ subtrm
- end
+ let
+ val subtrm = apply_subt (regularize_trm ctxt) (t, t')
+ val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
+ in
+ if resrel <> needrel
+ then term_mismatch "regularize (Ball)" ctxt resrel needrel
+ else mk_ball $ (mk_resp $ resrel) $ subtrm
+ end
| (Const (@{const_name Bex}, ty) $ (Const (@{const_name Respects}, _) $ resrel) $ t,
Const (@{const_name Ex}, ty') $ t') =>
- let
- val subtrm = apply_subt (regularize_trm ctxt) (t, t')
- val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
- in
- if resrel <> needrel
- then term_mismatch "regularize (Bex)" ctxt resrel needrel
- else mk_bex $ (mk_resp $ resrel) $ subtrm
- end
+ let
+ val subtrm = apply_subt (regularize_trm ctxt) (t, t')
+ val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
+ in
+ if resrel <> needrel
+ then term_mismatch "regularize (Bex)" ctxt resrel needrel
+ else mk_bex $ (mk_resp $ resrel) $ subtrm
+ end
| (Const (@{const_name Bex1_rel}, ty) $ resrel $ t, Const (@{const_name Ex1}, ty') $ t') =>
- let
- val subtrm = apply_subt (regularize_trm ctxt) (t, t')
- val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
- in
- if resrel <> needrel
- then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel
- else mk_bex1_rel $ resrel $ subtrm
- end
+ let
+ val subtrm = apply_subt (regularize_trm ctxt) (t, t')
+ val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
+ in
+ if resrel <> needrel
+ then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel
+ else mk_bex1_rel $ resrel $ subtrm
+ end
| (* equalities need to be replaced by appropriate equivalence relations *)
(Const (@{const_name HOL.eq}, ty), Const (@{const_name HOL.eq}, ty')) =>
- if ty = ty' then rtrm
- else equiv_relation ctxt (domain_type ty, domain_type ty')
+ if ty = ty' then rtrm
+ else equiv_relation ctxt (domain_type ty, domain_type ty')
| (* in this case we just check whether the given equivalence relation is correct *)
(rel, Const (@{const_name HOL.eq}, ty')) =>
- let
- val rel_ty = fastype_of rel
- val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty')
- in
- if rel' aconv rel then rtrm
- else term_mismatch "regularize (relation mismatch)" ctxt rel rel'
- end
+ let
+ val rel_ty = fastype_of rel
+ val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty')
+ in
+ if rel' aconv rel then rtrm
+ else term_mismatch "regularize (relation mismatch)" ctxt rel rel'
+ end
| (_, Const _) =>
- let
- val thy = ProofContext.theory_of ctxt
- fun same_const (Const (s, T)) (Const (s', T')) = (s = s') andalso matches_typ thy T T'
- | same_const _ _ = false
- in
- if same_const rtrm qtrm then rtrm
- else
- let
- val rtrm' = #rconst (qconsts_lookup thy qtrm)
- handle Quotient_Info.NotFound =>
+ let
+ val thy = ProofContext.theory_of ctxt
+ fun same_const (Const (s, T)) (Const (s', T')) = (s = s') andalso matches_typ thy T T'
+ | same_const _ _ = false
+ in
+ if same_const rtrm qtrm then rtrm
+ else
+ let
+ val rtrm' = #rconst (qconsts_lookup thy qtrm)
+ handle Quotient_Info.NotFound =>
term_mismatch "regularize (constant not found)" ctxt rtrm qtrm
- in
- if Pattern.matches thy (rtrm', rtrm)
- then rtrm else term_mismatch "regularize (constant mismatch)" ctxt rtrm qtrm
- end
- end
+ in
+ if Pattern.matches thy (rtrm', rtrm)
+ then rtrm else term_mismatch "regularize (constant mismatch)" ctxt rtrm qtrm
+ end
+ end
| (((t1 as Const (@{const_name prod_case}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
((t2 as Const (@{const_name prod_case}, _)) $ Abs (v2, _ , Abs(v2', _ , s2)))) =>
@@ -583,16 +584,16 @@
regularize_trm ctxt (t1, t1') $ regularize_trm ctxt (t2, t2')
| (Bound i, Bound i') =>
- if i = i' then rtrm
- else raise (LIFT_MATCH "regularize (bounds mismatch)")
+ if i = i' then rtrm
+ else raise (LIFT_MATCH "regularize (bounds mismatch)")
| _ =>
- let
- val rtrm_str = Syntax.string_of_term ctxt rtrm
- val qtrm_str = Syntax.string_of_term ctxt qtrm
- in
- raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")"))
- end
+ let
+ val rtrm_str = Syntax.string_of_term ctxt rtrm
+ val qtrm_str = Syntax.string_of_term ctxt qtrm
+ in
+ raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")"))
+ end
fun regularize_trm_chk ctxt (rtrm, qtrm) =
regularize_trm ctxt (rtrm, qtrm)
@@ -635,12 +636,12 @@
absrep_fun RepF ctxt (T, T') $ (absrep_fun AbsF ctxt (T, T') $ trm)
fun inj_repabs_err ctxt msg rtrm qtrm =
-let
- val rtrm_str = Syntax.string_of_term ctxt rtrm
- val qtrm_str = Syntax.string_of_term ctxt qtrm
-in
- raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str])
-end
+ let
+ val rtrm_str = Syntax.string_of_term ctxt rtrm
+ val qtrm_str = Syntax.string_of_term ctxt qtrm
+ in
+ raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str])
+ end
(* bound variables need to be treated properly,
@@ -717,8 +718,8 @@
NONE => matches tail
| SOME inst => Envir.subst_type inst qty
in
- matches ty_subst
- end
+ matches ty_subst
+ end
| _ => rty
fun subst_trm ctxt ty_subst trm_subst rtrm =
@@ -728,7 +729,7 @@
| Free(n, ty) => Free(n, subst_typ ctxt ty_subst ty)
| Var(n, ty) => Var(n, subst_typ ctxt ty_subst ty)
| Bound i => Bound i
- | Const (a, ty) =>
+ | Const (a, ty) =>
let
val thy = ProofContext.theory_of ctxt
@@ -742,43 +743,43 @@
end
(* generate type and term substitutions out of the
- qtypes involved in a quotient; the direction flag
- indicates in which direction the substitutions work:
-
+ qtypes involved in a quotient; the direction flag
+ indicates in which direction the substitutions work:
+
true: quotient -> raw
false: raw -> quotient
*)
fun mk_ty_subst qtys direction ctxt =
-let
- val thy = ProofContext.theory_of ctxt
-in
- quotdata_dest ctxt
- |> map (fn x => (#rtyp x, #qtyp x))
- |> filter (fn (_, qty) => member (Sign.typ_instance thy o swap) qtys qty)
- |> map (if direction then swap else I)
-end
+ let
+ val thy = ProofContext.theory_of ctxt
+ in
+ quotdata_dest ctxt
+ |> map (fn x => (#rtyp x, #qtyp x))
+ |> filter (fn (_, qty) => member (Sign.typ_instance thy o swap) qtys qty)
+ |> map (if direction then swap else I)
+ end
fun mk_trm_subst qtys direction ctxt =
-let
- val subst_typ' = subst_typ ctxt (mk_ty_subst qtys direction ctxt)
- fun proper (t1, t2) = subst_typ' (fastype_of t1) = fastype_of t2
+ let
+ val subst_typ' = subst_typ ctxt (mk_ty_subst qtys direction ctxt)
+ fun proper (t1, t2) = subst_typ' (fastype_of t1) = fastype_of t2
- val const_substs =
- qconsts_dest ctxt
- |> map (fn x => (#rconst x, #qconst x))
- |> map (if direction then swap else I)
+ val const_substs =
+ qconsts_dest ctxt
+ |> map (fn x => (#rconst x, #qconst x))
+ |> map (if direction then swap else I)
- val rel_substs =
- quotdata_dest ctxt
- |> map (fn x => (#equiv_rel x, HOLogic.eq_const (#qtyp x)))
- |> map (if direction then swap else I)
-in
- filter proper (const_substs @ rel_substs)
-end
+ val rel_substs =
+ quotdata_dest ctxt
+ |> map (fn x => (#equiv_rel x, HOLogic.eq_const (#qtyp x)))
+ |> map (if direction then swap else I)
+ in
+ filter proper (const_substs @ rel_substs)
+ end
(* derives a qtyp and qtrm out of a rtyp and rtrm,
- respectively
+ respectively
*)
fun derive_qtyp ctxt qtys rty =
subst_typ ctxt (mk_ty_subst qtys false ctxt) rty
@@ -787,7 +788,7 @@
subst_trm ctxt (mk_ty_subst qtys false ctxt) (mk_trm_subst qtys false ctxt) rtrm
(* derives a rtyp and rtrm out of a qtyp and qtrm,
- respectively
+ respectively
*)
fun derive_rtyp ctxt qtys qty =
subst_typ ctxt (mk_ty_subst qtys true ctxt) qty
--- a/src/HOL/Tools/Quotient/quotient_typ.ML Fri Jan 07 14:58:15 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML Fri Jan 07 15:35:00 2011 +0100
@@ -24,12 +24,12 @@
(* wrappers for define, note, Attrib.internal and theorem_i *)
fun define (name, mx, rhs) lthy =
-let
- val ((rhs, (_ , thm)), lthy') =
- Local_Theory.define ((name, mx), (Attrib.empty_binding, rhs)) lthy
-in
- ((rhs, thm), lthy')
-end
+ let
+ val ((rhs, (_ , thm)), lthy') =
+ Local_Theory.define ((name, mx), (Attrib.empty_binding, rhs)) lthy
+ in
+ ((rhs, thm), lthy')
+ end
fun note (name, thm, attrs) lthy =
Local_Theory.note ((name, attrs), [thm]) lthy |> snd
@@ -38,12 +38,12 @@
fun intern_attr at = Attrib.internal (K at)
fun theorem after_qed goals ctxt =
-let
- val goals' = map (rpair []) goals
- fun after_qed' thms = after_qed (the_single thms)
-in
- Proof.theorem NONE after_qed' [goals'] ctxt
-end
+ let
+ val goals' = map (rpair []) goals
+ fun after_qed' thms = after_qed (the_single thms)
+ in
+ Proof.theorem NONE after_qed' [goals'] ctxt
+ end
@@ -54,178 +54,179 @@
(* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *)
fun typedef_term rel rty lthy =
-let
- val [x, c] =
- [("x", rty), ("c", HOLogic.mk_setT rty)]
- |> Variable.variant_frees lthy [rel]
- |> map Free
-in
- lambda c (HOLogic.exists_const rty $
- lambda x (HOLogic.mk_conj (rel $ x $ x, HOLogic.mk_eq (c, rel $ x))))
-end
+ let
+ val [x, c] =
+ [("x", rty), ("c", HOLogic.mk_setT rty)]
+ |> Variable.variant_frees lthy [rel]
+ |> map Free
+ in
+ lambda c (HOLogic.exists_const rty $
+ lambda x (HOLogic.mk_conj (rel $ x $ x, HOLogic.mk_eq (c, rel $ x))))
+ end
(* makes the new type definitions and proves non-emptyness *)
fun typedef_make (vs, qty_name, mx, rel, rty) equiv_thm lthy =
-let
- val typedef_tac =
- EVERY1 (map rtac [@{thm part_equivp_typedef}, equiv_thm])
-in
-(* FIXME: purely local typedef causes at the moment
- problems with type variables
-
- Typedef.add_typedef false NONE (qty_name, vs, mx)
- (typedef_term rel rty lthy) NONE typedef_tac lthy
-*)
-(* FIXME should really use local typedef here *)
- Local_Theory.background_theory_result
+ let
+ val typedef_tac =
+ EVERY1 (map rtac [@{thm part_equivp_typedef}, equiv_thm])
+ in
+ (* FIXME: purely local typedef causes at the moment
+ problems with type variables
+
+ Typedef.add_typedef false NONE (qty_name, vs, mx)
+ (typedef_term rel rty lthy) NONE typedef_tac lthy
+ *)
+ (* FIXME should really use local typedef here *)
+ Local_Theory.background_theory_result
(Typedef.add_typedef_global false NONE
(qty_name, map (rpair dummyS) vs, mx)
(typedef_term rel rty lthy)
NONE typedef_tac) lthy
-end
+ end
(* tactic to prove the quot_type theorem for the new type *)
fun typedef_quot_type_tac equiv_thm ((_, typedef_info): Typedef.info) =
-let
- val rep_thm = #Rep typedef_info RS mem_def1
- val rep_inv = #Rep_inverse typedef_info
- val abs_inv = #Abs_inverse typedef_info
- val rep_inj = #Rep_inject typedef_info
-in
- (rtac @{thm quot_type.intro} THEN' RANGE [
- rtac equiv_thm,
- rtac rep_thm,
- rtac rep_inv,
- rtac abs_inv THEN' rtac mem_def2 THEN' atac,
- rtac rep_inj]) 1
-end
+ let
+ val rep_thm = #Rep typedef_info RS mem_def1
+ val rep_inv = #Rep_inverse typedef_info
+ val abs_inv = #Abs_inverse typedef_info
+ val rep_inj = #Rep_inject typedef_info
+ in
+ (rtac @{thm quot_type.intro} THEN' RANGE [
+ rtac equiv_thm,
+ rtac rep_thm,
+ rtac rep_inv,
+ rtac abs_inv THEN' rtac mem_def2 THEN' atac,
+ rtac rep_inj]) 1
+ end
(* proves the quot_type theorem for the new type *)
fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy =
-let
- val quot_type_const = Const (@{const_name "quot_type"}, dummyT)
- val goal =
- HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)
- |> Syntax.check_term lthy
-in
- Goal.prove lthy [] [] goal
- (K (typedef_quot_type_tac equiv_thm typedef_info))
-end
+ let
+ val quot_type_const = Const (@{const_name "quot_type"}, dummyT)
+ val goal =
+ HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)
+ |> Syntax.check_term lthy
+ in
+ Goal.prove lthy [] [] goal
+ (K (typedef_quot_type_tac equiv_thm typedef_info))
+ end
(* main function for constructing a quotient type *)
fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial)), equiv_thm) lthy =
-let
- val part_equiv =
- if partial
- then equiv_thm
- else equiv_thm RS @{thm equivp_implies_part_equivp}
+ let
+ val part_equiv =
+ if partial
+ then equiv_thm
+ else equiv_thm RS @{thm equivp_implies_part_equivp}
- (* generates the typedef *)
- val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) part_equiv lthy
+ (* generates the typedef *)
+ val ((qty_full_name, typedef_info), lthy1) =
+ typedef_make (vs, qty_name, mx, rel, rty) part_equiv lthy
- (* abs and rep functions from the typedef *)
- val Abs_ty = #abs_type (#1 typedef_info)
- val Rep_ty = #rep_type (#1 typedef_info)
- val Abs_name = #Abs_name (#1 typedef_info)
- val Rep_name = #Rep_name (#1 typedef_info)
- val Abs_const = Const (Abs_name, Rep_ty --> Abs_ty)
- val Rep_const = Const (Rep_name, Abs_ty --> Rep_ty)
+ (* abs and rep functions from the typedef *)
+ val Abs_ty = #abs_type (#1 typedef_info)
+ val Rep_ty = #rep_type (#1 typedef_info)
+ val Abs_name = #Abs_name (#1 typedef_info)
+ val Rep_name = #Rep_name (#1 typedef_info)
+ val Abs_const = Const (Abs_name, Rep_ty --> Abs_ty)
+ val Rep_const = Const (Rep_name, Abs_ty --> Rep_ty)
- (* more useful abs and rep definitions *)
- val abs_const = Const (@{const_name "quot_type.abs"}, dummyT )
- val rep_const = Const (@{const_name "quot_type.rep"}, dummyT )
- val abs_trm = Syntax.check_term lthy1 (abs_const $ rel $ Abs_const)
- val rep_trm = Syntax.check_term lthy1 (rep_const $ Rep_const)
- val abs_name = Binding.prefix_name "abs_" qty_name
- val rep_name = Binding.prefix_name "rep_" qty_name
+ (* more useful abs and rep definitions *)
+ val abs_const = Const (@{const_name "quot_type.abs"}, dummyT )
+ val rep_const = Const (@{const_name "quot_type.rep"}, dummyT )
+ val abs_trm = Syntax.check_term lthy1 (abs_const $ rel $ Abs_const)
+ val rep_trm = Syntax.check_term lthy1 (rep_const $ Rep_const)
+ val abs_name = Binding.prefix_name "abs_" qty_name
+ val rep_name = Binding.prefix_name "rep_" qty_name
- val ((_, abs_def), lthy2) = define (abs_name, NoSyn, abs_trm) lthy1
- val ((_, rep_def), lthy3) = define (rep_name, NoSyn, rep_trm) lthy2
+ val ((_, abs_def), lthy2) = define (abs_name, NoSyn, abs_trm) lthy1
+ val ((_, rep_def), lthy3) = define (rep_name, NoSyn, rep_trm) lthy2
- (* quot_type theorem *)
- val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, part_equiv, typedef_info) lthy3
+ (* quot_type theorem *)
+ val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, part_equiv, typedef_info) lthy3
- (* quotient theorem *)
- val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name
- val quotient_thm =
- (quot_thm RS @{thm quot_type.Quotient})
- |> fold_rule [abs_def, rep_def]
+ (* quotient theorem *)
+ val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name
+ val quotient_thm =
+ (quot_thm RS @{thm quot_type.Quotient})
+ |> fold_rule [abs_def, rep_def]
- (* name equivalence theorem *)
- val equiv_thm_name = Binding.suffix_name "_equivp" qty_name
+ (* name equivalence theorem *)
+ val equiv_thm_name = Binding.suffix_name "_equivp" qty_name
- (* storing the quotdata *)
- val quotdata = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm}
+ (* storing the quotdata *)
+ val quotdata = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm}
- fun qinfo phi = transform_quotdata phi quotdata
+ fun qinfo phi = transform_quotdata phi quotdata
- val lthy4 = lthy3
- |> Local_Theory.declaration true (fn phi => quotdata_update_gen qty_full_name (qinfo phi))
- |> note (equiv_thm_name, equiv_thm, if partial then [] else [intern_attr equiv_rules_add])
- |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add])
-in
- (quotdata, lthy4)
-end
+ val lthy4 = lthy3
+ |> Local_Theory.declaration true (fn phi => quotdata_update_gen qty_full_name (qinfo phi))
+ |> note (equiv_thm_name, equiv_thm, if partial then [] else [intern_attr equiv_rules_add])
+ |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add])
+ in
+ (quotdata, lthy4)
+ end
(* sanity checks for the quotient type specifications *)
fun sanity_check ((vs, qty_name, _), (rty, rel, _)) =
-let
- val rty_tfreesT = map fst (Term.add_tfreesT rty [])
- val rel_tfrees = map fst (Term.add_tfrees rel [])
- val rel_frees = map fst (Term.add_frees rel [])
- val rel_vars = Term.add_vars rel []
- val rel_tvars = Term.add_tvars rel []
- val qty_str = Binding.str_of qty_name ^ ": "
+ let
+ val rty_tfreesT = map fst (Term.add_tfreesT rty [])
+ val rel_tfrees = map fst (Term.add_tfrees rel [])
+ val rel_frees = map fst (Term.add_frees rel [])
+ val rel_vars = Term.add_vars rel []
+ val rel_tvars = Term.add_tvars rel []
+ val qty_str = Binding.str_of qty_name ^ ": "
- val illegal_rel_vars =
- if null rel_vars andalso null rel_tvars then []
- else [qty_str ^ "illegal schematic variable(s) in the relation."]
+ val illegal_rel_vars =
+ if null rel_vars andalso null rel_tvars then []
+ else [qty_str ^ "illegal schematic variable(s) in the relation."]
- val dup_vs =
- (case duplicates (op =) vs of
- [] => []
- | dups => [qty_str ^ "duplicate type variable(s) on the lhs: " ^ commas_quote dups])
+ val dup_vs =
+ (case duplicates (op =) vs of
+ [] => []
+ | dups => [qty_str ^ "duplicate type variable(s) on the lhs: " ^ commas_quote dups])
- val extra_rty_tfrees =
- (case subtract (op =) vs rty_tfreesT of
- [] => []
- | extras => [qty_str ^ "extra type variable(s) on the lhs: " ^ commas_quote extras])
+ val extra_rty_tfrees =
+ (case subtract (op =) vs rty_tfreesT of
+ [] => []
+ | extras => [qty_str ^ "extra type variable(s) on the lhs: " ^ commas_quote extras])
- val extra_rel_tfrees =
- (case subtract (op =) vs rel_tfrees of
- [] => []
- | extras => [qty_str ^ "extra type variable(s) in the relation: " ^ commas_quote extras])
+ val extra_rel_tfrees =
+ (case subtract (op =) vs rel_tfrees of
+ [] => []
+ | extras => [qty_str ^ "extra type variable(s) in the relation: " ^ commas_quote extras])
- val illegal_rel_frees =
- (case rel_frees of
- [] => []
- | xs => [qty_str ^ "illegal variable(s) in the relation: " ^ commas_quote xs])
+ val illegal_rel_frees =
+ (case rel_frees of
+ [] => []
+ | xs => [qty_str ^ "illegal variable(s) in the relation: " ^ commas_quote xs])
- val errs = illegal_rel_vars @ dup_vs @ extra_rty_tfrees @ extra_rel_tfrees @ illegal_rel_frees
-in
- if null errs then () else error (cat_lines errs)
-end
+ val errs = illegal_rel_vars @ dup_vs @ extra_rty_tfrees @ extra_rel_tfrees @ illegal_rel_frees
+ in
+ if null errs then () else error (cat_lines errs)
+ end
(* check for existence of map functions *)
fun map_check ctxt (_, (rty, _, _)) =
-let
- val thy = ProofContext.theory_of ctxt
+ let
+ val thy = ProofContext.theory_of ctxt
- fun map_check_aux rty warns =
- case rty of
- Type (_, []) => warns
- | Type (s, _) => if maps_defined thy s then warns else s::warns
- | _ => warns
+ fun map_check_aux rty warns =
+ case rty of
+ Type (_, []) => warns
+ | Type (s, _) => if maps_defined thy s then warns else s::warns
+ | _ => warns
- val warns = map_check_aux rty []
-in
- if null warns then ()
- else warning ("No map function defined for " ^ commas warns ^
- ". This will cause problems later on.")
-end
+ val warns = map_check_aux rty []
+ in
+ if null warns then ()
+ else warning ("No map function defined for " ^ commas warns ^
+ ". This will cause problems later on.")
+ end
@@ -246,48 +247,48 @@
*)
fun quotient_type quot_list lthy =
-let
- (* sanity check *)
- val _ = List.app sanity_check quot_list
- val _ = List.app (map_check lthy) quot_list
+ let
+ (* sanity check *)
+ val _ = List.app sanity_check quot_list
+ val _ = List.app (map_check lthy) quot_list
- fun mk_goal (rty, rel, partial) =
- let
- val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
- val const =
- if partial then @{const_name part_equivp} else @{const_name equivp}
+ fun mk_goal (rty, rel, partial) =
+ let
+ val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
+ val const =
+ if partial then @{const_name part_equivp} else @{const_name equivp}
+ in
+ HOLogic.mk_Trueprop (Const (const, equivp_ty) $ rel)
+ end
+
+ val goals = map (mk_goal o snd) quot_list
+
+ fun after_qed thms lthy =
+ fold_map add_quotient_type (quot_list ~~ thms) lthy |> snd
in
- HOLogic.mk_Trueprop (Const (const, equivp_ty) $ rel)
+ theorem after_qed goals lthy
end
- val goals = map (mk_goal o snd) quot_list
-
- fun after_qed thms lthy =
- fold_map add_quotient_type (quot_list ~~ thms) lthy |> snd
-in
- theorem after_qed goals lthy
-end
-
fun quotient_type_cmd specs lthy =
-let
- fun parse_spec ((((vs, qty_name), mx), rty_str), (partial, rel_str)) lthy =
let
- val rty = Syntax.read_typ lthy rty_str
- val lthy1 = Variable.declare_typ rty lthy
- val rel =
- Syntax.parse_term lthy1 rel_str
- |> Type.constraint (rty --> rty --> @{typ bool})
- |> Syntax.check_term lthy1
- val lthy2 = Variable.declare_term rel lthy1
+ fun parse_spec ((((vs, qty_name), mx), rty_str), (partial, rel_str)) lthy =
+ let
+ val rty = Syntax.read_typ lthy rty_str
+ val lthy1 = Variable.declare_typ rty lthy
+ val rel =
+ Syntax.parse_term lthy1 rel_str
+ |> Type.constraint (rty --> rty --> @{typ bool})
+ |> Syntax.check_term lthy1
+ val lthy2 = Variable.declare_term rel lthy1
+ in
+ (((vs, qty_name, mx), (rty, rel, partial)), lthy2)
+ end
+
+ val (spec', lthy') = fold_map parse_spec specs lthy
in
- (((vs, qty_name, mx), (rty, rel, partial)), lthy2)
+ quotient_type spec' lthy'
end
- val (spec', lthy') = fold_map parse_spec specs lthy
-in
- quotient_type spec' lthy'
-end
-
val partial = Scan.optional (Parse.reserved "partial" -- Parse.$$$ ":" >> K true) false
val quotspec_parser =
@@ -299,8 +300,8 @@
val _ = Keyword.keyword "/"
val _ =
- Outer_Syntax.local_theory_to_proof "quotient_type"
- "quotient type definitions (require equivalence proofs)"
- Keyword.thy_goal (quotspec_parser >> quotient_type_cmd)
+ Outer_Syntax.local_theory_to_proof "quotient_type"
+ "quotient type definitions (require equivalence proofs)"
+ Keyword.thy_goal (quotspec_parser >> quotient_type_cmd)
end; (* structure *)