isabelle: src/HOLCF/Sprod1.ML@6754fa0f2af7 (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
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
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	(* less_sprod is a partial order on Sprod *)
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
9248 e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc. paulson parents: 9245 diff changeset	12	Goalw [less_sprod_def]"(p::'a ** 'b) << p";
9245 428385c4bc50 removed most batch-style proofs paulson parents: 3323 diff changeset	13	by (fast_tac (HOL_cs addIs [refl_less]) 1);
428385c4bc50 removed most batch-style proofs paulson parents: 3323 diff changeset	14	qed "refl_less_sprod";
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	15
9248 e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc. paulson parents: 9245 diff changeset	16	Goalw [less_sprod_def]
9245 428385c4bc50 removed most batch-style proofs paulson parents: 3323 diff changeset	17	"[\|(p1::'a ** 'b) << p2;p2 << p1\|] ==> p1=p2";
428385c4bc50 removed most batch-style proofs paulson parents: 3323 diff changeset	18	by (rtac Sel_injective_Sprod 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	by (fast_tac (HOL_cs addIs [antisym_less]) 1);
428385c4bc50 removed most batch-style proofs paulson parents: 3323 diff changeset	21	qed "antisym_less_sprod";
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_sprod_def]
9245 428385c4bc50 removed most batch-style proofs paulson parents: 3323 diff changeset	24	"[\|(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	25	by (blast_tac (HOL_cs addIs [trans_less]) 1);
9245 428385c4bc50 removed most batch-style proofs paulson parents: 3323 diff changeset	26	qed "trans_less_sprod";

author	oheimb
	Tue, 30 Jan 2001 18:48:33 +0100
changeset 11001	6754fa0f2af7
parent 9248	e1dee89de037
child 12030	46d57d0290a2
permissions	-rw-r--r--