src/CTT/bool.ML
author wenzelm
Wed, 09 Jul 1997 17:00:34 +0200
changeset 3511 da4dd8b7ced4
parent 0 a5a9c433f639
permissions -rw-r--r--
removed obsolete init_pps and init_thy_reader;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	CTT/bool
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1991  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Theorems for bool.thy (booleans and conditionals)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
open Bool;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
val bool_defs = [Bool_def,true_def,false_def,cond_def];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
(*Derivation of rules for the type Bool*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
(*formation rule*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
val boolF = prove_goal Bool.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
    "Bool type"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
  [ (rewrite_goals_tac bool_defs),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
    (typechk_tac[]) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
(*introduction rules for true, false*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
val boolI_true = prove_goal Bool.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
    "true : Bool"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
  [ (rewrite_goals_tac bool_defs),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
    (typechk_tac[]) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
val boolI_false = prove_goal Bool.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
    "false : Bool"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
  [ (rewrite_goals_tac bool_defs),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
    (typechk_tac[]) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
(*elimination rule: typing of cond*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
val boolE = prove_goal Bool.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
    "[| p:Bool;  a : C(true);  b : C(false) |] ==> cond(p,a,b) : C(p)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
  [ (cut_facts_tac prems 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
    (rewrite_goals_tac bool_defs),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
    (typechk_tac prems),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
    (ALLGOALS (etac TE)),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
    (typechk_tac prems) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
val boolEL = prove_goal Bool.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
    "[| p = q : Bool;  a = c : C(true);  b = d : C(false) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
\    cond(p,a,b) = cond(q,c,d) : C(p)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
  [ (cut_facts_tac prems 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
    (rewrite_goals_tac bool_defs),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
    (resolve_tac [PlusEL] 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
    (REPEAT (eresolve_tac [asm_rl, refl_elem RS TEL] 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
(*computation rules for true, false*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
val boolC_true = prove_goal Bool.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
    "[| a : C(true);  b : C(false) |] ==> cond(true,a,b) = a : C(true)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
  [ (cut_facts_tac prems 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
    (rewrite_goals_tac bool_defs),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
    (resolve_tac comp_rls 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
    (typechk_tac[]),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
    (ALLGOALS (etac TE)),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
    (typechk_tac prems) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
val boolC_false = prove_goal Bool.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
    "[| a : C(true);  b : C(false) |] ==> cond(false,a,b) = b : C(false)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
 (fn prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
  [ (cut_facts_tac prems 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
    (rewrite_goals_tac bool_defs),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
    (resolve_tac comp_rls 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
    (typechk_tac[]),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
    (ALLGOALS (etac TE)),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
    (typechk_tac prems) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
writeln"Reached end of file.";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79