src/CTT/Bool.ML
author obua
Fri, 16 Sep 2005 21:02:15 +0200
changeset 17440 df77edc4f5d0
parent 9251 bd57acd44fc1
child 17441 5b5feca0344a
permissions -rw-r--r--
fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9251
bd57acd44fc1 more tidying. also generalized some tactics to prove "Type A" and
paulson
parents: 9249
diff changeset
     1
(*  Title:      CTT/Bool
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1459
d12da312eff4 expanded tabs
clasohm
parents: 1294
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1991  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
9251
bd57acd44fc1 more tidying. also generalized some tactics to prove "Type A" and
paulson
parents: 9249
diff changeset
     6
The two-element type (booleans and conditionals)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
val bool_defs = [Bool_def,true_def,false_def,cond_def];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
(*Derivation of rules for the type Bool*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
(*formation rule*)
9249
c71db8c28727 removed batch proofs
paulson
parents: 1459
diff changeset
    14
Goalw bool_defs "Bool type";
c71db8c28727 removed batch proofs
paulson
parents: 1459
diff changeset
    15
by (typechk_tac []) ;
c71db8c28727 removed batch proofs
paulson
parents: 1459
diff changeset
    16
qed "boolF";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
(*introduction rules for true, false*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
9249
c71db8c28727 removed batch proofs
paulson
parents: 1459
diff changeset
    21
Goalw bool_defs "true : Bool";
c71db8c28727 removed batch proofs
paulson
parents: 1459
diff changeset
    22
by (typechk_tac []) ;
c71db8c28727 removed batch proofs
paulson
parents: 1459
diff changeset
    23
qed "boolI_true";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
9249
c71db8c28727 removed batch proofs
paulson
parents: 1459
diff changeset
    25
Goalw bool_defs "false : Bool";
c71db8c28727 removed batch proofs
paulson
parents: 1459
diff changeset
    26
by (typechk_tac []) ;
c71db8c28727 removed batch proofs
paulson
parents: 1459
diff changeset
    27
qed "boolI_false";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
(*elimination rule: typing of cond*)
9249
c71db8c28727 removed batch proofs
paulson
parents: 1459
diff changeset
    30
Goalw bool_defs 
c71db8c28727 removed batch proofs
paulson
parents: 1459
diff changeset
    31
    "[| p:Bool;  a : C(true);  b : C(false) |] ==> cond(p,a,b) : C(p)";
c71db8c28727 removed batch proofs
paulson
parents: 1459
diff changeset
    32
by (typechk_tac []);
c71db8c28727 removed batch proofs
paulson
parents: 1459
diff changeset
    33
by (ALLGOALS (etac TE));
c71db8c28727 removed batch proofs
paulson
parents: 1459
diff changeset
    34
by (typechk_tac []) ;
c71db8c28727 removed batch proofs
paulson
parents: 1459
diff changeset
    35
qed "boolE";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
9249
c71db8c28727 removed batch proofs
paulson
parents: 1459
diff changeset
    37
Goalw bool_defs
c71db8c28727 removed batch proofs
paulson
parents: 1459
diff changeset
    38
    "[| p = q : Bool;  a = c : C(true);  b = d : C(false) |] \
c71db8c28727 removed batch proofs
paulson
parents: 1459
diff changeset
    39
\    ==> cond(p,a,b) = cond(q,c,d) : C(p)";
c71db8c28727 removed batch proofs
paulson
parents: 1459
diff changeset
    40
by (rtac PlusEL 1);
c71db8c28727 removed batch proofs
paulson
parents: 1459
diff changeset
    41
by (REPEAT (eresolve_tac [asm_rl, refl_elem RS TEL] 1)) ;
c71db8c28727 removed batch proofs
paulson
parents: 1459
diff changeset
    42
qed "boolEL";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
(*computation rules for true, false*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
9249
c71db8c28727 removed batch proofs
paulson
parents: 1459
diff changeset
    46
Goalw bool_defs 
c71db8c28727 removed batch proofs
paulson
parents: 1459
diff changeset
    47
    "[| a : C(true);  b : C(false) |] ==> cond(true,a,b) = a : C(true)";
c71db8c28727 removed batch proofs
paulson
parents: 1459
diff changeset
    48
by (resolve_tac comp_rls 1);
c71db8c28727 removed batch proofs
paulson
parents: 1459
diff changeset
    49
by (typechk_tac []);
c71db8c28727 removed batch proofs
paulson
parents: 1459
diff changeset
    50
by (ALLGOALS (etac TE));
c71db8c28727 removed batch proofs
paulson
parents: 1459
diff changeset
    51
by (typechk_tac []) ;
c71db8c28727 removed batch proofs
paulson
parents: 1459
diff changeset
    52
qed "boolC_true";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
9249
c71db8c28727 removed batch proofs
paulson
parents: 1459
diff changeset
    54
Goalw bool_defs
c71db8c28727 removed batch proofs
paulson
parents: 1459
diff changeset
    55
    "[| a : C(true);  b : C(false) |] ==> cond(false,a,b) = b : C(false)";
c71db8c28727 removed batch proofs
paulson
parents: 1459
diff changeset
    56
by (resolve_tac comp_rls 1);
c71db8c28727 removed batch proofs
paulson
parents: 1459
diff changeset
    57
by (typechk_tac []);
c71db8c28727 removed batch proofs
paulson
parents: 1459
diff changeset
    58
by (ALLGOALS (etac TE));
c71db8c28727 removed batch proofs
paulson
parents: 1459
diff changeset
    59
by (typechk_tac []) ;
c71db8c28727 removed batch proofs
paulson
parents: 1459
diff changeset
    60
qed "boolC_false";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
writeln"Reached end of file.";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63