1(* Title: HOL/HOLCF/IOA/Pred.thy 2 Author: Olaf M��ller 3*) 4 5section \<open>Logical Connectives lifted to predicates\<close> 6 7theory Pred 8imports Main 9begin 10 11default_sort type 12 13type_synonym 'a predicate = "'a \<Rightarrow> bool" 14 15definition satisfies :: "'a \<Rightarrow> 'a predicate \<Rightarrow> bool" ("_ \<Turnstile> _" [100, 9] 8) 16 where "(s \<Turnstile> P) \<longleftrightarrow> P s" 17 18definition valid :: "'a predicate \<Rightarrow> bool" ("\<TTurnstile> _" [9] 8) 19 where "(\<TTurnstile> P) \<longleftrightarrow> (\<forall>s. (s \<Turnstile> P))" 20 21definition NOT :: "'a predicate \<Rightarrow> 'a predicate" ("\<^bold>\<not> _" [40] 40) 22 where "NOT P s \<longleftrightarrow> \<not> P s" 23 24definition AND :: "'a predicate \<Rightarrow> 'a predicate \<Rightarrow> 'a predicate" (infixr "\<^bold>\<and>" 35) 25 where "(P \<^bold>\<and> Q) s \<longleftrightarrow> P s \<and> Q s" 26 27definition OR :: "'a predicate \<Rightarrow> 'a predicate \<Rightarrow> 'a predicate" (infixr "\<^bold>\<or>" 30) 28 where "(P \<^bold>\<or> Q) s \<longleftrightarrow> P s \<or> Q s" 29 30definition IMPLIES :: "'a predicate \<Rightarrow> 'a predicate \<Rightarrow> 'a predicate" (infixr "\<^bold>\<longrightarrow>" 25) 31 where "(P \<^bold>\<longrightarrow> Q) s \<longleftrightarrow> P s \<longrightarrow> Q s" 32 33end 34