Refactor HoTT_Methods.thy, proved more stuff with new methods.

9 files changed, 133 insertions, 205 deletions

diff --git a/Equal.thy b/Equal.thy
index f0ced68..51a69ae 100644
--- a/Equal.thy
+++ b/Equal.thy
@@ -53,7 +53,7 @@ and
     \<rbrakk> \<Longrightarrow> indEqual[A] C f a a refl(a) \<equiv> f a"
 
 lemmas Equal_rules [intro] = Equal_form Equal_intro Equal_elim Equal_comp
-lemmas Equal_form_conds [elim] = Equal_form_cond1 Equal_form_cond2 Equal_form_cond3
+lemmas Equal_form_conds [elim, wellform] = Equal_form_cond1 Equal_form_cond2 Equal_form_cond3
 
 
 end
\ No newline at end of file
diff --git a/EqualProps.thy b/EqualProps.thy
index 10d3b17..8960a90 100644
--- a/EqualProps.thy
+++ b/EqualProps.thy
@@ -22,18 +22,7 @@ definition inv :: "[Term, Term, Term] \<Rightarrow> Term"  ("(1inv[_,/ _,/ _])")
 lemma inv_type:
   assumes "p : x =\<^sub>A y"
   shows "inv[A,x,y]`p : y =\<^sub>A x"
-
-proof
-  show "inv[A,x,y] : (x =\<^sub>A y) \<rightarrow> (y =\<^sub>A x)"
-  proof (unfold inv_def, standard)
-    fix p assume asm: "p : x =\<^sub>A y"
-    show "indEqual[A] (\<lambda>x y _. y =[A] x) refl x y p : y =\<^sub>A x"
-    proof standard+
-      show "x : A" by (wellformed jdgmt: asm)
-      show "y : A" by (wellformed jdgmt: asm)
-    qed (assumption | rule | rule asm)+
-  qed (wellformed jdgmt: assms)
-qed (rule assms)
+  by (derive lems: assms unfolds: inv_def)
       
 
 lemma inv_comp:
@@ -42,19 +31,10 @@ lemma inv_comp:
 
 proof -
   have "inv[A,a,a]`refl(a) \<equiv> indEqual[A] (\<lambda>x y _. y =\<^sub>A x) (\<lambda>x. refl(x)) a a refl(a)"
-  proof (unfold inv_def, standard)
-    show "refl(a) : a =\<^sub>A a" using assms ..
-
-    fix p assume asm: "p : a =\<^sub>A a"
-    show "indEqual[A] (\<lambda>x y _. y =\<^sub>A x) refl a a p : a =\<^sub>A a"
-    proof standard+
-      show "a : A" by (wellformed jdgmt: asm)
-      then show "a : A" .  \<comment> \<open>The elimination rule requires that both arguments to \<open>indEqual\<close> be shown to have the correct type.\<close>
-    qed (assumption | rule | rule asm)+
-  qed
+    by (derive lems: assms unfolds: inv_def)
 
   also have "indEqual[A] (\<lambda>x y _. y =\<^sub>A x) (\<lambda>x. refl(x)) a a refl(a) \<equiv> refl(a)"
-    by (standard | assumption | rule assms)+
+    by (simple lems: assms)
 
   finally show "inv[A,a,a]`refl(a) \<equiv> refl(a)" .
 qed
