Reorganize methods

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