isabelle: src/HOL/Imperative_HOL/Relational.thy@346caefc9f57 (annotated)

27656 d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: diff changeset	1	theory Relational
28744 9257bb7bcd2d removed Assert.thy haftmann parents: 28145 diff changeset	2	imports Array Ref
27656 d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: diff changeset	3	begin
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: diff changeset	4
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: diff changeset	5	lemma crel_option_case:
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: diff changeset	6	assumes "crel (case x of None \<Rightarrow> n \| Some y \<Rightarrow> s y) h h' r"
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: diff changeset	7	obtains "x = None" "crel n h h' r"
d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: diff changeset	8	\| y where "x = Some y" "crel (s y) h h' r"
37771 1bec64044b5e spelt out relational framework in a consistent way haftmann parents: 37758 diff changeset	9	using assms unfolding crel_def by (auto split: option.splits)
27656 d4f6e64ee7cc added verification framework for the HeapMonad and quicksort as example for this framework bulwahn parents: diff changeset	10
37771 1bec64044b5e spelt out relational framework in a consistent way haftmann parents: 37758 diff changeset	11	end

author	haftmann
	Mon, 12 Jul 2010 16:26:48 +0200
changeset 37774	346caefc9f57
parent 37773	786ecb1af09b
child 37775	7371534297a9
permissions	-rw-r--r--