isabelle: src/HOLCF/Cprod1.ML@6f463d16cbd0 (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
12030 46d57d0290a2 GPLed; wenzelm parents: 11343 diff changeset	4	License: GPL (GNU GENERAL PUBLIC LICENSE)
243 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	Goalw [less_cprod_def] "(p::'a*'b) << p";
9245 428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	15	by (Simp_tac 1);
428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	16	qed "refl_less_cprod";
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	17
9245 428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	18	Goalw [less_cprod_def] "[\|(p1::'a * 'b) << p2;p2 << p1\|] ==> p1=p2";
11343 d5f1b482bfbf replaced Sel_injective_cprod by new injective_fst_snd oheimb parents: 11025 diff changeset	19	by (rtac injective_fst_snd 1);
9245 428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	20	by (fast_tac (HOL_cs addIs [antisym_less]) 1);
428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	21	by (fast_tac (HOL_cs addIs [antisym_less]) 1);
428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	22	qed "antisym_less_cprod";
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	23
9248 e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc. paulson parents: 9245 diff changeset	24	Goalw [less_cprod_def]
9245 428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	25	"[\|(p1::'a*'b) << p2;p2 << p3\|] ==> p1 << p3";
428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	26	by (rtac conjI 1);
428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	27	by (fast_tac (HOL_cs addIs [trans_less]) 1);
428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	28	by (fast_tac (HOL_cs addIs [trans_less]) 1);
428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	29	qed "trans_less_cprod";

author	paulson
	Wed, 07 Nov 2001 12:29:07 +0100
changeset 12088	6f463d16cbd0
parent 12030	46d57d0290a2
child 14981	e73f8140af78
permissions	-rw-r--r--