1.1 --- a/src/HOL/Predicate.thy	Fri Nov 19 11:44:46 2010 +0100
     1.2 +++ b/src/HOL/Predicate.thy	Fri Nov 19 14:35:58 2010 +0100
     1.3 @@ -377,14 +377,17 @@
     1.4    "Pred (eval x) = x"
     1.5    by (cases x) simp
     1.6  
     1.7 -lemma eval_inject: "eval x = eval y \<longleftrightarrow> x = y"
     1.8 -  by (cases x) auto
     1.9 +lemma pred_eqI:
    1.10 +  "(\<And>w. eval P w \<longleftrightarrow> eval Q w) \<Longrightarrow> P = Q"
    1.11 +  by (cases P, cases Q) (auto simp add: fun_eq_iff)
    1.12  
    1.13 -definition single :: "'a \<Rightarrow> 'a pred" where
    1.14 -  "single x = Pred ((op =) x)"
    1.15 +lemma eval_mem [simp]:
    1.16 +  "x \<in> eval P \<longleftrightarrow> eval P x"
    1.17 +  by (simp add: mem_def)
    1.18  
    1.19 -definition bind :: "'a pred \<Rightarrow> ('a \<Rightarrow> 'b pred) \<Rightarrow> 'b pred" (infixl "\<guillemotright>=" 70) where
    1.20 -  "P \<guillemotright>= f = Pred (\<lambda>x. (\<exists>y. eval P y \<and> eval (f y) x))"
    1.21 +lemma eq_mem [simp]:
    1.22 +  "x \<in> (op =) y \<longleftrightarrow> x = y"
    1.23 +  by (auto simp add: mem_def)
    1.24  
    1.25  instantiation pred :: (type) "{complete_lattice, boolean_algebra}"
    1.26  begin
    1.27 @@ -398,97 +401,146 @@
    1.28  definition
    1.29    "\<bottom> = Pred \<bottom>"
    1.30  
    1.31 +lemma eval_bot [simp]:
    1.32 +  "eval \<bottom>  = \<bottom>"
    1.33 +  by (simp add: bot_pred_def)
    1.34 +
    1.35  definition
    1.36    "\<top> = Pred \<top>"
    1.37  
    1.38 +lemma eval_top [simp]:
    1.39 +  "eval \<top>  = \<top>"
    1.40 +  by (simp add: top_pred_def)
    1.41 +
    1.42  definition
    1.43    "P \<sqinter> Q = Pred (eval P \<sqinter> eval Q)"
    1.44  
    1.45 +lemma eval_inf [simp]:
    1.46 +  "eval (P \<sqinter> Q) = eval P \<sqinter> eval Q"
    1.47 +  by (simp add: inf_pred_def)
    1.48 +
    1.49  definition
    1.50    "P \<squnion> Q = Pred (eval P \<squnion> eval Q)"
    1.51  
    1.52 +lemma eval_sup [simp]:
    1.53 +  "eval (P \<squnion> Q) = eval P \<squnion> eval Q"
    1.54 +  by (simp add: sup_pred_def)
    1.55 +
    1.56  definition
    1.57    "\<Sqinter>A = Pred (INFI A eval)"
    1.58  
    1.59 +lemma eval_Inf [simp]:
    1.60 +  "eval (\<Sqinter>A) = INFI A eval"
    1.61 +  by (simp add: Inf_pred_def)
    1.62 +
    1.63  definition
    1.64    "\<Squnion>A = Pred (SUPR A eval)"
    1.65  
    1.66 +lemma eval_Sup [simp]:
    1.67 +  "eval (\<Squnion>A) = SUPR A eval"
    1.68 +  by (simp add: Sup_pred_def)
    1.69 +
    1.70  definition
    1.71    "- P = Pred (- eval P)"
    1.72  
    1.73 +lemma eval_compl [simp]:
    1.74 +  "eval (- P) = - eval P"
    1.75 +  by (simp add: uminus_pred_def)
    1.76 +
    1.77  definition
    1.78    "P - Q = Pred (eval P - eval Q)"
    1.79  
    1.80 +lemma eval_minus [simp]:
    1.81 +  "eval (P - Q) = eval P - eval Q"
    1.82 +  by (simp add: minus_pred_def)
    1.83 +
    1.84  instance proof
    1.85 -qed (auto simp add: less_eq_pred_def less_pred_def
    1.86 -    inf_pred_def sup_pred_def bot_pred_def top_pred_def
    1.87 -    Inf_pred_def Sup_pred_def uminus_pred_def minus_pred_def fun_Compl_def bool_Compl_def,
    1.88 -    auto simp add: le_fun_def less_fun_def le_bool_def less_bool_def
    1.89 -    eval_inject mem_def)
    1.90 +qed (auto intro!: pred_eqI simp add: less_eq_pred_def less_pred_def
    1.91 +  fun_Compl_def fun_diff_def bool_Compl_def bool_diff_def)
    1.92  
    1.93  end
    1.94  
    1.95 +lemma eval_INFI [simp]:
    1.96 +  "eval (INFI A f) = INFI A (eval \<circ> f)"
    1.97 +  by (unfold INFI_def) simp
    1.98 +
    1.99 +lemma eval_SUPR [simp]:
   1.100 +  "eval (SUPR A f) = SUPR A (eval \<circ> f)"
   1.101 +  by (unfold SUPR_def) simp
   1.102 +
   1.103 +definition single :: "'a \<Rightarrow> 'a pred" where
   1.104 +  "single x = Pred ((op =) x)"
   1.105 +
   1.106 +lemma eval_single [simp]:
   1.107 +  "eval (single x) = (op =) x"
   1.108 +  by (simp add: single_def)
   1.109 +
   1.110 +definition bind :: "'a pred \<Rightarrow> ('a \<Rightarrow> 'b pred) \<Rightarrow> 'b pred" (infixl "\<guillemotright>=" 70) where
   1.111 +  "P \<guillemotright>= f = (SUPR (Predicate.eval P) f)"
   1.112 +
   1.113 +lemma eval_bind [simp]:
   1.114 +  "eval (P \<guillemotright>= f) = Predicate.eval (SUPR (Predicate.eval P) f)"
   1.115 +  by (simp add: bind_def)
   1.116 +
   1.117  lemma bind_bind:
   1.118    "(P \<guillemotright>= Q) \<guillemotright>= R = P \<guillemotright>= (\<lambda>x. Q x \<guillemotright>= R)"
   1.119 -  by (auto simp add: bind_def fun_eq_iff)
   1.120 +  by (rule pred_eqI) simp
   1.121  
   1.122  lemma bind_single:
   1.123    "P \<guillemotright>= single = P"
   1.124 -  by (simp add: bind_def single_def)
   1.125 +  by (rule pred_eqI) auto
   1.126  
   1.127  lemma single_bind:
   1.128    "single x \<guillemotright>= P = P x"
   1.129 -  by (simp add: bind_def single_def)
   1.130 +  by (rule pred_eqI) auto
   1.131  
   1.132  lemma bottom_bind:
   1.133    "\<bottom> \<guillemotright>= P = \<bottom>"
   1.134 -  by (auto simp add: bot_pred_def bind_def fun_eq_iff)
   1.135 +  by (rule pred_eqI) simp
   1.136  
   1.137  lemma sup_bind:
   1.138    "(P \<squnion> Q) \<guillemotright>= R = P \<guillemotright>= R \<squnion> Q \<guillemotright>= R"
   1.139 -  by (auto simp add: bind_def sup_pred_def fun_eq_iff)
   1.140 +  by (rule pred_eqI) simp
   1.141  
   1.142 -lemma Sup_bind: "(\<Squnion>A \<guillemotright>= f) = \<Squnion>((\<lambda>x. x \<guillemotright>= f) ` A)"
   1.143 -  by (auto simp add: bind_def Sup_pred_def SUP1_iff fun_eq_iff)
   1.144 +lemma Sup_bind:
   1.145 +  "(\<Squnion>A \<guillemotright>= f) = \<Squnion>((\<lambda>x. x \<guillemotright>= f) ` A)"
   1.146 +  by (rule pred_eqI) simp
   1.147  
   1.148  lemma pred_iffI:
   1.149    assumes "\<And>x. eval A x \<Longrightarrow> eval B x"
   1.150    and "\<And>x. eval B x \<Longrightarrow> eval A x"
   1.151    shows "A = B"
   1.152 -proof -
   1.153 -  from assms have "\<And>x. eval A x \<longleftrightarrow> eval B x" by blast
   1.154 -  then show ?thesis by (cases A, cases B) (simp add: fun_eq_iff)
   1.155 -qed
   1.156 +  using assms by (auto intro: pred_eqI)
   1.157    
   1.158  lemma singleI: "eval (single x) x"
   1.159 -  unfolding single_def by simp
   1.160 +  by simp
   1.161  
   1.162  lemma singleI_unit: "eval (single ()) x"
   1.163 -  by simp (rule singleI)
   1.164 +  by simp
   1.165  
   1.166  lemma singleE: "eval (single x) y \<Longrightarrow> (y = x \<Longrightarrow> P) \<Longrightarrow> P"
   1.167 -  unfolding single_def by simp
   1.168 +  by simp
   1.169  
   1.170  lemma singleE': "eval (single x) y \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> P"
   1.171 -  by (erule singleE) simp
   1.172 +  by simp
   1.173  
   1.174  lemma bindI: "eval P x \<Longrightarrow> eval (Q x) y \<Longrightarrow> eval (P \<guillemotright>= Q) y"
   1.175 -  unfolding bind_def by auto
   1.176 +  by auto
   1.177  
   1.178  lemma bindE: "eval (R \<guillemotright>= Q) y \<Longrightarrow> (\<And>x. eval R x \<Longrightarrow> eval (Q x) y \<Longrightarrow> P) \<Longrightarrow> P"
   1.179 -  unfolding bind_def by auto
   1.180 +  by auto
   1.181  
   1.182  lemma botE: "eval \<bottom> x \<Longrightarrow> P"
   1.183 -  unfolding bot_pred_def by auto
   1.184 +  by auto
   1.185  
   1.186  lemma supI1: "eval A x \<Longrightarrow> eval (A \<squnion> B) x"
   1.187 -  unfolding sup_pred_def by (simp add: sup_fun_eq sup_bool_eq)
   1.188 +  by auto
   1.189  
   1.190  lemma supI2: "eval B x \<Longrightarrow> eval (A \<squnion> B) x" 
   1.191 -  unfolding sup_pred_def by (simp add: sup_fun_eq sup_bool_eq)
   1.192 +  by auto
   1.193  
   1.194  lemma supE: "eval (A \<squnion> B) x \<Longrightarrow> (eval A x \<Longrightarrow> P) \<Longrightarrow> (eval B x \<Longrightarrow> P) \<Longrightarrow> P"
   1.195 -  unfolding sup_pred_def by auto
   1.196 +  by auto
   1.197  
   1.198  lemma single_not_bot [simp]:
   1.199    "single x \<noteq> \<bottom>"
   1.200 @@ -497,8 +549,8 @@
   1.201  lemma not_bot:
   1.202    assumes "A \<noteq> \<bottom>"
   1.203    obtains x where "eval A x"
   1.204 -using assms by (cases A)
   1.205 -  (auto simp add: bot_pred_def, auto simp add: mem_def)
   1.206 +  using assms by (cases A)
   1.207 +    (auto simp add: bot_pred_def, auto simp add: mem_def)
   1.208    
   1.209  
   1.210  subsubsection {* Emptiness check and definite choice *}
   1.211 @@ -518,7 +570,7 @@
   1.212    "is_empty (A \<squnion> B) \<longleftrightarrow> is_empty A \<and> is_empty B"
   1.213    by (auto simp add: is_empty_def)
   1.214  
   1.215 -definition singleton :: "(unit => 'a) \<Rightarrow> 'a pred \<Rightarrow> 'a" where
   1.216 +definition singleton :: "(unit \<Rightarrow> 'a) \<Rightarrow> 'a pred \<Rightarrow> 'a" where
   1.217    "singleton dfault A = (if \<exists>!x. eval A x then THE x. eval A x else dfault ())"
   1.218  
   1.219  lemma singleton_eqI:
   1.220 @@ -544,7 +596,9 @@
   1.221      by (rule singleton_eqI)
   1.222    ultimately have "eval (single (singleton dfault A)) = eval A"
   1.223      by (simp (no_asm_use) add: single_def fun_eq_iff) blast
   1.224 -  then show ?thesis by (simp add: eval_inject)
   1.225 +  then have "\<And>x. eval (single (singleton dfault A)) x = eval A x"
   1.226 +    by simp
   1.227 +  then show ?thesis by (rule pred_eqI)
   1.228  qed
   1.229  
   1.230  lemma singleton_undefinedI: