diff options
author | Josh Chen | 2020-07-31 14:56:24 +0200 |
---|---|---|
committer | Josh Chen | 2020-07-31 14:56:24 +0200 |
commit | ff5454812f9e2720bd90c3a5437505644f63b487 (patch) | |
tree | 2df5f45de006c56391118db75e2f185036b02cd7 /hott/More_Nat.thy | |
parent | 2b0e14b16dcef0e829da95800b3c0af1975bb1ce (diff) |
(FEAT) Term elaboration of assumption and goal statements.
. spartan/core/goals.ML
. spartan/core/elaboration.ML
. spartan/core/elaborated_statement.ML
(FEAT) More context tacticals and search tacticals.
. spartan/core/context_tactical.ML
(FEAT) Improved subgoal focus.
Moves fully elaborated assumptions into the context (MINOR INCOMPATIBILITY).
. spartan/core/focus.ML
(FIX) Normalize facts in order to be able to resolve properly.
. spartan/core/typechecking.ML
(MAIN) New definitions.
(MAIN) Renamed theories and theorems.
(MAIN) Refactor theories to fit new features.
Diffstat (limited to 'hott/More_Nat.thy')
-rw-r--r-- | hott/More_Nat.thy | 43 |
1 files changed, 0 insertions, 43 deletions
diff --git a/hott/More_Nat.thy b/hott/More_Nat.thy deleted file mode 100644 index 59c8d54..0000000 --- a/hott/More_Nat.thy +++ /dev/null @@ -1,43 +0,0 @@ -theory More_Nat -imports Nat Spartan.More_Types - -begin - -section \<open>Equality on Nat\<close> - -text \<open>Via the encode-decode method.\<close> - -context begin - -Lemma (derive) eq: shows "Nat \<rightarrow> Nat \<rightarrow> U O" - apply intro focus vars m apply elim - \<comment> \<open>m \<equiv> 0\<close> - apply intro focus vars n apply elim - \<guillemotright> by (rule TopF) \<comment> \<open>n \<equiv> 0\<close> - \<guillemotright> by (rule BotF) \<comment> \<open>n \<equiv> suc _\<close> - \<guillemotright> by (rule Ui_in_USi) - done - \<comment> \<open>m \<equiv> suc k\<close> - apply intro focus vars k k_eq n apply (elim n) - \<guillemotright> by (rule BotF) \<comment> \<open>n \<equiv> 0\<close> - \<guillemotright> prems vars l proof - show "k_eq l: U O" by typechk qed - \<guillemotright> by (rule Ui_in_USi) - done - by (rule Ui_in_USi) - done - -text \<open> -\<^term>\<open>eq\<close> is defined by - eq 0 0 \<equiv> \<top> - eq 0 (suc k) \<equiv> \<bottom> - eq (suc k) 0 \<equiv> \<bottom> - eq (suc k) (suc l) \<equiv> eq k l -\<close> - - - - -end - - -end |