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 /tests | |
| parent | 03c734ea067bd28210530d862137133e2215ca80 (diff) | |
Regrouping type rules
Diffstat (limited to '')
| -rw-r--r-- | tests/Subgoal.thy | 10 | ||||
| -rw-r--r-- | tests/Test.thy | 12 |
2 files changed, 7 insertions, 15 deletions
diff --git a/tests/Subgoal.thy b/tests/Subgoal.thy index 4fcffad..9690013 100644 --- a/tests/Subgoal.thy +++ b/tests/Subgoal.thy @@ -13,21 +13,16 @@ lemma rpathcomp_type: shows "rpathcomp: \<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" unfolding rpathcomp_def apply standard -prefer 2 subgoal premises 1 for x \<comment> \<open>\<open>subgoal\<close> is the proof script version of \<open>fix-assume-show\<close>.\<close> apply standard - prefer 2 subgoal premises 2 for y apply standard - prefer 2 subgoal premises 3 for p apply (rule Equal_elim[where ?x=x and ?y=y and ?A=A]) \<comment> \<open>specifying \<open>?A=A\<close> is crucial here to prevent the next \<open>subgoal\<close> from binding a schematic ?A which should be instantiated to \<open>A\<close>.\<close> - prefer 2 + prefer 4 apply standard - prefer 2 apply (rule Prod_intro) - prefer 2 subgoal premises 4 for u z q apply (rule Equal_elim[where ?x=u and ?y=z]) apply (simple lems: assms 4) @@ -58,11 +53,8 @@ text " " apply (rule Prod_intro) -prefer 2 apply (rule Prod_intro) - prefer 2 apply (rule Prod_intro) - prefer 2 subgoal 123 for x y p apply (rule Equal_elim[where ?x=x and ?y=y and ?A=A]) oops diff --git a/tests/Test.thy b/tests/Test.thy index 433039c..c0dc0dd 100644 --- a/tests/Test.thy +++ b/tests/Test.thy @@ -6,8 +6,8 @@ This is an old "test suite" from early implementations of the theory. It is not always guaranteed to be up to date, or reflect most recent versions of the theory. *) -theory HoTT_Test - imports HoTT +theory Test + imports "../HoTT" begin @@ -31,14 +31,14 @@ text " Declaring \<open>Prod_intro\<close> with the \<open>intro\<close> attribute (in HoTT.thy) enables \<open>standard\<close> to prove the following. " -proposition assumes "A : U(i)" shows "\<^bold>\<lambda>x. x: A \<rightarrow> A" using assms .. +proposition assumes "A : U(i)" shows "\<^bold>\<lambda>x. x: A \<rightarrow> A" by (simple lems: assms) proposition assumes "A : U(i)" and "A \<equiv> B" shows "\<^bold>\<lambda>x. x : B \<rightarrow> A" proof - - have "A\<rightarrow>A \<equiv> B\<rightarrow>A" using assms by simp - moreover have "\<^bold>\<lambda>x. x : A \<rightarrow> A" using assms(1) .. + have "A \<rightarrow> A \<equiv> B \<rightarrow> A" using assms by simp + moreover have "\<^bold>\<lambda>x. x : A \<rightarrow> A" by (simple lems: assms) ultimately show "\<^bold>\<lambda>x. x : B \<rightarrow> A" by simp qed @@ -102,7 +102,7 @@ lemma curried_type_judgment: text " - Polymorphic identity function. Trivial due to lambda expression polymorphism. + Polymorphic identity function is now trivial due to lambda expression polymorphism. (Was more involved in previous monomorphic incarnations.) " |