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