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 (ccc1_ss 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 (ccc1_ss addsimps tr_when) 1), |
|
33 (asm_simp_tac (ccc1_ss addsimps tr_when) 1), |
|
34 (asm_simp_tac (ccc1_ss 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 (ccc1_ss 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 (ccc1_ss addsimps tr_when) 1), |
|
59 (asm_simp_tac (ccc1_ss addsimps tr_when) 1), |
|
60 (asm_simp_tac (ccc1_ss addsimps tr_when) 1) |
|
61 ])]; |
|
62 |
|
63 |
|
64 (* ------------------------------------------------------------------------ *) |
|
65 (* lemmas about If_then_else_fi *) |
|
66 (* ------------------------------------------------------------------------ *) |
|
67 |
|
68 fun prover s = prove_goalw Tr2.thy [ifte_def] s |
|
69 (fn prems => |
|
70 [ |
|
71 (simp_tac (ccc1_ss addsimps tr_when) 1) |
|
72 ]); |
|
73 |
|
74 val ifte_thms = map prover [ |
|
75 "If UU then e1 else e2 fi = UU", |
|
76 "If FF then e1 else e2 fi = e2", |
|
77 "If TT then e1 else e2 fi = e1"]; |
|
78 |
|
79 |
|
80 |
|
81 |
|
82 |
|