# HG changeset patch
# User haftmann
# Date 1232552823 -3600
# Node ID 8c4e961fcb08f0ded511f9edd15a90c19b9ac49f
# Parent  08f783c5fcf01ed068e18a22634847836a65abcb
refined witness algebra

diff -r 08f783c5fcf0 -r 8c4e961fcb08 src/Pure/Isar/element.ML
--- 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
diff -r 08f783c5fcf0 -r 8c4e961fcb08 src/Pure/Isar/expression.ML
--- 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