12 (* lemmas about andalso *) |
12 (* lemmas about andalso *) |
13 (* ------------------------------------------------------------------------ *) |
13 (* ------------------------------------------------------------------------ *) |
14 |
14 |
15 fun prover s = prove_goalw Tr2.thy [andalso_def] s |
15 fun prover s = prove_goalw Tr2.thy [andalso_def] s |
16 (fn prems => |
16 (fn prems => |
17 [ |
17 [ |
18 (simp_tac (!simpset addsimps tr_when) 1) |
18 (simp_tac (!simpset addsimps tr_when) 1) |
19 ]); |
19 ]); |
20 |
20 |
21 val andalso_thms = map prover [ |
21 val andalso_thms = map prover [ |
22 "(TT andalso y) = y", |
22 "(TT andalso y) = y", |
23 "(FF andalso y) = FF", |
23 "(FF andalso y) = FF", |
24 "(UU andalso y) = UU" |
24 "(UU andalso y) = UU" |
25 ]; |
25 ]; |
26 |
26 |
27 val andalso_thms = andalso_thms @ |
27 val andalso_thms = andalso_thms @ |
28 [prove_goalw Tr2.thy [andalso_def] "(x andalso TT) = x" |
28 [prove_goalw Tr2.thy [andalso_def] "(x andalso TT) = x" |
29 (fn prems => |
29 (fn prems => |
30 [ |
30 [ |
31 (res_inst_tac [("p","x")] trE 1), |
31 (res_inst_tac [("p","x")] trE 1), |
32 (asm_simp_tac (!simpset addsimps tr_when) 1), |
32 (asm_simp_tac (!simpset addsimps tr_when) 1), |
33 (asm_simp_tac (!simpset addsimps tr_when) 1), |
33 (asm_simp_tac (!simpset addsimps tr_when) 1), |
34 (asm_simp_tac (!simpset addsimps tr_when) 1) |
34 (asm_simp_tac (!simpset addsimps tr_when) 1) |
35 ])]; |
35 ])]; |
36 |
36 |
37 (* ------------------------------------------------------------------------ *) |
37 (* ------------------------------------------------------------------------ *) |
38 (* lemmas about orelse *) |
38 (* lemmas about orelse *) |
39 (* ------------------------------------------------------------------------ *) |
39 (* ------------------------------------------------------------------------ *) |
40 |
40 |
41 fun prover s = prove_goalw Tr2.thy [orelse_def] s |
41 fun prover s = prove_goalw Tr2.thy [orelse_def] s |
42 (fn prems => |
42 (fn prems => |
43 [ |
43 [ |
44 (simp_tac (!simpset addsimps tr_when) 1) |
44 (simp_tac (!simpset addsimps tr_when) 1) |
45 ]); |
45 ]); |
46 |
46 |
47 val orelse_thms = map prover [ |
47 val orelse_thms = map prover [ |
48 "(TT orelse y) = TT", |
48 "(TT orelse y) = TT", |
49 "(FF orelse y) = y", |
49 "(FF orelse y) = y", |
50 "(UU orelse y) = UU" |
50 "(UU orelse y) = UU" |
51 ]; |
51 ]; |
52 |
52 |
53 val orelse_thms = orelse_thms @ |
53 val orelse_thms = orelse_thms @ |
54 [prove_goalw Tr2.thy [orelse_def] "(x orelse FF) = x" |
54 [prove_goalw Tr2.thy [orelse_def] "(x orelse FF) = x" |
55 (fn prems => |
55 (fn prems => |
56 [ |
56 [ |
57 (res_inst_tac [("p","x")] trE 1), |
57 (res_inst_tac [("p","x")] trE 1), |
58 (asm_simp_tac (!simpset addsimps tr_when) 1), |
58 (asm_simp_tac (!simpset addsimps tr_when) 1), |
59 (asm_simp_tac (!simpset addsimps tr_when) 1), |
59 (asm_simp_tac (!simpset addsimps tr_when) 1), |
60 (asm_simp_tac (!simpset addsimps tr_when) 1) |
60 (asm_simp_tac (!simpset addsimps tr_when) 1) |
61 ])]; |
61 ])]; |
62 |
62 |
63 |
63 |
64 (* ------------------------------------------------------------------------ *) |
64 (* ------------------------------------------------------------------------ *) |
65 (* lemmas about neg *) |
65 (* lemmas about neg *) |
66 (* ------------------------------------------------------------------------ *) |
66 (* ------------------------------------------------------------------------ *) |
67 |
67 |
68 fun prover s = prove_goalw Tr2.thy [neg_def] s |
68 fun prover s = prove_goalw Tr2.thy [neg_def] s |
69 (fn prems => |
69 (fn prems => |
70 [ |
70 [ |
71 (simp_tac (!simpset addsimps tr_when) 1) |
71 (simp_tac (!simpset addsimps tr_when) 1) |
72 ]); |
72 ]); |
73 |
73 |
74 val neg_thms = map prover [ |
74 val neg_thms = map prover [ |
75 "neg`TT = FF", |
75 "neg`TT = FF", |
76 "neg`FF = TT", |
76 "neg`FF = TT", |
77 "neg`UU = UU" |
77 "neg`UU = UU" |
78 ]; |
78 ]; |
79 |
79 |
80 (* ------------------------------------------------------------------------ *) |
80 (* ------------------------------------------------------------------------ *) |
81 (* lemmas about If_then_else_fi *) |
81 (* lemmas about If_then_else_fi *) |
82 (* ------------------------------------------------------------------------ *) |
82 (* ------------------------------------------------------------------------ *) |
83 |
83 |
84 fun prover s = prove_goalw Tr2.thy [ifte_def] s |
84 fun prover s = prove_goalw Tr2.thy [ifte_def] s |
85 (fn prems => |
85 (fn prems => |
86 [ |
86 [ |
87 (simp_tac (!simpset addsimps tr_when) 1) |
87 (simp_tac (!simpset addsimps tr_when) 1) |
88 ]); |
88 ]); |
89 |
89 |
90 val ifte_thms = map prover [ |
90 val ifte_thms = map prover [ |
91 "If UU then e1 else e2 fi = UU", |
91 "If UU then e1 else e2 fi = UU", |
92 "If FF then e1 else e2 fi = e2", |
92 "If FF then e1 else e2 fi = e2", |
93 "If TT then e1 else e2 fi = e1"]; |
93 "If TT then e1 else e2 fi = e1"]; |
94 |
94 |
95 |
95 |
96 |
96 |
97 |
97 |
98 |
98 |