diff options
author | Josh Chen | 2018-09-18 11:39:40 +0200 |
---|---|---|
committer | Josh Chen | 2018-09-18 11:39:40 +0200 |
commit | a9588dfbd929fbc1b53a5c9b4f41fc5eb4ed4e46 (patch) | |
tree | ef21f4328214618f98ee465e92fb3308dfb786da /ex/Synthesis.thy | |
parent | a2bb39ee8002eccc04b0cdaa82143840e6ec2565 (diff) | |
parent | 6857e783fa5cb91f058be322a18fb9ea583f2aad (diff) |
Merge branch 'develop', ready for release 0.1.0
Diffstat (limited to 'ex/Synthesis.thy')
-rw-r--r-- | ex/Synthesis.thy | 94 |
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 |