isabelle: src/HOLCF/Porder0.thy@6f463d16cbd0 (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
12030 46d57d0290a2 GPLed; wenzelm parents: 7661 diff changeset	4	License: GPL (GNU GENERAL PUBLIC LICENSE)
298 3a0485439396 structural induction for strict lists nipkow parents: diff changeset	5
12030 46d57d0290a2 GPLed; wenzelm parents: 7661 diff changeset	6	Definition of class porder (partial order).
298 3a0485439396 structural induction for strict lists nipkow parents: diff changeset	7	*)
3a0485439396 structural induction for strict lists nipkow parents: diff changeset	8
7661 8c3190b173aa depend on Main; wenzelm parents: 3323 diff changeset	9	Porder0 = Main +
298 3a0485439396 structural induction for strict lists nipkow parents: diff changeset	10
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 3310 diff changeset	11	(* 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	12	axclass sq_ord<term
298 3a0485439396 structural induction for strict lists nipkow parents: diff changeset	13
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 3310 diff changeset	14	(* characteristic constant << for po *)
2394 91d8abf108be adaptions for symbol font oheimb parents: 2291 diff changeset	15	consts
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 3310 diff changeset	16	"<<" :: "['a,'a::sq_ord] => bool" (infixl 55)
2394 91d8abf108be adaptions for symbol font oheimb parents: 2291 diff changeset	17
91d8abf108be adaptions for symbol font oheimb parents: 2291 diff changeset	18	syntax (symbols)
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 3310 diff changeset	19	"op <<" :: "['a,'a::sq_ord] => bool" (infixl "\\<sqsubseteq>" 55)
298 3a0485439396 structural induction for strict lists nipkow parents: diff changeset	20
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 3310 diff changeset	21	axclass po < sq_ord
194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 3310 diff changeset	22	(* class axioms: *)
194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 3310 diff changeset	23	refl_less "x << x"
194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 3310 diff changeset	24	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	25	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	26
298 3a0485439396 structural induction for strict lists nipkow parents: diff changeset	27	end
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: 442 diff changeset	28
ea0668a1c0ba added 8bit pragmas regensbu parents: 442 diff changeset	29

author	paulson
	Wed, 07 Nov 2001 12:29:07 +0100
changeset 12088	6f463d16cbd0
parent 12030	46d57d0290a2
child 12114	a8e860c86252
permissions	-rw-r--r--