From 8833cdf99d3128466d85eb88aeb8e340e07e937c Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sat, 18 Aug 2018 23:27:25 +0200
Subject: Reorganize methods

---
 ex/Methods.thy   | 12 ++++++------
 ex/Synthesis.thy | 20 ++++++++++----------
 2 files changed, 16 insertions(+), 16 deletions(-)

(limited to 'ex')

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
-- 
cgit v1.2.3