aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Coprod.thy2
-rw-r--r--Equal.thy2
-rw-r--r--EqualProps.thy66
-rw-r--r--HoTT.thy8
-rw-r--r--HoTT_Methods.thy42
-rw-r--r--Nat.thy2
-rw-r--r--Prod.thy4
-rw-r--r--ProdProps.thy12
-rw-r--r--Proj.thy8
-rw-r--r--Sum.thy2
-rw-r--r--ex/Methods.thy12
-rw-r--r--ex/Synthesis.thy20
-rw-r--r--tests/Subgoal.thy12
13 files changed, 98 insertions, 94 deletions
diff --git a/Coprod.thy b/Coprod.thy
index f62bb06..4607d1d 100644
--- a/Coprod.thy
+++ b/Coprod.thy
@@ -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
diff --git a/Equal.thy b/Equal.thy
index 722a9b9..772072a 100644
--- a/Equal.thy
+++ b/Equal.thy
@@ -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
diff --git a/HoTT.thy b/HoTT.thy
index 789eed2..60e0e71 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -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
diff --git a/Nat.thy b/Nat.thy
index b48804a..45c3a2e 100644
--- a/Nat.thy
+++ b/Nat.thy
@@ -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
diff --git a/Prod.thy b/Prod.thy
index 323bef4..9dbb01e 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -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
diff --git a/Proj.thy b/Proj.thy
index dffc127..a1c4c8f 100644
--- a/Proj.thy
+++ b/Proj.thy
@@ -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:"
diff --git a/Sum.thy b/Sum.thy
index dce5834..f97bef1 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -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