isabelle: src/HOLCF/Porder0.thy@5efbb548107d (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 << *)
12338 de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type"); wenzelm parents: 12114 diff changeset	12	axclass sq_ord < type
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
12114 a8e860c86252 eliminated old "symbols" syntax, use "xsymbols" instead; wenzelm parents: 12030 diff changeset	18	syntax (xsymbols)
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
	Thu, 04 Dec 2003 10:29:17 +0100
changeset 14272	5efbb548107d
parent 12338	de0f4a63baa5
child 14981	e73f8140af78
permissions	-rw-r--r--