author | oheimb |
Mon, 02 Dec 1996 12:19:56 +0100 | |
changeset 2290 | e5c08f8b483b |
parent 1459 | d12da312eff4 |
child 9249 | c71db8c28727 |
permissions | -rw-r--r-- |
1459 | 1 |
(* Title: CTT/bool |
0 | 2 |
ID: $Id$ |
1459 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1991 University of Cambridge |
5 |
||
6 |
Theorems for bool.thy (booleans and conditionals) |
|
7 |
*) |
|
8 |
||
9 |
open Bool; |
|
10 |
||
11 |
val bool_defs = [Bool_def,true_def,false_def,cond_def]; |
|
12 |
||
13 |
(*Derivation of rules for the type Bool*) |
|
14 |
||
15 |
(*formation rule*) |
|
1294 | 16 |
qed_goalw "boolF" Bool.thy bool_defs |
0 | 17 |
"Bool type" |
360
2b74eebdbdb8
Bool.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset
|
18 |
(fn _ => [ (typechk_tac []) ]); |
0 | 19 |
|
20 |
||
21 |
(*introduction rules for true, false*) |
|
22 |
||
1294 | 23 |
qed_goalw "boolI_true" Bool.thy bool_defs |
0 | 24 |
"true : Bool" |
360
2b74eebdbdb8
Bool.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset
|
25 |
(fn _ => [ (typechk_tac []) ]); |
0 | 26 |
|
1294 | 27 |
qed_goalw "boolI_false" Bool.thy bool_defs |
0 | 28 |
"false : Bool" |
360
2b74eebdbdb8
Bool.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset
|
29 |
(fn _ => [ (typechk_tac []) ]); |
0 | 30 |
|
31 |
(*elimination rule: typing of cond*) |
|
1294 | 32 |
qed_goalw "boolE" Bool.thy bool_defs |
360
2b74eebdbdb8
Bool.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset
|
33 |
"!!C. [| p:Bool; a : C(true); b : C(false) |] ==> cond(p,a,b) : C(p)" |
2b74eebdbdb8
Bool.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset
|
34 |
(fn _ => |
2b74eebdbdb8
Bool.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset
|
35 |
[ (typechk_tac []), |
0 | 36 |
(ALLGOALS (etac TE)), |
360
2b74eebdbdb8
Bool.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset
|
37 |
(typechk_tac []) ]); |
0 | 38 |
|
1294 | 39 |
qed_goalw "boolEL" Bool.thy bool_defs |
360
2b74eebdbdb8
Bool.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset
|
40 |
"!!C. [| p = q : Bool; a = c : C(true); b = d : C(false) |] ==> \ |
2b74eebdbdb8
Bool.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset
|
41 |
\ cond(p,a,b) = cond(q,c,d) : C(p)" |
2b74eebdbdb8
Bool.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset
|
42 |
(fn _ => |
1459 | 43 |
[ (rtac PlusEL 1), |
0 | 44 |
(REPEAT (eresolve_tac [asm_rl, refl_elem RS TEL] 1)) ]); |
45 |
||
46 |
(*computation rules for true, false*) |
|
47 |
||
1294 | 48 |
qed_goalw "boolC_true" Bool.thy bool_defs |
360
2b74eebdbdb8
Bool.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset
|
49 |
"!!C. [| a : C(true); b : C(false) |] ==> cond(true,a,b) = a : C(true)" |
2b74eebdbdb8
Bool.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset
|
50 |
(fn _ => |
2b74eebdbdb8
Bool.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset
|
51 |
[ (resolve_tac comp_rls 1), |
2b74eebdbdb8
Bool.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset
|
52 |
(typechk_tac []), |
0 | 53 |
(ALLGOALS (etac TE)), |
360
2b74eebdbdb8
Bool.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset
|
54 |
(typechk_tac []) ]); |
0 | 55 |
|
1294 | 56 |
qed_goalw "boolC_false" Bool.thy bool_defs |
360
2b74eebdbdb8
Bool.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset
|
57 |
"!!C. [| a : C(true); b : C(false) |] ==> cond(false,a,b) = b : C(false)" |
2b74eebdbdb8
Bool.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset
|
58 |
(fn _ => |
2b74eebdbdb8
Bool.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset
|
59 |
[ (resolve_tac comp_rls 1), |
2b74eebdbdb8
Bool.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset
|
60 |
(typechk_tac []), |
0 | 61 |
(ALLGOALS (etac TE)), |
360
2b74eebdbdb8
Bool.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset
|
62 |
(typechk_tac []) ]); |
0 | 63 |
|
64 |
writeln"Reached end of file."; |
|
65 |