equal
deleted
inserted
replaced
7 |
7 |
8 Server keys; initial states of agents; new nonces and keys; function "sees" |
8 Server keys; initial states of agents; new nonces and keys; function "sees" |
9 *) |
9 *) |
10 |
10 |
11 |
11 |
12 Addsimps [de_Morgan_conj, de_Morgan_disj, not_all, not_ex]; |
|
13 (**Addsimps [all_conj_distrib, ex_disj_distrib];**) |
|
14 |
|
15 |
|
16 val prems = goal HOL.thy "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)"; |
12 val prems = goal HOL.thy "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)"; |
17 by (excluded_middle_tac "P" 1); |
13 by (case_tac "P" 1); |
18 by (asm_simp_tac (!simpset addsimps prems) 1); |
14 by (ALLGOALS (asm_simp_tac (!simpset addsimps prems))); |
19 by (asm_simp_tac (!simpset addsimps prems) 1); |
|
20 val expand_case = result(); |
15 val expand_case = result(); |
21 |
16 |
22 fun expand_case_tac P i = |
17 fun expand_case_tac P i = |
23 res_inst_tac [("P",P)] expand_case i THEN |
18 res_inst_tac [("P",P)] expand_case i THEN |
24 Simp_tac (i+1) THEN |
19 Simp_tac (i+1) THEN |