From a1603ffdddcbe333a3e4f0f328a4c25698c2d475 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sat, 18 Aug 2018 15:07:33 +0200
Subject: Comments on subgoal test theory

---
 tests/Subgoal.thy | 52 +++++++++++++++++++++++++++++-----------------------
 1 file 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
-- 
cgit v1.2.3