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