14 |
14 |
15 val aexp1 = aexp_iff RS iffD1; |
15 val aexp1 = aexp_iff RS iffD1; |
16 val aexp2 = aexp_iff RS iffD2; |
16 val aexp2 = aexp_iff RS iffD2; |
17 |
17 |
18 |
18 |
|
19 goal Equiv.thy "!w. (<b,s> -b-> w) --> (B(b,s) = w)"; |
|
20 by (bexp.induct_tac "b" 1); |
|
21 by (rewrite_goals_tac B_simps); (*denotational semantics*) |
|
22 by (ALLGOALS (fast_tac (HOL_cs addSDs [aexp1] addSEs bexp_elim_cases))); |
|
23 val bexp_imp1 = result(); |
|
24 |
|
25 goal Equiv.thy "!w. (B(b,s) = w) --> (<b,s> -b-> w)"; |
|
26 by (bexp.induct_tac "b" 1); |
|
27 by (rewrite_goals_tac B_simps); (*denotational semantics*) |
|
28 by (ALLGOALS (best_tac (HOL_cs addSIs (aexp2::evalb.intrs)))); |
|
29 val bexp_imp2 = result(); |
|
30 |
|
31 val bexp1 = bexp_imp1 RS spec RS mp |> standard; |
|
32 val bexp2 = bexp_imp2 RS spec RS mp |> standard; |
|
33 |
19 goal Equiv.thy "(<b,s> -b-> w) = (B(b,s) = w)"; |
34 goal Equiv.thy "(<b,s> -b-> w) = (B(b,s) = w)"; |
20 by (res_inst_tac [("x","w")] spec 1); (* quantify w *) |
35 by (fast_tac (HOL_cs addSEs [bexp1,bexp2]) 1); |
21 by (bexp.induct_tac "b" 1); (* struct. ind. *) |
|
22 by(rewrite_goals_tac B_simps); |
|
23 (* simplification with HOL_ss too agressive: (True=x) == True *) |
|
24 by (safe_tac (HOL_cs addSIs (aexp2::evalb.intrs) |
|
25 addSDs [aexp1] addSEs bexp_elim_cases) |
|
26 THEN ALLGOALS(best_tac HOL_cs)); |
|
27 |
|
28 val bexp_iff = result(); |
36 val bexp_iff = result(); |
29 |
|
30 val bexp1 = bexp_iff RS iffD1; |
|
31 val bexp2 = bexp_iff RS iffD2; |
|
32 |
37 |
33 val BfstI = read_instantiate_sg (sign_of Equiv.thy) |
38 val BfstI = read_instantiate_sg (sign_of Equiv.thy) |
34 [("P","%x.B(?b,x)")] (fst_conv RS ssubst); |
39 [("P","%x.B(?b,x)")] (fst_conv RS ssubst); |
35 val BfstD = read_instantiate_sg (sign_of Equiv.thy) |
40 val BfstD = read_instantiate_sg (sign_of Equiv.thy) |
36 [("P","%x.B(?b,x)")] (fst_conv RS subst); |
41 [("P","%x.B(?b,x)")] (fst_conv RS subst); |