isabelle: src/HOLCF/Cprod1.ML@e73f8140af78 (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
10212 33fe2d701ddd * empty log message * nipkow parents: 9248 diff changeset	5	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	6	*)
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	(* 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	11	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	12
9248 e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc. paulson parents: 9245 diff changeset	13	Goalw [less_cprod_def] "(p::'a*'b) << p";
9245 428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	14	by (Simp_tac 1);
428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	15	qed "refl_less_cprod";
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	16
9245 428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	17	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	18	by (rtac injective_fst_snd 1);
9245 428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	19	by (fast_tac (HOL_cs addIs [antisym_less]) 1);
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	qed "antisym_less_cprod";
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	22
9248 e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc. paulson parents: 9245 diff changeset	23	Goalw [less_cprod_def]
9245 428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	24	"[\|(p1::'a*'b) << p2;p2 << p3\|] ==> p1 << p3";
428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	25	by (rtac conjI 1);
428385c4bc50 removed most batch-style proofs paulson parents: 7661 diff changeset	26	by (fast_tac (HOL_cs addIs [trans_less]) 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	qed "trans_less_cprod";

author	kleing
	Mon, 21 Jun 2004 10:25:57 +0200
changeset 14981	e73f8140af78
parent 12030	46d57d0290a2
permissions	-rw-r--r--