equal
deleted
inserted
replaced
33 \ (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x|y)))"]; |
33 \ (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x|y)))"]; |
34 |
34 |
35 goal Expr.thy "!n. ((a,s) -a-> n) = (n = A a s)"; |
35 goal Expr.thy "!n. ((a,s) -a-> n) = (n = A a s)"; |
36 by (aexp.induct_tac "a" 1); (* struct. ind. *) |
36 by (aexp.induct_tac "a" 1); (* struct. ind. *) |
37 by (ALLGOALS Simp_tac); (* rewr. Den. *) |
37 by (ALLGOALS Simp_tac); (* rewr. Den. *) |
38 by (TRYALL (fast_tac (set_cs addSIs (evala.intrs@prems) |
38 by (TRYALL (fast_tac (!claset addSIs (evala.intrs@prems) |
39 addSEs evala_elim_cases))); |
39 addSEs evala_elim_cases))); |
40 qed_spec_mp "aexp_iff"; |
40 qed_spec_mp "aexp_iff"; |
41 |
41 |
42 goal Expr.thy "!w. ((b,s) -b-> w) = (w = B b s)"; |
42 goal Expr.thy "!w. ((b,s) -b-> w) = (w = B b s)"; |
43 by (bexp.induct_tac "b" 1); |
43 by (bexp.induct_tac "b" 1); |