diff options
| -rw-r--r-- | tests/Subgoal.thy | 52 |
1 files changed, 29 insertions, 23 deletions
diff --git a/tests/Subgoal.thy b/tests/Subgoal.thy index 2226f08..4fcffad 100644 --- a/tests/Subgoal.thy +++ b/tests/Subgoal.thy @@ -2,32 +2,12 @@ theory Subgoal imports "../HoTT" begin -text " - \<open>subgoal\<close> converts schematic variables to fixed free variables, making it unsuitable for use in \<open>schematic_goal\<close> proofs. - This is the same thing as being unable to start a "sub-schematic goal" inside an ongoing proof. - - This is a problem for syntheses which need to use induction (elimination rules), as these often have to be applied to fixed variables, while keeping any schematic variables intact. -" - -schematic_goal rpathcomp_synthesis: - assumes "A: U(i)" - shows "?a: \<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" text " - Try (and fail) to synthesize the constant for path composition, following the proof of \<open>rpathcomp_type\<close> below. + Proof of \<open>rpathcomp_type\<close> (see EqualProps.thy) in apply-style. + Subgoaling can be used to fix variables and apply the elimination rules. " -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 - - lemma rpathcomp_type: assumes "A: U(i)" 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)" @@ -62,4 +42,30 @@ apply fact done -end
\ No newline at end of file +text " + \<open>subgoal\<close> converts schematic variables to fixed free variables, making it unsuitable for use in \<open>schematic_goal\<close> proofs. + This is the same thing as being unable to start a ``sub schematic-goal'' inside an ongoing proof. + + This is a problem for syntheses which need to use induction (elimination rules), as these often have to be applied to fixed variables, while keeping any schematic variables intact. +" + +schematic_goal rpathcomp_synthesis: + assumes "A: U(i)" + shows "?a: \<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" + +text " + Try (and fail) to synthesize the constant for path composition, following the proof of \<open>rpathcomp_type\<close> below. +" + +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 + + +end |