From 12eed8685674b7d5ff7bc45a44a061e01f99ce5f Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 21 Jul 2020 02:09:44 +0200 Subject: 1. Type-checking/inference now more principled, and the implementation is better. 2. Changed most tactics to context tactics. --- hott/Nat.thy | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) (limited to 'hott/Nat.thy') diff --git a/hott/Nat.thy b/hott/Nat.thy index 4abd315..177ec47 100644 --- a/hott/Nat.thy +++ b/hott/Nat.thy @@ -38,9 +38,10 @@ where f n (NatInd (fn n. C n) c\<^sub>0 (fn k rec. f k rec) n)" lemmas - [intros] = NatF Nat_zero Nat_suc and - [elims "?n"] = NatE and - [comps] = Nat_comp_zero Nat_comp_suc + [form] = NatF and + [intro, intros] = Nat_zero Nat_suc and + [elim "?n"] = NatE and + [comp] = Nat_comp_zero Nat_comp_suc abbreviation "NatRec C \ NatInd (fn _. C)" @@ -66,12 +67,12 @@ lemma add_type [typechk]: shows "m + n: Nat" unfolding add_def by typechk -lemma add_zero [comps]: +lemma add_zero [comp]: assumes "m: Nat" shows "m + 0 \ m" unfolding add_def by reduce -lemma add_suc [comps]: +lemma add_suc [comp]: assumes "m: Nat" "n: Nat" shows "m + suc n \ suc (m + n)" unfolding add_def by reduce @@ -127,17 +128,17 @@ lemma mul_type [typechk]: shows "m * n: Nat" unfolding mul_def by typechk -lemma mul_zero [comps]: +lemma mul_zero [comp]: assumes "n: Nat" shows "n * 0 \ 0" unfolding mul_def by reduce -lemma mul_one [comps]: +lemma mul_one [comp]: assumes "n: Nat" shows "n * 1 \ n" unfolding mul_def by reduce -lemma mul_suc [comps]: +lemma mul_suc [comp]: assumes "m: Nat" "n: Nat" shows "m * suc n \ m + m * n" unfolding mul_def by reduce -- cgit v1.2.3