diff options
| -rw-r--r-- | README.md | 6 | ||||
| -rw-r--r-- | ROOT | 1 | ||||
| -rw-r--r-- | hott/Nat.thy | 22 | ||||
| -rw-r--r-- | spartan/lib/equality.ML | 2 | ||||
| -rw-r--r-- | spartan/lib/goals.ML | 2 |
5 files changed, 19 insertions, 14 deletions
@@ -4,11 +4,11 @@ An experimental implementation of [homotopy type theory](https://en.wikipedia.or ### Usage -Isabelle/HoTT is compatible with Isabelle2019. -To use, add the Isabelle/HoTT folder path to `.isabelle/Isabelle2019/ROOTS` (on cygwin/Mac/Linux installations): +Isabelle/HoTT is compatible with Isabelle2020. +To use, add the Isabelle/HoTT folder path to `.isabelle/Isabelle2020/ROOTS` (on Mac/Linux/cygwin installations): ``` -echo path/to/Isabelle/HoTT >> ~/.isabelle/Isabelle2019/ROOTS +echo path/to/Isabelle/HoTT >> ~/.isabelle/Isabelle2020/ROOTS ``` ### What (and why) is this? @@ -22,3 +22,4 @@ session HoTT in hott = Spartan + theories Base Nat + diff --git a/hott/Nat.thy b/hott/Nat.thy index b88398b..59ec517 100644 --- a/hott/Nat.thy +++ b/hott/Nat.thy @@ -17,39 +17,43 @@ where NatE: "\<lbrakk> n: Nat; - n\<^sub>0: C 0; + c\<^sub>0: C 0; \<And>n. n: Nat \<Longrightarrow> C n: U i; \<And>k c. \<lbrakk>k: Nat; c: C k\<rbrakk> \<Longrightarrow> f k c: C (suc k) - \<rbrakk> \<Longrightarrow> NatInd (\<lambda>n. C n) n\<^sub>0 (\<lambda>k c. f k c) n: C n" and + \<rbrakk> \<Longrightarrow> NatInd (\<lambda>n. C n) c\<^sub>0 (\<lambda>k c. f k c) n: C n" and Nat_comp_zero: "\<lbrakk> - n\<^sub>0: C 0; + c\<^sub>0: C 0; \<And>k c. \<lbrakk>k: Nat; c: C k\<rbrakk> \<Longrightarrow> f k c: C (suc k); \<And>n. n: Nat \<Longrightarrow> C n: U i - \<rbrakk> \<Longrightarrow> NatInd (\<lambda>n. C n) n\<^sub>0 (\<lambda>k c. f k c) 0 \<equiv> n\<^sub>0" and + \<rbrakk> \<Longrightarrow> NatInd (\<lambda>n. C n) c\<^sub>0 (\<lambda>k c. f k c) 0 \<equiv> c\<^sub>0" and Nat_comp_suc: "\<lbrakk> n: Nat; - n\<^sub>0: C 0; + c\<^sub>0: C 0; \<And>k c. \<lbrakk>k: Nat; c: C k\<rbrakk> \<Longrightarrow> f k c: C (suc k); \<And>n. n: Nat \<Longrightarrow> C n: U i \<rbrakk> \<Longrightarrow> - NatInd (\<lambda>n. C n) n\<^sub>0 (\<lambda>k c. f k c) (suc n) \<equiv> - f n (NatInd (\<lambda>n. C n) n\<^sub>0 (\<lambda>k c. f k c) n)" + NatInd (\<lambda>n. C n) c\<^sub>0 (\<lambda>k c. f k c) (suc n) \<equiv> + f n (NatInd (\<lambda>n. C n) c\<^sub>0 (\<lambda>k c. f k c) n)" lemmas [intros] = NatF Nat_zero Nat_suc and [elims] = NatE and [comps] = Nat_comp_zero Nat_comp_suc +text \<open>Non-dependent recursion\<close> + +abbreviation "NatRec C \<equiv> NatInd (K C)" + section \<open>Basic arithmetic\<close> definition add (infixl "+" 50) where - [comps]: "m + n \<equiv> NatInd (K Nat) n (K suc) m" + [comps]: "m + n \<equiv> NatRec Nat n (K suc) m" definition mul (infixl "*" 55) where - [comps]: "m * n \<equiv> NatInd (K Nat) 0 (K $ add n) m" + [comps]: "m * n \<equiv> NatRec Nat 0 (K $ add n) m" end diff --git a/spartan/lib/equality.ML b/spartan/lib/equality.ML index 79b4086..023147b 100644 --- a/spartan/lib/equality.ML +++ b/spartan/lib/equality.ML @@ -84,7 +84,7 @@ fun equality_context_tac fact ctxt = THEN ALLGOALS (side_conds_tac ctxt) ) in - fn (ctxt, st) => Method.CONTEXT (record_inserts ctxt) (tac st) + fn (ctxt, st) => Context_Tactic.TACTIC_CONTEXT (record_inserts ctxt) (tac st) end end diff --git a/spartan/lib/goals.ML b/spartan/lib/goals.ML index ce23751..9f394f0 100644 --- a/spartan/lib/goals.ML +++ b/spartan/lib/goals.ML @@ -31,7 +31,7 @@ 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 (Variable.auto_fixes o fst) o snd) + val stmt_ctxt = fold (fold (Proof_Context.augment o fst) o snd) stmt elems_ctxt in case raw_stmt of |