2198 apply(rule ACIfSL.axioms[OF ACIfSL_max]) |
2198 apply(rule ACIfSL.axioms[OF ACIfSL_max]) |
2199 apply(rule ACIfSLlin_axioms.intro) |
2199 apply(rule ACIfSLlin_axioms.intro) |
2200 apply(auto simp:max_def) |
2200 apply(auto simp:max_def) |
2201 done |
2201 done |
2202 |
2202 |
2203 lemma partial_order_order: |
|
2204 "partial_order (op \<le> :: 'a::order \<Rightarrow> 'a \<Rightarrow> bool)" |
|
2205 apply(rule partial_order.intro) |
|
2206 apply(simp_all) |
|
2207 done |
|
2208 |
|
2209 lemma lower_semilattice_lin_min: |
|
2210 "lower_semilattice(op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)" |
|
2211 apply(rule lower_semilattice.intro) |
|
2212 apply(rule partial_order_order) |
|
2213 apply(rule lower_semilattice_axioms.intro) |
|
2214 apply(simp add:min_def linorder_not_le order_less_imp_le) |
|
2215 apply(simp add:min_def linorder_not_le order_less_imp_le) |
|
2216 apply(simp add:min_def linorder_not_le order_less_imp_le) |
|
2217 done |
|
2218 |
|
2219 lemma upper_semilattice_lin_min: |
|
2220 "upper_semilattice(op \<le>) (max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)" |
|
2221 apply(rule upper_semilattice.intro) |
|
2222 apply(rule partial_order_order) |
|
2223 apply(rule upper_semilattice_axioms.intro) |
|
2224 apply(simp add: max_def linorder_not_le order_less_imp_le) |
|
2225 apply(simp add: max_def linorder_not_le order_less_imp_le) |
|
2226 apply(simp add: max_def linorder_not_le order_less_imp_le) |
|
2227 done |
|
2228 |
|
2229 lemma Lattice_min_max: "Lattice (op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) max" |
2203 lemma Lattice_min_max: "Lattice (op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) max" |
2230 apply(rule Lattice.intro) |
2204 apply(rule Lattice.intro) |
2231 apply(rule partial_order_order) |
2205 apply(rule partial_order_order) |
2232 apply(rule lower_semilattice.axioms[OF lower_semilattice_lin_min]) |
2206 apply(rule lower_semilattice.axioms[OF lower_semilattice_lin_min]) |
2233 apply(rule upper_semilattice.axioms[OF upper_semilattice_lin_min]) |
2207 apply(rule upper_semilattice.axioms[OF upper_semilattice_lin_max]) |
2234 done |
2208 done |
2235 |
2209 |
2236 lemma Distrib_Lattice_min_max: |
2210 lemma Distrib_Lattice_min_max: |
2237 "Distrib_Lattice (op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) max" |
2211 "Distrib_Lattice (op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) max" |
2238 apply(rule Distrib_Lattice.intro) |
2212 apply(rule Distrib_Lattice.intro) |
2239 apply(rule partial_order_order) |
2213 apply(rule partial_order_order) |
2240 apply(rule lower_semilattice.axioms[OF lower_semilattice_lin_min]) |
2214 apply(rule lower_semilattice.axioms[OF lower_semilattice_lin_min]) |
2241 apply(rule upper_semilattice.axioms[OF upper_semilattice_lin_min]) |
2215 apply(rule upper_semilattice.axioms[OF upper_semilattice_lin_max]) |
2242 apply(rule distrib_lattice_axioms.intro) |
2216 apply(rule distrib_lattice.axioms[OF distrib_lattice_min_max]) |
2243 apply(rule_tac x=x and y=y in linorder_le_cases) |
|
2244 apply(rule_tac x=x and y=z in linorder_le_cases) |
|
2245 apply(rule_tac x=y and y=z in linorder_le_cases) |
|
2246 apply(simp add:min_def max_def) |
|
2247 apply(simp add:min_def max_def) |
|
2248 apply(rule_tac x=y and y=z in linorder_le_cases) |
|
2249 apply(simp add:min_def max_def) |
|
2250 apply(simp add:min_def max_def) |
|
2251 apply(rule_tac x=x and y=z in linorder_le_cases) |
|
2252 apply(rule_tac x=y and y=z in linorder_le_cases) |
|
2253 apply(simp add:min_def max_def) |
|
2254 apply(simp add:min_def max_def) |
|
2255 apply(rule_tac x=y and y=z in linorder_le_cases) |
|
2256 apply(simp add:min_def max_def) |
|
2257 apply(simp add:min_def max_def) |
|
2258 done |
2217 done |
2259 |
2218 |
2260 text{* Now we instantiate the recursion equations and declare them |
2219 text{* Now we instantiate the recursion equations and declare them |
2261 simplification rules: *} |
2220 simplification rules: *} |
2262 |
2221 |