diff options
author | Josh Chen | 2018-08-15 11:47:30 +0200 |
---|---|---|
committer | Josh Chen | 2018-08-15 11:47:30 +0200 |
commit | f4f468878fc0459a806b02cdf8921af6fcac2759 (patch) | |
tree | 5f646632b36c97cc783fe3209d7df1e4b47d59b0 /ex/Synthesis.thy | |
parent | e94784953a751b0720689b686e607c95ba0f0592 (diff) |
Tweak proof methods, some type rules; add HoTT Book examples
Diffstat (limited to 'ex/Synthesis.thy')
-rw-r--r-- | ex/Synthesis.thy | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/ex/Synthesis.thy b/ex/Synthesis.thy index 60655e5..48d762c 100644 --- a/ex/Synthesis.thy +++ b/ex/Synthesis.thy @@ -33,10 +33,10 @@ text " " schematic_goal "?p`0 \<equiv> 0" and "\<And>n. n: \<nat> \<Longrightarrow> (?p`(succ n)) \<equiv> n" -apply (subst comp, rule Nat_rules) -prefer 3 apply (subst comp, rule Nat_rules) +apply (subst comp) +prefer 4 apply (subst comp) prefer 3 apply (rule Nat_rules) -prefer 8 apply (rule Nat_rules | assumption)+ +apply (rule Nat_rules | assumption)+ done text " @@ -49,7 +49,7 @@ definition pred :: Term where "pred \<equiv> \<^bold>\<lambda>n. ind\<^sub>\<nat lemma pred_type: "pred: \<nat> \<rightarrow> \<nat>" unfolding pred_def by simple 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 lem: pred_type) +proof (simple lems: pred_type) have *: "pred`0 \<equiv> 0" unfolding pred_def proof (subst comp) show "\<And>n. n: \<nat> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>a b. a) n n: \<nat>" by simple @@ -75,7 +75,7 @@ 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 lem: pred_welltyped pred_type pred_props) +by (simple lems: pred_welltyped pred_type pred_props) end
\ No newline at end of file |