equal
deleted
inserted
replaced
1 (* Title: HOL/IMP/Hoare.ML |
1 (* Title: HOL/IMP/Hoare.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1995 TUM |
4 Copyright 1995 TUM |
5 |
5 |
6 Soundness of Hoare rules wrt denotational semantics |
6 Soundness of Hoare rules wrt denotational semantics |
7 *) |
7 *) |
8 |
8 |
9 open Hoare; |
9 open Hoare; |
10 |
10 |
11 goalw Hoare.thy [spec_def] "!P c Q. ({{P}}c{{Q}}) --> spec P c Q"; |
11 goalw Hoare.thy [spec_def] "!P c Q. ({{P}}c{{Q}}) --> spec P c Q"; |
12 br hoare.mutual_induct 1; |
12 by (rtac hoare.mutual_induct 1); |
13 by(ALLGOALS Asm_simp_tac); |
13 by(ALLGOALS Asm_simp_tac); |
14 by(fast_tac rel_cs 1); |
14 by(fast_tac rel_cs 1); |
15 by(fast_tac HOL_cs 1); |
15 by(fast_tac HOL_cs 1); |
16 br allI 1; |
16 by (rtac allI 1); |
17 br allI 1; |
17 by (rtac allI 1); |
18 br impI 1; |
18 by (rtac impI 1); |
19 be induct2 1; |
19 by (etac induct2 1); |
20 br Gamma_mono 1; |
20 br Gamma_mono 1; |
21 by (rewrite_goals_tac [Gamma_def]); |
21 by (rewtac Gamma_def); |
22 by(eres_inst_tac [("x","a")] allE 1); |
22 by(eres_inst_tac [("x","a")] allE 1); |
23 by (safe_tac comp_cs); |
23 by (safe_tac comp_cs); |
24 by(ALLGOALS Asm_full_simp_tac); |
24 by(ALLGOALS Asm_full_simp_tac); |
25 qed "hoare_sound"; |
25 qed "hoare_sound"; |
26 |
26 |