equal
deleted
inserted
replaced
6 |
6 |
7 header {* Hoare Logic *} |
7 header {* Hoare Logic *} |
8 |
8 |
9 theory Hoare |
9 theory Hoare |
10 imports Main |
10 imports Main |
11 uses ("~~/src/HOL/Hoare/hoare_tac.ML") |
|
12 begin |
11 begin |
13 |
12 |
14 subsection {* Abstract syntax and semantics *} |
13 subsection {* Abstract syntax and semantics *} |
15 |
14 |
16 text {* The following abstract syntax and semantics of Hoare Logic |
15 text {* The following abstract syntax and semantics of Hoare Logic |
400 lemma Compl_Collect: "- Collect b = {x. \<not> b x}" |
399 lemma Compl_Collect: "- Collect b = {x. \<not> b x}" |
401 by blast |
400 by blast |
402 |
401 |
403 lemmas AbortRule = SkipRule -- "dummy version" |
402 lemmas AbortRule = SkipRule -- "dummy version" |
404 |
403 |
405 use "~~/src/HOL/Hoare/hoare_tac.ML" |
404 ML_file "~~/src/HOL/Hoare/hoare_tac.ML" |
406 |
405 |
407 method_setup hoare = {* |
406 method_setup hoare = {* |
408 Scan.succeed (fn ctxt => |
407 Scan.succeed (fn ctxt => |
409 (SIMPLE_METHOD' |
408 (SIMPLE_METHOD' |
410 (hoare_tac ctxt (simp_tac (HOL_basic_ss addsimps [@{thm "Record.K_record_comp"}] ))))) *} |
409 (hoare_tac ctxt (simp_tac (HOL_basic_ss addsimps [@{thm "Record.K_record_comp"}] ))))) *} |