diff options
| -rw-r--r-- | Coprod.thy | 2 | ||||
| -rw-r--r-- | Equal.thy | 2 | ||||
| -rw-r--r-- | EqualProps.thy | 66 | ||||
| -rw-r--r-- | HoTT.thy | 8 | ||||
| -rw-r--r-- | HoTT_Methods.thy | 42 | ||||
| -rw-r--r-- | Nat.thy | 2 | ||||
| -rw-r--r-- | Prod.thy | 4 | ||||
| -rw-r--r-- | ProdProps.thy | 12 | ||||
| -rw-r--r-- | Proj.thy | 8 | ||||
| -rw-r--r-- | Sum.thy | 2 | ||||
| -rw-r--r-- | ex/Methods.thy | 12 | ||||
| -rw-r--r-- | ex/Synthesis.thy | 20 | ||||
| -rw-r--r-- | tests/Subgoal.thy | 12 |
13 files changed, 98 insertions, 94 deletions
@@ -59,7 +59,7 @@ lemmas Coprod_intro = Coprod_intro_inl Coprod_intro_inr lemmas Coprod_comp [comp] = Coprod_comp_inl Coprod_comp_inr lemmas Coprod_wellform [wellform] = Coprod_wellform1 Coprod_wellform2 -lemmas Coprod_routine [intro] = Coprod_form Coprod_intro Coprod_comp Coprod_elim +lemmas Coprod_routine [intro] = Coprod_form Coprod_intro Coprod_elim end @@ -60,7 +60,7 @@ text "Rule attribute declarations:" lemmas Equal_comp [comp] lemmas Equal_wellform [wellform] = Equal_wellform1 Equal_wellform2 Equal_wellform3 -lemmas Equal_routine [intro] = Equal_form Equal_intro Equal_comp Equal_elim +lemmas Equal_routine [intro] = Equal_form Equal_intro Equal_elim end diff --git a/EqualProps.thy b/EqualProps.thy index 8b83c5b..a1d4c45 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -24,7 +24,7 @@ text " lemma inv_type: assumes "A : U(i)" and "x : A" and "y : A" and "p: x =\<^sub>A y" shows "p\<inverse>: y =\<^sub>A x" unfolding inv_def -by (rule Equal_elim[where ?x=x and ?y=y]) (simple lems: assms) +by (rule Equal_elim[where ?x=x and ?y=y]) (routine lems: assms) \<comment> \<open>The type doesn't depend on \<open>p\<close> so we don't need to specify \<open>?p\<close> in the \<open>where\<close> clause above.\<close> text " @@ -35,9 +35,9 @@ text " lemma inv_comp: assumes "A : U(i)" and "a : A" shows "(refl a)\<inverse> \<equiv> refl(a)" unfolding inv_def -proof +proof compute show "\<And>x. x: A \<Longrightarrow> refl x: x =\<^sub>A x" .. -qed (simple lems: assms) +qed (routine lems: assms) section \<open>Transitivity / Path composition\<close> @@ -72,18 +72,18 @@ proof proof fix u z q assume asm: "u: A" "z: A" "q: u =\<^sub>A z" show "ind\<^sub>= refl q: u =\<^sub>A z" - by (rule Equal_elim[where ?x=u and ?y=z]) (simple lems: assms asm) - qed (simple lems: assms) + by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms asm) + qed (routine lems: assms) qed (rule assms) - qed (simple lems: assms 1 2 3) - qed (simple lems: assms 1 2) + qed (routine lems: assms 1 2 3) + qed (routine lems: assms 1 2) qed (rule assms) qed fact corollary assumes "A: U(i)" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" shows "rpathcomp`x`y`p`z`q: x =\<^sub>A z" - by (simple lems: assms rpathcomp_type) + by (routine lems: assms rpathcomp_type) text " The following proof is very long, chiefly because for every application of \<open>`\<close> we have to show the wellformedness of the type family appearing in the equality computation rule. @@ -109,11 +109,11 @@ proof compute proof fix u z assume asm: "u: A" "z: A" show "\<And>q. q: u =\<^sub>A z \<Longrightarrow> ind\<^sub>= refl q: u =\<^sub>A z" - by (rule Equal_elim[where ?x=u and ?y=z]) (simple lems: assms asm) - qed (simple lems: assms) + by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms asm) + qed (routine lems: assms) qed (rule assms) - qed (simple lems: assms 1 2 3) - qed (simple lems: assms 1 2) + qed (routine lems: assms 1 2 3) + qed (routine lems: assms 1 2) qed (rule assms) } show "(\<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p)`a`refl(a)`a`refl(a) \<equiv> refl(a)" @@ -131,11 +131,11 @@ proof compute show "\<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A z \<rightarrow> u =\<^sub>A z" proof show "\<And>q. q: u =\<^sub>A z \<Longrightarrow> ind\<^sub>= refl q: u =\<^sub>A z" - by (rule Equal_elim[where ?x=u and ?y=z]) (simple lems: assms 3 4) - qed (simple lems: assms 3 4) + by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms 3 4) + qed (routine lems: assms 3 4) qed fact - qed (simple lems: assms 1 2) - qed (simple lems: assms 1) } + qed (routine lems: assms 1 2) + qed (routine lems: assms 1) } show "(\<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z. \<^bold>\<lambda>q. ind\<^sub>= refl q) p)`refl(a)`a`refl(a) \<equiv> refl(a)" proof compute @@ -149,10 +149,10 @@ proof compute show "\<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A z \<rightarrow> u =\<^sub>A z" proof show "\<And>q. q: u =\<^sub>A z \<Longrightarrow> ind\<^sub>= refl q: u =\<^sub>A z" - by (rule Equal_elim[where ?x=u and ?y=z]) (simple lems: assms 2 3) - qed (simple lems: assms 2 3) + by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms 2 3) + qed (routine lems: assms 2 3) qed fact - qed (simple lems: assms 1) } + qed (routine lems: assms 1) } show "(ind\<^sub>=(\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q)(refl(a)))`a`refl(a) \<equiv> refl(a)" proof compute @@ -163,8 +163,8 @@ proof compute show "\<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A z \<rightarrow> u =\<^sub>A z" proof show "\<And>q. q: u =\<^sub>A z \<Longrightarrow> ind\<^sub>= refl q: u =\<^sub>A z" - by (rule Equal_elim[where ?x=u and ?y=z]) (simple lems: assms 1 2) - qed (simple lems: assms 1 2) + by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms 1 2) + qed (routine lems: assms 1 2) qed fact } show "(\<^bold>\<lambda>z q. ind\<^sub>= refl q)`a`refl(a) \<equiv> refl(a)" @@ -173,21 +173,21 @@ proof compute show "\<^bold>\<lambda>q. ind\<^sub>= refl q: a =\<^sub>A a \<rightarrow> a =\<^sub>A a" proof show "\<And>q. q: a =\<^sub>A a \<Longrightarrow> ind\<^sub>= refl q: a =\<^sub>A a" - by (rule Equal_elim[where ?x=a and ?y=a]) (simple lems: assms 1) - qed (simple lems: assms 1) } + by (rule Equal_elim[where ?x=a and ?y=a]) (routine lems: assms 1) + qed (routine lems: assms 1) } show "(\<^bold>\<lambda>q. ind\<^sub>= refl q)`refl(a) \<equiv> refl(a)" proof compute show "\<And>p. p: a =\<^sub>A a \<Longrightarrow> ind\<^sub>= refl p: a =\<^sub>A a" - by (rule Equal_elim[where ?x=a and ?y=a]) (simple lems: assms) + by (rule Equal_elim[where ?x=a and ?y=a]) (routine lems: assms) show "ind\<^sub>= refl (refl(a)) \<equiv> refl(a)" - proof + proof compute show "\<And>x. x: A \<Longrightarrow> refl(x): x =\<^sub>A x" .. - qed (simple lems: assms) - qed (simple lems: assms) + qed (routine lems: assms) + qed (routine lems: assms) qed fact - qed (simple lems: assms) - qed (simple lems: assms) + qed (routine lems: assms) + qed (routine lems: assms) qed fact qed fact @@ -207,15 +207,15 @@ lemma pathcomp_type: shows "p \<bullet> q: x =\<^sub>A z" proof (subst pathcomp_def) show "A: U(i)" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" by fact+ -qed (simple lems: assms rpathcomp_type) +qed (routine lems: assms rpathcomp_type) lemma pathcomp_comp: assumes "A : U(i)" and "a : A" shows "refl(a) \<bullet> refl(a) \<equiv> refl(a)" -by (subst pathcomp_def) (simple lems: assms rpathcomp_comp) +by (subst pathcomp_def) (routine lems: assms rpathcomp_comp) -lemmas EqualProps_rules [intro] = inv_type pathcomp_type -lemmas EqualProps_comps [comp] = inv_comp pathcomp_comp +lemmas EqualProps_type [intro] = inv_type pathcomp_type +lemmas EqualProps_comp [comp] = inv_comp pathcomp_comp end @@ -25,13 +25,13 @@ Proj begin -lemmas form_rules = +lemmas forms = Nat_form Prod_form Sum_form Coprod_form Equal_form Unit_form Empty_form -lemmas intro_rules = +lemmas intros = Nat_intro Prod_intro Sum_intro Equal_intro Coprod_intro Unit_intro -lemmas elim_rules = +lemmas elims = Nat_elim Prod_elim Sum_elim Equal_elim Coprod_elim Unit_elim Empty_elim -lemmas routine_rules = +lemmas routines = Nat_routine Prod_routine Sum_routine Equal_routine Coprod_routine Unit_routine Empty_routine end diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index 4d2174b..32e412b 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -12,23 +12,19 @@ theory HoTT_Methods begin -section \<open>Method definitions\<close> - -subsection \<open>Simple type rule proof search\<close> +section \<open>Deriving typing judgments\<close> text " - Prove type judgments \<open>A : U\<close> and inhabitation judgments \<open>a : A\<close> using the type rules declared [intro] in the respective theory files, as well as additional provided lemmas. - - Can also perform typechecking, and search for elements of a type. + \<open>routine\<close> proves routine type judgments \<open>a : A\<close> using the rules declared [intro] in the respective theory files, as well as additional provided lemmas. " -method simple uses lems = (assumption | rule lems | standard)+ - - -subsection \<open>Wellformedness checker\<close> +method routine uses lems = (assumption | rule lems | standard)+ text " - \<open>wellformed\<close> finds a proof of any valid typing judgment derivable from the judgments passed as \<open>lem\<close>. + \<open>wellformed'\<close> finds a proof of any valid typing judgment derivable from the judgment passed as \<open>jdmt\<close>. + If no judgment is passed, it will try to resolve with the theorems declared \<open>wellform\<close>. + \<open>wellform\<close> is like \<open>wellformed'\<close> but takes multiple judgments. + The named theorem \<open>wellform\<close> is declared in HoTT_Base.thy. " @@ -42,14 +38,7 @@ method wellformed uses lems = match lems in lem: "?X : ?Y" \<Rightarrow> \<open>wellformed' jdmt: lem\<close> -subsection \<open>Derivation search\<close> - -text " Combine \<open>simple\<close> and \<open>wellformed\<close> to search for derivations of judgments." - -method derive uses lems = (simple lems: lems | wellformed lems: lems)+ - - -subsection \<open>Substitution and simplification\<close> +section \<open>Substitution and simplification\<close> text "Import the \<open>subst\<close> method, used for substituting definitional equalities." @@ -64,4 +53,19 @@ text "Perform basic single-step computations:" method compute uses lems = (subst lems comp | rule lems comp) +section \<open>Derivation search\<close> + +text " Combine \<open>routine\<close>, \<open>wellformed\<close>, and \<open>compute\<close> to search for derivations of judgments." + +method derive uses lems = (routine lems: lems | compute lems: lems | wellformed lems: lems)+ + + +section \<open>Induction\<close> + +text " + Placeholder section for the automation of induction, i.e. using the elimination rules. + At the moment one must directly apply them with \<open>rule X_elim\<close>. +" + + end @@ -48,7 +48,7 @@ text "Rule attribute declarations:" lemmas Nat_intro = Nat_intro_0 Nat_intro_succ lemmas Nat_comp [comp] = Nat_comp_0 Nat_comp_succ -lemmas Nat_routine [intro] = Nat_form Nat_intro Nat_comp Nat_elim +lemmas Nat_routine [intro] = Nat_form Nat_intro Nat_elim end @@ -70,7 +70,7 @@ text "Rule attribute declarations---set up various methods to use the type rules lemmas Prod_comp [comp] = Prod_appl Prod_uniq lemmas Prod_wellform [wellform] = Prod_wellform1 Prod_wellform2 -lemmas Prod_routine [intro] = Prod_form Prod_intro Prod_comp Prod_elim +lemmas Prod_routine [intro] = Prod_form Prod_intro Prod_elim section \<open>Function composition\<close> @@ -97,7 +97,7 @@ and Unit_comp: "\<lbrakk>C: \<one> \<longrightarrow> U(i); c: C(\<star>)\<rbrakk> \<Longrightarrow> ind\<^sub>\<one>(c)(\<star>) \<equiv> c" lemmas Unit_comp [comp] -lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_comp Unit_elim +lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_elim end diff --git a/ProdProps.thy b/ProdProps.thy index 3e51102..1af6ad3 100644 --- a/ProdProps.thy +++ b/ProdProps.thy @@ -29,10 +29,10 @@ proof (subst (0 1 2 3) compose_def) proof compute show "\<And>x. x: A \<Longrightarrow> h`(g`(f`x)) \<equiv> h`((\<^bold>\<lambda>y. g`(f`y))`x)" proof compute - show "\<And>x. x: A \<Longrightarrow> g`(f`x): C" by (simple lems: assms) + show "\<And>x. x: A \<Longrightarrow> g`(f`x): C" by (routine lems: assms) qed - show "\<And>x. x: B \<Longrightarrow> h`(g`x): D(g`x)" by (simple lems: assms) - qed (simple lems: assms) + show "\<And>x. x: B \<Longrightarrow> h`(g`x): D(g`x)" by (routine lems: assms) + qed (routine lems: assms) qed fact qed @@ -44,9 +44,9 @@ proof (subst compose_def, subst Prod_eq) show "\<And>a. a: A \<Longrightarrow> (\<^bold>\<lambda>x. c(x))`((\<^bold>\<lambda>x. b(x))`a) \<equiv> (\<^bold>\<lambda>x. c (b x))`a" proof compute show "\<And>a. a: A \<Longrightarrow> c((\<^bold>\<lambda>x. b(x))`a) \<equiv> (\<^bold>\<lambda>x. c(b(x)))`a" - by compute (simple lems: assms, compute?)+ - qed (simple lems: assms) -qed (simple lems: assms) + by (derive lems: assms) + qed (routine lems: assms) +qed (derive lems: assms) end @@ -24,9 +24,9 @@ unfolding fst_def by (derive lems: assms) lemma fst_comp: assumes "A: U(i)" and "B: A \<longrightarrow> U(i)" and "a: A" and "b: B(a)" shows "fst(<a,b>) \<equiv> a" unfolding fst_def -proof +proof compute show "a: A" and "b: B(a)" by fact+ -qed (simple lems: assms)+ +qed (routine lems: assms)+ lemma snd_type: assumes "\<Sum>x:A. B(x): U(i)" and "p: \<Sum>x:A. B(x)" shows "snd(p): B(fst p)" @@ -46,11 +46,11 @@ qed fact lemma snd_comp: assumes "A: U(i)" and "B: A \<longrightarrow> U(i)" and "a: A" and "b: B(a)" shows "snd(<a,b>) \<equiv> b" unfolding snd_def -proof +proof compute show "\<And>x y. y: B(x) \<Longrightarrow> y: B(x)" . show "a: A" by fact show "b: B(a)" by fact -qed (simple lems: assms) +qed (routine lems: assms) text "Rule attribute declarations:" @@ -63,7 +63,7 @@ text "Rule attribute declarations:" lemmas Sum_comp [comp] lemmas Sum_wellform [wellform] = Sum_wellform1 Sum_wellform2 -lemmas Sum_routine [intro] = Sum_form Sum_intro Sum_comp Sum_elim +lemmas Sum_routine [intro] = Sum_form Sum_intro Sum_elim section \<open>Empty type\<close> diff --git a/ex/Methods.thy b/ex/Methods.thy index 415fbc3..c78af14 100644 --- a/ex/Methods.thy +++ b/ex/Methods.thy @@ -14,7 +14,7 @@ text "Wellformedness results, metatheorems written into the object theory using lemma assumes "A : U(i)" "B: A \<longrightarrow> U(i)" "\<And>x. x : A \<Longrightarrow> C x: B x \<longrightarrow> U(i)" shows "\<Sum>x:A. \<Prod>y:B x. \<Sum>z:C x y. \<Prod>w:A. x =\<^sub>A w : U(i)" -by (simple lems: assms) +by (routine lems: assms) lemma @@ -38,7 +38,7 @@ text "Typechecking and constructing inhabitants:" \<comment> \<open>Correctly determines the type of the pair\<close> schematic_goal "\<lbrakk>A: U(i); B: U(i); a : A; b : B\<rbrakk> \<Longrightarrow> <a, b> : ?A" -by simple +by routine \<comment> \<open>Finds pair (too easy).\<close> schematic_goal "\<lbrakk>A: U(i); B: U(i); a : A; b : B\<rbrakk> \<Longrightarrow> ?x : A \<times> B" @@ -56,19 +56,19 @@ lemma assumes "A: U(i)" "a: A" shows "(\<^bold>\<lambda>x. <x,0>)`a \<equiv> <a,0>" proof compute - show "\<And>x. x: A \<Longrightarrow> <x,0>: A \<times> \<nat>" by simple -qed (simple lems: assms) + show "\<And>x. x: A \<Longrightarrow> <x,0>: A \<times> \<nat>" by routine +qed (routine lems: assms) lemma assumes "A: U(i)" "B: A \<longrightarrow> U(i)" "a: A" "b: B(a)" shows "(\<^bold>\<lambda>x y. <x,y>)`a`b \<equiv> <a,b>" proof compute - show "\<And>x. x: A \<Longrightarrow> \<^bold>\<lambda>y. <x,y>: \<Prod>y:B(x). \<Sum>x:A. B(x)" by (simple lems: assms) + show "\<And>x. x: A \<Longrightarrow> \<^bold>\<lambda>y. <x,y>: \<Prod>y:B(x). \<Sum>x:A. B(x)" by (routine lems: assms) show "(\<^bold>\<lambda>b. <a,b>)`b \<equiv> <a, b>" proof compute - show "\<And>b. b: B(a) \<Longrightarrow> <a, b>: \<Sum>x:A. B(x)" by (simple lems: assms) + show "\<And>b. b: B(a) \<Longrightarrow> <a, b>: \<Sum>x:A. B(x)" by (routine lems: assms) qed fact qed fact diff --git a/ex/Synthesis.thy b/ex/Synthesis.thy index cff9374..a5e77ec 100644 --- a/ex/Synthesis.thy +++ b/ex/Synthesis.thy @@ -21,7 +21,7 @@ text " text "First we show that the property we want is well-defined." lemma pred_welltyped: "\<Sum>pred:\<nat>\<rightarrow>\<nat> . ((pred`0) =\<^sub>\<nat> 0) \<times> (\<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n): U(O)" -by simple +by routine text " Now we look for an inhabitant of this type. @@ -33,7 +33,7 @@ schematic_goal "?p`0 \<equiv> 0" and "\<And>n. n: \<nat> \<Longrightarrow> (?p`( apply compute prefer 4 apply compute prefer 3 apply compute -apply (rule Nat_routine Nat_elim | assumption)+ +apply (rule Nat_routine Nat_elim | compute | assumption)+ done text " @@ -43,36 +43,36 @@ text " definition pred :: Term where "pred \<equiv> \<^bold>\<lambda>n. ind\<^sub>\<nat> (\<lambda>a b. a) 0 n" -lemma pred_type: "pred: \<nat> \<rightarrow> \<nat>" unfolding pred_def by simple +lemma pred_type: "pred: \<nat> \<rightarrow> \<nat>" unfolding pred_def by routine lemma pred_props: "<refl(0), \<^bold>\<lambda>n. refl(n)>: ((pred`0) =\<^sub>\<nat> 0) \<times> (\<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n)" -proof (simple lems: pred_type) +proof (routine lems: pred_type) have *: "pred`0 \<equiv> 0" unfolding pred_def proof compute - show "\<And>n. n: \<nat> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>a b. a) 0 n: \<nat>" by simple + show "\<And>n. n: \<nat> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>a b. a) 0 n: \<nat>" by routine show "ind\<^sub>\<nat> (\<lambda>a b. a) 0 0 \<equiv> 0" proof compute show "\<nat>: U(O)" .. - qed simple + qed routine qed rule - then show "refl(0): (pred`0) =\<^sub>\<nat> 0" by (subst *) simple + then show "refl(0): (pred`0) =\<^sub>\<nat> 0" by (subst *) routine show "\<^bold>\<lambda>n. refl(n): \<Prod>n:\<nat>. (pred`(succ(n))) =\<^sub>\<nat> n" unfolding pred_def proof show "\<And>n. n: \<nat> \<Longrightarrow> refl(n): ((\<^bold>\<lambda>n. ind\<^sub>\<nat> (\<lambda>a b. a) 0 n)`succ(n)) =\<^sub>\<nat> n" proof compute - show "\<And>n. n: \<nat> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>a b. a) 0 n: \<nat>" by simple + show "\<And>n. n: \<nat> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>a b. a) 0 n: \<nat>" by routine show "\<And>n. n: \<nat> \<Longrightarrow> refl(n): ind\<^sub>\<nat> (\<lambda>a b. a) 0 (succ n) =\<^sub>\<nat> n" proof compute show "\<nat>: U(O)" .. - qed simple + qed routine qed rule qed rule qed theorem "<pred, <refl(0), \<^bold>\<lambda>n. refl(n)>>: \<Sum>pred:\<nat>\<rightarrow>\<nat> . ((pred`0) =\<^sub>\<nat> 0) \<times> (\<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n)" -by (simple lems: pred_welltyped pred_type pred_props) +by (routine lems: pred_welltyped pred_type pred_props) end diff --git a/tests/Subgoal.thy b/tests/Subgoal.thy index 9690013..82d7e5d 100644 --- a/tests/Subgoal.thy +++ b/tests/Subgoal.thy @@ -25,11 +25,11 @@ apply standard apply (rule Prod_intro) subgoal premises 4 for u z q apply (rule Equal_elim[where ?x=u and ?y=z]) - apply (simple lems: assms 4) + apply (routine lems: assms 4) done - apply (simple lems: assms 1 2 3) + apply (routine lems: assms 1 2 3) done - apply (simple lems: assms 1 2) + apply (routine lems: assms 1 2) done apply fact done @@ -52,9 +52,9 @@ text " Try (and fail) to synthesize the constant for path composition, following the proof of \<open>rpathcomp_type\<close> below. " -apply (rule Prod_intro) - apply (rule Prod_intro) - apply (rule Prod_intro) +apply (rule intros) + apply (rule intros) + apply (rule intros) subgoal 123 for x y p apply (rule Equal_elim[where ?x=x and ?y=y and ?A=A]) oops |