@@ -79,14 +59,34 @@ abbreviation compose :: "[Term, Term, Term, Term] \<Rightarrow> Term"  ("(1compo
 lemma compose_type:
   assumes "p : x =\<^sub>A y" and "q : y =\<^sub>A z"
   shows "compose[A,x,y,z]`p`q : x =\<^sub>A z"
-
-sorry
+  by (derive lems: assms unfolds: rcompose_def)
 
 
 lemma compose_comp:
   assumes "a : A"
   shows "compose[A,a,a,a]`refl(a)`refl(a) \<equiv> refl(a)"
 
+proof (unfold rcompose_def)
+  show "(\<^bold>\<lambda>p:a =[A] a.
+        lambda (a =[A] a)
+         (op `
+           ((\<^bold>\<lambda>x:A.
+                \<^bold>\<lambda>y:A.
+                   lambda (x =[A] y)
+                    (indEqual[A]
+                      (\<lambda>x y _. \<Prod>z:A. y =[A] z \<rightarrow> x =[A] z)
+                      (\<lambda>x. \<^bold>\<lambda>z:A.
+ lambda (x =[A] z)
+  (indEqual[A] (\<lambda>x z _. x =[A] z) refl x z))
+                      x y)) `
+            a `
+            a `
+            p `
+            a))) `
+    refl(a) `
+    refl(a) \<equiv>
+    refl(a)"
+
 sorry \<comment> \<open>Long and tedious proof if the Simplifier is not set up.\<close>
 
 
diff --git a/HoTT.thy b/HoTT.thy
index b500150..42796c1 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -7,10 +7,19 @@ Load all the component modules for the HoTT logic.
 theory HoTT
 
 imports
-  HoTT_Base
-  HoTT_Methods
-  Prod
-  Sum
+
+(* Basic theories *)
+HoTT_Base
+HoTT_Methods
+
+(* Types *)
+Equal
+Prod
+Sum
+
+(* Additional properties *)
+EqualProps
+Proj
 
 begin
 end
diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index e5c0776..eaebfb0 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -9,12 +9,14 @@ theory HoTT_Base
   imports Pure
 begin
 
+
 section \<open>Setup\<close>
 
-text "Declare rules expressing necessary wellformedness conditions for type and inhabitation judgments."
+text "Declare rules expressing necessary wellformedness conditions for type and inhabitation judgments, to be used by proof methods later (see HoTT_Methods.thy)."
 
 named_theorems wellform
 
+
 section \<open>Metalogical definitions\<close>
 
 text "A single meta-type \<open>Term\<close> suffices to implement the object-logic types and terms.
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy
index bce5123..20f3ece 100644
--- a/HoTT_Methods.thy
+++ b/HoTT_Methods.thy
@@ -2,8 +2,7 @@
     Author: Josh Chen
     Date:   Jun 2018
 
-Method setup for the HoTT library.
-Relies heavily on Eisbach.
+Method setup for the HoTT library. Relies heavily on Eisbach.
 *)
 
 theory HoTT_Methods
@@ -11,14 +10,14 @@ theory HoTT_Methods
     "HOL-Eisbach.Eisbach"
     "HOL-Eisbach.Eisbach_Tools"
     HoTT_Base
-    Equal
-    Prod
-    Sum
 begin
 
+
 section \<open>Method setup\<close>
 
-text "Prove type judgments \<open>A : U\<close> and inhabitation judgments \<open>a : A\<close> using rules declared [intro] and [elim], as well as additional provided lemmas."
+text "Prove type judgments \<open>A : U\<close> and inhabitation judgments \<open>a : A\<close> using rules declared [intro] and [elim], as well as additional provided lemmas.
+
+Can also perform typechecking, and search for elements of a type."
 
 method simple uses lems = (assumption|standard|rule lems)+
 
@@ -33,83 +32,20 @@ method wellformed uses jdgmt = (
   )
 
 
-text "Combine \<open>simple\<close> and \<open>wellformed\<close> to search for derivations."
+text "Combine \<open>simple\<close> and \<open>wellformed\<close> to search for derivations.
+\<open>wellformed\<close> uses the facts passed as \<open>lems\<close> to derive any required typing judgments.
+Definitions passed as \<open>unfolds\<close> are unfolded throughout.
+
+Roughly speaking \<open>derive\<close> is more powerful than \<open>simple\<close>, but may fail to find a proof where \<open>simple\<close> does if it reduces too eagerly."
 
-method derive uses lems = (
-  catch \<open>unfold lems\<close> \<open>fail\<close> |
-  catch \<open>simple lems: lems\<close> \<open>fail\<close> |
+method derive uses lems unfolds = (
+  unfold unfolds |
+  simple lems: lems |
   match lems in lem: "?X : ?Y" \<Rightarrow> \<open>wellformed jdgmt: lem\<close>
   )+
 
 
-section \<open>Examples\<close>
-
-lemma
-  assumes "A : U" "B: A \<rightarrow> U" "\<And>x. x : A \<Longrightarrow> C x: B x \<rightarrow> U"
-  shows "\<Sum>x:A. \<Prod>y:B x. \<Sum>z:C x y. \<Prod>w:A. x =\<^sub>A w : U"
-by (simple lems: assms)
-
-lemma
-  assumes "f : \<Sum>x:A. \<Prod>y: B x. \<Sum>z: C x y. D x y z"
-  shows
-    "A : U" and
-    "B: A \<rightarrow> U" and
-    "\<And>x. x : A \<Longrightarrow> C x: B x \<rightarrow> U" and
-    "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> D x y: C x y \<rightarrow> U"
-proof -
-  show "A : U" by (wellformed jdgmt: assms)
-  show "B: A \<rightarrow> U" by (wellformed jdgmt: assms)
-  show "\<And>x. x : A \<Longrightarrow> C x: B x \<rightarrow> U" by (wellformed jdgmt: assms)
-  show "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> D x y: C x y \<rightarrow> U" by (wellformed jdgmt: assms)
-qed
-
-
-section \<open>Experimental methods\<close>
-
-text "Playing around with ML, following CTT/CTT.thy by Larry Paulson."
-
-lemmas forms = Prod_form Sum_form Equal_form
-lemmas intros = Prod_intro Sum_intro Equal_intro
-lemmas elims = Prod_elim Sum_elim Equal_elim
-lemmas elements = intros elims
-
-ML \<open>
-(* Try solving \<open>a : A\<close> by assumption provided \<open>a\<close> is rigid *)
-fun test_assume_tac ctxt = let
-    fun is_rigid (Const(@{const_name is_of_type},_) $ a $ _) = not(is_Var (head_of a))
-      | is_rigid (Const(@{const_name is_a_type},_) $ a $ _ $ _) = not(is_Var (head_of a))
-      | is_rigid _ = false
-  in
-    SUBGOAL (fn (prem, i) =>
-      if is_rigid (Logic.strip_assums_concl prem)
-      then assume_tac ctxt i else no_tac)
-  end
-
-fun ASSUME ctxt tf i = test_assume_tac ctxt i ORELSE tf i
-
-(* Solve all subgoals \<open>A : U\<close> using formation rules. *)
-val form_net = Tactic.build_net @{thms forms};
-fun form_tac ctxt =
-  REPEAT_FIRST (ASSUME ctxt (filt_resolve_from_net_tac ctxt 1 form_net));
-
-(* Try to prove inhabitation judgments \<open>a : A\<close> (\<open>a\<close> flexible, \<open>A\<close> rigid) by introduction rules. *)
-fun intro_tac ctxt thms =
-  let val tac =
-    filt_resolve_from_net_tac ctxt 1
-      (Tactic.build_net (thms @ @{thms forms} @ @{thms intros}))
-  in  REPEAT_FIRST (ASSUME ctxt tac)  end
-
-(*Type checking: solve \<open>a : A\<close> (\<open>a\<close> rigid, \<open>A\<close> flexible) by formation, introduction and elimination rules. *)
-fun typecheck_tac ctxt thms =
-  let val tac =
-    filt_resolve_from_net_tac ctxt 3
-      (Tactic.build_net (thms @ @{thms forms} @ @{thms elements}))
-  in  REPEAT_FIRST (ASSUME ctxt tac)  end
-\<close>
-
-method_setup form = \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (form_tac ctxt))\<close>
-method_setup intro = \<open>Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (intro_tac ctxt ths))\<close>
-method_setup typecheck = \<open>Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (typecheck_tac ctxt ths))\<close>
+text "Simplify function applications."
 
 
 end
\ No newline at end of file
diff --git a/Proj.thy b/Proj.thy
index fe80c4c..7957669 100644
--- a/Proj.thy
+++ b/Proj.thy
@@ -49,7 +49,7 @@ text "Typing judgments and computation rules for the dependent and non-dependent
 lemma fst_dep_type:
   assumes "p : \<Sum>x:A. B x"
   shows "fst[A,B]`p : A"
-  by (derive lems: fst_dep_def assms)
+  by (derive lems: assms unfolds: fst_dep_def)
 
 
 lemma fst_dep_comp:
@@ -58,7 +58,7 @@ lemma fst_dep_comp:
 
 proof -
   have "fst[A,B]`(a,b) \<equiv> indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) (a,b)"
-    by (derive lems: fst_dep_def assms)
+    by (derive lems: assms unfolds: fst_dep_def)
   
   also have "indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) (a,b) \<equiv> a"
     by (derive lems: assms)
@@ -67,15 +67,9 @@ proof -
 qed
 
 
-text "In proving results about the second dependent projection function we often use the following two lemmas."
+text "In proving results about the second dependent projection function we often use the following lemma."
 
-lemma lemma1:
-  assumes "p : \<Sum>x:A. B x"
-  shows "B (fst[A,B]`p) : U"
-  by (derive lems: assms fst_dep_def)
-
-
-lemma lemma2:
+lemma lem:
   assumes "B: A \<rightarrow> U" and "x : A" and "y : B x"
   shows "y : B (fst[A,B]`(x,y))"
 
@@ -89,18 +83,13 @@ lemma snd_dep_type:
   assumes "p : \<Sum>x:A. B x"
   shows "snd[A,B]`p : B (fst[A,B]`p)"
 
-proof (derive lems: assms snd_dep_def)
-  show "snd[A, B] : \<Prod>p:(\<Sum>x:A. B x). B (fst[A,B]`p)"
-  proof (unfold snd_dep_def, standard)
-    show "\<And>p. p : \<Sum>x:A. B x \<Longrightarrow> indSum[A,B] (\<lambda>q. B (fst[A,B]`q)) (\<lambda>x y. y) p : B (fst[A,B]`p)"
-    proof (standard, elim lemma1)
-      fix p assume *: "p : \<Sum>x:A. B x"
-      have **: "B: A \<rightarrow> U" by (wellformed jdgmt: *)
-      fix x y assume "x : A" and "y : B x"
-      with ** show "y : B (fst[A,B]`(x,y))" by (rule lemma2)
-    qed
-  qed (wellformed jdgmt: assms)
-qed (rule assms)
+proof (derive lems: assms unfolds: snd_dep_def)
+  show "fst[A, B] : (\<Sum>x:A. B x) \<rightarrow> A" by (derive lems: assms unfolds: fst_dep_def)
+  
+  fix x y assume asm: "x : A" "y : B x"
+  have "B: A \<rightarrow> U" by (wellformed jdgmt: assms)
+  then show "y : B (fst[A, B]`(x,y))" using asm by (rule lem)
+qed (assumption | rule assms)+
 
 
 lemma snd_dep_comp:
@@ -109,22 +98,20 @@ lemma snd_dep_comp:
 
 proof -
   have "snd[A,B]`(a,b) \<equiv> indSum[A, B] (\<lambda>q. B (fst[A,B]`q)) (\<lambda>x y. y) (a,b)"
-  proof (unfold snd_dep_def, standard)
-    show "(a,b) : \<Sum>x:A. B x" using assms ..
+  proof (derive lems: assms unfolds: snd_dep_def)
+    show "fst[A, B] : (\<Sum>x:A. B x) \<rightarrow> A" by (derive lems: assms unfolds: fst_dep_def)
 
-    fix p assume *: "p : \<Sum>x:A. B x"
-    show "indSum[A,B] (\<lambda>q. B (fst[A,B]`q)) (\<lambda>x y. y) p : B (fst[A,B]`p)"
-    proof (standard, elim lemma1)
-      fix x y assume "x : A" and "y : B x"
-      with assms(1) show "y : B (fst[A,B]`(x,y))" by (rule lemma2)
-    qed (rule *)
-  qed
+    fix x y assume asm: "x : A" "y : B x"
+    with assms(1) show "y : B (fst[A, B]`(x,y))" by (rule lem)
+  qed (assumption | derive lems: assms)+
 
   also have "indSum[A, B] (\<lambda>q. B (fst[A,B]`q)) (\<lambda>x y. y) (a,b) \<equiv> b"
-  proof (standard, elim lemma1)
+  proof (simple lems: assms)
+    show "fst[A, B] : (\<Sum>x:A. B x) \<rightarrow> A" by (derive lems: assms unfolds: fst_dep_def)
+
     fix x y assume "x : A" and "y : B x"
-    with assms(1) show "y : B (fst[A,B]`(x,y))" by (rule lemma2)
-  qed (rule assms)+
+    with assms(1) show "y : B (fst[A,B]`(x,y))" by (rule lem)
+  qed (assumption | rule assms)+
 
   finally show "snd[A,B]`(a,b) \<equiv> b" .
 qed
@@ -135,17 +122,7 @@ text "For non-dependent projection functions:"
 lemma fst_nondep_type:
   assumes "p : A \<times> B"
   shows "fst[A,B]`p : A"
-
-proof
-  show "fst[A,B] : A \<times> B \<rightarrow> A"
-  proof (unfold fst_nondep_def, standard)
-    fix q assume *: "q : A \<times> B"
-    show "indSum[A, \<lambda>_. B] (\<lambda>_. A) (\<lambda>x y. x) q : A"
-    proof
-      show "A : U" by (wellformed jdgmt: assms)
-    qed (assumption, rule *)
-  qed (wellformed jdgmt: assms)
-qed (rule assms)
+  by (derive lems: assms unfolds: fst_nondep_def)
 
 
 lemma fst_nondep_comp:
@@ -154,18 +131,10 @@ lemma fst_nondep_comp:
 
 proof -
   have "fst[A,B]`(a,b) \<equiv> indSum[A, \<lambda>_. B] (\<lambda>_. A) (\<lambda>x y. x) (a,b)"
-  proof (unfold fst_nondep_def, standard)
-    show "(a,b) : A \<times> B" using assms ..
-    show "\<And>p. p : A \<times> B \<Longrightarrow> indSum[A, \<lambda>_. B] (\<lambda>_. A) (\<lambda>x y. x) p : A"
-    proof
-      show "A : U" by (wellformed jdgmt: assms(1))
-    qed
-  qed
+    by (derive lems: assms unfolds: fst_nondep_def)
 
   also have "indSum[A, \<lambda>_. B] (\<lambda>_. A) (\<lambda>x y. x) (a,b) \<equiv> a"
-  proof
-    show "A : U" by (wellformed jdgmt: assms(1))
-  qed (assumption, (rule assms)+)
+    by (derive lems: assms)
 
   finally show "fst[A,B]`(a,b) \<equiv> a" .
 qed
@@ -177,15 +146,10 @@ lemma snd_nondep_type:
 
 proof
   show "snd[A,B] : A \<times> B \<rightarrow> B"
-  proof (unfold snd_nondep_def, standard)
-    fix q assume *: "q : A \<times> B"
-    show "indSum[A, \<lambda>_. B] (\<lambda>_. B) (\<lambda>x y. y) q : B"
-    proof
-      have **: "\<lambda>_. B: A \<rightarrow> U" by (wellformed jdgmt: assms)
-      have "fst[A,B]`p : A" using assms by (rule fst_nondep_type)
-      then show "B : U" by (rule **)
-    qed (assumption, rule *)
-  qed (wellformed jdgmt: assms)
+  proof (derive unfolds: snd_nondep_def)
+    fix q assume asm: "q : A \<times> B"
+    show "indSum[A, \<lambda>_. B] (\<lambda>_. B) (\<lambda>x y. y) q : B" by (derive lems: asm)
+  qed (wellformed jdgmt: assms)+
 qed (rule assms)
 
 
@@ -194,18 +158,10 @@ lemma snd_nondep_comp:
   shows "snd[A,B]`(a,b) \<equiv> b"
 proof -
   have "snd[A,B]`(a,b) \<equiv> indSum[A, \<lambda>_. B] (\<lambda>_. B) (\<lambda>x y. y) (a,b)"
-  proof (unfold snd_nondep_def, standard)
-    show "(a,b) : A \<times> B" by (simple conds: assms)
-    show "\<And>p. p : A \<times> B \<Longrightarrow> indSum[A, \<lambda>_. B] (\<lambda>_. B) (\<lambda>x y. y) p : B"
-    proof
-      show "B : U" by (wellformed jdgmt: assms(2))
-    qed
-  qed
+    by (derive lems: assms unfolds: snd_nondep_def)
 
   also have "indSum[A, \<lambda>_. B] (\<lambda>_. B) (\<lambda>x y. y) (a,b) \<equiv> b"
-  proof
-    show "B : U" by (wellformed jdgmt: assms(2))
-  qed (assumption, (rule assms)+)
+    by (derive lems: assms)
 
   finally show "snd[A,B]`(a,b) \<equiv> b" .
 qed
diff --git a/Sum.thy b/Sum.thy
index 7e688a2..bf7b829 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -59,10 +59,10 @@ abbreviation Pair :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<times>" 50)
 
 lemma
   Pair_intro [intro]: "\<And>A B a b. \<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (a,b) : A \<times> B"
-proof
-  fix b B assume "b : B"
-  then show "B : U" ..
-qed
+  proof
+    fix b B assume "b : B"
+    then show "B : U" ..
+  qed
 
 
 end
\ No newline at end of file
diff --git a/ex/Methods.thy b/ex/Methods.thy
new file mode 100644
index 0000000..d174dde
--- /dev/null
+++ b/ex/Methods.thy
@@ -0,0 +1,41 @@
+(*  Title:  HoTT/ex/Methods.thy
+    Author: Josh Chen
+    Date:   Jul 2018
+
+HoTT method usage examples
+*)
+
+theory Methods
+  imports "../HoTT"
+begin
+
+lemma
+  assumes "A : U" "B: A \<rightarrow> U" "\<And>x. x : A \<Longrightarrow> C x: B x \<rightarrow> U"
+  shows "\<Sum>x:A. \<Prod>y:B x. \<Sum>z:C x y. \<Prod>w:A. x =\<^sub>A w : U"
+by (simple lems: assms)
+
+
+lemma
+  assumes "f : \<Sum>x:A. \<Prod>y: B x. \<Sum>z: C x y. D x y z"
+  shows
+    "A : U" and
+    "B: A \<rightarrow> U" and
+    "\<And>x. x : A \<Longrightarrow> C x: B x \<rightarrow> U" and
+    "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> D x y: C x y \<rightarrow> U"
+proof -
+  show "A : U" by (wellformed jdgmt: assms)
+  show "B: A \<rightarrow> U" by (wellformed jdgmt: assms)
+  show "\<And>x. x : A \<Longrightarrow> C x: B x \<rightarrow> U" by (wellformed jdgmt: assms)
+  show "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> D x y: C x y \<rightarrow> U" by (wellformed jdgmt: assms)
+qed
+
+
+text "Typechecking:"
+
+\<comment> \<open>Correctly determines the type of the pair\<close>
+schematic_goal "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (a, b) : ?A" by simple
+
+\<comment> \<open>Finds element\<close>
+schematic_goal "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> ?x : A \<times> B" by simple
+
+end
\ No newline at end of file
diff --git a/scratch.thy b/scratch.thy
index 331b607..b90fd59 100644
--- a/scratch.thy
+++ b/scratch.thy
@@ -1,24 +1,8 @@
 theory scratch
-  imports IFOL
+  imports HoTT
 
 begin
 
-lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P"
-apply (erule disjE)  (* Compare with the less useful \<open>rule disjE\<close> *)
-  apply (rule disjI2)
-  apply assumption
-apply (rule disjI1)
-apply assumption
-done
-
-lemma imp_uncurry: "P \<longrightarrow> (Q \<longrightarrow> R) \<Longrightarrow> P \<and> Q \<longrightarrow> R"
-apply (rule impI)
-apply (erule conjE)
-apply (drule mp)
-apply assumption
-apply (drule mp)
-apply assumption
-apply assumption
-done
+schematic_goal "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> ?x : A \<times> B" by simple
 
 end
\ No newline at end of file