equal
deleted
inserted
replaced
30 "((b0 ori b1,sigma) -b-> w) = \ |
30 "((b0 ori b1,sigma) -b-> w) = \ |
31 \ (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x|y)))"]; |
31 \ (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x|y)))"]; |
32 |
32 |
33 Goal "!n. ((a,s) -a-> n) = (A a s = n)"; |
33 Goal "!n. ((a,s) -a-> n) = (A a s = n)"; |
34 by (induct_tac "a" 1); |
34 by (induct_tac "a" 1); |
35 by (ALLGOALS |
35 by (auto_tac (claset() addSIs evala.intrs addSEs evala_elim_cases, |
36 (fast_tac (claset() addSIs evala.intrs |
36 simpset())); |
37 addSEs evala_elim_cases addss (simpset())))); |
|
38 qed_spec_mp "aexp_iff"; |
37 qed_spec_mp "aexp_iff"; |
39 |
38 |
40 Goal "!w. ((b,s) -b-> w) = (B b s = w)"; |
39 Goal "!w. ((b,s) -b-> w) = (B b s = w)"; |
41 by (induct_tac "b" 1); |
40 by (induct_tac "b" 1); |
42 by (ALLGOALS |
41 by (auto_tac (claset(), |
43 (fast_tac (claset() |
42 simpset() addsimps aexp_iff::evalb_simps)); |
44 addss (simpset() addsimps (aexp_iff::evalb_simps))))); |
|
45 qed_spec_mp "bexp_iff"; |
43 qed_spec_mp "bexp_iff"; |