isabelle: src/HOLCF/Sprod1.ML@3fac3e8d5d3e (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
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2033 diff changeset	15	qed_goalw "refl_less_sprod" thy [less_sprod_def]"less (p::'a ** 'b) p"
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]
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2033 diff changeset	19	"[\|less (p1::'a ** 'b) p2;less p2 p1\|] ==> p1=p2"
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]
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2033 diff changeset	29	"[\|less (p1::'a**'b) p2;less p2 p3\|] ==> less p1 p3"
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	nipkow
	Fri, 04 Apr 1997 16:33:28 +0200
changeset 2912	3fac3e8d5d3e
parent 2640	ee4dfce170a0
child 3323	194ae2e0c193
permissions	-rw-r--r--