aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--hott/Equivalence.thy32
-rw-r--r--hott/Identity.thy4
-rw-r--r--hott/Nat.thy6
-rw-r--r--spartan/core/Spartan.thy29
-rw-r--r--spartan/core/goals.ML2
-rw-r--r--spartan/core/tactics.ML2
-rw-r--r--spartan/core/typechecking.ML7
-rw-r--r--spartan/lib/List.thy10
-rw-r--r--spartan/lib/Maybe.thy2
-rw-r--r--spartan/lib/Prelude.thy8
10 files changed, 52 insertions, 50 deletions
diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy
index 66c64f6..619ed84 100644
--- a/hott/Equivalence.thy
+++ b/hott/Equivalence.thy
@@ -12,7 +12,7 @@ definition homotopy_i (infix "~" 100)
translations "f ~ g" \<leftharpoondown> "CONST homotopy A B f g"
-Lemma homotopy_type [typechk]:
+Lemma homotopy_type [type]:
assumes
"A: U i"
"\<And>x. x: A \<Longrightarrow> B x: U i"
@@ -161,7 +161,7 @@ subsection \<open>Quasi-inverses\<close>
definition "is_qinv A B f \<equiv> \<Sum>g: B \<rightarrow> A.
homotopy A (fn _. A) (g \<circ>\<^bsub>A\<^esub> f) (id A) \<times> homotopy B (fn _. B) (f \<circ>\<^bsub>B\<^esub> g) (id B)"
-lemma is_qinv_type [typechk]:
+lemma is_qinv_type [type]:
assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
shows "is_qinv A B f: U i"
unfolding is_qinv_def
@@ -193,12 +193,12 @@ Lemma is_qinvI:
show "g \<circ> f ~ id A \<and> f \<circ> g ~ id B" by (intro; fact)
qed
-Lemma is_qinv_components [typechk]:
+Lemma is_qinv_components [type]:
assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "pf: is_qinv f"
shows
- fst_of_is_qinv: "fst pf: B \<rightarrow> A" and
- p\<^sub>2\<^sub>1_of_is_qinv: "p\<^sub>2\<^sub>1 pf: fst pf \<circ> f ~ id A" and
- p\<^sub>2\<^sub>2_of_is_qinv: "p\<^sub>2\<^sub>2 pf: f \<circ> fst pf ~ id B"
+ qinv_of_is_qinv: "fst pf: B \<rightarrow> A" and
+ ret_of_is_qinv: "p\<^sub>2\<^sub>1 pf: fst pf \<circ> f ~ id A" and
+ sec_of_is_qinv: "p\<^sub>2\<^sub>2 pf: f \<circ> fst pf ~ id B"
using assms unfolding is_qinv_def
by typechk+
@@ -211,8 +211,8 @@ using [[debug_typechk]]
back \<comment> \<open>Typechecking/inference goes too far here. Problem would likely be
solved with definitional unfolding\<close>
\<^item> by (fact \<open>f:_\<close>)
- \<^item> by (rule p\<^sub>2\<^sub>2_of_is_qinv)
- \<^item> by (rule p\<^sub>2\<^sub>1_of_is_qinv)
+ \<^item> by (rule sec_of_is_qinv)
+ \<^item> by (rule ret_of_is_qinv)
done
Lemma (def) funcomp_is_qinv:
@@ -251,7 +251,7 @@ definition "is_biinv A B f \<equiv>
(\<Sum>g: B \<rightarrow> A. homotopy A (fn _. A) (g \<circ>\<^bsub>A\<^esub> f) (id A))
\<times> (\<Sum>g: B \<rightarrow> A. homotopy B (fn _. B) (f \<circ>\<^bsub>B\<^esub> g) (id B))"
-lemma is_biinv_type [typechk]:
+lemma is_biinv_type [type]:
assumes "A: U i" "B: U i" "f: A \<rightarrow> B"
shows "is_biinv A B f: U i"
unfolding is_biinv_def by typechk
@@ -273,13 +273,13 @@ Lemma is_biinvI:
show "<h, H2>: {}" by typechk
qed
-Lemma is_biinv_components [typechk]:
+Lemma is_biinv_components [type]:
assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "pf: is_biinv f"
shows
- p\<^sub>1\<^sub>1_of_is_biinv: "p\<^sub>1\<^sub>1 pf: B \<rightarrow> A" and
- p\<^sub>2\<^sub>1_of_is_biinv: "p\<^sub>2\<^sub>1 pf: B \<rightarrow> A" and
- p\<^sub>1\<^sub>2_of_is_biinv: "p\<^sub>1\<^sub>2 pf: p\<^sub>1\<^sub>1 pf \<circ> f ~ id A" and
- p\<^sub>2\<^sub>2_of_is_biinv: "p\<^sub>2\<^sub>2 pf: f \<circ> p\<^sub>2\<^sub>1 pf ~ id B"
+ section_of_is_biinv: "p\<^sub>1\<^sub>1 pf: B \<rightarrow> A" and
+ retraction_of_is_biinv: "p\<^sub>2\<^sub>1 pf: B \<rightarrow> A" and
+ ret_of_is_biinv: "p\<^sub>1\<^sub>2 pf: p\<^sub>1\<^sub>1 pf \<circ> f ~ id A" and
+ sec_of_is_biinv: "p\<^sub>2\<^sub>2 pf: f \<circ> p\<^sub>2\<^sub>1 pf ~ id B"
using assms unfolding is_biinv_def
by typechk+
@@ -350,7 +350,7 @@ text \<open>
definition equivalence (infix "\<simeq>" 110)
where "A \<simeq> B \<equiv> \<Sum>f: A \<rightarrow> B. Equivalence.is_biinv A B f"
-lemma equivalence_type [typechk]:
+lemma equivalence_type [type]:
assumes "A: U i" "B: U i"
shows "A \<simeq> B: U i"
unfolding equivalence_def by typechk
@@ -376,7 +376,7 @@ Lemma (def) equivalence_symmetric:
apply elim
apply (dest (4) is_biinv_imp_is_qinv)
apply intro
- \<^item> by (rule fst_of_is_qinv) facts
+ \<^item> by (rule qinv_of_is_qinv) facts
\<^item> by (rule is_qinv_imp_is_biinv) (rule qinv_is_qinv)
done
diff --git a/hott/Identity.thy b/hott/Identity.thy
index d6efbf8..b9ebafb 100644
--- a/hott/Identity.thy
+++ b/hott/Identity.thy
@@ -41,7 +41,7 @@ axiomatization where
lemmas
[form] = IdF and
- [intro, intros] = IdI and
+ [intr, intro] = IdI and
[elim ?p ?a ?b] = IdE and
[comp] = Id_comp and
[refl] = IdI
@@ -567,7 +567,7 @@ interpretation \<Omega>2:
notation \<Omega>2.horiz_pathcomp (infix "\<star>" 121)
notation \<Omega>2.horiz_pathcomp' (infix "\<star>''" 121)
-Lemma [typechk]:
+Lemma [type]:
assumes "\<alpha>: \<Omega>2 A a" and "\<beta>: \<Omega>2 A a"
shows horiz_pathcomp_type: "\<alpha> \<star> \<beta>: \<Omega>2 A a"
and horiz_pathcomp'_type: "\<alpha> \<star>' \<beta>: \<Omega>2 A a"
diff --git a/hott/Nat.thy b/hott/Nat.thy
index fd567f3..716703a 100644
--- a/hott/Nat.thy
+++ b/hott/Nat.thy
@@ -39,7 +39,7 @@ where
lemmas
[form] = NatF and
- [intro, intros] = Nat_zero Nat_suc and
+ [intr, intro] = Nat_zero Nat_suc and
[elim "?n"] = NatE and
[comp] = Nat_comp_zero Nat_comp_suc
@@ -62,7 +62,7 @@ subsection \<open>Addition\<close>
definition add (infixl "+" 120) where "m + n \<equiv> NatRec Nat m (K suc) n"
-lemma add_type [typechk]:
+lemma add_type [type]:
assumes "m: Nat" "n: Nat"
shows "m + n: Nat"
unfolding add_def by typechk
@@ -123,7 +123,7 @@ subsection \<open>Multiplication\<close>
definition mul (infixl "*" 121) where "m * n \<equiv> NatRec Nat 0 (K $ add m) n"
-lemma mul_type [typechk]:
+lemma mul_type [type]:
assumes "m: Nat" "n: Nat"
shows "m * n: Nat"
unfolding mul_def by typechk
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)
diff --git a/spartan/lib/List.thy b/spartan/lib/List.thy
index 34873e4..dd51582 100644
--- a/spartan/lib/List.thy
+++ b/spartan/lib/List.thy
@@ -45,7 +45,7 @@ where
lemmas
[form] = ListF and
- [intro, intros] = List_nil List_cons and
+ [intr, intro] = List_nil List_cons and
[elim "?xs"] = ListE and
[comp] = List_comp_nil List_comp_cons
@@ -106,7 +106,7 @@ translations
"head" \<leftharpoondown> "CONST List.head A"
"tail" \<leftharpoondown> "CONST List.tail A"
-Lemma head_type [typechk]:
+Lemma head_type [type]:
assumes "A: U i" "xs: List A"
shows "head xs: Maybe A"
unfolding head_def by typechk
@@ -116,7 +116,7 @@ Lemma head_of_cons [comp]:
shows "head (x # xs) \<equiv> some x"
unfolding head_def by reduce
-Lemma tail_type [typechk]:
+Lemma tail_type [type]:
assumes "A: U i" "xs: List A"
shows "tail xs: List A"
unfolding tail_def by typechk
@@ -157,7 +157,7 @@ definition map_i ("map") where [implicit]: "map \<equiv> List.map ? ?"
translations "map" \<leftharpoondown> "CONST List.map A B"
-Lemma map_type [typechk]:
+Lemma map_type [type]:
assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "xs: List A"
shows "map f xs: List B"
unfolding map_def by typechk
@@ -177,7 +177,7 @@ definition rev_i ("rev") where [implicit]: "rev \<equiv> List.rev ?"
translations "rev" \<leftharpoondown> "CONST List.rev A"
-Lemma rev_type [typechk]:
+Lemma rev_type [type]:
assumes "A: U i" "xs: List A"
shows "rev xs: List A"
unfolding rev_def by typechk
diff --git a/spartan/lib/Maybe.thy b/spartan/lib/Maybe.thy
index a2e1638..0a7ec21 100644
--- a/spartan/lib/Maybe.thy
+++ b/spartan/lib/Maybe.thy
@@ -56,7 +56,7 @@ Lemma Maybe_comp_some:
lemmas
[form] = MaybeF and
- [intro, intros] = Maybe_none Maybe_some and
+ [intr, intro] = Maybe_none Maybe_some and
[comp] = Maybe_comp_none Maybe_comp_some and
MaybeE [elim "?m"] = MaybeInd[rotated 4]
lemmas
diff --git a/spartan/lib/Prelude.thy b/spartan/lib/Prelude.thy
index 36f12d2..6adbce8 100644
--- a/spartan/lib/Prelude.thy
+++ b/spartan/lib/Prelude.thy
@@ -43,8 +43,8 @@ axiomatization where
lemmas
[form] = SumF and
- [intro] = Sum_inl Sum_inr and
- [intros] = Sum_inl[rotated] Sum_inr[rotated] and
+ [intr] = Sum_inl Sum_inr and
+ [intro] = Sum_inl[rotated] Sum_inr[rotated] and
[elim ?s] = SumE and
[comp] = Sum_comp_inl Sum_comp_inr
@@ -79,7 +79,7 @@ and
lemmas
[form] = TopF BotF and
- [intro, intros] = TopI and
+ [intr, intro] = TopI and
[elim ?a] = TopE and
[elim ?x] = BotE and
[comp] = Top_comp
@@ -129,7 +129,7 @@ Lemma if_false:
lemmas
[form] = BoolF and
- [intro, intros] = Bool_true Bool_false and
+ [intr, intro] = Bool_true Bool_false and
[comp] = if_true if_false and
[elim ?x] = ifelse
lemmas
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 10:50:07 +0000