isabelle: src/HOLCF/Cprod1.ML@8d42a7bccf0b (annotated)

1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	1	(* Title: HOLCF/cprod1.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
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	6	Lemmas for theory cprod1.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 Cprod1;
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	10
892 d0dc8d057929 added qed, qed_goal[w] clasohm parents: 243 diff changeset	11	qed_goalw "less_cprod1b" Cprod1.thy [less_cprod_def]
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 899 diff changeset	12	"less_cprod p1 p2 = ( fst(p1) << fst(p2) & snd(p1) << snd(p2))"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	13	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	14	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	15	(rtac refl 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	16	]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	17
892 d0dc8d057929 added qed, qed_goal[w] clasohm parents: 243 diff changeset	18	qed_goalw "less_cprod2a" Cprod1.thy [less_cprod_def]
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 899 diff changeset	19	"less_cprod (x,y) (UU,UU) ==> x = UU & y = UU"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	20	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	21	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	22	(cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	23	(etac conjE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	24	(dtac (fst_conv RS subst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	25	(dtac (fst_conv RS subst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	26	(dtac (fst_conv RS subst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	27	(dtac (snd_conv RS subst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	28	(dtac (snd_conv RS subst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	29	(dtac (snd_conv RS subst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	30	(rtac conjI 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	31	(etac UU_I 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	32	(etac UU_I 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	33	]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	34
892 d0dc8d057929 added qed, qed_goal[w] clasohm parents: 243 diff changeset	35	qed_goal "less_cprod2b" Cprod1.thy
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 899 diff changeset	36	"less_cprod p (UU,UU) ==> p = (UU,UU)"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	37	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	38	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	39	(cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	40	(res_inst_tac [("p","p")] PairE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	41	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	42	(dtac less_cprod2a 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	43	(Asm_simp_tac 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	44	]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	45
892 d0dc8d057929 added qed, qed_goal[w] clasohm parents: 243 diff changeset	46	qed_goalw "less_cprod2c" Cprod1.thy [less_cprod_def]
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 899 diff changeset	47	"less_cprod (x1,y1) (x2,y2) ==> x1 << x2 & y1 << y2"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	48	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	49	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	50	(cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	51	(etac conjE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	52	(dtac (fst_conv RS subst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	53	(dtac (fst_conv RS subst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	54	(dtac (fst_conv RS subst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	55	(dtac (snd_conv RS subst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	56	(dtac (snd_conv RS subst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	57	(dtac (snd_conv RS subst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	58	(rtac conjI 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	59	(atac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	60	(atac 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	(* less_cprod is a partial order on 'a * 'b *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	65	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	66
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 899 diff changeset	67	qed_goalw "refl_less_cprod" Cprod1.thy [less_cprod_def] "less_cprod p p"
1267 bca91b4e1710 added local simpsets clasohm parents: 1168 diff changeset	68	(fn prems => [Simp_tac 1]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	69
892 d0dc8d057929 added qed, qed_goal[w] clasohm parents: 243 diff changeset	70	qed_goal "antisym_less_cprod" Cprod1.thy
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 899 diff changeset	71	"[\|less_cprod p1 p2;less_cprod p2 p1\|] ==> p1=p2"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	72	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	73	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	74	(cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	75	(res_inst_tac [("p","p1")] PairE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	76	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	77	(res_inst_tac [("p","p2")] PairE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	78	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	79	(dtac less_cprod2c 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	80	(dtac less_cprod2c 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	81	(etac conjE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	82	(etac conjE 1),
2033 639de962ded4 Ran expandshort; used stac instead of ssubst paulson parents: 1461 diff changeset	83	(stac Pair_eq 1),
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	84	(fast_tac (HOL_cs addSIs [antisym_less]) 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	85	]);
243 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
892 d0dc8d057929 added qed, qed_goal[w] clasohm parents: 243 diff changeset	88	qed_goal "trans_less_cprod" Cprod1.thy
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 899 diff changeset	89	"[\|less_cprod p1 p2;less_cprod p2 p3\|] ==> less_cprod p1 p3"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	90	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	91	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	92	(cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	93	(res_inst_tac [("p","p1")] PairE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	94	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	95	(res_inst_tac [("p","p3")] PairE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	96	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	97	(res_inst_tac [("p","p2")] PairE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	98	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	99	(dtac less_cprod2c 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	100	(dtac less_cprod2c 1),
2033 639de962ded4 Ran expandshort; used stac instead of ssubst paulson parents: 1461 diff changeset	101	(stac less_cprod1b 1),
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	102	(Simp_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	103	(etac conjE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	104	(etac conjE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	105	(rtac conjI 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	106	(etac trans_less 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	107	(atac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	108	(etac trans_less 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	109	(atac 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	110	]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	111
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 899 diff changeset	112
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 899 diff changeset	113

author	paulson
	Wed, 13 Nov 1996 10:47:08 +0100
changeset 2183	8d42a7bccf0b
parent 2033	639de962ded4
child 2640	ee4dfce170a0
permissions	-rw-r--r--