author  wenzelm 
Wed, 09 Jul 1997 17:00:34 +0200  
changeset 3511  da4dd8b7ced4 
parent 1459  d12da312eff4 
child 9249  c71db8c28727 
permissions  rwrr 
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 