equal
deleted
inserted
replaced
38 inductive_cases [elim!]: |
38 inductive_cases [elim!]: |
39 "Sem (Basic f) s s'" "Sem (c1;c2) s s'" |
39 "Sem (Basic f) s s'" "Sem (c1;c2) s s'" |
40 "Sem (IF b THEN c1 ELSE c2 FI) s s'" |
40 "Sem (IF b THEN c1 ELSE c2 FI) s s'" |
41 |
41 |
42 definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool" |
42 definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool" |
43 where "Valid p c q \<longleftrightarrow> (!s s'. Sem c s s' --> s : p --> s' : q)" |
43 where "Valid p c q \<longleftrightarrow> (\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> p \<longrightarrow> s' \<in> q)" |
44 |
44 |
45 |
45 |
46 syntax |
46 syntax |
47 "_assign" :: "idt => 'b => 'a com" ("(2_ :=/ _)" [70, 65] 61) |
47 "_assign" :: "idt => 'b => 'a com" ("(2_ :=/ _)" [70, 65] 61) |
48 |
48 |