eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
--- a/src/Pure/Isar/element.ML Sat Jun 13 15:51:19 2015 +0200
+++ b/src/Pure/Isar/element.ML Sat Jun 13 16:35:27 2015 +0200
@@ -33,8 +33,6 @@
val pretty_ctxt: Proof.context -> context_i -> Pretty.T list
val pretty_ctxt_no_attribs: Proof.context -> context_i -> Pretty.T list
val pretty_statement: Proof.context -> string -> thm -> Pretty.T
- val close_form: Proof.context -> (string -> string option) -> (string -> typ option) ->
- term -> term
type witness
val prove_witness: Proof.context -> term -> tactic -> witness
val witness_proof: (witness list list -> Proof.context -> Proof.context) ->
@@ -250,26 +248,6 @@
end;
-(** abstract syntax operations: before type-inference **)
-
-fun close_form ctxt default_name default_type A =
- let
- fun abs_body lev y (Abs (x, T, b)) = Abs (x, T, abs_body (lev + 1) y b)
- | abs_body lev y (t $ u) = abs_body lev y t $ abs_body lev y u
- | abs_body lev y (t as Free (x, T)) =
- if x = y then
- Type.constraint (the_default dummyT (default_type x))
- (Type.constraint T (Bound lev))
- else t
- | abs_body _ _ a = a;
- fun close y B =
- let
- val y' = perhaps default_name y;
- val B' = abs_body 0 y (Term.incr_boundvars 1 B);
- in if Term.is_dependent B' then Logic.all_const dummyT $ Abs (y', dummyT, B') else B end;
- in fold close (Variable.add_free_names ctxt A []) A end;
-
-
(** logical operations **)
--- a/src/Pure/Isar/obtain.ML Sat Jun 13 15:51:19 2015 +0200
+++ b/src/Pure/Isar/obtain.ML Sat Jun 13 16:35:27 2015 +0200
@@ -96,12 +96,9 @@
let
val (xs', ctxt') = ctxt |> Proof_Context.add_fixes vars;
val xs = map (Variable.check_name o #1) vars;
-
- val default_name = AList.lookup (op =) (xs' ~~ xs);
- val default_type = Variable.default_type ctxt';
in
Logic.list_implies (map (parse_prop ctxt') raw_props, thesis)
- |> Element.close_form ctxt default_name default_type
+ |> fold_rev (Logic.all_constraint (Variable.default_type ctxt')) (xs ~~ xs')
end;
fun prepare_obtains prep_var parse_prop ctxt thesis raw_obtains =
--- a/src/Pure/Isar/specification.ML Sat Jun 13 15:51:19 2015 +0200
+++ b/src/Pure/Isar/specification.ML Sat Jun 13 16:35:27 2015 +0200
@@ -105,11 +105,12 @@
fun close_forms ctxt i As =
let
- val frees = rev (fold (Variable.add_free_names ctxt) As []);
+ val xs = rev (fold (Variable.add_free_names ctxt) As []);
val types =
- map (Type_Infer.param i o rpair []) (Name.invent Name.context Name.aT (length frees));
- val uniform_typing = AList.lookup (op =) (frees ~~ types);
- in map (Element.close_form ctxt (K NONE) uniform_typing) As end;
+ map (Type_Infer.param i o rpair []) (Name.invent Name.context Name.aT (length xs));
+ val uniform_typing = AList.lookup (op =) (xs ~~ types);
+ val close = fold_rev (Logic.dependent_all_constraint uniform_typing) (xs ~~ xs);
+ in map close As end;
fun prepare prep_var parse_prop prep_att do_close raw_vars raw_specss ctxt =
let
--- a/src/Pure/logic.ML Sat Jun 13 15:51:19 2015 +0200
+++ b/src/Pure/logic.ML Sat Jun 13 16:35:27 2015 +0200
@@ -12,6 +12,8 @@
val is_all: term -> bool
val dest_all: term -> (string * typ) * term
val list_all: (string * typ) list * term -> term
+ val all_constraint: (string -> typ option) -> string * string -> term -> term
+ val dependent_all_constraint: (string -> typ option) -> string * string -> term -> term
val mk_equals: term * term -> term
val dest_equals: term -> term * term
val implies: term
@@ -109,6 +111,35 @@
| list_all ((a, T) :: vars, t) = all_const T $ Abs (a, T, list_all (vars, t));
+(* operations before type-inference *)
+
+local
+
+fun abs_body default_type z tm =
+ let
+ fun abs lev (Abs (x, T, b)) = Abs (x, T, abs (lev + 1) b)
+ | abs lev (t $ u) = abs lev t $ abs lev u
+ | abs lev (a as Free (x, T)) =
+ if x = z then
+ Type.constraint (the_default dummyT (default_type x))
+ (Type.constraint T (Bound lev))
+ else a
+ | abs _ a = a;
+ in abs 0 (Term.incr_boundvars 1 tm) end;
+
+in
+
+fun all_constraint default_type (y, z) t =
+ all_const dummyT $ Abs (y, dummyT, abs_body default_type z t);
+
+fun dependent_all_constraint default_type (y, z) t =
+ let val t' = abs_body default_type z t
+ in if Term.is_dependent t' then all_const dummyT $ Abs (y, dummyT, t') else t end;
+
+end;
+
+
+
(** equality **)
fun mk_equals (t, u) =