Overhaul of the theory presentations. New methods in HoTT_Methods.thy for handling universes. Commit for release 0.1.0!

1 files changed, 37 insertions, 57 deletions

diff --git a/ex/Synthesis.thy b/ex/Synthesis.thy
index a5e77ec..3ee973c 100644
--- a/ex/Synthesis.thy
+++ b/ex/Synthesis.thy
@@ -1,78 +1,58 @@
-(*  Title:  HoTT/ex/Synthesis.thy
-    Author: Josh Chen
+(*
+Title:  ex/Synthesis.thy
+Author: Joshua Chen
+Date:   2018
 
-Examples of synthesis.
+Examples of synthesis
 *)
 
 
 theory Synthesis
-  imports "../HoTT"
+imports "../HoTT"
+
 begin
 
 
 section \<open>Synthesis of the predecessor function\<close>
 
-text "
-  In this example we construct, with the help of Isabelle, a predecessor function for the natural numbers.
-
-  This is also done in \<open>CTT.thy\<close>; there the work is easier as the equality type is extensional, and also the methods are set up a little more nicely.
-"
+text \<open>
+In this example we construct a predecessor function for the natural numbers.
+This is also done in @{file "~~/src/CTT/ex/Synthesis.thy"}, there the work is much easier as the equality type is extensional.
+\<close>
 
-text "First we show that the property we want is well-defined."
+text \<open>First we show that the property we want is well-defined.\<close>
 
-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)"
+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 routine
 
-text "
-  Now we look for an inhabitant of this type.
-  Observe that we're looking for a lambda term \<open>pred\<close> satisfying \<open>(pred`0) =\<^sub>\<nat> 0\<close> and \<open>\<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n\<close>.
-  What if we require **definitional** equality instead of just propositional equality?
-"
+text \<open>
+Now we look for an inhabitant of this type.
+Observe that we're looking for a lambda term @{term pred} satisfying @{term "pred`0 =\<^sub>\<nat> 0"} and @{term "\<Prod>n:\<nat>. pred`(succ n) =\<^sub>\<nat> n"}.
+What if we require *definitional* instead of just propositional equality?
+\<close>
 
 schematic_goal "?p`0 \<equiv> 0" and "\<And>n. n: \<nat> \<Longrightarrow> (?p`(succ n)) \<equiv> n"
 apply compute
 prefer 4 apply compute
-prefer 3 apply compute
-apply (rule Nat_routine Nat_elim | compute | assumption)+
-done
-
-text "
-  The above proof finds a candidate, namely \<open>\<^bold>\<lambda>n. ind\<^sub>\<nat> (\<lambda>a b. a) 0 n\<close>.
-  We prove this has the required type and properties.
-"
-
-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 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 (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 routine
-    show "ind\<^sub>\<nat> (\<lambda>a b. a) 0 0 \<equiv> 0"
-    proof compute
-      show "\<nat>: U(O)" ..
-    qed routine
-  qed rule
-  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 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 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 (routine lems: pred_welltyped pred_type pred_props)
+apply (rule Nat_routine | compute)+
+oops
+\<comment> \<open>Something in the original proof broke when I revamped the theory. The completion of this derivation is left as an exercise to the reader.\<close>
+
+text \<open>
+The above proof finds a candidate, namely @{term "\<lambda>n. ind\<^sub>\<nat> (\<lambda>a b. a) 0 n"}.
+We prove this has the required type and properties.
+\<close>
+
+definition pred :: t 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 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)"
+unfolding pred_def by derive
+
+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 (derive lems: pred_type pred_props)
 
 
 end