521 qed |
521 qed |
522 qed |
522 qed |
523 qed |
523 qed |
524 qed |
524 qed |
525 |
525 |
|
526 text {* Equality of environments for code generation *} |
|
527 |
|
528 lemma [code func, code func del]: |
|
529 fixes e1 e2 :: "('b\<Colon>eq, 'a\<Colon>eq, 'c\<Colon>eq) env" |
|
530 shows "e1 = e2 \<longleftrightarrow> e1 = e2" .. |
|
531 |
|
532 lemma eq_env_code [code func]: |
|
533 fixes x y :: "'a\<Colon>eq" |
|
534 and f g :: "'c\<Colon>{eq, finite} \<Rightarrow> ('b\<Colon>eq, 'a, 'c) env option" |
|
535 shows "Env x f = Env y g \<longleftrightarrow> |
|
536 x = y \<and> (\<forall>z\<in>UNIV. case f z |
|
537 of None \<Rightarrow> (case g z |
|
538 of None \<Rightarrow> True | Some _ \<Rightarrow> False) |
|
539 | Some a \<Rightarrow> (case g z |
|
540 of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" (is ?env) |
|
541 and "Val a = Val b \<longleftrightarrow> a = b" |
|
542 and "Val a = Env y g \<longleftrightarrow> False" |
|
543 and "Env x f = Val b \<longleftrightarrow> False" |
|
544 proof - |
|
545 have "f = g \<longleftrightarrow> (\<forall>z. case f z |
|
546 of None \<Rightarrow> (case g z |
|
547 of None \<Rightarrow> True | Some _ \<Rightarrow> False) |
|
548 | Some a \<Rightarrow> (case g z |
|
549 of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" (is "?lhs = ?rhs") |
|
550 proof |
|
551 assume ?lhs |
|
552 then show ?rhs by (auto split: option.splits) |
|
553 next |
|
554 assume assm: ?rhs (is "\<forall>z. ?prop z") |
|
555 show ?lhs |
|
556 proof |
|
557 fix z |
|
558 from assm have "?prop z" .. |
|
559 then show "f z = g z" by (auto split: option.splits) |
|
560 qed |
|
561 qed |
|
562 then show ?env by simp |
|
563 qed simp_all |
|
564 |
526 end |
565 end |