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/Subgoal.thy | |
parent | 03c734ea067bd28210530d862137133e2215ca80 (diff) |
Regrouping type rules
Diffstat (limited to 'tests/Subgoal.thy')
-rw-r--r-- | tests/Subgoal.thy | 10 |
1 files changed, 1 insertions, 9 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 |