(FEAT) Context data slots for known types and conditional type rules, as well as a separate one for judgmental equality rules.

(REF) Goal statement assumptions are now put into the new context data slots.

(FEAT) `assuming` Isar keyword—like `assume` but puts assumptions into context data.

(REF) Typechecking and all other tactics refactored to use type information from the context data, as opposed to looking at all facts visible in context.
  MINOR INCOMPATIBILITY: facts that were implicitly used in proofs now have to be annotated with [type] to make them visible throughout the context, else explicitly passed to methods via `using`, or declared with `assuming`.

(REF) Fixed incompatibilities in theories.

1 files changed, 16 insertions, 0 deletions

diff --git a/spartan/core/lib.ML b/spartan/core/lib.ML
index 392ae2e..e43ad98 100644
--- a/spartan/core/lib.ML
+++ b/spartan/core/lib.ML
@@ -27,6 +27,9 @@ val typing_of_term: term -> term
 val decompose_goal: Proof.context -> term -> term list * term
 val rigid_typing_concl: term -> bool
 
+(*Theorems*)
+val partition_judgments: thm list -> thm list * thm list * thm list
+
 (*Subterms*)
 val has_subterm: term list -> term -> bool
 val subterm_count: term -> term -> int
@@ -121,6 +124,19 @@ fun rigid_typing_concl goal =
   in is_typing concl andalso is_rigid (term_of_typing concl) end
 
 
+(** Theorems **)
+fun partition_judgments ths =
+  let
+    fun part [] facts conds eqs = (facts, conds, eqs)
+      | part (th::ths) facts conds eqs =
+          if is_typing (Thm.prop_of th) then
+            part ths (th::facts) conds eqs
+          else if is_typing (Thm.concl_of th) then
+            part ths facts (th::conds) eqs
+          else part ths facts conds (th::eqs)
+  in part ths [] [] [] end
+
+
 (** Subterms **)
 
 fun has_subterm tms =