equal
deleted
inserted
replaced
51 ("VARS _// {_} // _ // {_}" [0,0,55,0] 50) |
51 ("VARS _// {_} // _ // {_}" [0,0,55,0] 50) |
52 syntax ("" output) |
52 syntax ("" output) |
53 "_hoare" :: "['a assn,'a com,'a assn] => bool" |
53 "_hoare" :: "['a assn,'a com,'a assn] => bool" |
54 ("{_} // _ // {_}" [0,55,0] 50) |
54 ("{_} // _ // {_}" [0,55,0] 50) |
55 |
55 |
56 ML_file "hoare_syntax.ML" |
56 ML_file \<open>hoare_syntax.ML\<close> |
57 parse_translation \<open>[(\<^syntax_const>\<open>_hoare_vars\<close>, K Hoare_Syntax.hoare_vars_tr)]\<close> |
57 parse_translation \<open>[(\<^syntax_const>\<open>_hoare_vars\<close>, K Hoare_Syntax.hoare_vars_tr)]\<close> |
58 print_translation \<open>[(\<^const_syntax>\<open>Valid\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare\<close>))]\<close> |
58 print_translation \<open>[(\<^const_syntax>\<open>Valid\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare\<close>))]\<close> |
59 |
59 |
60 |
60 |
61 lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q" |
61 lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q" |
91 |
91 |
92 lemma Compl_Collect: "-(Collect b) = {x. ~(b x)}" |
92 lemma Compl_Collect: "-(Collect b) = {x. ~(b x)}" |
93 by blast |
93 by blast |
94 |
94 |
95 lemmas AbortRule = SkipRule \<comment> \<open>dummy version\<close> |
95 lemmas AbortRule = SkipRule \<comment> \<open>dummy version\<close> |
96 ML_file "hoare_tac.ML" |
96 ML_file \<open>hoare_tac.ML\<close> |
97 |
97 |
98 method_setup vcg = \<open> |
98 method_setup vcg = \<open> |
99 Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tac ctxt (K all_tac)))\<close> |
99 Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tac ctxt (K all_tac)))\<close> |
100 "verification condition generator" |
100 "verification condition generator" |
101 |
101 |