diff options
Diffstat (limited to 'ex/Synthesis.thy')
| -rw-r--r-- | ex/Synthesis.thy | 16 |
1 files changed, 7 insertions, 9 deletions
diff --git a/ex/Synthesis.thy b/ex/Synthesis.thy index ef6673c..cd5c4e1 100644 --- a/ex/Synthesis.thy +++ b/ex/Synthesis.thy @@ -19,9 +19,7 @@ text " 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 " - First we show that the property we want is well-defined. -" +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 @@ -40,11 +38,11 @@ apply (rule Nat_rules | assumption)+ done text " - The above proof finds a candidate, namely \<open>\<^bold>\<lambda>n. ind\<^sub>\<nat> (\<lambda>a b. a) n n\<close>. + 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) n n" +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 @@ -52,7 +50,7 @@ lemma pred_props: "<refl(0), \<^bold>\<lambda>n. refl(n)>: ((pred`0) =\<^sub>\<n proof (simple 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) n n: \<nat>" by simple + show "\<And>n. n: \<nat> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>a b. a) 0 n: \<nat>" by simple show "ind\<^sub>\<nat> (\<lambda>a b. a) 0 0 \<equiv> 0" proof (rule Nat_comps) show "\<nat>: U(O)" .. @@ -62,10 +60,10 @@ proof (simple lems: pred_type) 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) n n)`succ(n)) =\<^sub>\<nat> n" + 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) n n: \<nat>" by simple - show "\<And>n. n: \<nat> \<Longrightarrow> refl(n): ind\<^sub>\<nat> (\<lambda>a b. a) (succ n) (succ n) =\<^sub>\<nat> n" + show "\<And>n. n: \<nat> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>a b. a) 0 n: \<nat>" by simple + 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 |