isabelle: src/HOLCF/Porder0.thy@8e58b3045e29 (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
7661 8c3190b173aa depend on Main; wenzelm parents: 3323 diff changeset	10	Porder0 = Main +
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	berghofe
	Fri, 29 Sep 2000 18:02:24 +0200
changeset 10117	8e58b3045e29
parent 7661	8c3190b173aa
child 12030	46d57d0290a2
permissions	-rw-r--r--