6 |
6 |
7 constdefs |
7 constdefs |
8 "if" :: "[o,o,o]=>o" |
8 "if" :: "[o,o,o]=>o" |
9 "if(P,Q,R) == P&Q | ~P&R" |
9 "if(P,Q,R) == P&Q | ~P&R" |
10 |
10 |
11 ML {* use_legacy_bindings (the_context ()) *} |
11 lemma ifI: |
|
12 assumes "!!x. x : P ==> f(x) : Q" "!!x. x : ~P ==> g(x) : R" |
|
13 shows "?p : if(P,Q,R)" |
|
14 apply (unfold if_def) |
|
15 apply (tactic {* fast_tac (FOLP_cs addIs @{thms assms}) 1 *}) |
|
16 done |
|
17 |
|
18 lemma ifE: |
|
19 assumes 1: "p : if(P,Q,R)" and |
|
20 2: "!!x y. [| x : P; y : Q |] ==> f(x, y) : S" and |
|
21 3: "!!x y. [| x : ~P; y : R |] ==> g(x, y) : S" |
|
22 shows "?p : S" |
|
23 apply (insert 1) |
|
24 apply (unfold if_def) |
|
25 apply (tactic {* fast_tac (FOLP_cs addIs [@{thm 2}, @{thm 3}]) 1 *}) |
|
26 done |
|
27 |
|
28 lemma if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))" |
|
29 apply (rule iffI) |
|
30 apply (erule ifE) |
|
31 apply (erule ifE) |
|
32 apply (rule ifI) |
|
33 apply (rule ifI) |
|
34 oops |
|
35 |
|
36 ML {* val if_cs = FOLP_cs addSIs [@{thm ifI}] addSEs [@{thm ifE}] *} |
|
37 |
|
38 lemma if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))" |
|
39 apply (tactic {* fast_tac if_cs 1 *}) |
|
40 done |
|
41 |
|
42 lemma nested_ifs: "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))" |
|
43 apply (tactic {* fast_tac if_cs 1 *}) |
|
44 done |
12 |
45 |
13 end |
46 end |