equal
deleted
inserted
replaced
13 "abs_sorted cmp [] \<longleftrightarrow> True" |
13 "abs_sorted cmp [] \<longleftrightarrow> True" |
14 "abs_sorted cmp [x] \<longleftrightarrow> True" |
14 "abs_sorted cmp [x] \<longleftrightarrow> True" |
15 "abs_sorted cmp (x#y#xs) \<longleftrightarrow> cmp x y \<and> abs_sorted cmp (y#xs)" |
15 "abs_sorted cmp (x#y#xs) \<longleftrightarrow> cmp x y \<and> abs_sorted cmp (y#xs)" |
16 |
16 |
17 abbreviation (in ord) |
17 abbreviation (in ord) |
18 "sorted \<equiv> abs_sorted less_eq" |
|
19 |
|
20 abbreviation |
|
21 "sorted \<equiv> abs_sorted less_eq" |
18 "sorted \<equiv> abs_sorted less_eq" |
22 |
19 |
23 lemma (in order) sorted_weakening: |
20 lemma (in order) sorted_weakening: |
24 assumes "sorted (x # xs)" |
21 assumes "sorted (x # xs)" |
25 shows "sorted xs" |
22 shows "sorted xs" |
136 "fin == product fin fin" |
133 "fin == product fin fin" |
137 apply default |
134 apply default |
138 apply (simp_all add: "fin_*_def") |
135 apply (simp_all add: "fin_*_def") |
139 apply (unfold split_paired_all) |
136 apply (unfold split_paired_all) |
140 apply (rule product_all) |
137 apply (rule product_all) |
141 apply (rule finite_class.member_fin)+ |
138 apply (rule member_fin)+ |
142 done |
139 done |
143 |
140 |
144 instance option :: (finite) finite |
141 instance option :: (finite) finite |
145 "fin == None # map Some fin" |
142 "fin == None # map Some fin" |
146 proof (default, unfold fin_option_def) |
143 proof (default, unfold fin_option_def) |
147 fix x :: "'a::finite option" |
144 fix x :: "'a::finite option" |
148 show "x \<in> set (None # map Some fin)" |
145 show "x \<in> set (None # map Some fin)" |
149 proof (cases x) |
146 proof (cases x) |
150 case None then show ?thesis by auto |
147 case None then show ?thesis by auto |
151 next |
148 next |
152 case (Some x) then show ?thesis by (auto intro: finite_class.member_fin) |
149 case (Some x) then show ?thesis by (auto intro: member_fin) |
153 qed |
150 qed |
154 qed |
151 qed |
155 |
152 |
156 consts |
153 consts |
157 get_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a option" |
154 get_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a option" |