minor

2 files changed, 57 insertions, 68 deletions

diff --git a/.gitignore b/.gitignore
index fb8160e..de525c3 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,5 +1,5 @@
 *~
+*.bak
 \#*.thy#
 \#*.ML#
-Test.thy
 
diff --git a/spartan/core/goals.ML b/spartan/core/goals.ML
index 4b53a7f..51a853e 100644
--- a/spartan/core/goals.ML
+++ b/spartan/core/goals.ML
@@ -15,27 +15,27 @@ val long_keyword =
 val long_statement =
   Scan.optional
     (Parse_Spec.opt_thm_name ":" --| Scan.ahead long_keyword)
-    Binding.empty_atts --
-  Scan.optional Parse_Spec.includes [] -- Parse_Spec.long_statement
-    >> (fn ((binding, includes), (elems, concl)) =>
-        (true, binding, includes, elems, concl))
+    Binding.empty_atts
+  -- Scan.optional Parse_Spec.includes []
+  -- Parse_Spec.long_statement >>
+    (fn ((binding, includes), (elems, concl)) =>
+      (true, binding, includes, elems, concl))
 
 val short_statement =
-  Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes
-    >> (fn ((shows, assumes), fixes) =>
+  Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes >>
+    (fn ((shows, assumes), fixes) =>
       (false, Binding.empty_atts, [],
-        [Element.Fixes fixes, Element.Assumes assumes],
-        Element.Shows shows))
+      [Element.Fixes fixes, Element.Assumes assumes], Element.Shows shows)
+    )
 
 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 (Proof_Context.augment o fst) o snd)
