# HG changeset patch # User haftmann # Date 1188207254 -7200 # Node ID 4a405457e9d60f98b5603da14052adb65872979d # Parent d555d941f983cc3f819036177822d29c0d903bb5 added explicit equation for equality of nested environments diff -r d555d941f983 -r 4a405457e9d6 src/HOL/Library/Nested_Environment.thy --- a/src/HOL/Library/Nested_Environment.thy Mon Aug 27 08:31:01 2007 +0200 +++ b/src/HOL/Library/Nested_Environment.thy Mon Aug 27 11:34:14 2007 +0200 @@ -523,4 +523,43 @@ qed qed +text {* Equality of environments for code generation *} + +lemma [code func, code func del]: + fixes e1 e2 :: "('b\eq, 'a\eq, 'c\eq) env" + shows "e1 = e2 \ e1 = e2" .. + +lemma eq_env_code [code func]: + fixes x y :: "'a\eq" + and f g :: "'c\{eq, finite} \ ('b\eq, 'a, 'c) env option" + shows "Env x f = Env y g \ + x = y \ (\z\UNIV. case f z + of None \ (case g z + of None \ True | Some _ \ False) + | Some a \ (case g z + of None \ False | Some b \ a = b))" (is ?env) + and "Val a = Val b \ a = b" + and "Val a = Env y g \ False" + and "Env x f = Val b \ False" +proof - + have "f = g \ (\z. case f z + of None \ (case g z + of None \ True | Some _ \ False) + | Some a \ (case g z + of None \ False | Some b \ a = b))" (is "?lhs = ?rhs") + proof + assume ?lhs + then show ?rhs by (auto split: option.splits) + next + assume assm: ?rhs (is "\z. ?prop z") + show ?lhs + proof + fix z + from assm have "?prop z" .. + then show "f z = g z" by (auto split: option.splits) + qed + qed + then show ?env by simp +qed simp_all + end diff -r d555d941f983 -r 4a405457e9d6 src/HOL/ex/ExecutableContent.thy --- a/src/HOL/ex/ExecutableContent.thy Mon Aug 27 08:31:01 2007 +0200 +++ b/src/HOL/ex/ExecutableContent.thy Mon Aug 27 11:34:14 2007 +0200 @@ -19,7 +19,7 @@ List_Prefix Nat_Infinity NatPair - (*Nested_Environment*) + Nested_Environment Permutation Primes Product_ord