9 by (ALLGOALS(simp_tac (HOL_ss addsimps A_simps))); (* rewr. Den. *) |
9 by (ALLGOALS(simp_tac (HOL_ss addsimps A_simps))); (* rewr. Den. *) |
10 by (TRYALL (fast_tac (set_cs addSIs (evala.intrs@prems) |
10 by (TRYALL (fast_tac (set_cs addSIs (evala.intrs@prems) |
11 addSEs evala_elim_cases))); |
11 addSEs evala_elim_cases))); |
12 val aexp_iff = store_thm("aexp_iff", result() RS spec); |
12 val aexp_iff = store_thm("aexp_iff", result() RS spec); |
13 |
13 |
14 |
|
15 goal HOL.thy "(? x. x=t & P) = P"; |
|
16 by(fast_tac HOL_cs 1); |
|
17 qed "elim_ex_conv"; |
|
18 |
|
19 goal Equiv.thy "!w. (<b,s> -b-> w) = (w = B(b,s))"; |
14 goal Equiv.thy "!w. (<b,s> -b-> w) = (w = B(b,s))"; |
20 by (bexp.induct_tac "b" 1); |
15 by (bexp.induct_tac "b" 1); |
21 by (ALLGOALS(asm_simp_tac (HOL_ss addcongs [conj_cong] |
16 by (ALLGOALS(asm_simp_tac (HOL_ss addcongs [conj_cong] |
22 addsimps (aexp_iff::elim_ex_conv::B_simps@evalb_simps)))); |
17 addsimps (aexp_iff::B_simps@evalb_simps)))); |
23 val bexp_iff = store_thm("bexp_iff", result() RS spec); |
18 val bexp_iff = store_thm("bexp_iff", result() RS spec); |
24 |
19 |
25 val bexp1 = bexp_iff RS iffD1; |
20 val bexp1 = bexp_iff RS iffD1; |
26 val bexp2 = bexp_iff RS iffD2; |
21 val bexp2 = bexp_iff RS iffD2; |
27 |
22 |