diff options
| author | Josh Chen | 2018-08-18 21:28:21 +0200 |
|---|---|---|
| committer | Josh Chen | 2018-08-18 21:28:21 +0200 |
| commit | e1be5f97bb2a42b3179bc24b118d69af137f8e5d (patch) | |
| tree | 37fa2dacc40261bf37726e23121df0ba5b9af68e /ex | |
| parent | 03c734ea067bd28210530d862137133e2215ca80 (diff) | |
Regrouping type rules
Diffstat (limited to '')
| -rw-r--r-- | ex/HoTT book/Ch1.thy | 3 | ||||
| -rw-r--r-- | ex/Methods.thy | 3 | ||||
| -rw-r--r-- | ex/Synthesis.thy | 7 |
3 files changed, 5 insertions, 8 deletions
diff --git a/ex/HoTT book/Ch1.thy b/ex/HoTT book/Ch1.thy index cc0adf5..d5f05dd 100644 --- a/ex/HoTT book/Ch1.thy +++ b/ex/HoTT book/Ch1.thy @@ -1,6 +1,5 @@ (* Title: HoTT/ex/HoTT book/Ch1.thy Author: Josh Chen - Date: Aug 2018 A formalization of some content of Chapter 1 of the Homotopy Type Theory book. *) @@ -41,4 +40,4 @@ proof (rule Sum_elim[where ?p=p]) qed (derive lems: assms) -end
\ No newline at end of file +end diff --git a/ex/Methods.thy b/ex/Methods.thy index 871964f..415fbc3 100644 --- a/ex/Methods.thy +++ b/ex/Methods.thy @@ -1,6 +1,5 @@ (* Title: HoTT/ex/Methods.thy Author: Josh Chen - Date: Aug 2018 HoTT method usage examples *) @@ -74,4 +73,4 @@ proof compute qed fact -end
\ No newline at end of file +end diff --git a/ex/Synthesis.thy b/ex/Synthesis.thy index e5a8ecf..cff9374 100644 --- a/ex/Synthesis.thy +++ b/ex/Synthesis.thy @@ -1,6 +1,5 @@ (* Title: HoTT/ex/Synthesis.thy Author: Josh Chen - Date: Aug 2018 Examples of synthesis. *) @@ -33,8 +32,8 @@ text " schematic_goal "?p`0 \<equiv> 0" and "\<And>n. n: \<nat> \<Longrightarrow> (?p`(succ n)) \<equiv> n" apply compute prefer 4 apply compute -prefer 3 apply (rule Nat_rules) -apply (rule Nat_rules | assumption)+ +prefer 3 apply compute +apply (rule Nat_routine Nat_elim | assumption)+ done text " @@ -52,7 +51,7 @@ proof (simple lems: pred_type) proof compute show "\<And>n. n: \<nat> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>a b. a) 0 n: \<nat>" by simple show "ind\<^sub>\<nat> (\<lambda>a b. a) 0 0 \<equiv> 0" - proof (rule Nat_comps) + proof compute show "\<nat>: U(O)" .. qed simple qed rule |