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

243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	1	(* Title: HOLCF/tr2.ML
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	2	ID: $Id$
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	3	Author: Franz Regensburger
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
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	6	Lemmas for tr2.thy
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 =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	17	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	18	(simp_tac (ccc1_ss addsimps tr_when) 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	19	]);
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 [
430 89e1986125fe Franz Regensburger's changes. nipkow parents: 243 diff changeset	22	"(TT andalso y) = y",
89e1986125fe Franz Regensburger's changes. nipkow parents: 243 diff changeset	23	"(FF andalso y) = FF",
89e1986125fe Franz Regensburger's changes. nipkow parents: 243 diff changeset	24	"(UU andalso y) = UU"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	25	];
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 =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	30	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	31	(res_inst_tac [("p","x")] trE 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	32	(asm_simp_tac (ccc1_ss addsimps tr_when) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	33	(asm_simp_tac (ccc1_ss addsimps tr_when) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	34	(asm_simp_tac (ccc1_ss addsimps tr_when) 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	35	])];
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 =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	43	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	44	(simp_tac (ccc1_ss addsimps tr_when) 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	45	]);
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 [
430 89e1986125fe Franz Regensburger's changes. nipkow parents: 243 diff changeset	48	"(TT orelse y) = TT",
89e1986125fe Franz Regensburger's changes. nipkow parents: 243 diff changeset	49	"(FF orelse y) = y",
89e1986125fe Franz Regensburger's changes. nipkow parents: 243 diff changeset	50	"(UU orelse y) = UU"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	51	];
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 =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	56	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	57	(res_inst_tac [("p","x")] trE 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	58	(asm_simp_tac (ccc1_ss addsimps tr_when) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	59	(asm_simp_tac (ccc1_ss addsimps tr_when) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	60	(asm_simp_tac (ccc1_ss addsimps tr_when) 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	61	])];
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 =>
89e1986125fe Franz Regensburger's changes. nipkow parents: 243 diff changeset	70	[
89e1986125fe Franz Regensburger's changes. nipkow parents: 243 diff changeset	71	(simp_tac (ccc1_ss addsimps tr_when) 1)
89e1986125fe Franz Regensburger's changes. nipkow parents: 243 diff changeset	72	]);
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 [
89e1986125fe Franz Regensburger's changes. nipkow parents: 243 diff changeset	75	"neg[TT] = FF",
89e1986125fe Franz Regensburger's changes. nipkow parents: 243 diff changeset	76	"neg[FF] = TT",
89e1986125fe Franz Regensburger's changes. nipkow parents: 243 diff changeset	77	"neg[UU] = UU"
89e1986125fe Franz Regensburger's changes. nipkow parents: 243 diff changeset	78	];
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 =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	86	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	87	(simp_tac (ccc1_ss addsimps tr_when) 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	88	]);
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 [
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	91	"If UU then e1 else e2 fi = UU",
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	92	"If FF then e1 else e2 fi = e2",
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	93	"If TT then e1 else e2 fi = e1"];
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	94
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	95
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	96
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

author	lcp
	Tue, 21 Jun 1994 17:20:34 +0200
changeset 435	ca5356bd315a
parent 430	89e1986125fe
child 1168	74be52691d62
permissions	-rw-r--r--