15 by (bexp.induct_tac "b" 1); |
15 by (bexp.induct_tac "b" 1); |
16 by (ALLGOALS(asm_simp_tac (HOL_ss addcongs [conj_cong] |
16 by (ALLGOALS(asm_simp_tac (HOL_ss addcongs [conj_cong] |
17 addsimps (aexp_iff::B_simps@evalb_simps)))); |
17 addsimps (aexp_iff::B_simps@evalb_simps)))); |
18 bind_thm("bexp_iff", result() RS spec); |
18 bind_thm("bexp_iff", result() RS spec); |
19 |
19 |
20 val bexp1 = bexp_iff RS iffD1; |
20 val equiv_cs = comp_cs addss |
21 val bexp2 = bexp_iff RS iffD2; |
21 (prod_ss addsimps (aexp_iff::bexp_iff::evalc.intrs)); |
22 |
|
23 val BfstI = read_instantiate_sg (sign_of Equiv.thy) |
|
24 [("P","%x.B ?b x")] (fst_conv RS ssubst); |
|
25 val BfstD = read_instantiate_sg (sign_of Equiv.thy) |
|
26 [("P","%x.B ?b x")] (fst_conv RS subst); |
|
27 |
22 |
28 goal Equiv.thy "!!c. <c,s> -c-> t ==> (s,t) : C(c)"; |
23 goal Equiv.thy "!!c. <c,s> -c-> t ==> (s,t) : C(c)"; |
29 |
24 |
30 (* start with rule induction *) |
25 (* start with rule induction *) |
31 be (evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1; |
26 be (evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1; |
32 by (rewrite_tac (Gamma_def::C_simps)); |
27 by (rewrite_tac (Gamma_def::C_simps)); |
33 (* simplification with HOL_ss again too agressive *) |
28 (* simplification with HOL_ss again too agressive *) |
34 (* skip *) |
29 (* skip *) |
35 by (fast_tac comp_cs 1); |
30 by (fast_tac equiv_cs 1); |
36 (* assign *) |
31 (* assign *) |
37 by (asm_full_simp_tac (prod_ss addsimps [aexp_iff]) 1); |
32 by (fast_tac equiv_cs 1); |
38 (* comp *) |
33 (* comp *) |
39 by (fast_tac comp_cs 1); |
34 by (fast_tac equiv_cs 1); |
40 (* if *) |
35 (* if *) |
41 by(fast_tac (set_cs addSIs [BfstI] addSDs [BfstD,bexp1]) 1); |
36 by (fast_tac equiv_cs 1); |
42 by(fast_tac (set_cs addSIs [BfstI] addSDs [BfstD,bexp1]) 1); |
37 by (fast_tac equiv_cs 1); |
43 (* while *) |
38 (* while *) |
44 by (rtac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski RS ssubst)) 1); |
39 by (rtac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski RS ssubst)) 1); |
45 by (fast_tac (comp_cs addSIs [bexp1,BfstI] addSDs [BfstD,bexp1]) 1); |
40 by (fast_tac equiv_cs 1); |
46 by (rtac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski RS ssubst)) 1); |
41 by (rtac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski RS ssubst)) 1); |
47 by (fast_tac (comp_cs addSIs [bexp1,BfstI] addSDs [BfstD,bexp1]) 1); |
42 by (fast_tac equiv_cs 1); |
48 |
43 |
49 qed "com1"; |
44 qed "com1"; |
50 |
45 |
51 |
46 |
52 val com_ss = prod_ss addsimps (aexp_iff::bexp_iff::evalc.intrs); |
47 goal Equiv.thy "!s t. (s,t):C(c) --> <c,s> -c-> t"; |
53 |
|
54 goal Equiv.thy "!io:C(c). <c,fst(io)> -c-> snd(io)"; |
|
55 by (com.induct_tac "c" 1); |
48 by (com.induct_tac "c" 1); |
56 by (rewrite_tac C_simps); |
49 by (rewrite_tac C_simps); |
57 by (safe_tac comp_cs); |
50 by (ALLGOALS (TRY o fast_tac equiv_cs)); |
58 by (ALLGOALS (asm_full_simp_tac com_ss)); |
|
59 |
|
60 (* comp *) |
|
61 by (REPEAT (EVERY [(dtac bspec 1),(atac 1)])); |
|
62 by (asm_full_simp_tac com_ss 1); |
|
63 |
51 |
64 (* while *) |
52 (* while *) |
|
53 by (strip_tac 1); |
65 by (etac (Gamma_mono RSN (2,induct)) 1); |
54 by (etac (Gamma_mono RSN (2,induct)) 1); |
66 by (rewrite_goals_tac [Gamma_def]); |
55 by (rewrite_goals_tac [Gamma_def]); |
67 by (safe_tac comp_cs); |
56 by (fast_tac equiv_cs 1); |
68 by (EVERY1 [dtac bspec, atac]); |
|
69 by (ALLGOALS (asm_full_simp_tac com_ss)); |
|
70 |
57 |
71 qed "com2"; |
58 bind_thm("com2", result() RS spec RS spec RS mp); |
72 |
59 |
73 |
60 |
74 (**** Proof of Equivalence ****) |
61 (**** Proof of Equivalence ****) |
75 |
62 |
76 val com_iff_cs = set_cs addEs [com2 RS bspec] addDs [com1]; |
63 goal Equiv.thy "(s,t) : C(c) = (<c,s> -c-> t)"; |
77 |
64 by (fast_tac (set_cs addEs [com2] addDs [com1]) 1); |
78 goal Equiv.thy "C(c) = {io . <c,fst(io)> -c-> snd(io)}"; |
|
79 by (rtac equalityI 1); |
|
80 (* => *) |
|
81 by (fast_tac com_iff_cs 1); |
|
82 (* <= *) |
|
83 by (REPEAT (step_tac com_iff_cs 1)); |
|
84 by (asm_full_simp_tac (prod_ss addsimps [surjective_pairing RS sym])1); |
|
85 qed "com_equivalence"; |
65 qed "com_equivalence"; |