# HG changeset patch
# User haftmann
# Date 1278944808 -7200
# Node ID 346caefc9f575056b4c8b9e82efac3d831a2942c
# Parent  786ecb1af09ba2b98508dd4a78b136e30fe8f3b6
dropped unused lemmas of dubious value

diff -r 786ecb1af09b -r 346caefc9f57 src/HOL/Imperative_HOL/Relational.thy
--- a/src/HOL/Imperative_HOL/Relational.thy	Mon Jul 12 16:23:30 2010 +0200
+++ b/src/HOL/Imperative_HOL/Relational.thy	Mon Jul 12 16:26:48 2010 +0200
@@ -2,33 +2,6 @@
 imports Array Ref
 begin
 
-lemma crel_assert_eq: "(\<And>h h' r. crel f h h' r \<Longrightarrow> P r) \<Longrightarrow> f \<guillemotright>= assert P = f"
-unfolding crel_def bind_def Let_def assert_def
-  raise_def return_def prod_case_beta
-apply (cases f)
-apply simp
-apply (simp add: expand_fun_eq split_def)
-apply (auto split: option.split)
-done
-
-lemma crel_option_caseI:
-  assumes "\<And>y. x = Some y \<Longrightarrow> crel (s y) h h' r"
-  assumes "x = None \<Longrightarrow> crel n h h' r"
-  shows "crel (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h h' r"
-using assms
-by (auto split: option.split)
-
-lemma crelI2:
-  assumes "\<exists>h' rs'. crel f h h' rs' \<and> (\<exists>h'' rs. crel (g rs') h' h'' rs)"
-  shows "\<exists>h'' rs. crel (f\<guillemotright>= g) h h'' rs"
-  oops
-
-lemma crel_ifI2:
-  assumes "c \<Longrightarrow> \<exists>h' r. crel t h h' r"
-  "\<not> c \<Longrightarrow> \<exists>h' r. crel e h h' r"
-  shows "\<exists> h' r. crel (if c then t else e) h h' r"
-  oops
-
 lemma crel_option_case:
   assumes "crel (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h h' r"
   obtains "x = None" "crel n h h' r"