diff options
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 |