isabelle: src/HOLCF/Tr2.ML@8a47f85e7a03 (annotated)

1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	1	(* Title: HOLCF/tr2.ML
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	2	ID: $Id$
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	3	Author: Franz Regensburger
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	4	Copyright 1993 Technische Universitaet Muenchen
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	5
2453 2d416226b27d corrected headers oheimb parents: 2355 diff changeset	6	Lemmas for Tr2.thy
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	7	*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	8
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	9	open Tr2;
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	10
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	11	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	12	(* lemmas about andalso *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	13	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	14
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	15	fun prover s = prove_goalw Tr2.thy [andalso_def] s
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	16	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	17	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	18	(simp_tac (!simpset addsimps tr_when) 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	19	]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	20
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	21	val andalso_thms = map prover [
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	22	"(TT andalso y) = y",
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	23	"(FF andalso y) = FF",
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	24	"(UU andalso y) = UU"
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	25	];
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	26
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	27	val andalso_thms = andalso_thms @
430 89e1986125fe Franz Regensburger's changes. nipkow parents: 243 diff changeset	28	[prove_goalw Tr2.thy [andalso_def] "(x andalso TT) = x"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	29	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	30	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	31	(res_inst_tac [("p","x")] trE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	32	(asm_simp_tac (!simpset addsimps tr_when) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	33	(asm_simp_tac (!simpset addsimps tr_when) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	34	(asm_simp_tac (!simpset addsimps tr_when) 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	35	])];
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	36
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	37	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	38	(* lemmas about orelse *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	39	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	40
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	41	fun prover s = prove_goalw Tr2.thy [orelse_def] s
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	42	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	43	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	44	(simp_tac (!simpset addsimps tr_when) 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	45	]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	46
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	47	val orelse_thms = map prover [
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	48	"(TT orelse y) = TT",
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	49	"(FF orelse y) = y",
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	50	"(UU orelse y) = UU"
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	51	];
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	52
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	53	val orelse_thms = orelse_thms @
430 89e1986125fe Franz Regensburger's changes. nipkow parents: 243 diff changeset	54	[prove_goalw Tr2.thy [orelse_def] "(x orelse FF) = x"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	55	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	56	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	57	(res_inst_tac [("p","x")] trE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	58	(asm_simp_tac (!simpset addsimps tr_when) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	59	(asm_simp_tac (!simpset addsimps tr_when) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	60	(asm_simp_tac (!simpset addsimps tr_when) 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	61	])];
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	62
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	63
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	64	(* ------------------------------------------------------------------------ *)
430 89e1986125fe Franz Regensburger's changes. nipkow parents: 243 diff changeset	65	(* lemmas about neg *)
89e1986125fe Franz Regensburger's changes. nipkow parents: 243 diff changeset	66	(* ------------------------------------------------------------------------ *)
89e1986125fe Franz Regensburger's changes. nipkow parents: 243 diff changeset	67
89e1986125fe Franz Regensburger's changes. nipkow parents: 243 diff changeset	68	fun prover s = prove_goalw Tr2.thy [neg_def] s
89e1986125fe Franz Regensburger's changes. nipkow parents: 243 diff changeset	69	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	70	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	71	(simp_tac (!simpset addsimps tr_when) 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	72	]);
430 89e1986125fe Franz Regensburger's changes. nipkow parents: 243 diff changeset	73
89e1986125fe Franz Regensburger's changes. nipkow parents: 243 diff changeset	74	val neg_thms = map prover [
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	75	"neg`TT = FF",
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	76	"neg`FF = TT",
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	77	"neg`UU = UU"
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	78	];
430 89e1986125fe Franz Regensburger's changes. nipkow parents: 243 diff changeset	79
89e1986125fe Franz Regensburger's changes. nipkow parents: 243 diff changeset	80	(* ------------------------------------------------------------------------ *)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	81	(* lemmas about If_then_else_fi *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	82	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	83
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	84	fun prover s = prove_goalw Tr2.thy [ifte_def] s
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	85	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	86	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	87	(simp_tac (!simpset addsimps tr_when) 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	88	]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	89
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	90	val ifte_thms = map prover [
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	91	"If UU then e1 else e2 fi = UU",
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	92	"If FF then e1 else e2 fi = e2",
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	93	"If TT then e1 else e2 fi = e1"];
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	94
2355 ee9bdbe2ac8a simpset extension moved from HOLCF.ML to One.ML and Tr2.ML sandnerr parents: 1461 diff changeset	95	Addsimps (dist_less_tr @ dist_eq_tr @ tr_when @ andalso_thms @
ee9bdbe2ac8a simpset extension moved from HOLCF.ML to One.ML and Tr2.ML sandnerr parents: 1461 diff changeset	96	orelse_thms @ neg_thms @ ifte_thms);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	97
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	98
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	99

author	paulson
	Fri, 31 Jan 1997 17:13:19 +0100
changeset 2572	8a47f85e7a03
parent 2453	2d416226b27d
permissions	-rw-r--r--