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