|
17480
|
1 |
(* $Id$ *)
|
|
|
2 |
|
|
|
3 |
theory If
|
|
|
4 |
imports FOLP
|
|
|
5 |
begin
|
|
|
6 |
|
|
|
7 |
constdefs
|
|
19796
|
8 |
"if" :: "[o,o,o]=>o"
|
|
17480
|
9 |
"if(P,Q,R) == P&Q | ~P&R"
|
|
|
10 |
|
|
25991
|
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
|
|
17480
|
45 |
|
|
0
|
46 |
end
|