aboutsummaryrefslogtreecommitdiff
path: root/spartan
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--mltt/core/MLTT.thy (renamed from spartan/core/Spartan.thy)20
-rw-r--r--mltt/core/calc.ML (renamed from spartan/core/calc.ML)0
-rw-r--r--mltt/core/cases.ML (renamed from spartan/core/cases.ML)0
-rw-r--r--mltt/core/comp.ML (renamed from spartan/core/comp.ML)0
-rw-r--r--mltt/core/context_facts.ML (renamed from spartan/core/context_facts.ML)0
-rw-r--r--mltt/core/context_tactical.ML (renamed from spartan/core/context_tactical.ML)0
-rw-r--r--mltt/core/elaborated_statement.ML (renamed from spartan/core/elaborated_statement.ML)0
-rw-r--r--mltt/core/elaboration.ML (renamed from spartan/core/elaboration.ML)0
-rw-r--r--mltt/core/elimination.ML (renamed from spartan/core/elimination.ML)0
-rw-r--r--mltt/core/eqsubst.ML (renamed from spartan/core/eqsubst.ML)0
-rw-r--r--mltt/core/focus.ML (renamed from spartan/core/focus.ML)0
-rw-r--r--mltt/core/goals.ML (renamed from spartan/core/goals.ML)0
-rw-r--r--mltt/core/implicits.ML (renamed from spartan/core/implicits.ML)0
-rw-r--r--mltt/core/lib.ML (renamed from spartan/core/lib.ML)0
-rw-r--r--mltt/core/tactics.ML (renamed from spartan/core/tactics.ML)2
-rw-r--r--mltt/core/types.ML (renamed from spartan/core/types.ML)0
-rw-r--r--mltt/lib/List.thy (renamed from spartan/lib/List.thy)0
-rw-r--r--mltt/lib/Maybe.thy (renamed from spartan/lib/Maybe.thy)0
-rw-r--r--mltt/lib/Prelude.thy (renamed from spartan/lib/Prelude.thy)4
-rw-r--r--spartan/core/equality.ML90
20 files changed, 13 insertions, 103 deletions
diff --git a/spartan/core/Spartan.thy b/mltt/core/MLTT.thy
index 5046b6a..18bd2b7 100644
--- a/spartan/core/Spartan.thy
+++ b/mltt/core/MLTT.thy
@@ -1,6 +1,4 @@
-text \<open>Spartan type theory\<close>
-
-theory Spartan
+theory MLTT
imports
Pure
"HOL-Eisbach.Eisbach"
@@ -511,14 +509,14 @@ Lemma snd_comp [comp]:
subsection \<open>Notation\<close>
definition fst_i ("fst")
- where [implicit]: "fst \<equiv> Spartan.fst {} {}"
+ where [implicit]: "fst \<equiv> MLTT.fst {} {}"
definition snd_i ("snd")
- where [implicit]: "snd \<equiv> Spartan.snd {} {}"
+ where [implicit]: "snd \<equiv> MLTT.snd {} {}"
translations
- "fst" \<leftharpoondown> "CONST Spartan.fst A B"
- "snd" \<leftharpoondown> "CONST Spartan.snd A B"
+ "fst" \<leftharpoondown> "CONST MLTT.fst A B"
+ "snd" \<leftharpoondown> "CONST MLTT.snd A B"
subsection \<open>Projections\<close>
@@ -541,10 +539,10 @@ method snd for p::o = rule snd[where ?p=p]
text \<open>Double projections:\<close>
-definition [implicit]: "p\<^sub>1\<^sub>1 p \<equiv> Spartan.fst {} {} (Spartan.fst {} {} p)"
-definition [implicit]: "p\<^sub>1\<^sub>2 p \<equiv> Spartan.snd {} {} (Spartan.fst {} {} p)"
-definition [implicit]: "p\<^sub>2\<^sub>1 p \<equiv> Spartan.fst {} {} (Spartan.snd {} {} p)"
-definition [implicit]: "p\<^sub>2\<^sub>2 p \<equiv> Spartan.snd {} {} (Spartan.snd {} {} p)"
+definition [implicit]: "p\<^sub>1\<^sub>1 p \<equiv> MLTT.fst {} {} (MLTT.fst {} {} p)"
+definition [implicit]: "p\<^sub>1\<^sub>2 p \<equiv> MLTT.snd {} {} (MLTT.fst {} {} p)"
+definition [implicit]: "p\<^sub>2\<^sub>1 p \<equiv> MLTT.fst {} {} (MLTT.snd {} {} p)"
+definition [implicit]: "p\<^sub>2\<^sub>2 p \<equiv> MLTT.snd {} {} (MLTT.snd {} {} p)"
translations
"CONST p\<^sub>1\<^sub>1 p" \<leftharpoondown> "fst (fst p)"
diff --git a/spartan/core/calc.ML b/mltt/core/calc.ML
index 67dc7fc..67dc7fc 100644
--- a/spartan/core/calc.ML
+++ b/mltt/core/calc.ML
diff --git a/spartan/core/cases.ML b/mltt/core/cases.ML
index 560a9f1..560a9f1 100644
--- a/spartan/core/cases.ML
+++ b/mltt/core/cases.ML
diff --git a/spartan/core/comp.ML b/mltt/core/comp.ML
index 2e50753..2e50753 100644
--- a/spartan/core/comp.ML
+++ b/mltt/core/comp.ML
diff --git a/spartan/core/context_facts.ML b/mltt/core/context_facts.ML
index 5aa7c70..5aa7c70 100644
--- a/spartan/core/context_facts.ML
+++ b/mltt/core/context_facts.ML
diff --git a/spartan/core/context_tactical.ML b/mltt/core/context_tactical.ML
index d0fed61..d0fed61 100644
--- a/spartan/core/context_tactical.ML
+++ b/mltt/core/context_tactical.ML
diff --git a/spartan/core/elaborated_statement.ML b/mltt/core/elaborated_statement.ML
index 33f88cf..33f88cf 100644
--- a/spartan/core/elaborated_statement.ML
+++ b/mltt/core/elaborated_statement.ML
diff --git a/spartan/core/elaboration.ML b/mltt/core/elaboration.ML
index 9e5e0bd..9e5e0bd 100644
--- a/spartan/core/elaboration.ML
+++ b/mltt/core/elaboration.ML
diff --git a/spartan/core/elimination.ML b/mltt/core/elimination.ML
index cf9d21e..cf9d21e 100644
--- a/spartan/core/elimination.ML
+++ b/mltt/core/elimination.ML
diff --git a/spartan/core/eqsubst.ML b/mltt/core/eqsubst.ML
index 5ae8c73..5ae8c73 100644
--- a/spartan/core/eqsubst.ML
+++ b/mltt/core/eqsubst.ML
diff --git a/spartan/core/focus.ML b/mltt/core/focus.ML
index b963cfe..b963cfe 100644
--- a/spartan/core/focus.ML
+++ b/mltt/core/focus.ML
diff --git a/spartan/core/goals.ML b/mltt/core/goals.ML
index 7d52495..7d52495 100644
--- a/spartan/core/goals.ML
+++ b/mltt/core/goals.ML
diff --git a/spartan/core/implicits.ML b/mltt/core/implicits.ML
index 2b63f49..2b63f49 100644
--- a/spartan/core/implicits.ML
+++ b/mltt/core/implicits.ML
diff --git a/spartan/core/lib.ML b/mltt/core/lib.ML
index e43ad98..e43ad98 100644
--- a/spartan/core/lib.ML
+++ b/mltt/core/lib.ML
diff --git a/spartan/core/tactics.ML b/mltt/core/tactics.ML
index 923a3a7..6876d5c 100644
--- a/spartan/core/tactics.ML
+++ b/mltt/core/tactics.ML
@@ -129,7 +129,7 @@ fun elim_ctac tms =
|> filter (fn (_, i) => i > 0)
(*`t1: T1` comes before `t2: T2` if T1 contains t2 as subterm.
If they are incomparable, then order by decreasing
- `subterm_count [p, x, y] T`*)
+ `subterm_count_distinct tms T`*)
|> sort (fn (((t1, _), i), ((_, T2), j)) =>
Lib.cond_order (Lib.subterm_order T2 t1) (int_ord (j, i)))
|> map (#1 o #1)
diff --git a/spartan/core/types.ML b/mltt/core/types.ML
index 5e0d484..5e0d484 100644
--- a/spartan/core/types.ML
+++ b/mltt/core/types.ML
diff --git a/spartan/lib/List.thy b/mltt/lib/List.thy
index 4beb9b6..4beb9b6 100644
--- a/spartan/lib/List.thy
+++ b/mltt/lib/List.thy
diff --git a/spartan/lib/Maybe.thy b/mltt/lib/Maybe.thy
index 452acc2..452acc2 100644
--- a/spartan/lib/Maybe.thy
+++ b/mltt/lib/Maybe.thy
diff --git a/spartan/lib/Prelude.thy b/mltt/lib/Prelude.thy
index 56adbfc..0393968 100644
--- a/spartan/lib/Prelude.thy
+++ b/mltt/lib/Prelude.thy
@@ -1,5 +1,5 @@
theory Prelude
-imports Spartan
+imports MLTT
begin
@@ -84,6 +84,8 @@ lemmas
[elim ?x] = BotE and
[comp] = Top_comp
+abbreviation (input) Not ("\<not>_" [1000] 1000) where "\<not>A \<equiv> A \<rightarrow> \<bottom>"
+
section \<open>Booleans\<close>
diff --git a/spartan/core/equality.ML b/spartan/core/equality.ML
deleted file mode 100644
index 023147b..0000000
--- a/spartan/core/equality.ML
+++ /dev/null
@@ -1,90 +0,0 @@
-(* Title: equality.ML
- Author: Joshua Chen
-
-Equality reasoning with identity types.
-*)
-
-structure Equality:
-sig
-
-val dest_Id: term -> term * term * term
-
-val push_hyp_tac: term * term -> Proof.context -> int -> tactic
-val induction_tac: term -> term -> term -> term -> Proof.context -> tactic
-val equality_context_tac: Facts.ref -> Proof.context -> context_tactic
-
-end = struct
-
-fun dest_Id tm = case tm of
- Const (\<^const_name>\<open>Id\<close>, _) $ A $ x $ y => (A, x, y)
- | _ => error "dest_Id"
-
-(*Context assumptions that have already been pushed into the type family*)
-structure Inserts = Proof_Data (
- type T = term Item_Net.T
- val init = K (Item_Net.init Term.aconv_untyped single)
-)
-
-fun push_hyp_tac (t, _) =
- Subgoal.FOCUS_PARAMS (fn {context = ctxt, concl, ...} =>
- let
- val (_, C) = Lib.dest_typing (Thm.term_of concl)
- val B = Thm.cterm_of ctxt (Lib.lambda_var t C)
- val a = Thm.cterm_of ctxt t
- (*The resolvent is PiE[where ?B=B and ?a=a]*)
- val resolvent =
- Drule.infer_instantiate' ctxt [NONE, NONE, SOME B, SOME a] @{thm PiE}
- in
- HEADGOAL (resolve_tac ctxt [resolvent])
- THEN SOMEGOAL (known_tac ctxt)
- end)
-
-fun induction_tac p A x y ctxt =
- let
- val [p, A, x, y] = map (Thm.cterm_of ctxt) [p, A, x, y]
- in
- HEADGOAL (resolve_tac ctxt
- [Drule.infer_instantiate' ctxt [SOME p, SOME A, SOME x, SOME y] @{thm IdE}])
- end
-
-val side_conds_tac = TRY oo typechk_tac
-
-fun equality_context_tac fact ctxt =
- let
- val eq_th = Proof_Context.get_fact_single ctxt fact
- val (p, (A, x, y)) = (Lib.dest_typing ##> dest_Id) (Thm.prop_of eq_th)
-
- val hyps =
- Facts.props (Proof_Context.facts_of ctxt)
- |> filter (fn (th, _) => Lib.is_typing (Thm.prop_of th))
- |> map (Lib.dest_typing o Thm.prop_of o fst)
- |> filter_out (fn (t, _) =>
- Term.aconv (t, p) orelse Item_Net.member (Inserts.get ctxt) t)
- |> map (fn (t, T) => ((t, T), Lib.subterm_count_distinct [p, x, y] T))
- |> filter (fn (_, i) => i > 0)
- (*`t1: T1` comes before `t2: T2` if T1 contains t2 as subterm.
- If they are incomparable, then order by decreasing
- `subterm_count [p, x, y] T`*)
- |> sort (fn (((t1, _), i), ((_, T2), j)) =>
- Lib.cond_order (Lib.subterm_order T2 t1) (int_ord (j, i)))
- |> map #1
-
- val record_inserts =
- Inserts.map (fold (fn (t, _) => fn net => Item_Net.update t net) hyps)
-
- val tac =
- fold (fn hyp => fn tac => tac THEN HEADGOAL (push_hyp_tac hyp ctxt))
- hyps all_tac
- THEN (
- induction_tac p A x y ctxt
- THEN RANGE (replicate 3 (typechk_tac ctxt) @ [side_conds_tac ctxt]) 1
- )
- THEN (
- REPEAT_DETERM_N (length hyps) (SOMEGOAL (resolve_tac ctxt @{thms PiI}))
- THEN ALLGOALS (side_conds_tac ctxt)
- )
- in
- fn (ctxt, st) => Context_Tactic.TACTIC_CONTEXT (record_inserts ctxt) (tac st)
- end
-
-end
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-06 10:36:00 +0000