1 (* Title: HOLCF/tr2.ML |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 Lemmas for Tr2.thy |
|
7 *) |
|
8 |
|
9 open Tr2; |
|
10 |
|
11 (* ------------------------------------------------------------------------ *) |
|
12 (* lemmas about andalso *) |
|
13 (* ------------------------------------------------------------------------ *) |
|
14 |
|
15 fun prover s = prove_goalw Tr2.thy [andalso_def] s |
|
16 (fn prems => |
|
17 [ |
|
18 (simp_tac (!simpset addsimps tr_when) 1) |
|
19 ]); |
|
20 |
|
21 val andalso_thms = map prover [ |
|
22 "(TT andalso y) = y", |
|
23 "(FF andalso y) = FF", |
|
24 "(UU andalso y) = UU" |
|
25 ]; |
|
26 |
|
27 val andalso_thms = andalso_thms @ |
|
28 [prove_goalw Tr2.thy [andalso_def] "(x andalso TT) = x" |
|
29 (fn prems => |
|
30 [ |
|
31 (res_inst_tac [("p","x")] trE 1), |
|
32 (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) |
|
35 ])]; |
|
36 |
|
37 (* ------------------------------------------------------------------------ *) |
|
38 (* lemmas about orelse *) |
|
39 (* ------------------------------------------------------------------------ *) |
|
40 |
|
41 fun prover s = prove_goalw Tr2.thy [orelse_def] s |
|
42 (fn prems => |
|
43 [ |
|
44 (simp_tac (!simpset addsimps tr_when) 1) |
|
45 ]); |
|
46 |
|
47 val orelse_thms = map prover [ |
|
48 "(TT orelse y) = TT", |
|
49 "(FF orelse y) = y", |
|
50 "(UU orelse y) = UU" |
|
51 ]; |
|
52 |
|
53 val orelse_thms = orelse_thms @ |
|
54 [prove_goalw Tr2.thy [orelse_def] "(x orelse FF) = x" |
|
55 (fn prems => |
|
56 [ |
|
57 (res_inst_tac [("p","x")] trE 1), |
|
58 (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) |
|
61 ])]; |
|
62 |
|
63 |
|
64 (* ------------------------------------------------------------------------ *) |
|
65 (* lemmas about neg *) |
|
66 (* ------------------------------------------------------------------------ *) |
|
67 |
|
68 fun prover s = prove_goalw Tr2.thy [neg_def] s |
|
69 (fn prems => |
|
70 [ |
|
71 (simp_tac (!simpset addsimps tr_when) 1) |
|
72 ]); |
|
73 |
|
74 val neg_thms = map prover [ |
|
75 "neg`TT = FF", |
|
76 "neg`FF = TT", |
|
77 "neg`UU = UU" |
|
78 ]; |
|
79 |
|
80 (* ------------------------------------------------------------------------ *) |
|
81 (* lemmas about If_then_else_fi *) |
|
82 (* ------------------------------------------------------------------------ *) |
|
83 |
|
84 fun prover s = prove_goalw Tr2.thy [ifte_def] s |
|
85 (fn prems => |
|
86 [ |
|
87 (simp_tac (!simpset addsimps tr_when) 1) |
|
88 ]); |
|
89 |
|
90 val ifte_thms = map prover [ |
|
91 "If UU then e1 else e2 fi = UU", |
|
92 "If FF then e1 else e2 fi = e2", |
|
93 "If TT then e1 else e2 fi = e1"]; |
|
94 |
|
95 Addsimps (dist_less_tr @ dist_eq_tr @ tr_when @ andalso_thms @ |
|
96 orelse_thms @ neg_thms @ ifte_thms); |
|
97 |
|
98 |
|
99 |
|