2326 apply(rule ACIfSLlin_axioms.intro) |
2326 apply(rule ACIfSLlin_axioms.intro) |
2327 apply(auto simp:max_def) |
2327 apply(auto simp:max_def) |
2328 done |
2328 done |
2329 |
2329 |
2330 lemma Lattice_min_max: "Lattice (op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) max" |
2330 lemma Lattice_min_max: "Lattice (op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) max" |
2331 apply (rule Lattice.intro, simp) |
2331 apply(rule Lattice.intro) |
|
2332 apply simp |
2332 apply(erule (1) order_trans) |
2333 apply(erule (1) order_trans) |
2333 apply(erule (1) order_antisym) |
2334 apply(erule (1) order_antisym) |
2334 apply(simp add:min_def max_def linorder_not_le order_less_imp_le) |
2335 apply(simp add:min_def max_def linorder_not_le order_less_imp_le) |
2335 apply(simp add:min_def max_def linorder_not_le order_less_imp_le) |
2336 apply(simp add:min_def max_def linorder_not_le order_less_imp_le) |
2336 apply(simp add:min_def max_def linorder_not_le order_less_imp_le) |
2337 apply(simp add:min_def max_def linorder_not_le order_less_imp_le) |
2337 apply(simp add:min_def max_def linorder_not_le order_less_imp_le) |
2338 apply(simp add:min_def max_def linorder_not_le order_less_imp_le) |
2338 apply(simp add:min_def max_def linorder_not_le order_less_imp_le) |
2339 apply(simp add:min_def max_def linorder_not_le order_less_imp_le) |
2339 apply(simp add:min_def max_def linorder_not_le order_less_imp_le) |
2340 apply(simp add:min_def max_def linorder_not_le order_less_imp_le) |
|
2341 apply(rule_tac x=x and y=y in linorder_le_cases) |
|
2342 apply(simp add:min_def max_def) |
|
2343 apply(simp add:min_def max_def) |
|
2344 apply(rule_tac x=y and y=z in linorder_le_cases) |
|
2345 apply(simp add:min_def max_def) |
|
2346 apply(simp add:min_def max_def) |
|
2347 done |
|
2348 |
|
2349 lemma DistribLattice_min_max: "DistribLattice (op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) max" |
|
2350 apply(rule DistribLattice.intro) |
|
2351 apply(rule Lattice_min_max) |
|
2352 apply(rule DistribLattice_axioms.intro) |
2340 apply(rule_tac x=x and y=y in linorder_le_cases) |
2353 apply(rule_tac x=x and y=y in linorder_le_cases) |
2341 apply(rule_tac x=x and y=z in linorder_le_cases) |
2354 apply(rule_tac x=x and y=z in linorder_le_cases) |
2342 apply(rule_tac x=y and y=z in linorder_le_cases) |
2355 apply(rule_tac x=y and y=z in linorder_le_cases) |
2343 apply(simp add:min_def max_def) |
2356 apply(simp add:min_def max_def) |
2344 apply(simp add:min_def max_def) |
2357 apply(simp add:min_def max_def) |
2350 apply(simp add:min_def max_def) |
2363 apply(simp add:min_def max_def) |
2351 apply(simp add:min_def max_def) |
2364 apply(simp add:min_def max_def) |
2352 apply(rule_tac x=y and y=z in linorder_le_cases) |
2365 apply(rule_tac x=y and y=z in linorder_le_cases) |
2353 apply(simp add:min_def max_def) |
2366 apply(simp add:min_def max_def) |
2354 apply(simp add:min_def max_def) |
2367 apply(simp add:min_def max_def) |
2355 |
|
2356 apply(rule_tac x=x and y=y in linorder_le_cases) |
|
2357 apply(rule_tac x=x and y=z in linorder_le_cases) |
|
2358 apply(rule_tac x=y and y=z in linorder_le_cases) |
|
2359 apply(simp add:min_def max_def) |
|
2360 apply(simp add:min_def max_def) |
|
2361 apply(rule_tac x=y and y=z in linorder_le_cases) |
|
2362 apply(simp add:min_def max_def) |
|
2363 apply(simp add:min_def max_def) |
|
2364 apply(rule_tac x=x and y=z in linorder_le_cases) |
|
2365 apply(rule_tac x=y and y=z in linorder_le_cases) |
|
2366 apply(simp add:min_def max_def) |
|
2367 apply(simp add:min_def max_def) |
|
2368 apply(rule_tac x=y and y=z in linorder_le_cases) |
|
2369 apply(simp add:min_def max_def) |
|
2370 apply(simp add:min_def max_def) |
|
2371 done |
2368 done |
2372 |
2369 |
2373 text{* Now we instantiate the recursion equations and declare them |
2370 text{* Now we instantiate the recursion equations and declare them |
2374 simplification rules: *} |
2371 simplification rules: *} |
2375 |
2372 |
2415 |
2412 |
2416 lemma Min_le_Max: |
2413 lemma Min_le_Max: |
2417 "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A \<le> Max A" |
2414 "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A \<le> Max A" |
2418 by(simp add: Min_def Max_def Lattice.Inf_le_Sup[OF Lattice_min_max]) |
2415 by(simp add: Min_def Max_def Lattice.Inf_le_Sup[OF Lattice_min_max]) |
2419 |
2416 |
2420 (* FIXME |
|
2421 lemma max_Min2_distrib: |
2417 lemma max_Min2_distrib: |
2422 "\<lbrakk> finite A; A \<noteq> {}; finite B; B \<noteq> {} \<rbrakk> \<Longrightarrow> |
2418 "\<lbrakk> finite A; A \<noteq> {}; finite B; B \<noteq> {} \<rbrakk> \<Longrightarrow> |
2423 max (Min A) (Min B) = Min{ max a b |a b. a \<in> A \<and> b \<in> B}" |
2419 max (Min A) (Min B) = Min{ max a b |a b. a \<in> A \<and> b \<in> B}" |
2424 by(simp add: Min_def Max_def Lattice.sup_Inf2_distrib[OF Lattice_min_max]) |
2420 by(simp add: Min_def DistribLattice.sup_Inf2_distrib[OF DistribLattice_min_max]) |
2425 *) |
|
2426 |
2421 |
2427 end |
2422 end |