equal
deleted
inserted
replaced
53 "Sem (c1; c2) s s' = (EX s''. Sem c1 s s'' & Sem c2 s'' s')" |
53 "Sem (c1; c2) s s' = (EX s''. Sem c1 s s'' & Sem c2 s'' s')" |
54 "Sem (Cond b c1 c2) s s' = |
54 "Sem (Cond b c1 c2) s s' = |
55 (if s : b then Sem c1 s s' else Sem c2 s s')" |
55 (if s : b then Sem c1 s s' else Sem c2 s s')" |
56 "Sem (While b x c) s s' = (EX n. iter n b (Sem c) s s')" |
56 "Sem (While b x c) s s' = (EX n. iter n b (Sem c) s s')" |
57 |
57 |
58 constdefs |
58 definition Valid :: "'a bexp => 'a com => 'a bexp => bool" ("(3|- _/ (2_)/ _)" [100, 55, 100] 50) where |
59 Valid :: "'a bexp => 'a com => 'a bexp => bool" |
|
60 ("(3|- _/ (2_)/ _)" [100, 55, 100] 50) |
|
61 "|- P c Q == ALL s s'. Sem c s s' --> s : P --> s' : Q" |
59 "|- P c Q == ALL s s'. Sem c s s' --> s : P --> s' : Q" |
62 |
60 |
63 syntax (xsymbols) |
61 notation (xsymbols) Valid ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50) |
64 Valid :: "'a bexp => 'a com => 'a bexp => bool" |
|
65 ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50) |
|
66 |
62 |
67 lemma ValidI [intro?]: |
63 lemma ValidI [intro?]: |
68 "(!!s s'. Sem c s s' ==> s : P ==> s' : Q) ==> |- P c Q" |
64 "(!!s s'. Sem c s s' ==> s : P ==> s' : Q) ==> |- P c Q" |
69 by (simp add: Valid_def) |
65 by (simp add: Valid_def) |
70 |
66 |