lib: factor out and generalise bool syntax for functions

pred_conj, pred_disj, and pred_neg only worked for functions with a
single argument and did not have the standard boolean laws available.

This commit factors out these declarations into their own theory, so
they can be used independently. It generalises them to functions of
arbitrarily many arguments, using the existing instance of fun in class
boolean_algebra.

We also factor out top/bottom, but leave them as abbreviations for now,
because the impact of changing them to the type class is too large.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

lib/Fun_Pred_Syntax.thy

@@ -0,0 +1,210 @@
+(*
+ * Copyright 2022, Proofcraft Pty Ltd
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ *)
+
+(* Syntax for using multi-argument functions as predicates, e.g "P and Q" where P and Q are
+   functions to bool, taking one or more parameters. *)
+
+theory Fun_Pred_Syntax
+imports Main
+begin
+
+section \<open>Definitions\<close>
+
+text \<open>
+  Functions are already instances of Boolean algebras and provide all the standard laws one
+  would like to have. Default simplifications are automatic. Search for @{const inf}/
+  @{const sup}/@{const uminus} to find further laws and/or unfold via the definitions below.
+
+  The abbreviations here provide special syntax for the function instance of Boolean
+  algebras only, leaving other instances (such as @{typ bool}) untouched.\<close>
+
+abbreviation pred_conj :: "('a \<Rightarrow> 'b::boolean_algebra) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" where
+  "pred_conj \<equiv> inf"
+
+abbreviation pred_disj :: "('a \<Rightarrow> 'b::boolean_algebra) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" where
+  "pred_disj \<equiv> sup"
+
+abbreviation pred_neg :: "('a \<Rightarrow> 'b::boolean_algebra) \<Rightarrow> ('a \<Rightarrow> 'b)" where
+  "pred_neg \<equiv> uminus"
+
+
+text \<open>
+  Lifted True/False: ideally, we'd map these to top/bot, but top/bot are constants and there are
+  currently too many rules and tools that expect these conditions to beta-reduce and match against
+  True/False directly.\<close>
+
+abbreviation (input) pred_top :: "'a \<Rightarrow> bool" where
+  "pred_top \<equiv> \<lambda>_. True"
+
+abbreviation (input) pred_bot :: "'a \<Rightarrow> bool" where
+  "pred_bot \<equiv> \<lambda>_. False"
+
+
+text \<open>Version with two arguments for compatibility. Can hopefully be eliminated at some point.\<close>
+
+abbreviation (input) pred_top2 :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
+  "pred_top2 \<equiv> \<lambda>_ _. True"
+
+abbreviation (input) pred_bot2 :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
+  "pred_bot2 \<equiv> \<lambda>_ _. False"
+
+
+section \<open>Syntax bundles\<close>
+
+bundle fun_pred_syntax
+begin
+  (* infixl instead of infixr, because we want to split off conjuncts from the left *)
+  notation pred_conj (infixl "and" 35)
+  notation pred_disj (infixl "or" 30)
+  notation pred_neg ("not _" [40] 40)
+  notation pred_top ("\<top>")
+  notation pred_bot ("\<bottom>")
+  notation pred_top2 ("\<top>\<top>")
+  notation pred_bot2 ("\<bottom>\<bottom>")
+end
+
+bundle no_fun_pred_syntax
+begin
+  no_notation pred_conj (infixl "and" 35)
+  no_notation pred_disj (infixl "or" 30)
+  no_notation pred_neg ("not _" [40] 40)
+  no_notation pred_top ("\<top>")
+  no_notation pred_bot ("\<bottom>")
+  no_notation pred_top2 ("\<top>\<top>")
+  no_notation pred_bot2 ("\<bottom>\<bottom>")
+end
+
+unbundle fun_pred_syntax
+
+
+section \<open>Definitions specialised to @{typ bool} and @{text fun} instance of @{class boolean_algebra}\<close>
+
+lemmas pred_conj_def =
+  inf_fun_def[where 'b=bool, simplified]
+  inf_fun_def[where f="f::'a \<Rightarrow> 'b::boolean_algebra" for f]
+
+lemmas pred_disj_def =
+  sup_fun_def[where 'b=bool, simplified]
+  sup_fun_def[where f="f::'a \<Rightarrow> 'b::boolean_algebra" for f]
+
+lemmas pred_neg_def =
+  fun_Compl_def[where 'b=bool, simplified]
+  fun_Compl_def[where A="A::'a \<Rightarrow> 'b::boolean_algebra" for A]
+
+lemmas pred_top_def[simp] =
+  top_fun_def[where 'b=bool, simplified] top_fun_def[where 'b="'b::boolean_algebra"]
+
+lemmas pred_bot_def[simp] =
+  bot_fun_def[where 'b=bool, simplified] bot_fun_def[where 'b="'b::boolean_algebra"]
+
+
+section \<open>Other lemmas\<close>
+
+text \<open>AC rewriting renamed and specialised, so we don't have to remember inf/sup\<close>
+
+lemmas pred_conj_aci = inf_aci[where 'a="'a \<Rightarrow> 'b::boolean_algebra"]
+lemmas pred_disj_aci = sup_aci[where 'a="'a \<Rightarrow> 'b::boolean_algebra"]
+
+
+text \<open>Useful legacy names\<close>
+
+lemmas pred_conjI = inf1I inf2I
+
+lemmas pred_disjI1 = sup1I1[where 'a="'a \<Rightarrow> 'b::boolean_algebra"]
+lemmas pred_disjI2 = sup1I2[where 'a="'a \<Rightarrow> 'b::boolean_algebra"]
+
+lemmas pred_disj1CI[intro!] = sup1CI[where 'a="'a \<Rightarrow> 'b::boolean_algebra"]
+lemmas pred_disj2CI = sup2CI[where 'a="'a \<Rightarrow> 'b::boolean_algebra"]
+
+lemmas pred_conj_assoc = inf.assoc[where 'a="'a \<Rightarrow> 'b::boolean_algebra", symmetric]
+lemmas pred_conj_comm = inf.commute[where 'a="'a \<Rightarrow> 'b::boolean_algebra"]
+
+lemmas pred_disj_assoc = sup.assoc[where 'a="'a \<Rightarrow> 'b::boolean_algebra", symmetric]
+lemmas pred_disj_comm = sup.commute[where 'a="'a \<Rightarrow> 'b::boolean_algebra"]
+
+
+text \<open>Top/bot and function composition\<close>
+
+lemma pred_top_comp[simp]:
+  "\<top> \<circ> f = \<top>"
+  by (simp add: comp_def)
+
+lemma pred_bot_comp[simp]:
+  "\<bottom> \<circ> f = \<bottom>"
+  by (simp add: comp_def)
+
+
+text \<open>We would get these for free if we could instantiate pred_top/pred_bot to top/bot directly:\<close>
+
+lemmas pred_top_left_neutral[simp] =
+  inf_top.left_neutral[where 'a="'a \<Rightarrow> bool", unfolded pred_top_def]
+
+lemmas pred_top_right_neutral[simp] =
+  inf_top.right_neutral[where 'a="'a \<Rightarrow> bool", unfolded pred_top_def]
+
+lemmas pred_bot_left_neutral[simp] =
+  sup_bot.left_neutral[where 'a="'a \<Rightarrow> bool", unfolded pred_bot_def]
+
+lemmas pred_bot_right_neutral[simp] =
+  sup_bot.right_neutral[where 'a="'a \<Rightarrow> bool", unfolded pred_bot_def]
+
+lemmas pred_top_left[simp] =
+  sup_top_left[where 'a="'a \<Rightarrow> bool", unfolded pred_top_def]
+
+lemmas pred_top_right[simp] =
+  sup_top_right[where 'a="'a \<Rightarrow> bool", unfolded pred_top_def]
+
+lemmas pred_bot_left[simp] =
+  inf_bot_left[where 'a="'a \<Rightarrow> bool", unfolded pred_bot_def]
+
+lemmas pred_bot_right[simp] =
+  inf_bot_right[where 'a="'a \<Rightarrow> bool", unfolded pred_bot_def]
+
+lemmas pred_neg_top_eq[simp] =
+  compl_top_eq[where 'a="'a \<Rightarrow> bool", unfolded pred_bot_def pred_top_def]
+
+lemmas pred_neg_bot_eq[simp] =
+  compl_bot_eq[where 'a="'a \<Rightarrow> bool", unfolded pred_bot_def pred_top_def]
+
+(* no special setup for pred_top2/pred_bot2 at the moment, since we hope to eliminate these
+   entirely in the future *)
+
+
+section \<open>Examples\<close>
+
+experiment
+begin
+
+(* Standard laws are available by default: *)
+lemma "(P and P) = P" for P :: "'a \<Rightarrow> bool"
+  by simp
+
+(* Works for functions with multiple arguments: *)
+lemma "(P and Q) = (Q and P)" for P :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
+  by (simp add: pred_conj_aci)
+
+(* Unfolds automatically when applied: *)
+lemma "(P and Q) s t = (P s t \<and> Q s t)"
+  by simp
+
+(* pred_top and pred_bot work for only one argument currently: *)
+lemma "(P and not P) = \<bottom>" for P :: "'a \<Rightarrow> bool"
+  by simp
+
+(* You can still use them with more arguments and sometimes get simplification: *)
+lemma "(P and not P) = (\<lambda>_ _. \<bottom>)" for P :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> bool"
+  by simp
+
+(* But sometimes you need to fold pred_top_def/pred_bot_def for rules on top/bot to fire: *)
+lemma "(P and (\<lambda>_ _. \<bottom>)) = (\<lambda>_ _. \<bottom>)"
+  by (simp flip: pred_bot_def)
+
+lemma "(P and \<bottom>\<bottom>) = \<bottom>\<bottom>"
+  by (simp flip: pred_bot_def)
+
+end
+
+end

lib/Lib.thy

@@ -18,6 +18,7 @@ imports
   Extract_Conjunct
   ML_Goal
   Eval_Bool
+  Fun_Pred_Syntax
   NICTATools
   "Word_Lib.WordSetup"
 begin
@@ -78,33 +79,6 @@ lemma prod_injects:
   "p = (x,y) \<Longrightarrow> x = fst p \<and> y = snd p"
   by auto
 
-definition
-  pred_conj :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)" (infixl "and" 35)
-where
-  "pred_conj P Q \<equiv> \<lambda>x. P x \<and> Q x"
-
-lemma pred_conj_absorb[simp]:
-  "(P and P) = P"
-  by (simp add: pred_conj_def)
-
-definition
-  pred_disj :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)" (infixl "or" 30)
-where
-  "pred_disj P Q \<equiv> \<lambda>x. P x \<or> Q x"
-
-lemma pred_disj_absorb[simp]:
-  "(P or P) = P"
-  by (simp add: pred_disj_def)
-
-definition
-  pred_neg :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)" ("not _" [40] 40)
-where
-  "pred_neg P \<equiv> \<lambda>x. \<not> P x"
-
-lemma pred_neg_simp[simp]:
-  "(not P) s \<longleftrightarrow> \<not> (P s)"
-  by (simp add: pred_neg_def)
-
 definition "K \<equiv> \<lambda>x y. x"
 
 definition
@@ -238,7 +212,7 @@ lemma delete_remove1:
 
 lemma ignore_if:
   "(y and z) s \<Longrightarrow> (if x then y else z) s"
-  by (clarsimp simp: pred_conj_def)
+  by simp
 
 lemma zipWith_Nil2 :
   "zipWith f xs [] = []"

lib/Monad_WP/NonDetMonad.thy

@@ -791,46 +791,6 @@ where
  "\<lbrace>P\<rbrace> f -,\<lbrace>Q\<rbrace> \<equiv> validE P f (\<lambda>x y. True) Q"
 
 
-text \<open>Abbreviations for trivial preconditions:\<close>
-abbreviation(input)
-  top :: "'a \<Rightarrow> bool" ("\<top>")
-where
-  "\<top> \<equiv> \<lambda>_. True"
-
-abbreviation(input)
-  bottom :: "'a \<Rightarrow> bool" ("\<bottom>")
-where
-  "\<bottom> \<equiv> \<lambda>_. False"
-
-text \<open>Abbreviations for trivial postconditions (taking two arguments):\<close>
-abbreviation(input)
-  toptop :: "'a \<Rightarrow> 'b \<Rightarrow> bool" ("\<top>\<top>")
-where
- "\<top>\<top> \<equiv> \<lambda>_ _. True"
-
-abbreviation(input)
-  botbot :: "'a \<Rightarrow> 'b \<Rightarrow> bool" ("\<bottom>\<bottom>")
-where
- "\<bottom>\<bottom> \<equiv> \<lambda>_ _. False"
-
-text \<open>
-  Lifting @{text "\<and>"} and @{text "\<or>"} over two arguments.
-  Lifting @{text "\<and>"} and @{text "\<or>"} over one argument is already
-  defined (written @{text "and"} and @{text "or"}).
-\<close>
-definition
-  bipred_conj :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool)"
-  (infixl "And" 96)
-where
-  "bipred_conj P Q \<equiv> \<lambda>x y. P x y \<and> Q x y"
-
-definition
-  bipred_disj :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool)"
-  (infixl "Or" 91)
-where
-  "bipred_disj P Q \<equiv> \<lambda>x y. P x y \<or> Q x y"
-
-
 subsection "Determinism"
 
 text \<open>A monad of type @{text nondet_monad} is deterministic iff it

lib/Monad_WP/NonDetMonadVCG.thy

@@ -148,70 +148,6 @@ lemma bind_eqI:
   apply (auto simp: split_def)
   done
 
-subsection "Simplification Rules for Lifted And/Or"
-
-lemma pred_andE[elim!]: "\<lbrakk> (A and B) x; \<lbrakk> A x; B x \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
-  by(simp add:pred_conj_def)
-
-lemma pred_andI[intro!]: "\<lbrakk> A x; B x \<rbrakk> \<Longrightarrow> (A and B) x"
-  by(simp add:pred_conj_def)
-
-lemma pred_conj_app[simp]: "(P and Q) x = (P x \<and> Q x)"
-  by(simp add:pred_conj_def)
-
-lemma bipred_andE[elim!]: "\<lbrakk> (A And B) x y; \<lbrakk> A x y; B x y \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
-  by(simp add:bipred_conj_def)
-
-lemma bipred_andI[intro!]: "\<lbrakk> A x y; B x y \<rbrakk> \<Longrightarrow> (A And B) x y"
-  by (simp add:bipred_conj_def)
-
-lemma bipred_conj_app[simp]: "(P And Q) x = (P x and Q x)"
-  by(simp add:pred_conj_def bipred_conj_def)
-
-lemma pred_disjE[elim!]: "\<lbrakk> (P or Q) x; P x \<Longrightarrow> R; Q x \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
-  by (fastforce simp: pred_disj_def)
-
-lemma pred_disjI1[intro]: "P x \<Longrightarrow> (P or Q) x"
-  by (simp add: pred_disj_def)
-
-lemma pred_disjI2[intro]: "Q x \<Longrightarrow> (P or Q) x"
-  by (simp add: pred_disj_def)
-
-lemma pred_disj_app[simp]: "(P or Q) x = (P x \<or> Q x)"
-  by auto
-
-lemma bipred_disjI1[intro]: "P x y \<Longrightarrow> (P Or Q) x y"
-  by (simp add: bipred_disj_def)
-
-lemma bipred_disjI2[intro]: "Q x y \<Longrightarrow> (P Or Q) x y"
-  by (simp add: bipred_disj_def)
-
-lemma bipred_disj_app[simp]: "(P Or Q) x = (P x or Q x)"
-  by(simp add:pred_disj_def bipred_disj_def)
-
-lemma pred_notnotD[simp]: "(not not P) = P"
-  by(simp add:pred_neg_def)
-
-lemma pred_and_true[simp]: "(P and \<top>) = P"
-  by(simp add:pred_conj_def)
-
-lemma pred_and_true_var[simp]: "(\<top> and P) = P"
-  by(simp add:pred_conj_def)
-
-lemma pred_and_false[simp]: "(P and \<bottom>) = \<bottom>"
-  by(simp add:pred_conj_def)
-
-lemma pred_and_false_var[simp]: "(\<bottom> and P) = \<bottom>"
-  by(simp add:pred_conj_def)
-
-lemma pred_conj_assoc:
-  "(P and Q and R) = (P and (Q and R))"
-  unfolding pred_conj_def by simp
-
-lemma pred_conj_comm:
-  "(P and Q) = (Q and P)"
-  by (auto simp: pred_conj_def)
-
 subsection "Hoare Logic Rules"
 
 lemma validE_def2:
@@ -280,15 +216,15 @@ lemma hoare_True_E_R [simp]:
   by (auto simp add: validE_R_def validE_def valid_def split: sum.splits)
 
 lemma hoare_post_conj [intro]:
-  "\<lbrakk> \<lbrace> P \<rbrace> a \<lbrace> Q \<rbrace>; \<lbrace> P \<rbrace> a \<lbrace> R \<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> a \<lbrace> Q And R \<rbrace>"
+  "\<lbrakk> \<lbrace> P \<rbrace> a \<lbrace> Q \<rbrace>; \<lbrace> P \<rbrace> a \<lbrace> R \<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> a \<lbrace> Q and R \<rbrace>"
-  by (fastforce simp: valid_def split_def bipred_conj_def)
+  by (fastforce simp: valid_def)
 
 lemma hoare_pre_disj [intro]:
   "\<lbrakk> \<lbrace> P \<rbrace> a \<lbrace> R \<rbrace>; \<lbrace> Q \<rbrace> a \<lbrace> R \<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace> P or Q \<rbrace> a \<lbrace> R \<rbrace>"
   by (simp add:valid_def pred_disj_def)
 
 lemma hoare_conj:
-  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace> f \<lbrace>Q And Q'\<rbrace>"
+  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace> f \<lbrace>Q and Q'\<rbrace>"
   unfolding valid_def by auto
 
 lemma hoare_post_taut: "\<lbrace> P \<rbrace> a \<lbrace> \<top>\<top> \<rbrace>"
@@ -1247,7 +1183,7 @@ lemma hoare_vcg_conj_lift:
   assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
   assumes y: "\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>"
   shows      "\<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>"
-  apply (subst bipred_conj_def[symmetric], rule hoare_post_conj)
+  apply (subst pred_conj_def[symmetric], subst pred_conj_def[symmetric], rule hoare_post_conj)
    apply (rule hoare_pre_imp [OF _ x], simp)
   apply (rule hoare_pre_imp [OF _ y], simp)
   done
@@ -1808,7 +1744,7 @@ lemma hoare_fun_app_wp[wp]:
   by simp+
 
 lemma hoare_validE_pred_conj:
-  "\<lbrakk> \<lbrace>P\<rbrace>f\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<lbrace>P\<rbrace>f\<lbrace>R\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>f\<lbrace>Q And R\<rbrace>,\<lbrace>E\<rbrace>"
+  "\<lbrakk> \<lbrace>P\<rbrace>f\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<lbrace>P\<rbrace>f\<lbrace>R\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>f\<lbrace>Q and R\<rbrace>,\<lbrace>E\<rbrace>"
   unfolding valid_def validE_def by (simp add: split_def split: sum.splits)
 
 lemma hoare_validE_conj:
@@ -2038,7 +1974,7 @@ lemma validNF_prop [wp_unsafe]:
   by (wp validNF)+
 
 lemma validNF_post_conj [intro!]:
-  "\<lbrakk> \<lbrace> P \<rbrace> a \<lbrace> Q \<rbrace>!; \<lbrace> P \<rbrace> a \<lbrace> R \<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> a \<lbrace> Q And R \<rbrace>!"
+  "\<lbrakk> \<lbrace> P \<rbrace> a \<lbrace> Q \<rbrace>!; \<lbrace> P \<rbrace> a \<lbrace> R \<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> a \<lbrace> Q and R \<rbrace>!"
   by (auto simp: validNF_def)
 
 lemma no_fail_or:
@@ -2095,7 +2031,7 @@ lemma validNF_if_split [wp_split]:
 lemma validNF_vcg_conj_lift:
   "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>!; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>! \<rbrakk> \<Longrightarrow>
       \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>!"
-  apply (subst bipred_conj_def[symmetric], rule validNF_post_conj)
+  apply (subst pred_conj_def[symmetric], subst pred_conj_def[symmetric], rule validNF_post_conj)
    apply (erule validNF_weaken_pre, fastforce)
   apply (erule validNF_weaken_pre, fastforce)
   done

lib/Monad_WP/TraceMonad.thy

@@ -941,54 +941,17 @@ where
   "\<lbrace>P\<rbrace> f -,\<lbrace>Q\<rbrace> \<equiv> validE P f (\<lambda>x y. True) Q"
 
 
-text \<open> Abbreviations for trivial preconditions: \<close>
+text \<open> Abbreviations for trivial postconditions (taking three arguments): \<close>
-abbreviation(input)
-  top :: "'a \<Rightarrow> bool" ("\<top>")
-where
-  "\<top> \<equiv> \<lambda>_. True"
-
-abbreviation(input)
-  bottom :: "'a \<Rightarrow> bool" ("\<bottom>")
-where
-  "\<bottom> \<equiv> \<lambda>_. False"
-
-text \<open> Abbreviations for trivial postconditions (taking two arguments): \<close>
-abbreviation(input)
-  toptop :: "'a \<Rightarrow> 'b \<Rightarrow> bool" ("\<top>\<top>")
-where
-  "\<top>\<top> \<equiv> \<lambda>_ _. True"
-
 abbreviation(input)
   toptoptop :: "'a \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> bool" ("\<top>\<top>\<top>")
 where
   "\<top>\<top>\<top> \<equiv> \<lambda>_ _ _. True"
 
-abbreviation(input)
-  botbot :: "'a \<Rightarrow> 'b \<Rightarrow> bool" ("\<bottom>\<bottom>")
-where
-  "\<bottom>\<bottom> \<equiv> \<lambda>_ _. False"
-
 abbreviation(input)
   botbotbot :: "'a \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> bool" ("\<bottom>\<bottom>\<bottom>")
 where
   "\<bottom>\<bottom>\<bottom> \<equiv> \<lambda>_ _ _. False"
 
-text \<open>
-  Lifting @{text "\<and>"} and @{text "\<or>"} over two arguments.
-  Lifting @{text "\<and>"} and @{text "\<or>"} over one argument is already
-  defined (written @{text "and"} and @{text "or"}).
-\<close>
-definition
-  bipred_conj :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool)"
-  (infixl "And" 96)
-where
-  "bipred_conj P Q \<equiv> \<lambda>x y. P x y \<and> Q x y"
-
-definition
-  bipred_disj :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool)"
-  (infixl "Or" 91)
-where
-  "bipred_disj P Q \<equiv> \<lambda>x y. P x y \<or> Q x y"
 
 subsection "Determinism"
 

lib/Monad_WP/TraceMonadVCG.thy

@@ -256,8 +256,8 @@ lemma rg_validI:
      "\<lbrace>Pg\<rbrace>,\<lbrace>Rg\<rbrace> g \<lbrace>Gg\<rbrace>,\<lbrace>Qg\<rbrace>"
   and compat: "R \<le> Rf" "R \<le> Rg" "Gf \<le> G" "Gg \<le> G"
      "Gf \<le> Rg" "Gg \<le> Rf"
-  shows "\<lbrace>Pf And Pg\<rbrace>,\<lbrace>R\<rbrace> parallel f g \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv. Qf rv And Qg rv\<rbrace>"
+  shows "\<lbrace>Pf and Pg\<rbrace>,\<lbrace>R\<rbrace> parallel f g \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv. Qf rv and Qg rv\<rbrace>"
-  apply (clarsimp simp: validI_def rely_def bipred_conj_def
+  apply (clarsimp simp: validI_def rely_def pred_conj_def
                         parallel_prefix_closed validI[THEN validI_prefix_closed])
   apply (drule(3) parallel_rely_induct0[OF _ _ _ validI order_refl order_refl compat])
   apply clarsimp
@@ -633,62 +633,8 @@ lemma bind_eqI:
 
 subsection "Simplification Rules for Lifted And/Or"
 
-lemma pred_andE[elim!]: "\<lbrakk> (A and B) x; \<lbrakk> A x; B x \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
-  by(simp add:pred_conj_def)
-
-lemma pred_andI[intro!]: "\<lbrakk> A x; B x \<rbrakk> \<Longrightarrow> (A and B) x"
-  by(simp add:pred_conj_def)
-
-lemma pred_conj_app[simp]: "(P and Q) x = (P x \<and> Q x)"
-  by(simp add:pred_conj_def)
-
-lemma bipred_andE[elim!]: "\<lbrakk> (A And B) x y; \<lbrakk> A x y; B x y \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
-  by(simp add:bipred_conj_def)
-
-lemma bipred_andI[intro!]: "\<lbrakk> A x y; B x y \<rbrakk> \<Longrightarrow> (A And B) x y"
-  by (simp add:bipred_conj_def)
-
-lemma bipred_conj_app[simp]: "(P And Q) x = (P x and Q x)"
-  by(simp add:pred_conj_def bipred_conj_def)
-
-lemma pred_disjE[elim!]: "\<lbrakk> (P or Q) x; P x \<Longrightarrow> R; Q x \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
-  by (fastforce simp: pred_disj_def)
-
-lemma pred_disjI1[intro]: "P x \<Longrightarrow> (P or Q) x"
-  by (simp add: pred_disj_def)
-
-lemma pred_disjI2[intro]: "Q x \<Longrightarrow> (P or Q) x"
-  by (simp add: pred_disj_def)
-
-lemma pred_disj_app[simp]: "(P or Q) x = (P x \<or> Q x)"
-  by auto
-
-lemma bipred_disjI1[intro]: "P x y \<Longrightarrow> (P Or Q) x y"
-  by (simp add: bipred_disj_def)
-
-lemma bipred_disjI2[intro]: "Q x y \<Longrightarrow> (P Or Q) x y"
-  by (simp add: bipred_disj_def)
-
-lemma bipred_disj_app[simp]: "(P Or Q) x = (P x or Q x)"
-  by(simp add:pred_disj_def bipred_disj_def)
-
-lemma pred_notnotD[simp]: "(not not P) = P"
-  by(simp add:pred_neg_def)
-
-lemma pred_and_true[simp]: "(P and \<top>) = P"
-  by(simp add:pred_conj_def)
-
-lemma pred_and_true_var[simp]: "(\<top> and P) = P"
-  by(simp add:pred_conj_def)
-
-lemma pred_and_false[simp]: "(P and \<bottom>) = \<bottom>"
-  by(simp add:pred_conj_def)
-
-lemma pred_and_false_var[simp]: "(\<bottom> and P) = \<bottom>"
-  by(simp add:pred_conj_def)
-
 lemma bipred_disj_op_eq[simp]:
-  "reflp R \<Longrightarrow> (=) Or R = R"
+  "reflp R \<Longrightarrow> ((=) or R) = R"
   apply (rule ext, rule ext)
   apply (auto simp: reflp_def)
   done
@@ -759,15 +705,15 @@ lemma hoare_True_E_R [simp]:
   by (auto simp add: validE_R_def validE_def valid_def split: sum.splits)
 
 lemma hoare_post_conj [intro!]:
-  "\<lbrakk> \<lbrace> P \<rbrace> a \<lbrace> Q \<rbrace>; \<lbrace> P \<rbrace> a \<lbrace> R \<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> a \<lbrace> Q And R \<rbrace>"
+  "\<lbrakk> \<lbrace> P \<rbrace> a \<lbrace> Q \<rbrace>; \<lbrace> P \<rbrace> a \<lbrace> R \<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> a \<lbrace> Q and R \<rbrace>"
-  by (fastforce simp: valid_def split_def bipred_conj_def)
+  by (fastforce simp: valid_def split_def pred_conj_def)
 
 lemma hoare_pre_disj [intro!]:
   "\<lbrakk> \<lbrace> P \<rbrace> a \<lbrace> R \<rbrace>; \<lbrace> Q \<rbrace> a \<lbrace> R \<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace> P or Q \<rbrace> a \<lbrace> R \<rbrace>"
   by (simp add:valid_def pred_disj_def)
 
 lemma hoare_conj:
-  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace> f \<lbrace>Q And Q'\<rbrace>"
+  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace> f \<lbrace>Q and Q'\<rbrace>"
   unfolding valid_def
   by (auto)
 
@@ -1656,7 +1602,7 @@ lemma hoare_vcg_conj_lift:
   assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
   assumes y: "\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>"
   shows      "\<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>"
-  apply (subst bipred_conj_def[symmetric], rule hoare_post_conj)
+  apply (subst pred_conj_def[symmetric], subst pred_conj_def[symmetric], rule hoare_post_conj)
    apply (rule hoare_pre_imp [OF _ x], simp)
   apply (rule hoare_pre_imp [OF _ y], simp)
   done
@@ -2082,7 +2028,7 @@ lemma hoare_fun_app_wp[wp]:
   by simp+
 
 lemma hoare_validE_pred_conj:
-  "\<lbrakk> \<lbrace>P\<rbrace>f\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<lbrace>P\<rbrace>f\<lbrace>R\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>f\<lbrace>Q And R\<rbrace>,\<lbrace>E\<rbrace>"
+  "\<lbrakk> \<lbrace>P\<rbrace>f\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<lbrace>P\<rbrace>f\<lbrace>R\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>f\<lbrace>Q and R\<rbrace>,\<lbrace>E\<rbrace>"
   unfolding valid_def validE_def by (simp add: split_def split: sum.splits)
 
 lemma hoare_validE_conj:
@@ -2285,7 +2231,7 @@ lemma validNF_prop [wp_unsafe]:
   by (wp validNF)+
 
 lemma validNF_post_conj [intro!]:
-  "\<lbrakk> \<lbrace> P \<rbrace> a \<lbrace> Q \<rbrace>!; \<lbrace> P \<rbrace> a \<lbrace> R \<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> a \<lbrace> Q And R \<rbrace>!"
+  "\<lbrakk> \<lbrace> P \<rbrace> a \<lbrace> Q \<rbrace>!; \<lbrace> P \<rbrace> a \<lbrace> R \<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> a \<lbrace> Q and R \<rbrace>!"
   by (clarsimp simp: validNF_def)
 
 lemma no_fail_or:
@@ -2342,7 +2288,7 @@ lemma validNF_split_if [wp_split]:
 lemma validNF_vcg_conj_lift:
   "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>!; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>! \<rbrakk> \<Longrightarrow>
       \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>!"
-  apply (subst bipred_conj_def[symmetric], rule validNF_post_conj)
+  apply (subst pred_conj_def[symmetric], subst pred_conj_def[symmetric], rule validNF_post_conj)
    apply (erule validNF_weaken_pre, fastforce)
   apply (erule validNF_weaken_pre, fastforce)
   done

lib/Monad_WP/wp/Eisbach_WP.thy

@@ -66,7 +66,7 @@ method post_asm_raw methods m =
    rule trivial_imp)
 
 method post_asm methods m =
-  (post_asm_raw \<open>(simp only: bipred_conj_def pred_conj_def)?,(elim conjE)?,m\<close>)
+  (post_asm_raw \<open>(simp only: pred_conj_def)?,(elim conjE)?,m\<close>)
 
 
 named_theorems packed_validEs
@@ -86,7 +86,7 @@ method post_raw methods m =
 
 method post_strong methods m_distinct m_all =
   (post_raw
-     \<open>(simp only: pred_conj_def bipred_conj_def)?,
+     \<open>(simp only: pred_conj_def)?,
       (intro impI conjI allI)?,
       distinct_subgoals_strong \<open>m_distinct\<close>,
       all \<open>m_all\<close>,
@@ -122,6 +122,9 @@ private lemma hoare_decomposeE:
 
 private lemmas hoare_decomposes' = hoare_decompose hoare_decomposeE_R hoare_decomposeE_E hoare_decomposeE
 
+private lemmas bipred_conj_def =
+  inf_fun_def[where 'b="'b \<Rightarrow> bool", unfolded inf_fun_def[where 'b="bool"], simplified]
+
 private method add_pred_conj = (subst pred_conj_def[symmetric])
 private method add_bipred_conj = (subst bipred_conj_def[symmetric])
 

lib/Monad_WP/wp/WPEx.thy

@@ -95,7 +95,7 @@ fun get_wp_simps_strgs ctxt rules asms = let
 
 fun postcond_ss ctxt = ctxt
     |> put_simpset HOL_basic_ss
-    |> (fn ctxt => ctxt addsimps [@{thm pred_conj_def}])
+    |> (fn ctxt => ctxt addsimps @{thms pred_conj_def})
     |> simpset_of
 
 fun wp_default_ss ctxt = ctxt

lib/StateMonad.thy

@@ -10,7 +10,7 @@
 
 chapter "Monads"
 
-theory StateMonad (* FIXME: untested/unused *)
+theory StateMonad (* unused *)
 imports Lib
 begin
 
@@ -400,34 +400,6 @@ lemma validE_def2:
   "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>R\<rbrace> \<equiv> \<lbrace>P\<rbrace> f \<lbrace> \<lambda>r s. case r of Inr b \<Rightarrow> Q b s | Inl a \<Rightarrow> R a s \<rbrace>"
   by (unfold valid_def validE_def)
 
-(* FIXME: modernize *)
-syntax top :: "'a \<Rightarrow> bool" ("\<top>")
-       bottom :: "'a \<Rightarrow> bool" ("\<bottom>")
-
-translations
-  "\<top>" == "\<lambda>_. CONST True"
-  "\<bottom>" == "\<lambda>_. CONST False"
-
-definition
-  bipred_conj :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool)" (infixl "And" 96)
-where
-  "bipred_conj P Q \<equiv> \<lambda>x y. P x y \<and> Q x y"
-
-definition
-  bipred_disj :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool)" (infixl "Or" 91)
-where
-  "bipred_disj P Q \<equiv> \<lambda>x y. P x y \<or> Q x y"
-
-definition
-  bipred_neg :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool)" ("Not _") where
-  "bipred_neg P \<equiv> \<lambda>x y. \<not> P x y"
-
-syntax toptop :: "'a \<Rightarrow> 'b \<Rightarrow> bool" ("\<top>\<top>")
-       botbot :: "'a \<Rightarrow> 'b \<Rightarrow> bool" ("\<bottom>\<bottom>")
-
-translations "\<top>\<top>" == "\<lambda>_ _. CONST True"
-             "\<bottom>\<bottom>" == "\<lambda>_ _. CONST False"
-
 definition
   pred_lift_exact :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool)" ("\<guillemotleft>_,_\<guillemotright>") where
   "pred_lift_exact P Q \<equiv> \<lambda>x y. P x \<and> Q y"
@@ -445,48 +417,12 @@ lemma pred_liftI[intro!]: "\<lbrakk> P x; Q y \<rbrakk> \<Longrightarrow> \<guil
   by (simp add:pred_lift_exact_def)
 
 lemma pred_exact_split:
-  "\<guillemotleft>P,Q\<guillemotright> = (\<guillemotleft>P,\<top>\<guillemotright> And \<guillemotleft>\<top>,Q\<guillemotright>)"
+  "\<guillemotleft>P,Q\<guillemotright> = (\<guillemotleft>P,\<top>\<guillemotright> and \<guillemotleft>\<top>,Q\<guillemotright>)"
-  by (simp add:pred_lift_exact_def bipred_conj_def)
+  by (simp add:pred_lift_exact_def pred_conj_def)
-
-lemma pred_andE[elim!]: "\<lbrakk> (A and B) x; \<lbrakk> A x; B x \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
-  by (simp add:pred_conj_def)
-
-lemma pred_andI[intro!]: "\<lbrakk> A x; B x \<rbrakk> \<Longrightarrow> (A and B) x"
-  by (simp add:pred_conj_def)
-
-lemma bipred_conj_app[simp]: "(P And Q) x = (P x and Q x)"
-  by (simp add:pred_conj_def bipred_conj_def)
-
-lemma bipred_disj_app[simp]: "(P Or Q) x = (P x or Q x)"
-  by (simp add:pred_disj_def bipred_disj_def)
-
-lemma pred_conj_app[simp]: "(P and Q) x = (P x \<and> Q x)"
-  by (simp add:pred_conj_def)
-
-lemma pred_disj_app[simp]: "(P or Q) x = (P x \<or> Q x)"
-  by (simp add:pred_disj_def)
-
-lemma pred_notnotD[simp]: "(not not P) = P"
-  by (simp add:pred_neg_def)
-
-lemma bipred_notnotD[simp]: "(Not Not P) = P"
-  by (simp add:bipred_neg_def)
 
 lemma pred_lift_add[simp]: "\<guillemotleft>P,Q\<guillemotright> x = ((\<lambda>s. P x) and Q)"
   by (simp add:pred_lift_exact_def pred_conj_def)
 
-lemma pred_and_true[simp]: "(P and \<top>) = P"
-  by (simp add:pred_conj_def)
-
-lemma pred_and_true_var[simp]: "(\<top> and P) = P"
-  by (simp add:pred_conj_def)
-
-lemma pred_and_false[simp]: "(P and \<bottom>) = \<bottom>"
-  by (simp add:pred_conj_def)
-
-lemma pred_and_false_var[simp]: "(\<bottom> and P) = \<bottom>"
-  by (simp add:pred_conj_def)
-
 lemma seq':
   "\<lbrakk> \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>;
      \<forall>x. P x \<longrightarrow> \<lbrace>C\<rbrace> g x \<lbrace>D\<rbrace>;
@@ -569,8 +505,8 @@ lemma return_sp:
   by (simp add:return_def valid_def)
 
 lemma hoare_post_conj [intro!]:
-  "\<lbrakk> \<lbrace> P \<rbrace> a \<lbrace> Q \<rbrace>; \<lbrace> P \<rbrace> a \<lbrace> R \<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> a \<lbrace> Q And R \<rbrace>"
+  "\<lbrakk> \<lbrace> P \<rbrace> a \<lbrace> Q \<rbrace>; \<lbrace> P \<rbrace> a \<lbrace> R \<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> a \<lbrace> Q and R \<rbrace>"
-  by (simp add:valid_def split_def bipred_conj_def)
+  by (simp add:valid_def split_def pred_conj_def)
 
 lemma hoare_pre_disj [intro!]:
   "\<lbrakk> \<lbrace> P \<rbrace> a \<lbrace> R \<rbrace>; \<lbrace> Q \<rbrace> a \<lbrace> R \<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace> P or Q \<rbrace> a \<lbrace> R \<rbrace>"