8 imports Main |
8 imports Main |
9 begin |
9 begin |
10 |
10 |
11 default_sort type |
11 default_sort type |
12 |
12 |
13 type_synonym |
13 type_synonym 'a predicate = "'a \<Rightarrow> bool" |
14 'a predicate = "'a => bool" |
|
15 |
14 |
16 consts |
15 definition satisfies :: "'a \<Rightarrow> 'a predicate \<Rightarrow> bool" ("_ \<Turnstile> _" [100,9] 8) |
|
16 where "(s \<Turnstile> P) \<longleftrightarrow> P s" |
17 |
17 |
18 satisfies ::"'a => 'a predicate => bool" ("_ \<Turnstile> _" [100,9] 8) |
18 definition valid :: "'a predicate \<Rightarrow> bool" (* ("|-") *) |
19 valid ::"'a predicate => bool" (* ("|-") *) |
19 where "valid P \<longleftrightarrow> (\<forall>s. (s \<Turnstile> P))" |
20 |
20 |
21 NOT ::"'a predicate => 'a predicate" ("\<^bold>\<not> _" [40] 40) |
21 definition NOT :: "'a predicate \<Rightarrow> 'a predicate" ("\<^bold>\<not> _" [40] 40) |
22 AND ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<^bold>\<and>" 35) |
22 where "NOT P s \<longleftrightarrow> ~ (P s)" |
23 OR ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<^bold>\<or>" 30) |
|
24 IMPLIES ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<^bold>\<longrightarrow>" 25) |
|
25 |
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 |
26 |
27 defs |
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" |
28 |
29 |
29 satisfies_def: |
30 definition IMPLIES :: "'a predicate \<Rightarrow> 'a predicate \<Rightarrow> 'a predicate" (infixr "\<^bold>\<longrightarrow>" 25) |
30 "s \<Turnstile> P == P s" |
31 where "(P \<^bold>\<longrightarrow> Q) s \<longleftrightarrow> P s \<longrightarrow> Q s" |
31 |
|
32 valid_def: |
|
33 "valid P == (! s. (s \<Turnstile> P))" |
|
34 |
|
35 NOT_def: |
|
36 "NOT P s == ~ (P s)" |
|
37 |
|
38 AND_def: |
|
39 "(P \<^bold>\<and> Q) s == (P s) & (Q s)" |
|
40 |
|
41 OR_def: |
|
42 "(P \<^bold>\<or> Q) s == (P s) | (Q s)" |
|
43 |
|
44 IMPLIES_def: |
|
45 "(P \<^bold>\<longrightarrow> Q) s == (P s) --> (Q s)" |
|
46 |
32 |
47 end |
33 end |