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