equal
deleted
inserted
replaced
1 (* Title: HOL/HOLCF/IOA/meta_theory/Pred.thy |
|
2 Author: Olaf Müller |
|
3 *) |
|
4 |
|
5 section \<open>Logical Connectives lifted to predicates\<close> |
|
6 |
|
7 theory Pred |
|
8 imports Main |
|
9 begin |
|
10 |
|
11 default_sort type |
|
12 |
|
13 type_synonym 'a predicate = "'a \<Rightarrow> bool" |
|
14 |
|
15 definition satisfies :: "'a \<Rightarrow> 'a predicate \<Rightarrow> bool" ("_ \<Turnstile> _" [100,9] 8) |
|
16 where "(s \<Turnstile> P) \<longleftrightarrow> P s" |
|
17 |
|
18 definition valid :: "'a predicate \<Rightarrow> bool" (* ("|-") *) |
|
19 where "valid P \<longleftrightarrow> (\<forall>s. (s \<Turnstile> P))" |
|
20 |
|
21 definition NOT :: "'a predicate \<Rightarrow> 'a predicate" ("\<^bold>\<not> _" [40] 40) |
|
22 where "NOT P s \<longleftrightarrow> ~ (P s)" |
|
23 |
|
24 definition 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 |
|
27 definition 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 |
|
30 definition 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 |
|
33 end |
|