-      stmt elems_ctxt
-  in
-    case raw_stmt of
-      Element.Shows _ =>
+    val stmt_ctxt =
+      fold (fold (Proof_Context.augment 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 =>
@@ -50,11 +50,8 @@ fun prep_statement prep_att prep_stmt raw_elems raw_stmt ctxt =
             |> Proof_Context.note_thmss ""
                 [((Binding.name Auto_Bind.thatN, []), [(that, [])])]
             ||> Proof_Context.restore_stmt asms_ctxt
-
-          val stmt' = [
-              (Binding.empty_atts,
-              [(#2 (#1 (Obtain.obtain_thesis ctxt)), [])])
-            ]
+          val stmt' =
+            [(Binding.empty_atts, [(#2 (#1 (Obtain.obtain_thesis ctxt)), [])])]
         in
           ((Obtain.obtains_attribs raw_obtains, prems, stmt', SOME that'),
           that_ctxt)
@@ -65,23 +62,19 @@ fun define_proof_term name (local_name, [th]) lthy =
       let
         fun make_name_binding suffix local_name =
           let val base_local_name = Long_Name.base_name local_name
-          in
-            Binding.qualified_name
-              ((case base_local_name of
-                  "" => name
-                | _ => base_local_name)
-              ^(case suffix of
-                  SOME "prf" => "_prf"
-                | SOME "def" => "_def"
-                | _ => ""))
+          in Binding.qualified_name
+            ((case base_local_name of "" => name | _ => base_local_name) ^
+             (case suffix
+              of SOME "prf" => "_prf"
+              | SOME "def" => "_def"
+              | _ => ""))
           end
 
         val (prems, concl) =
           (Logic.strip_assums_hyp (Thm.prop_of th),
-          Logic.strip_assums_concl (Thm.prop_of th))
+           Logic.strip_assums_concl (Thm.prop_of th))
       in
-        if not (Lib.is_typing concl) then
-          ([], lthy)
+        if not (Lib.is_typing concl) then ([], lthy)
         else let
           val prems_vars = distinct Term.aconv (flat
             (map (Lib.collect_subterms is_Var) prems))
@@ -91,18 +84,16 @@ fun define_proof_term name (local_name, [th]) lthy =
 
           val params = inter Term.aconv concl_vars prems_vars
 
-          val prf_tm =
-            fold_rev lambda params (Lib.term_of_typing concl)
+          val prf_tm = fold_rev lambda params (Lib.term_of_typing concl)
 
           val ((_, (_, raw_def)), lthy') = Local_Theory.define
             ((make_name_binding NONE local_name, Mixfix.NoSyn),
             ((make_name_binding (SOME "prf") local_name, []), prf_tm)) lthy
 
-          val def =
-            fold
-              (fn th1 => fn th2 => Thm.combination th2 th1)
-              (map (Thm.reflexive o Thm.cterm_of lthy) params)
-              raw_def
+          val def = fold
+            (fn th1 => fn th2 => Thm.combination th2 th1)
+            (map (Thm.reflexive o Thm.cterm_of lthy) params)
+            raw_def
 
           val ((_, def'), lthy'') = Local_Theory.note
             ((make_name_binding (SOME "def") local_name, []), [def])
@@ -112,26 +103,26 @@ fun define_proof_term name (local_name, [th]) lthy =
         end
       end
   | define_proof_term _ _ _ = error
-      ("Unimplemented: handling proof terms of multiple facts in"
-      ^" single result")
+      ("Unimplemented: proof terms for multiple facts in one statement")
 
 fun gen_schematic_theorem
-      bundle_includes prep_att prep_stmt
-      gen_prf long kind before_qed after_qed (name, raw_atts)
-      raw_includes raw_elems raw_concl int lthy =
+  bundle_includes prep_att prep_stmt
+  gen_prf_tm long kind
+  before_qed after_qed
+  (name, raw_atts) raw_includes raw_elems raw_concl
+  do_print lthy
+  =
   let
-    val _ = Local_Theory.assert lthy;
-
+    val _ = Local_Theory.assert lthy
     val elems = raw_elems |> map (Element.map_ctxt_attrib (prep_att lthy))
     val ((more_atts, prems, stmt, facts), goal_ctxt) = lthy
       |> bundle_includes raw_includes
       |> prep_statement (prep_att lthy) prep_stmt elems raw_concl
     val atts = more_atts @ map (prep_att lthy) raw_atts
     val pos = Position.thread_data ()
-
     val prems_name = if long then Auto_Bind.assmsN else Auto_Bind.thatN
 
-    fun after_qed' results goal_ctxt' =
+    fun gen_and_after_qed results goal_ctxt' =
       let
         val results' = burrow
           (map (Goal.norm_result lthy) o Proof_Context.export goal_ctxt' lthy)
@@ -147,35 +138,34 @@ fun gen_schematic_theorem
             true)
 
         val (res', lthy'') =
-          if gen_prf
+          if gen_prf_tm
           then
             let
-              val (prf_tm_defs, lthy'') =
-                fold
-                  (fn result => fn (defs, lthy) =>
-                    apfst (fn new_defs => defs @ new_defs)
-                      (define_proof_term (Binding.name_of name) result lthy))
-                  res ([], lthy')
-  
+              val (prf_tm_defs, new_lthy) = fold
+                (fn result => fn (defs, lthy) =>
+                  apfst (fn new_defs => defs @ new_defs)
+                    (define_proof_term (Binding.name_of name) result lthy))
+                res
+                ([], lthy')
               val res_folded =
-                map (apsnd (map (Local_Defs.fold lthy'' prf_tm_defs))) res
+                map (apsnd (map (Local_Defs.fold new_lthy prf_tm_defs))) res
             in
               Local_Theory.notes_kind kind
                 [((name, @{attributes [typechk]} @ atts),
                   [(maps #2 res_folded, [])])]
-                lthy''
+                new_lthy
             end
           else
             Local_Theory.notes_kind kind
               [((name, atts), [(maps #2 res, [])])]
               lthy'
 
-        val _ = Proof_Display.print_results int pos lthy''
+        val _ = Proof_Display.print_results do_print pos lthy''
             ((kind, Binding.name_of name), map (fn (_, ths) => ("", ths)) res')
 
         val _ =
           if substmts then map
-            (fn (name, ths) => Proof_Display.print_results int pos lthy''
+            (fn (name, ths) => Proof_Display.print_results do_print pos lthy''
               (("and", name), [("", ths)]))
             res
           else []
@@ -186,7 +176,7 @@ fun gen_schematic_theorem
     goal_ctxt
     |> not (null prems) ?
       (Proof_Context.note_thmss "" [((Binding.name prems_name, []), [(prems, [])])] #> snd)
-    |> Proof.theorem before_qed after_qed' (map snd stmt)
+    |> Proof.theorem before_qed gen_and_after_qed (map snd stmt)
     |> (case facts of NONE => I | SOME ths => Proof.refine_insert ths)
   end
 
@@ -197,13 +187,13 @@ val schematic_theorem_cmd =
     Expression.read_statement
 
 fun theorem spec descr =
-  Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr)
-    (Scan.option (Args.parens (Args.$$$ "derive"))
-    -- (long_statement || short_statement) >>
-      (fn (opt_derive, (long, binding, includes, elems, concl)) =>
-        schematic_theorem_cmd
-          (case opt_derive of SOME "derive" => true | _ => false)
-          long descr NONE (K I) binding includes elems concl))
+  Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr) 
+    ( Scan.option (Args.parens (Args.$$$ "derive"))
+      -- (long_statement || short_statement) >>
+        (fn (opt_derive, (long, binding, includes, elems, concl)) =>
+          schematic_theorem_cmd
+            (case opt_derive of SOME "derive" => true | _ => false)
+            long descr NONE (K I) binding includes elems concl) )
 
 fun definition spec descr =
   Outer_Syntax.local_theory_to_proof' spec "definition via proof"
@@ -211,7 +201,6 @@ fun definition spec descr =
       (fn (long, binding, includes, elems, concl) => schematic_theorem_cmd
         true long descr NONE (K I) binding includes elems concl))
 
-
 in
 
 val _ = theorem \<^command_keyword>\<open>Theorem\<close> "Theorem"