isabelle: src/HOLCF/Cprod1.ML@dd5fb02ff872 (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
9248 e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc. paulson parents: 9245 diff changeset	14	Goal "[\|fst x = fst y; snd x = snd y\|] ==> x = y";
9245 428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	15	by (subgoal_tac "(fst x,snd x)=(fst y,snd y)" 1);
428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	16	by (rotate_tac ~1 1);
428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	17	by (asm_full_simp_tac(HOL_ss addsimps[surjective_pairing RS sym])1);
10212 33fe2d701ddd * empty log message * nipkow parents: 9248 diff changeset	18	by (asm_simp_tac (simpset_of Product_Type.thy) 1);
9245 428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	19	qed "Sel_injective_cprod";
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	20
9248 e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc. paulson parents: 9245 diff changeset	21	Goalw [less_cprod_def] "(p::'a*'b) << p";
9245 428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	22	by (Simp_tac 1);
428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	23	qed "refl_less_cprod";
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	24
9245 428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	25	Goalw [less_cprod_def] "[\|(p1::'a * 'b) << p2;p2 << p1\|] ==> p1=p2";
428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	26	by (rtac Sel_injective_cprod 1);
428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	27	by (fast_tac (HOL_cs addIs [antisym_less]) 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	qed "antisym_less_cprod";
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	30
9248 e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc. paulson parents: 9245 diff changeset	31	Goalw [less_cprod_def]
9245 428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	32	"[\|(p1::'a*'b) << p2;p2 << p3\|] ==> p1 << p3";
428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	33	by (rtac conjI 1);
428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	34	by (fast_tac (HOL_cs addIs [trans_less]) 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	qed "trans_less_cprod";

author	wenzelm
	Sun, 07 Jan 2001 21:35:11 +0100
changeset 10815	dd5fb02ff872
parent 10212	33fe2d701ddd
child 11025	a70b796d9af8
permissions	-rw-r--r--