(REF) Tweak attribute names in preparation for new logical introduction rule behavior

4 files changed, 21 insertions, 19 deletions

diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy
index 27edd51..180354c 100644
--- a/spartan/core/Spartan.thy
+++ b/spartan/core/Spartan.thy
@@ -188,16 +188,15 @@ ML_file \<open>context_tactical.ML\<close>
 
 subsection \<open>Type-checking/inference\<close>
 
-named_theorems form and intro and intros and comp and typechk
-\<comment> \<open>`intros` stores the introduction rule variants used by the
-  `intro` and `intros` methods.\<close>
+\<comment> \<open>Rule attributes for the type-checker\<close>
+named_theorems form and intr and comp and type
 
-ML_file \<open>elimination.ML\<close> \<comment> \<open>elimination rules\<close>
+\<comment> \<open>Defines elimination automation and the `elim` attribute\<close>
+ML_file \<open>elimination.ML\<close>  
 
 lemmas
   [form] = PiF SigF and
-  [intro] = PiI SigI and
-  [intros] = PiI[rotated] SigI and
+  [intr] = PiI SigI and
   [elim ?f] = PiE and
   [elim ?p] = SigE and
   [comp] = beta Sig_comp and
@@ -222,6 +221,10 @@ ML_file \<open>goals.ML\<close>
 
 subsection \<open>Proof methods\<close>
 
+named_theorems intro \<comment> \<open>Logical introduction rules\<close>
+
+lemmas [intro] = PiI[rotated] SigI
+
 ML_file \<open>cases.ML\<close> \<comment> \<open>case reasoning rules\<close>
 ML_file \<open>tactics.ML\<close>
 
@@ -394,7 +397,7 @@ syntax
 translations
   "g \<circ>\<^bsub>A\<^esub> f" \<rightleftharpoons> "CONST funcomp A g f"
 
-lemma funcompI [typechk]:
+lemma funcompI [type]:
   assumes
     "A: U i"
     "B: U i"
@@ -444,7 +447,7 @@ subsection \<open>Identity function\<close>
 abbreviation id where "id A \<equiv> \<lambda>x: A. x"
 
 lemma
-  id_type [typechk]: "A: U i \<Longrightarrow> id A: A \<rightarrow> A" and
+  id_type [type]: "A: U i \<Longrightarrow> id A: A \<rightarrow> A" and
   id_comp [comp]: "x: A \<Longrightarrow> (id A) x \<equiv> x" \<comment> \<open>for the occasional manual rewrite\<close>
   by reduce+
 
@@ -458,7 +461,7 @@ lemma id_right [comp]:
   shows "f \<circ>\<^bsub>A\<^esub> (id A) \<equiv> f"
   by (subst eta_exp[of f]) (reduce, rule eta)
 
-lemma id_U [typechk]:
+lemma id_U [type]:
   "id (U i): U i \<rightarrow> U i"
   using Ui_in_USi by typechk
 
@@ -468,7 +471,7 @@ section \<open>Pairs\<close>
 definition "fst A B \<equiv> \<lambda>p: \<Sum>x: A. B x. SigInd A B (fn _. A) (fn x y. x) p"
 definition "snd A B \<equiv> \<lambda>p: \<Sum>x: A. B x. SigInd A B (fn p. B (fst A B p)) (fn x y. y) p"
 
-lemma fst_type [typechk]:
+lemma fst_type [type]:
   assumes "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i"
   shows "fst A B: (\<Sum>x: A. B x) \<rightarrow> A"
   unfolding fst_def by typechk
@@ -479,7 +482,7 @@ lemma fst_comp [comp]:
   shows "fst A B <a, b> \<equiv> a"
   unfolding fst_def by reduce
 
-lemma snd_type [typechk]:
+lemma snd_type [type]:
   assumes "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i"
   shows "snd A B: \<Prod>p: \<Sum>x: A. B x. B (fst A B p)"
   unfolding snd_def by typechk reduce
@@ -503,14 +506,14 @@ translations
 
 subsection \<open>Projections\<close>
 
-Lemma fst [typechk]:
+Lemma fst [type]:
   assumes
     "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i"
     "p: \<Sum>x: A. B x"
   shows "fst p: A"
   by typechk
 
-Lemma snd [typechk]:
+Lemma snd [type]:
   assumes
     "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i"
     "p: \<Sum>x: A. B x"
diff --git a/spartan/core/goals.ML b/spartan/core/goals.ML
index 540f5c7..a04bd0e 100644
--- a/spartan/core/goals.ML
+++ b/spartan/core/goals.ML
@@ -151,7 +151,7 @@ fun gen_schematic_theorem
                 map (apsnd (map (Local_Defs.fold new_lthy prf_tm_defs))) res
             in
               Local_Theory.notes_kind kind
-                [((name, @{attributes [typechk]} @ atts),
+                [((name, @{attributes [type]} @ atts),
                   [(maps #2 res_folded, [])])]
                 new_lthy
             end
diff --git a/spartan/core/tactics.ML b/spartan/core/tactics.ML
index 19d3d71..959050e 100644
--- a/spartan/core/tactics.ML
+++ b/spartan/core/tactics.ML
@@ -57,7 +57,7 @@ end
 
 (*Applies some introduction rule*)
 fun intro_ctac i (ctxt, st) = TACTIC_CONTEXT ctxt (resolve_tac ctxt
-  (Named_Theorems.get ctxt \<^named_theorems>\<open>intros\<close>) i st)
+  (Named_Theorems.get ctxt \<^named_theorems>\<open>intro\<close>) i st)
 
 
 (* Induction/elimination *)
diff --git a/spartan/core/typechecking.ML b/spartan/core/typechecking.ML
index a6e1726..b7a7f9b 100644
--- a/spartan/core/typechecking.ML
+++ b/spartan/core/typechecking.ML
@@ -37,8 +37,7 @@ fun put_types typings = foldr1 (op o) (map put_type typings)
 
 (* Context tactics for type-checking *)
 
-val debug_typechk =
-  Attrib.setup_config_bool \<^binding>\<open>debug_typechk\<close> (K false)
+val debug_typechk = Attrib.setup_config_bool \<^binding>\<open>debug_typechk\<close> (K false)
 
 fun debug_tac ctxt s =
   if Config.get ctxt debug_typechk then print_tac ctxt s else all_tac
@@ -73,9 +72,9 @@ fun check_infer_step facts i (ctxt, st) =
           map (Simplifier.norm_hhf ctxt) facts
           (*MAYBE FIXME: Remove `typechk` from this list, and instead perform
             definitional unfolding to (w?)hnf.*)
-          @(Named_Theorems.get ctxt \<^named_theorems>\<open>typechk\<close>)
+          @(Named_Theorems.get ctxt \<^named_theorems>\<open>type\<close>)
           @(Named_Theorems.get ctxt \<^named_theorems>\<open>form\<close>)
-          @(Named_Theorems.get ctxt \<^named_theorems>\<open>intro\<close>)
+          @(Named_Theorems.get ctxt \<^named_theorems>\<open>intr\<close>)
           @(map #1 (Elim.rules ctxt)))
         in (resolve_from_net_tac ctxt net) i end
       else no_tac)