equal
deleted
inserted
replaced
40 inductive_cases [elim!]: |
40 inductive_cases [elim!]: |
41 "Sem (Basic f) s s'" "Sem (c1;c2) s s'" |
41 "Sem (Basic f) s s'" "Sem (c1;c2) s s'" |
42 "Sem (IF b THEN c1 ELSE c2 FI) s s'" |
42 "Sem (IF b THEN c1 ELSE c2 FI) s s'" |
43 |
43 |
44 definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool" where |
44 definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool" where |
45 "Valid p c q == \<forall>s s'. Sem c s s' \<longrightarrow> s : Some ` p \<longrightarrow> s' : Some ` q" |
45 "Valid p c q \<equiv> \<forall>s s'. Sem c s s' \<longrightarrow> s \<in> Some ` p \<longrightarrow> s' \<in> Some ` q" |
46 |
46 |
47 |
47 |
48 syntax |
48 syntax |
49 "_assign" :: "idt => 'b => 'a com" ("(2_ :=/ _)" [70, 65] 61) |
49 "_assign" :: "idt => 'b => 'a com" ("(2_ :=/ _)" [70, 65] 61) |
50 |
50 |
99 by(auto simp:Valid_def) |
99 by(auto simp:Valid_def) |
100 |
100 |
101 |
101 |
102 subsection \<open>Derivation of the proof rules and, most importantly, the VCG tactic\<close> |
102 subsection \<open>Derivation of the proof rules and, most importantly, the VCG tactic\<close> |
103 |
103 |
104 lemma Compl_Collect: "-(Collect b) = {x. ~(b x)}" |
104 lemma Compl_Collect: "-(Collect b) = {x. \<not>(b x)}" |
105 by blast |
105 by blast |
106 |
106 |
107 ML_file "hoare_tac.ML" |
107 ML_file "hoare_tac.ML" |
108 |
108 |
109 method_setup vcg = \<open> |
109 method_setup vcg = \<open> |