isabelle: src/HOLCF/Lift1.ML@5d45c2094ff6 (annotated)

2357 dd2e5e655fd2 Headers added sandnerr parents: 2356 diff changeset	1	(* Title: HOLCF/Lift1.ML
dd2e5e655fd2 Headers added sandnerr parents: 2356 diff changeset	2	ID: $Id$
dd2e5e655fd2 Headers added sandnerr parents: 2356 diff changeset	3	Author: Olaf Mueller, Robert Sandner
dd2e5e655fd2 Headers added sandnerr parents: 2356 diff changeset	4	Copyright 1996 Technische Universitaet Muenchen
dd2e5e655fd2 Headers added sandnerr parents: 2356 diff changeset	5
dd2e5e655fd2 Headers added sandnerr parents: 2356 diff changeset	6	Theorems for Lift1.thy
dd2e5e655fd2 Headers added sandnerr parents: 2356 diff changeset	7	*)
dd2e5e655fd2 Headers added sandnerr parents: 2356 diff changeset	8
2356 125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	9
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	10	open Lift1;
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	11
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	12	(* ------------------------------------------------------------------------ *)
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	13	(* less_lift is a partial order on type 'a -> 'b *)
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	14	(* ------------------------------------------------------------------------ *)
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	15
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	16	goalw Lift1.thy [less_lift_def] "less_lift x x";
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	17	by (fast_tac HOL_cs 1);
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	18	qed"refl_less_lift";
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	19
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	20	goalw Lift1.thy [less_lift_def]
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	21	"less_lift x1 x2 & less_lift x2 x1 --> x1 = x2";
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	22	by (fast_tac HOL_cs 1);
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	23	qed"antisym_less_lift";
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	24
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	25	goalw Lift1.thy [less_lift_def]
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	26	"less_lift x1 x2 & less_lift x2 x3 --> less_lift x1 x3";
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	27	by (fast_tac HOL_cs 1);
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	28	qed"trans_less_lift";

author	wenzelm
	Wed, 08 Jan 1997 15:12:44 +0100
changeset 2494	5d45c2094ff6
parent 2357	dd2e5e655fd2
child 2640	ee4dfce170a0
permissions	-rw-r--r--