From e1be5f97bb2a42b3179bc24b118d69af137f8e5d Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sat, 18 Aug 2018 21:28:21 +0200
Subject: Regrouping type rules

---
 tests/Subgoal.thy | 10 +---------
 tests/Test.thy    | 12 ++++++------
 2 files changed, 7 insertions(+), 15 deletions(-)

(limited to 'tests')

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.)
 "
 
-- 
cgit v1.2.3