isabelle: src/HOLCF/Sprod1.ML@38f96394c099 (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
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2033 diff changeset	6	Lemmas for theory Sprod1.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	open Sprod1;
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	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	12	(* less_sprod is a partial order on Sprod *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	13	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	14
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 2640 diff changeset	15	qed_goalw "refl_less_sprod" thy [less_sprod_def]"(p::'a ** 'b) << p"
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2033 diff changeset	16	(fn prems => [(fast_tac (HOL_cs addIs [refl_less]) 1)]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	17
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2033 diff changeset	18	qed_goalw "antisym_less_sprod" thy [less_sprod_def]
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 2640 diff changeset	19	"[\|(p1::'a ** 'b) << p2;p2 << p1\|] ==> p1=p2"
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2033 diff changeset	20	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1277 diff changeset	21	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1277 diff changeset	22	(cut_facts_tac prems 1),
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2033 diff changeset	23	(rtac Sel_injective_Sprod 1),
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2033 diff changeset	24	(fast_tac (HOL_cs addIs [antisym_less]) 1),
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2033 diff changeset	25	(fast_tac (HOL_cs addIs [antisym_less]) 1)
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1277 diff changeset	26	]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	27
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2033 diff changeset	28	qed_goalw "trans_less_sprod" thy [less_sprod_def]
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 2640 diff changeset	29	"[\|(p1::'a**'b) << p2;p2 << p3\|] ==> p1 << p3"
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2033 diff changeset	30	(fn prems =>
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2033 diff changeset	31	[
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2033 diff changeset	32	(cut_facts_tac prems 1),
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2033 diff changeset	33	(rtac conjI 1),
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2033 diff changeset	34	(fast_tac (HOL_cs addIs [trans_less]) 1),
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2033 diff changeset	35	(fast_tac (HOL_cs addIs [trans_less]) 1)
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2033 diff changeset	36	]);

author	paulson
	Fri, 18 Feb 2000 15:35:29 +0100
changeset 8255	38f96394c099
parent 3323	194ae2e0c193
child 9245	428385c4bc50
permissions	-rw-r--r--