--- a/src/Pure/Isar/element.ML Wed Jan 21 16:47:03 2009 +0100
+++ b/src/Pure/Isar/element.ML Wed Jan 21 16:47:03 2009 +0100
@@ -9,11 +9,11 @@
sig
datatype ('typ, 'term) stmt =
Shows of (Attrib.binding * ('term * 'term list) list) list |
- Obtains of (Binding.T * ((Binding.T * 'typ option) list * 'term list)) list
+ Obtains of (binding * ((binding * 'typ option) list * 'term list)) list
type statement = (string, string) stmt
type statement_i = (typ, term) stmt
datatype ('typ, 'term, 'fact) ctxt =
- Fixes of (Binding.T * 'typ option * mixfix) list |
+ Fixes of (binding * 'typ option * mixfix) list |
Constrains of (string * 'typ) list |
Assumes of (Attrib.binding * ('term * 'term list) list) list |
Defines of (Attrib.binding * ('term * 'term list)) list |
@@ -23,12 +23,12 @@
val facts_map: (('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt) ->
(Attrib.binding * ('fact * Attrib.src list) list) list ->
(Attrib.binding * ('c * Attrib.src list) list) list
- val map_ctxt': {binding: Binding.T -> Binding.T,
- var: Binding.T * mixfix -> Binding.T * mixfix,
+ val map_ctxt': {binding: binding -> binding,
+ var: binding * mixfix -> binding * mixfix,
typ: 'typ -> 'a, term: 'term -> 'b, pat: 'term -> 'b, fact: 'fact -> 'c,
attrib: Attrib.src -> Attrib.src} -> ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
- val map_ctxt: {binding: Binding.T -> Binding.T,
- var: Binding.T * mixfix -> Binding.T * mixfix,
+ val map_ctxt: {binding: binding -> binding,
+ var: binding * mixfix -> binding * mixfix,
typ: 'typ -> 'a, term: 'term -> 'b, fact: 'fact -> 'c,
attrib: Attrib.src -> Attrib.src} -> ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
val map_ctxt_attrib: (Attrib.src -> Attrib.src) ->
@@ -41,25 +41,21 @@
val pretty_ctxt: Proof.context -> context_i -> Pretty.T list
val pretty_statement: Proof.context -> string -> thm -> Pretty.T
type witness
- val map_witness: (term * thm -> term * thm) -> witness -> witness
+ val prove_witness: Proof.context -> term -> tactic -> witness
+ val witness_proof: (witness list list -> Proof.context -> Proof.context) ->
+ term list list -> Proof.context -> Proof.state
+ val witness_proof_eqs: (witness list list -> thm list -> Proof.context -> Proof.context) ->
+ term list list -> term list -> Proof.context -> Proof.state
+ val witness_local_proof: (witness list list -> Proof.state -> Proof.state) ->
+ string -> term list list -> Proof.context -> bool -> Proof.state -> Proof.state
val morph_witness: morphism -> witness -> witness
- val witness_prop: witness -> term
- val witness_hyps: witness -> term list
- val assume_witness: theory -> term -> witness
- val prove_witness: Proof.context -> term -> tactic -> witness
- val close_witness: witness -> witness
val conclude_witness: witness -> thm
- val mark_witness: term -> term
- val make_witness: term -> thm -> witness
- val dest_witness: witness -> term * thm
- val transfer_witness: theory -> witness -> witness
- val refine_witness: Proof.state -> Proof.state Seq.seq
val pretty_witness: Proof.context -> witness -> Pretty.T
val rename: (string * (string * mixfix option)) list -> string -> string
val rename_var_name: (string * (string * mixfix option)) list ->
string * mixfix -> string * mixfix
val rename_var: (string * (string * mixfix option)) list ->
- Binding.T * mixfix -> Binding.T * mixfix
+ binding * mixfix -> binding * mixfix
val rename_term: (string * (string * mixfix option)) list -> term -> term
val rename_thm: (string * (string * mixfix option)) list -> thm -> thm
val rename_morphism: (string * (string * mixfix option)) list -> morphism
@@ -93,7 +89,7 @@
datatype ('typ, 'term) stmt =
Shows of (Attrib.binding * ('term * 'term list) list) list |
- Obtains of (Binding.T * ((Binding.T * 'typ option) list * 'term list)) list;
+ Obtains of (binding * ((binding * 'typ option) list * 'term list)) list;
type statement = (string, string) stmt;
type statement_i = (typ, term) stmt;
@@ -102,7 +98,7 @@
(* context *)
datatype ('typ, 'term, 'fact) ctxt =
- Fixes of (Binding.T * 'typ option * mixfix) list |
+ Fixes of (binding * 'typ option * mixfix) list |
Constrains of (string * 'typ) list |
Assumes of (Attrib.binding * ('term * 'term list) list) list |
Defines of (Attrib.binding * ('term * 'term list)) list |
@@ -300,24 +296,51 @@
datatype witness = Witness of term * thm;
+val mark_witness = Logic.protect;
+fun witness_prop (Witness (t, _)) = t;
+fun witness_hyps (Witness (_, th)) = #hyps (Thm.rep_thm th);
fun map_witness f (Witness witn) = Witness (f witn);
fun morph_witness phi = map_witness (fn (t, th) => (Morphism.term phi t, Morphism.thm phi th));
-fun witness_prop (Witness (t, _)) = t;
-fun witness_hyps (Witness (_, th)) = #hyps (Thm.rep_thm th);
-
-fun assume_witness thy t =
- Witness (t, Goal.protect (Thm.assume (Thm.cterm_of thy t)));
-
fun prove_witness ctxt t tac =
- Witness (t, Thm.close_derivation (Goal.prove ctxt [] [] (Logic.protect t) (fn _ =>
+ Witness (t, Thm.close_derivation (Goal.prove ctxt [] [] (mark_witness t) (fn _ =>
Tactic.rtac Drule.protectI 1 THEN tac)));
-val close_witness = map_witness (fn (t, th) => (t, Thm.close_derivation th));
+local
+
+val refine_witness =
+ Proof.refine (Method.Basic (K (Method.RAW_METHOD
+ (K (ALLGOALS
+ (CONJUNCTS (ALLGOALS
+ (CONJUNCTS (TRYALL (Tactic.rtac Drule.protectI)))))))), Position.none));
-fun conclude_witness (Witness (_, th)) =
- Thm.close_derivation (MetaSimplifier.norm_hhf_protect (Goal.conclude th));
+fun gen_witness_proof proof after_qed wit_propss eq_props =
+ let
+ val propss = (map o map) (fn prop => (mark_witness prop, [])) wit_propss
+ @ [map (rpair []) eq_props];
+ fun after_qed' thmss =
+ let
+ val (wits, eqs) = split_last ((map o map) Thm.close_derivation thmss);
+ in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end;
+ in proof after_qed' propss #> refine_witness #> Seq.hd end;
+
+in
+
+fun witness_proof after_qed wit_propss =
+ gen_witness_proof (Proof.theorem_i NONE) (fn wits => fn _ => after_qed wits)
+ wit_propss [];
+
+val witness_proof_eqs = gen_witness_proof (Proof.theorem_i NONE);
+
+fun witness_local_proof after_qed cmd wit_propss goal_ctxt int =
+ gen_witness_proof (fn after_qed' => fn propss =>
+ Proof.map_context (K goal_ctxt)
+ #> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
+ cmd NONE after_qed' (map (pair (Binding.empty, [])) propss))
+ (fn wits => fn _ => after_qed wits) wit_propss [];
+
+end; (*local*)
fun compose_witness (Witness (_, th)) r =
let
@@ -330,18 +353,8 @@
(Thm.instantiate (Thm.match (Thm.cprop_of th', A)) th'))
end;
-val mark_witness = Logic.protect;
-
-fun make_witness t th = Witness (t, th);
-fun dest_witness (Witness w) = w;
-
-fun transfer_witness thy (Witness (t, th)) = Witness (t, Thm.transfer thy th);
-
-val refine_witness =
- Proof.refine (Method.Basic (K (Method.RAW_METHOD
- (K (ALLGOALS
- (CONJUNCTS (ALLGOALS
- (CONJUNCTS (TRYALL (Tactic.rtac Drule.protectI)))))))), Position.none));
+fun conclude_witness (Witness (_, th)) =
+ Thm.close_derivation (MetaSimplifier.norm_hhf_protect (Goal.conclude th));
fun pretty_witness ctxt witn =
let val prt_term = Pretty.quote o Syntax.pretty_term ctxt in
--- a/src/Pure/Isar/expression.ML Wed Jan 21 16:47:03 2009 +0100
+++ b/src/Pure/Isar/expression.ML Wed Jan 21 16:47:03 2009 +0100
@@ -9,8 +9,8 @@
(* Locale expressions *)
datatype 'term map = Positional of 'term option list | Named of (string * 'term) list
type 'term expr = (string * ((string * bool) * 'term map)) list
- type expression_i = term expr * (Binding.T * typ option * mixfix) list
- type expression = string expr * (Binding.T * string option * mixfix) list
+ type expression_i = term expr * (binding * typ option * mixfix) list
+ type expression = string expr * (binding * string option * mixfix) list
(* Processing of context statements *)
val cert_statement: Element.context_i list -> (term * term list) list list ->
@@ -20,14 +20,14 @@
(* Declaring locales *)
val cert_declaration: expression_i -> Element.context_i list -> Proof.context ->
- ((Binding.T * typ option * mixfix) list * (string * morphism) list
+ ((binding * typ option * mixfix) list * (string * morphism) list
* Element.context_i list) * ((string * typ) list * Proof.context)
val cert_read_declaration: expression_i -> Element.context list -> Proof.context ->
- ((Binding.T * typ option * mixfix) list * (string * morphism) list
+ ((binding * typ option * mixfix) list * (string * morphism) list
* Element.context_i list) * ((string * typ) list * Proof.context)
(*FIXME*)
val read_declaration: expression -> Element.context list -> Proof.context ->
- ((Binding.T * typ option * mixfix) list * (string * morphism) list
+ ((binding * typ option * mixfix) list * (string * morphism) list
* Element.context_i list) * ((string * typ) list * Proof.context)
val add_locale: bstring -> bstring -> expression_i -> Element.context_i list ->
theory -> string * local_theory
@@ -64,8 +64,8 @@
type 'term expr = (string * ((string * bool) * 'term map)) list;
-type expression = string expr * (Binding.T * string option * mixfix) list;
-type expression_i = term expr * (Binding.T * typ option * mixfix) list;
+type expression = string expr * (binding * string option * mixfix) list;
+type expression_i = term expr * (binding * typ option * mixfix) list;
(** Internalise locale names in expr **)
@@ -640,7 +640,7 @@
|> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
|> Sign.declare_const [] ((Binding.name bname, predT), NoSyn) |> snd
|> PureThy.add_defs false
- [((Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])];
+ [((Binding.name (Thm.def_name bname), Logic.mk_equals (head, body)), [Thm.kind_internal])];
val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
val cert = Thm.cterm_of defs_thy;
@@ -786,41 +786,23 @@
(*** Interpretation ***)
-(** Witnesses and goals **)
-
-fun prep_propp propss = propss |> map (map (rpair [] o Element.mark_witness));
-
-val prep_result = map2 (fn props => fn thms =>
- map2 Element.make_witness props (map Thm.close_derivation thms));
-
-
(** Interpretation between locales: declaring sublocale relationships **)
local
-fun gen_sublocale prep_expr intern
- raw_target expression thy =
+fun gen_sublocale prep_expr intern raw_target expression thy =
let
val target = intern thy raw_target;
val target_ctxt = Locale.init target thy;
val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
- fun store_dep (name, morph) thms =
- Locale.add_dependency target (name, morph $> Element.satisfy_morphism thms $> export);
-
- fun after_qed results =
- ProofContext.theory (
- (* store dependencies *)
- fold2 store_dep deps (prep_result propss results) #>
- (* propagate registrations *)
- (fn thy => fold_rev Locale.activate_global_facts
+ fun after_qed witss = ProofContext.theory (
+ fold2 (fn (name, morph) => fn wits => Locale.add_dependency target
+ (name, morph $> Element.satisfy_morphism wits $> export)) deps witss #>
+ (fn thy => fold_rev Locale.activate_global_facts
(Locale.get_registrations thy) thy));
- in
- goal_ctxt |>
- Proof.theorem_i NONE after_qed (prep_propp propss) |>
- Element.refine_witness |> Seq.hd
- end;
+ in Element.witness_proof after_qed propss goal_ctxt end;
in
@@ -845,10 +827,10 @@
val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
val export' = Variable.export_morphism goal_ctxt expr_ctxt;
- fun store_reg ((name, morph), thms) thy =
+ fun store_reg ((name, morph), wits) thy =
let
- val thms' = map (Element.morph_witness export') thms;
- val morph' = morph $> Element.satisfy_morphism thms';
+ val wits' = map (Element.morph_witness export') wits;
+ val morph' = morph $> Element.satisfy_morphism wits';
in
thy
|> Locale.add_registration (name, (morph', export))
@@ -859,35 +841,26 @@
thy
|> fold (fn (name, morph) =>
Locale.activate_global_facts (name, morph $> export)) regs
- | store_eqns_activate regs thms thy =
+ | store_eqns_activate regs eqs thy =
let
- val thms' = thms |> map (Element.conclude_witness #>
- Morphism.thm (export' $> export) #>
+ val eqs' = eqs |> map (Morphism.thm (export' $> export) #>
LocalDefs.meta_rewrite_rule (ProofContext.init thy) #>
Drule.abs_def);
- val eq_morph = Element.eq_morphism thy thms';
+ val eq_morph = Element.eq_morphism thy eqs';
val eq_attns' = map ((apsnd o map) (Attrib.attribute_i thy)) eq_attns;
in
thy
|> fold (fn (name, morph) =>
Locale.amend_registration eq_morph (name, morph) #>
Locale.activate_global_facts (name, morph $> eq_morph $> export)) regs
- |> PureThy.note_thmss Thm.lemmaK (eq_attns' ~~ map (fn th => [([th], [])]) thms')
+ |> PureThy.note_thmss Thm.lemmaK (eq_attns' ~~ map (fn eq => [([eq], [])]) eqs')
|> snd
end;
- fun after_qed results =
- let
- val (wits_reg, wits_eq) = split_last (prep_result (propss @ [eqns]) results);
- in ProofContext.theory (fold_map store_reg (regs ~~ wits_reg)
- #-> (fn regs => store_eqns_activate regs wits_eq))
- end;
+ fun after_qed wits eqs = ProofContext.theory (fold_map store_reg (regs ~~ wits)
+ #-> (fn regs => store_eqns_activate regs eqs));
- in
- goal_ctxt |>
- Proof.theorem_i NONE after_qed (prep_propp (propss @ [eqns])) |>
- Element.refine_witness |> Seq.hd
- end;
+ in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
in
@@ -910,20 +883,16 @@
val ((propss, regs, export), goal_ctxt) = prep_expr expression ctxt;
- fun store_reg ((name, morph), thms) =
+ fun store_reg (name, morph) thms =
let
val morph' = morph $> Element.satisfy_morphism thms $> export;
- in
- Locale.activate_local_facts (name, morph')
- end;
+ in Locale.activate_local_facts (name, morph') end;
- fun after_qed results =
- Proof.map_context (fold store_reg (regs ~~ prep_result propss results));
+ fun after_qed wits =
+ Proof.map_context (fold2 store_reg regs wits);
in
- state |> Proof.map_context (K goal_ctxt) |>
- Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
- "interpret" NONE after_qed (map (pair (Binding.empty, [])) (prep_propp propss)) |>
- Element.refine_witness |> Seq.hd
+ state
+ |> Element.witness_local_proof after_qed "interpret" propss goal_ctxt int
end;
in