isabelle: src/HOLCF/Porder0.thy@e567f3425267 (annotated)

2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	1	(* Title: HOLCF/Porder0.thy
298 3a0485439396 structural induction for strict lists nipkow parents: diff changeset	2	ID: $Id$
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	3	Author: Franz Regensburger
298 3a0485439396 structural induction for strict lists nipkow parents: diff changeset	4	Copyright 1993 Technische Universitaet Muenchen
3a0485439396 structural induction for strict lists nipkow parents: diff changeset	5
3a0485439396 structural induction for strict lists nipkow parents: diff changeset	6	Definition of class porder (partial order)
3a0485439396 structural induction for strict lists nipkow parents: diff changeset	7
3a0485439396 structural induction for strict lists nipkow parents: diff changeset	8	*)
3a0485439396 structural induction for strict lists nipkow parents: diff changeset	9
3310 0ceaad3c3f52 Base theory is now Arith, not Nat. (because all datatypes now require Arith). nipkow parents: 2850 diff changeset	10	Porder0 = Arith +
298 3a0485439396 structural induction for strict lists nipkow parents: diff changeset	11
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 3310 diff changeset	12	(* introduce a (syntactic) class for the constant << *)
194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 3310 diff changeset	13	axclass sq_ord<term
298 3a0485439396 structural induction for strict lists nipkow parents: diff changeset	14
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 3310 diff changeset	15	(* characteristic constant << for po *)
2394 91d8abf108be adaptions for symbol font oheimb parents: 2291 diff changeset	16	consts
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 3310 diff changeset	17	"<<" :: "['a,'a::sq_ord] => bool" (infixl 55)
2394 91d8abf108be adaptions for symbol font oheimb parents: 2291 diff changeset	18
91d8abf108be adaptions for symbol font oheimb parents: 2291 diff changeset	19	syntax (symbols)
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 3310 diff changeset	20	"op <<" :: "['a,'a::sq_ord] => bool" (infixl "\\<sqsubseteq>" 55)
298 3a0485439396 structural induction for strict lists nipkow parents: diff changeset	21
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 3310 diff changeset	22	axclass po < sq_ord
194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 3310 diff changeset	23	(* class axioms: *)
194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 3310 diff changeset	24	refl_less "x << x"
194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 3310 diff changeset	25	antisym_less "[\|x << y; y << x \|] ==> x = y"
194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 3310 diff changeset	26	trans_less "[\|x << y; y << z \|] ==> x << z"
194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 3310 diff changeset	27
298 3a0485439396 structural induction for strict lists nipkow parents: diff changeset	28	end
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: 442 diff changeset	29
ea0668a1c0ba added 8bit pragmas regensbu parents: 442 diff changeset	30

author	wenzelm
	Mon, 01 Dec 1997 18:22:38 +0100
changeset 4334	e567f3425267
parent 3323	194ae2e0c193
child 7661	8c3190b173aa
permissions	-rw-r--r--