isabelle: src/HOLCF/Cprod1.ML@60c83075e41f (annotated)

2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2033 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
10212 33fe2d701ddd * empty log message * nipkow parents: 9248 diff changeset	6	Partial ordering for cartesian product of HOL theory Product_Type.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
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	(* 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	12	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	13
11025 a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format oheimb parents: 10212 diff changeset	14	(###TO Product_Type_lemmas.ML )
9248 e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc. paulson parents: 9245 diff changeset	15	Goal "[\|fst x = fst y; snd x = snd y\|] ==> x = y";
9245 428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	16	by (subgoal_tac "(fst x,snd x)=(fst y,snd y)" 1);
428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	17	by (rotate_tac ~1 1);
428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	18	by (asm_full_simp_tac(HOL_ss addsimps[surjective_pairing RS sym])1);
11025 a70b796d9af8 converted to Isar therory, adding attributes complete_split and split_format oheimb parents: 10212 diff changeset	19	by (asm_simp_tac (simpset_of (theory "Product_Type")) 1);
9245 428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	20	qed "Sel_injective_cprod";
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	21
9248 e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc. paulson parents: 9245 diff changeset	22	Goalw [less_cprod_def] "(p::'a*'b) << p";
9245 428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	23	by (Simp_tac 1);
428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	24	qed "refl_less_cprod";
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	25
9245 428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	26	Goalw [less_cprod_def] "[\|(p1::'a * 'b) << p2;p2 << p1\|] ==> p1=p2";
428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	27	by (rtac Sel_injective_cprod 1);
428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	28	by (fast_tac (HOL_cs addIs [antisym_less]) 1);
428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	29	by (fast_tac (HOL_cs addIs [antisym_less]) 1);
428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	30	qed "antisym_less_cprod";
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	31
9248 e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc. paulson parents: 9245 diff changeset	32	Goalw [less_cprod_def]
9245 428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	33	"[\|(p1::'a*'b) << p2;p2 << p3\|] ==> p1 << p3";
428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	34	by (rtac conjI 1);
428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	35	by (fast_tac (HOL_cs addIs [trans_less]) 1);
428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	36	by (fast_tac (HOL_cs addIs [trans_less]) 1);
428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	37	qed "trans_less_cprod";

author	wenzelm
	Mon, 05 Feb 2001 14:54:04 +0100
changeset 11067	60c83075e41f
parent 11025	a70b796d9af8
child 11343	d5f1b482bfbf
permissions	-rw-r--r--