33 

    33 

    34 abbreviation (input)

    34 abbreviation (input)

    35   pred_K :: "'b \<Rightarrow> 'a \<Rightarrow> 'b" ("\<langle>_\<rangle>") where

    35   pred_K :: "'b \<Rightarrow> 'a \<Rightarrow> 'b" ("\<langle>_\<rangle>") where

    36   "\<langle>f\<rangle> \<equiv> \<lambda>s. f"

    36   "\<langle>f\<rangle> \<equiv> \<lambda>s. f"

    37 

    37 

    39   definition pred_ex :: "('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" (binder "EXS " 10) where

    39   definition pred_ex :: "('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" (binder "EXS " 10) where

    40   "EXS x. P x \<equiv> \<lambda>s. \<exists>x. P x s"

    40   "EXS x. P x \<equiv> \<lambda>s. \<exists>x. P x s"

    41 

    41 

    42 abbreviation (input)

    42 abbreviation (input)

    43   pred_all :: "('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" (binder "ALLS " 10) where

    43   pred_all :: "('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" (binder "ALLS " 10) where

   214   fix h

   214   fix h

   215   assume a: "?rhs h"

   215   assume a: "?rhs h"

   216   then obtain x y z where "P x" and "Q y" and "R z"

   216   then obtain x y z where "P x" and "Q y" and "R z"

   217                       and "x ## y" and "x ## z" and "y ## z" and "x ## y + z"

   217                       and "x ## y" and "x ## z" and "y ## z" and "x ## y + z"

   218                       and "h = x + y + z"

   218                       and "h = x + y + z"

   219     by (fastforce elim!: sep_conjE simp: sep_add_ac dest: sep_disj_addD)

   220     by (fastforce elim!: sep_conjE simp: sep_add_ac dest: sep_disj_addD)

   220   thus "?lhs h"

   221   thus "?lhs h"

   221     by (metis sep_conj_def sep_disj_addI1)

   222     by (metis sep_conj_def sep_disj_addI1)

   222 qed

   223 qed

   223 

   224