src/HOLCF/tr2.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 243 c22b85994e17
permissions -rw-r--r--
made tutorial first;
     1 (*  Title: 	HOLCF/tr2.ML
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Lemmas for tr2.thy
     7 *)
     8 
     9 open Tr2;
    10 
    11 (* ------------------------------------------------------------------------ *) 
    12 (* lemmas about andalso                                                     *) 
    13 (* ------------------------------------------------------------------------ *)
    14 
    15 fun prover s =  prove_goalw Tr2.thy [andalso_def] s
    16  (fn prems =>
    17 	[
    18 	(simp_tac (ccc1_ss addsimps tr_when) 1)
    19 	]);
    20 
    21 val andalso_thms = map prover [
    22 			"TT andalso y = y",
    23 			"FF andalso y = FF",
    24 			"UU andalso y = UU"
    25 			];
    26 
    27 val andalso_thms = andalso_thms @ 
    28  [prove_goalw Tr2.thy [andalso_def] "x andalso TT =  x"
    29  (fn prems =>
    30 	[
    31 	(res_inst_tac [("p","x")] trE 1),
    32 	(asm_simp_tac (ccc1_ss addsimps tr_when) 1),
    33 	(asm_simp_tac (ccc1_ss addsimps tr_when) 1),
    34 	(asm_simp_tac (ccc1_ss addsimps tr_when) 1)
    35 	])];
    36 
    37 (* ------------------------------------------------------------------------ *) 
    38 (* lemmas about orelse                                                      *) 
    39 (* ------------------------------------------------------------------------ *)
    40 
    41 fun prover s =  prove_goalw Tr2.thy [orelse_def] s
    42  (fn prems =>
    43 	[
    44 	(simp_tac (ccc1_ss addsimps tr_when) 1)
    45 	]);
    46 
    47 val orelse_thms = map prover [
    48 			"TT orelse y  = TT",
    49 			"FF orelse y =  y",
    50 			"UU orelse y = UU"
    51 			];
    52 
    53 val orelse_thms = orelse_thms @ 
    54  [prove_goalw Tr2.thy [orelse_def] "x orelse FF =  x"
    55  (fn prems =>
    56 	[
    57 	(res_inst_tac [("p","x")] trE 1),
    58 	(asm_simp_tac (ccc1_ss addsimps tr_when) 1),
    59 	(asm_simp_tac (ccc1_ss addsimps tr_when) 1),
    60 	(asm_simp_tac (ccc1_ss addsimps tr_when) 1)
    61 	])];
    62 
    63 
    64 (* ------------------------------------------------------------------------ *) 
    65 (* lemmas about If_then_else_fi                                             *) 
    66 (* ------------------------------------------------------------------------ *)
    67 
    68 fun prover s =  prove_goalw Tr2.thy [ifte_def] s
    69  (fn prems =>
    70 	[
    71 	(simp_tac (ccc1_ss addsimps tr_when) 1)
    72 	]);
    73 
    74 val ifte_thms = map prover [
    75 			"If UU then e1 else e2 fi = UU",
    76 			"If FF then e1 else e2 fi = e2",
    77 			"If TT then e1 else e2 fi = e1"];
    78 
    79 
    80 
    81 
    82