src/HOLCF/tr2.ML
changeset 243 c22b85994e17
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOLCF/tr2.ML	Wed Jan 19 17:35:01 1994 +0100
     1.3 @@ -0,0 +1,82 @@
     1.4 +(*  Title: 	HOLCF/tr2.ML
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Franz Regensburger
     1.7 +    Copyright   1993 Technische Universitaet Muenchen
     1.8 +
     1.9 +Lemmas for tr2.thy
    1.10 +*)
    1.11 +
    1.12 +open Tr2;
    1.13 +
    1.14 +(* ------------------------------------------------------------------------ *) 
    1.15 +(* lemmas about andalso                                                     *) 
    1.16 +(* ------------------------------------------------------------------------ *)
    1.17 +
    1.18 +fun prover s =  prove_goalw Tr2.thy [andalso_def] s
    1.19 + (fn prems =>
    1.20 +	[
    1.21 +	(simp_tac (ccc1_ss addsimps tr_when) 1)
    1.22 +	]);
    1.23 +
    1.24 +val andalso_thms = map prover [
    1.25 +			"TT andalso y = y",
    1.26 +			"FF andalso y = FF",
    1.27 +			"UU andalso y = UU"
    1.28 +			];
    1.29 +
    1.30 +val andalso_thms = andalso_thms @ 
    1.31 + [prove_goalw Tr2.thy [andalso_def] "x andalso TT =  x"
    1.32 + (fn prems =>
    1.33 +	[
    1.34 +	(res_inst_tac [("p","x")] trE 1),
    1.35 +	(asm_simp_tac (ccc1_ss addsimps tr_when) 1),
    1.36 +	(asm_simp_tac (ccc1_ss addsimps tr_when) 1),
    1.37 +	(asm_simp_tac (ccc1_ss addsimps tr_when) 1)
    1.38 +	])];
    1.39 +
    1.40 +(* ------------------------------------------------------------------------ *) 
    1.41 +(* lemmas about orelse                                                      *) 
    1.42 +(* ------------------------------------------------------------------------ *)
    1.43 +
    1.44 +fun prover s =  prove_goalw Tr2.thy [orelse_def] s
    1.45 + (fn prems =>
    1.46 +	[
    1.47 +	(simp_tac (ccc1_ss addsimps tr_when) 1)
    1.48 +	]);
    1.49 +
    1.50 +val orelse_thms = map prover [
    1.51 +			"TT orelse y  = TT",
    1.52 +			"FF orelse y =  y",
    1.53 +			"UU orelse y = UU"
    1.54 +			];
    1.55 +
    1.56 +val orelse_thms = orelse_thms @ 
    1.57 + [prove_goalw Tr2.thy [orelse_def] "x orelse FF =  x"
    1.58 + (fn prems =>
    1.59 +	[
    1.60 +	(res_inst_tac [("p","x")] trE 1),
    1.61 +	(asm_simp_tac (ccc1_ss addsimps tr_when) 1),
    1.62 +	(asm_simp_tac (ccc1_ss addsimps tr_when) 1),
    1.63 +	(asm_simp_tac (ccc1_ss addsimps tr_when) 1)
    1.64 +	])];
    1.65 +
    1.66 +
    1.67 +(* ------------------------------------------------------------------------ *) 
    1.68 +(* lemmas about If_then_else_fi                                             *) 
    1.69 +(* ------------------------------------------------------------------------ *)
    1.70 +
    1.71 +fun prover s =  prove_goalw Tr2.thy [ifte_def] s
    1.72 + (fn prems =>
    1.73 +	[
    1.74 +	(simp_tac (ccc1_ss addsimps tr_when) 1)
    1.75 +	]);
    1.76 +
    1.77 +val ifte_thms = map prover [
    1.78 +			"If UU then e1 else e2 fi = UU",
    1.79 +			"If FF then e1 else e2 fi = e2",
    1.80 +			"If TT then e1 else e2 fi = e1"];
    1.81 +
    1.82 +
    1.83 +
    1.84 +
    1.85 +