--- a/NEWS Sun Jun 14 18:51:34 2015 +0100
+++ b/NEWS Sun Jun 14 23:22:31 2015 +0200
@@ -12,6 +12,9 @@
* Command 'obtain' binds term abbreviations (via 'is' patterns) in the
proof body as well, abstracted over relevant parameters.
+* Improved type-inference for theorem statement 'obtains': separate
+parameter scope for of each clause.
+
* Term abbreviations via 'is' patterns also work for schematic
statements: result is abstracted over unknowns.
--- a/src/Pure/Isar/expression.ML Sun Jun 14 18:51:34 2015 +0100
+++ b/src/Pure/Isar/expression.ML Sun Jun 14 23:22:31 2015 +0200
@@ -13,10 +13,10 @@
type expression = (xstring * Position.T, string) expr * (binding * string option * mixfix) list
(* Processing of context statements *)
- val cert_statement: Element.context_i list -> (term * term list) list list ->
- Proof.context -> (term * term list) list list * Proof.context
- val read_statement: Element.context list -> (string * string list) list list ->
- Proof.context -> (term * term list) list list * Proof.context
+ val cert_statement: Element.context_i list -> Element.statement_i ->
+ Proof.context -> (Attrib.binding * (term * term list) list) list * Proof.context
+ val read_statement: Element.context list -> Element.statement ->
+ Proof.context -> (Attrib.binding * (term * term list) list) list * Proof.context
(* Declaring locales *)
val cert_declaration: expression_i -> (Proof.context -> Proof.context) ->
@@ -217,13 +217,20 @@
fact = I,
attrib = I};
-fun parse_concl prep_term ctxt concl =
- (map o map) (fn (t, ps) =>
- (prep_term (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) t,
- map (prep_term (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)) ps)) concl;
+fun prepare_stmt prep_prop prep_obtains ctxt stmt =
+ (case stmt of
+ Element.Shows raw_shows =>
+ raw_shows |> (map o apsnd o map) (fn (t, ps) =>
+ (prep_prop (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) t,
+ map (prep_prop (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)) ps))
+ | Element.Obtains raw_obtains =>
+ let
+ val ((_, thesis), thesis_ctxt) = Obtain.obtain_thesis ctxt;
+ val obtains = prep_obtains thesis_ctxt thesis raw_obtains;
+ in map (fn (b, t) => ((b, []), [(t, [])])) obtains end);
-(** Simultaneous type inference: instantiations + elements + conclusion **)
+(** Simultaneous type inference: instantiations + elements + statement **)
local
@@ -275,15 +282,15 @@
let
val inst_cs = map extract_inst insts;
val elem_css = map extract_elem elems;
- val concl_cs = (map o map) mk_propp concl;
+ val concl_cs = (map o map) mk_propp (map snd concl);
(* Type inference *)
val (inst_cs' :: css', ctxt') =
(fold_burrow o fold_burrow) check (inst_cs :: elem_css @ [concl_cs]) ctxt;
val (elem_css', [concl_cs']) = chop (length elem_css) css';
in
- (map restore_inst (insts ~~ inst_cs'),
+ ((map restore_inst (insts ~~ inst_cs'),
map restore_elem (elems ~~ elem_css'),
- concl_cs', ctxt')
+ map fst concl ~~ concl_cs'), ctxt')
end;
end;
@@ -351,15 +358,15 @@
end;
-(** Process full context statement: instantiations + elements + conclusion **)
+(** Process full context statement: instantiations + elements + statement **)
(* Interleave incremental parsing and type inference over entire parsed stretch. *)
local
fun prep_full_context_statement
- parse_typ parse_prop prep_var_elem prep_inst prep_var_inst prep_expr
- {strict, do_close, fixed_frees} raw_import init_body raw_elems raw_concl ctxt1 =
+ parse_typ parse_prop prep_obtains prep_var_elem prep_inst prep_var_inst prep_expr
+ {strict, do_close, fixed_frees} raw_import init_body raw_elems raw_stmt ctxt1 =
let
val thy = Proof_Context.theory_of ctxt1;
@@ -374,7 +381,7 @@
Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT_global);
val inst'' = map2 Type.constraint parm_types' inst';
val insts' = insts @ [(loc, (prfx, inst''))];
- val (insts'', _, _, _) = check_autofix insts' [] [] ctxt;
+ val ((insts'', _, _), _) = check_autofix insts' [] [] ctxt;
val inst''' = insts'' |> List.last |> snd |> snd;
val (morph, _) = inst_morphism (parm_names, parm_types) (prfx, inst''') ctxt;
val ctxt'' = Locale.activate_declarations (loc, morph) ctxt;
@@ -389,15 +396,13 @@
val elems' = parse_elem parse_typ parse_prop ctxt' raw_elem;
in (elems', ctxt') end;
- fun prep_concl raw_concl (insts, elems, ctxt) =
- let
- val concl = parse_concl parse_prop ctxt raw_concl;
- in check_autofix insts elems concl ctxt end;
-
val fors = fold_map prep_var_inst fixed ctxt1 |> fst;
val ctxt2 = ctxt1 |> Proof_Context.add_fixes fors |> snd;
val (_, insts', ctxt3) = fold prep_insts_cumulative raw_insts (0, [], ctxt2);
+ fun prep_stmt elems ctxt =
+ check_autofix insts' elems (prepare_stmt parse_prop prep_obtains ctxt raw_stmt) ctxt;
+
val _ =
if fixed_frees then ()
else
@@ -406,50 +411,51 @@
| frees => error ("Illegal free variables in expression: " ^
commas_quote (map (Syntax.string_of_term ctxt3 o Free) (rev frees))));
- val ctxt4 = init_body ctxt3;
- val (elems, ctxt5) = fold_map prep_elem raw_elems ctxt4;
- val (insts, elems', concl, ctxt6) = prep_concl raw_concl (insts', elems, ctxt5);
+ val ((insts, elems', concl), ctxt4) = ctxt3
+ |> init_body
+ |> fold_map prep_elem raw_elems
+ |-> prep_stmt;
(* parameters from expression and elements *)
val xs = maps (fn Fixes fixes => map (Variable.check_name o #1) fixes | _ => [])
(Fixes fors :: elems');
- val (parms, ctxt7) = fold_map Proof_Context.inferred_param xs ctxt6;
+ val (parms, ctxt5) = fold_map Proof_Context.inferred_param xs ctxt4;
val fors' = finish_fixes parms fors;
val fixed = map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fors';
- val deps = map (finish_inst ctxt6) insts;
- val elems'' = map (finish_elem (ctxt1, ctxt6) parms do_close) elems';
+ val deps = map (finish_inst ctxt5) insts;
+ val elems'' = map (finish_elem (ctxt1, ctxt5) parms do_close) elems';
- in ((fixed, deps, elems'', concl), (parms, ctxt7)) end;
+ in ((fixed, deps, elems'', concl), (parms, ctxt5)) end;
in
fun cert_full_context_statement x =
- prep_full_context_statement (K I) (K I) Proof_Context.cert_var
- make_inst Proof_Context.cert_var (K I) x;
+ prep_full_context_statement (K I) (K I) Obtain.cert_obtains
+ Proof_Context.cert_var make_inst Proof_Context.cert_var (K I) x;
fun cert_read_full_context_statement x =
- prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Proof_Context.read_var
- make_inst Proof_Context.cert_var (K I) x;
+ prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Obtain.parse_obtains
+ Proof_Context.read_var make_inst Proof_Context.cert_var (K I) x;
fun read_full_context_statement x =
- prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Proof_Context.read_var
- parse_inst Proof_Context.read_var check_expr x;
+ prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Obtain.parse_obtains
+ Proof_Context.read_var parse_inst Proof_Context.read_var check_expr x;
end;
-(* Context statement: elements + conclusion *)
+(* Context statement: elements + statement *)
local
-fun prep_statement prep activate raw_elems raw_concl context =
+fun prep_statement prep activate raw_elems raw_stmt context =
let
val ((_, _, elems, concl), _) =
prep {strict = true, do_close = false, fixed_frees = true}
- ([], []) I raw_elems raw_concl context;
+ ([], []) I raw_elems raw_stmt context;
val (_, context') = context
|> Proof_Context.set_stmt true
|> fold_map activate elems;
@@ -474,7 +480,7 @@
let
val ((fixed, deps, elems, _), (parms, ctxt')) =
prep {strict = false, do_close = true, fixed_frees = false}
- raw_import init_body raw_elems [] context;
+ raw_import init_body raw_elems (Element.Shows []) context;
(* Declare parameters and imported facts *)
val context' = context |>
fix_params fixed |>
@@ -510,7 +516,8 @@
val thy = Proof_Context.theory_of context;
val ((fixed, deps, _, _), _) =
- prep {strict = true, do_close = true, fixed_frees = true} expression I [] [] context;
+ prep {strict = true, do_close = true, fixed_frees = true} expression I []
+ (Element.Shows []) context;
(* proof obligations *)
val propss = map (props_of thy) deps;
--- a/src/Pure/Isar/obtain.ML Sun Jun 14 18:51:34 2015 +0100
+++ b/src/Pure/Isar/obtain.ML Sun Jun 14 23:22:31 2015 +0200
@@ -6,11 +6,11 @@
signature OBTAIN =
sig
+ val obtain_thesis: Proof.context -> ((string * typ) * term) * Proof.context
val obtains_attributes: ('typ, 'term) Element.obtain list -> attribute list
- val parse_clause: Proof.context -> term ->
- (binding * typ option * mixfix) list -> string list -> term
val read_obtains: Proof.context -> term -> Element.obtains -> (binding * term) list
val cert_obtains: Proof.context -> term -> Element.obtains_i -> (binding * term) list
+ val parse_obtains: Proof.context -> term -> Element.obtains -> (binding * term) list
val consider: Element.obtains_i -> bool -> Proof.state -> Proof.state
val consider_cmd: Element.obtains -> bool -> Proof.state -> Proof.state
val obtain: binding -> (binding * typ option * mixfix) list ->
@@ -92,38 +92,38 @@
local
-fun prepare_clause parse_prop ctxt thesis vars raw_props =
+val mk_all_external = Logic.all_constraint o Variable.default_type;
+fun mk_all_internal _ (y, z) t =
+ let val T = the (AList.lookup (op =) (Term.add_frees t []) z);
+ in Logic.all_const T $ Term.lambda_name (y, Free (z, T)) t end;
+
+fun prepare_clause prep_var parse_prop mk_all ctxt thesis raw_vars raw_props =
let
- val (xs', ctxt') = ctxt |> Proof_Context.add_fixes vars;
+ val ((xs', vars), ctxt') = ctxt
+ |> fold_map prep_var raw_vars
+ |-> (fn vars => Proof_Context.add_fixes vars ##>> pair vars);
val xs = map (Variable.check_name o #1) vars;
in
Logic.list_implies (map (parse_prop ctxt') raw_props, thesis)
- |> fold_rev (Logic.all_constraint (Variable.default_type ctxt')) (xs ~~ xs')
+ |> fold_rev (mk_all ctxt') (xs ~~ xs')
end;
-fun prepare_obtains prep_var parse_prop ctxt thesis raw_obtains =
+fun prepare_obtains prep_clause check_terms
+ ctxt thesis (raw_obtains: ('typ, 'term) Element.obtain list) =
let
- val all_types =
- fold_map prep_var (maps (fn (_, (vs, _)) => vs) raw_obtains)
- (ctxt |> Context_Position.set_visible false)
- |> #1 |> map_filter (fn (_, opt_T, _) => opt_T);
- val types_ctxt = fold Variable.declare_typ all_types ctxt;
+ val clauses = raw_obtains
+ |> map (fn (_, (raw_vars, raw_props)) => prep_clause ctxt thesis raw_vars raw_props)
+ |> check_terms ctxt;
+ in map fst raw_obtains ~~ clauses end;
- val clauses =
- raw_obtains |> map (fn (_, (raw_vars, raw_props)) =>
- let
- val (vars, vars_ctxt) = fold_map prep_var raw_vars types_ctxt;
- val clause = prepare_clause parse_prop vars_ctxt thesis vars raw_props;
- in clause end)
- |> Syntax.check_terms ctxt;
- in map fst raw_obtains ~~ clauses end;
+val parse_clause = prepare_clause Proof_Context.read_var Syntax.parse_prop mk_all_external;
+val cert_clause = prepare_clause Proof_Context.cert_var (K I) mk_all_internal;
in
-val parse_clause = prepare_clause Syntax.parse_prop;
-
-val read_obtains = prepare_obtains Proof_Context.read_var Syntax.parse_prop;
-val cert_obtains = prepare_obtains Proof_Context.cert_var (K I);
+val read_obtains = prepare_obtains parse_clause Syntax.check_terms;
+val cert_obtains = prepare_obtains cert_clause (K I);
+val parse_obtains = prepare_obtains parse_clause (K I);
end;
@@ -132,11 +132,11 @@
(** consider: generalized elimination and cases rule **)
(*
- consider x where (a) "A x" | y (b) where "B x" | ... ==
+ consider (a) x where "A x" | (b) y where "B y" | ... ==
have thesis
if a [intro?]: "!!x. A x ==> thesis"
- and b [intro?]: "!!x. B x ==> thesis"
+ and b [intro?]: "!!y. B y ==> thesis"
and ...
for thesis
apply (insert that)
@@ -287,9 +287,9 @@
{
fix thesis
<chain_facts> have "PROP ?guess"
- apply magic -- {* turns goal into "thesis ==> #thesis" *}
+ apply magic -- {* turn goal into "thesis ==> #thesis" *}
<proof body>
- apply_end magic -- {* turns final "(!!x. P x ==> thesis) ==> #thesis" into
+ apply_end magic -- {* turn final "(!!x. P x ==> thesis) ==> #thesis" into
"#((!!x. A x ==> thesis) ==> thesis)" which is a finished goal state *}
<proof end>
}
--- a/src/Pure/Isar/specification.ML Sun Jun 14 18:51:34 2015 +0100
+++ b/src/Pure/Isar/specification.ML Sun Jun 14 23:22:31 2015 +0200
@@ -318,56 +318,30 @@
local
-fun prep_statement prep_att prep_stmt elems concl ctxt =
- (case concl of
- Element.Shows shows =>
- let
- val (propp, elems_ctxt) = prep_stmt elems (map snd shows) ctxt;
- val prems = Assumption.local_prems_of elems_ctxt ctxt;
- val stmt = Attrib.map_specs (map prep_att) (map fst shows ~~ propp);
- val goal_ctxt = (fold o fold) (Variable.auto_fixes o fst) propp elems_ctxt;
- in (([], prems, stmt, NONE), goal_ctxt) end
- | Element.Obtains obtains =>
- let
- val constraints = obtains |> map (fn (_, (vars, _)) =>
- Element.Constrains
- (vars |> map_filter (fn (x, SOME T, _) => SOME (Variable.check_name x, T) | _ => NONE)));
-
- val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
- val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
-
- val thesis = Object_Logic.fixed_judgment ctxt Auto_Bind.thesisN;
+fun prep_statement prep_att prep_stmt raw_elems raw_stmt ctxt =
+ let
+ val (stmt, elems_ctxt) = prep_stmt raw_elems raw_stmt ctxt;
+ val prems = Assumption.local_prems_of elems_ctxt ctxt;
+ val stmt_ctxt = fold (fold (Variable.auto_fixes o fst) o snd) stmt elems_ctxt;
+ in
+ (case raw_stmt of
+ Element.Shows _ =>
+ let val stmt' = Attrib.map_specs (map prep_att) stmt
+ in (([], prems, stmt', NONE), stmt_ctxt) end
+ | Element.Obtains raw_obtains =>
+ let
+ val asms_ctxt = stmt_ctxt
+ |> fold (fn ((name, _), asm) =>
+ snd o Proof_Context.add_assms Assumption.assume_export
+ [((name, [Context_Rules.intro_query NONE]), asm)]) stmt;
+ val that = Assumption.local_prems_of asms_ctxt stmt_ctxt;
+ val ([(_, that')], that_ctxt) = asms_ctxt
+ |> Proof_Context.note_thmss "" [((Binding.name Auto_Bind.thatN, []), [(that, [])])];
- fun assume_case ((name, (vars, _)), asms) ctxt' =
- let
- val bs = map (fn (b, _, _) => b) vars;
- val xs = map Variable.check_name bs;
- val props = map fst asms;
- val (params, _) = ctxt'
- |> fold Variable.declare_term props
- |> fold_map Proof_Context.inferred_param xs
- |>> map Free;
- val asm = fold_rev Logic.all params (Logic.list_implies (props, thesis));
- val _ = ctxt' |> Proof_Context.add_fixes (map (fn b => (b, NONE, NoSyn)) bs);
- in
- ctxt'
- |> Variable.auto_fixes asm
- |> Proof_Context.add_assms Assumption.assume_export
- [((name, [Context_Rules.intro_query NONE]), [(asm, [])])]
- |>> (fn [(_, [th])] => th)
- end;
-
- val more_atts = map (Attrib.internal o K) (Obtain.obtains_attributes obtains);
- val prems = Assumption.local_prems_of elems_ctxt ctxt;
- val stmt = [((Binding.empty, []), [(thesis, [])])];
-
- val (facts, goal_ctxt) = elems_ctxt
- |> (snd o Proof_Context.add_fixes [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)])
- |> fold_map assume_case (obtains ~~ propp)
- |-> (fn ths =>
- Proof_Context.note_thmss "" [((Binding.name Auto_Bind.thatN, []), [(ths, [])])] #>
- #2 #> pair ths);
- in ((more_atts, prems, stmt, SOME facts), goal_ctxt) end);
+ val more_atts = map (Attrib.internal o K) (Obtain.obtains_attributes raw_obtains);
+ val stmt' = [((Binding.empty, []), [(#2 (#1 (Obtain.obtain_thesis ctxt)), [])])];
+ in ((more_atts, prems, stmt', SOME that'), that_ctxt) end)
+ end;
fun gen_theorem schematic bundle_includes prep_att prep_stmt
kind before_qed after_qed (name, raw_atts) raw_includes raw_elems raw_concl int lthy =