452 |
452 |
453 lemma bij_swap_iff: "bij (swap a b f) = bij f" |
453 lemma bij_swap_iff: "bij (swap a b f) = bij f" |
454 by (simp add: bij_def) |
454 by (simp add: bij_def) |
455 |
455 |
456 |
456 |
457 subsection {* Order on functions *} |
457 subsection {* Order and lattice on functions *} |
|
458 |
|
459 instance "fun" :: (type, ord) ord |
|
460 le_fun_def: "f \<le> g \<equiv> \<forall>x. f x \<le> g x" |
|
461 less_fun_def: "f < g \<equiv> f \<le> g \<and> f \<noteq> g" .. |
|
462 |
|
463 instance "fun" :: (type, preorder) preorder |
|
464 by default (auto simp add: le_fun_def less_fun_def intro: order_trans) |
458 |
465 |
459 instance "fun" :: (type, order) order |
466 instance "fun" :: (type, order) order |
460 le_fun_def: "f \<le> g \<equiv> \<forall>x. f x \<le> g x" |
467 by default (rule ext, auto simp add: le_fun_def less_fun_def intro: order_antisym) |
461 less_fun_def: "f < g \<equiv> f \<le> g \<and> f \<noteq> g" |
|
462 by default |
|
463 (auto simp add: le_fun_def less_fun_def intro: order_trans, rule ext, auto intro: order_antisym) |
|
464 |
468 |
465 lemma le_funI: "(\<And>x. f x \<le> g x) \<Longrightarrow> f \<le> g" |
469 lemma le_funI: "(\<And>x. f x \<le> g x) \<Longrightarrow> f \<le> g" |
466 unfolding le_fun_def by simp |
470 unfolding le_fun_def by simp |
467 |
471 |
468 lemma le_funE: "f \<le> g \<Longrightarrow> (f x \<le> g x \<Longrightarrow> P) \<Longrightarrow> P" |
472 lemma le_funE: "f \<le> g \<Longrightarrow> (f x \<le> g x \<Longrightarrow> P) \<Longrightarrow> P" |
469 unfolding le_fun_def by simp |
473 unfolding le_fun_def by simp |
470 |
474 |
471 lemma le_funD: "f \<le> g \<Longrightarrow> f x \<le> g x" |
475 lemma le_funD: "f \<le> g \<Longrightarrow> f x \<le> g x" |
472 unfolding le_fun_def by simp |
476 unfolding le_fun_def by simp |
473 |
477 |
474 instance "fun" :: (type, ord) ord .. |
478 text {* |
|
479 Handy introduction and elimination rules for @{text "\<le>"} |
|
480 on unary and binary predicates |
|
481 *} |
|
482 |
|
483 lemma predicate1I [Pure.intro!, intro!]: |
|
484 assumes PQ: "\<And>x. P x \<Longrightarrow> Q x" |
|
485 shows "P \<le> Q" |
|
486 apply (rule le_funI) |
|
487 apply (rule le_boolI) |
|
488 apply (rule PQ) |
|
489 apply assumption |
|
490 done |
|
491 |
|
492 lemma predicate1D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x" |
|
493 apply (erule le_funE) |
|
494 apply (erule le_boolE) |
|
495 apply assumption+ |
|
496 done |
|
497 |
|
498 lemma predicate2I [Pure.intro!, intro!]: |
|
499 assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y" |
|
500 shows "P \<le> Q" |
|
501 apply (rule le_funI)+ |
|
502 apply (rule le_boolI) |
|
503 apply (rule PQ) |
|
504 apply assumption |
|
505 done |
|
506 |
|
507 lemma predicate2D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y" |
|
508 apply (erule le_funE)+ |
|
509 apply (erule le_boolE) |
|
510 apply assumption+ |
|
511 done |
|
512 |
|
513 lemma rev_predicate1D: "P x ==> P <= Q ==> Q x" |
|
514 by (rule predicate1D) |
|
515 |
|
516 lemma rev_predicate2D: "P x y ==> P <= Q ==> Q x y" |
|
517 by (rule predicate2D) |
|
518 |
|
519 instance "fun" :: (type, lattice) lattice |
|
520 inf_fun_eq: "inf f g \<equiv> (\<lambda>x. inf (f x) (g x))" |
|
521 sup_fun_eq: "sup f g \<equiv> (\<lambda>x. sup (f x) (g x))" |
|
522 apply intro_classes |
|
523 unfolding inf_fun_eq sup_fun_eq |
|
524 apply (auto intro: le_funI) |
|
525 apply (rule le_funI) |
|
526 apply (auto dest: le_funD) |
|
527 apply (rule le_funI) |
|
528 apply (auto dest: le_funD) |
|
529 done |
|
530 |
|
531 instance "fun" :: (type, distrib_lattice) distrib_lattice |
|
532 by default (auto simp add: inf_fun_eq sup_fun_eq sup_inf_distrib1) |
475 |
533 |
476 |
534 |
477 subsection {* Code generator setup *} |
535 subsection {* Code generator setup *} |
478 |
536 |
479 code_const "op \<circ>" |
537 code_const "op \<circ>" |