isabelle: src/HOLCF/Sprod1.ML@e96d5c42c4b0 (annotated)

2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2033 diff changeset	1	(* Title: HOLCF/Sprod1.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: 1277 diff changeset	3	Author: Franz Regensburger
12030 46d57d0290a2 GPLed; wenzelm parents: 9248 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	*)
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	(* less_sprod is a partial order on Sprod *)
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
9248 e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc. paulson parents: 9245 diff changeset	11	Goalw [less_sprod_def]"(p::'a ** 'b) << p";
9245 428385c4bc50 removed most batch-style proofs paulson parents: 3323 diff changeset	12	by (fast_tac (HOL_cs addIs [refl_less]) 1);
428385c4bc50 removed most batch-style proofs paulson parents: 3323 diff changeset	13	qed "refl_less_sprod";
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	14
9248 e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc. paulson parents: 9245 diff changeset	15	Goalw [less_sprod_def]
9245 428385c4bc50 removed most batch-style proofs paulson parents: 3323 diff changeset	16	"[\|(p1::'a ** 'b) << p2;p2 << p1\|] ==> p1=p2";
428385c4bc50 removed most batch-style proofs paulson parents: 3323 diff changeset	17	by (rtac Sel_injective_Sprod 1);
428385c4bc50 removed most batch-style proofs paulson parents: 3323 diff changeset	18	by (fast_tac (HOL_cs addIs [antisym_less]) 1);
428385c4bc50 removed most batch-style proofs paulson parents: 3323 diff changeset	19	by (fast_tac (HOL_cs addIs [antisym_less]) 1);
428385c4bc50 removed most batch-style proofs paulson parents: 3323 diff changeset	20	qed "antisym_less_sprod";
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_sprod_def]
9245 428385c4bc50 removed most batch-style proofs paulson parents: 3323 diff changeset	23	"[\|(p1::'a**'b) << p2;p2 << p3\|] ==> p1 << p3";
9248 e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc. paulson parents: 9245 diff changeset	24	by (blast_tac (HOL_cs addIs [trans_less]) 1);
9245 428385c4bc50 removed most batch-style proofs paulson parents: 3323 diff changeset	25	qed "trans_less_sprod";

author	paulson
	Sun, 15 Feb 2004 10:46:37 +0100
changeset 14387	e96d5c42c4b0
parent 12030	46d57d0290a2
child 14981	e73f8140af78
permissions	-rw-r--r--