isabelle: src/HOLCF/Lift1.ML@0eb9ee70c8f8 (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$
3033 50e14d6d894f only in comments mueller parents: 2640 diff changeset	3	Author: Olaf Mueller
2357 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
5068 fb28eaa07e01 isatool fixgoal; wenzelm parents: 3323 diff changeset	16	Goalw [less_lift_def] "(x::'a lift) << x";
2356 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
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2357 diff changeset	20	val prems = goalw thy [less_lift_def]
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 3033 diff changeset	21	"[\|(x1::'a lift) << x2; x2 << x1\|] ==> x1 = x2";
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2357 diff changeset	22	by (cut_facts_tac prems 1);
2356 125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	23	by (fast_tac HOL_cs 1);
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	24	qed"antisym_less_lift";
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	25
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2357 diff changeset	26	val prems = goalw Lift1.thy [less_lift_def]
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 3033 diff changeset	27	"[\|(x1::'a lift) << x2; x2 << x3\|] ==> x1 << x3";
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2357 diff changeset	28	by (cut_facts_tac prems 1);
2356 125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	29	by (fast_tac HOL_cs 1);
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	30	qed"trans_less_lift";

author	wenzelm
	Wed, 08 Mar 2000 17:48:31 +0100
changeset 8364	0eb9ee70c8f8
parent 5068	fb28eaa07e01
child 9248	e1dee89de037
permissions	-rw-r--r--