--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/HOLCF/IOA/Pred.thy Thu Dec 31 12:43:09 2015 +0100
@@ -0,0 +1,33 @@
+(* Title: HOL/HOLCF/IOA/Pred.thy
+ Author: Olaf Müller
+*)
+
+section \<open>Logical Connectives lifted to predicates\<close>
+
+theory Pred
+imports Main
+begin
+
+default_sort type
+
+type_synonym 'a predicate = "'a \<Rightarrow> bool"
+
+definition satisfies :: "'a \<Rightarrow> 'a predicate \<Rightarrow> bool" ("_ \<Turnstile> _" [100,9] 8)
+ where "(s \<Turnstile> P) \<longleftrightarrow> P s"
+
+definition valid :: "'a predicate \<Rightarrow> bool" (* ("|-") *)
+ where "valid P \<longleftrightarrow> (\<forall>s. (s \<Turnstile> P))"
+
+definition NOT :: "'a predicate \<Rightarrow> 'a predicate" ("\<^bold>\<not> _" [40] 40)
+ where "NOT P s \<longleftrightarrow> ~ (P s)"
+
+definition AND :: "'a predicate \<Rightarrow> 'a predicate \<Rightarrow> 'a predicate" (infixr "\<^bold>\<and>" 35)
+ where "(P \<^bold>\<and> Q) s \<longleftrightarrow> P s \<and> Q s"
+
+definition OR :: "'a predicate \<Rightarrow> 'a predicate \<Rightarrow> 'a predicate" (infixr "\<^bold>\<or>" 30)
+ where "(P \<^bold>\<or> Q) s \<longleftrightarrow> P s \<or> Q s"
+
+definition IMPLIES :: "'a predicate \<Rightarrow> 'a predicate \<Rightarrow> 'a predicate" (infixr "\<^bold>\<longrightarrow>" 25)
+ where "(P \<^bold>\<longrightarrow> Q) s \<longleftrightarrow> P s \<longrightarrow> Q s"
+
+end