isabelle: src/HOL/Ord.ML@e60b8698ab15 (annotated)

1465 5d7a7e439cec expanded tabs clasohm parents: 923 diff changeset	1	(* Title: HOL/Ord.ML
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	2	ID: $Id$
1465 5d7a7e439cec expanded tabs clasohm parents: 923 diff changeset	3	Author: Tobias Nipkow, Cambridge University Computer Laboratory
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	4	Copyright 1993 University of Cambridge
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	5
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	6	The type class for ordered types
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	7	*)
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	8
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: 1465 diff changeset	9	( mono )
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	10
5316 7a8975451a89 even more tidying of Goal commands paulson parents: 5143 diff changeset	11	val [prem] = Goalw [mono_def]
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	12	"[\| !!A B. A <= B ==> f(A) <= f(B) \|] ==> mono(f)";
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	13	by (REPEAT (ares_tac [allI, impI, prem] 1));
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	14	qed "monoI";
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	15
5316 7a8975451a89 even more tidying of Goal commands paulson parents: 5143 diff changeset	16	Goalw [mono_def] "[\| mono(f); A <= B \|] ==> f(A) <= f(B)";
7a8975451a89 even more tidying of Goal commands paulson parents: 5143 diff changeset	17	by (Fast_tac 1);
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	18	qed "monoD";
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	19
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: 1465 diff changeset	20
450c9b682a92 New class "order" and accompanying changes. nipkow parents: 1465 diff changeset	21	section "Orders";
450c9b682a92 New class "order" and accompanying changes. nipkow parents: 1465 diff changeset	22
450c9b682a92 New class "order" and accompanying changes. nipkow parents: 1465 diff changeset	23	AddIffs [order_refl];
450c9b682a92 New class "order" and accompanying changes. nipkow parents: 1465 diff changeset	24
4600 e3e7e901ce6c New theorem order_eq_refl paulson parents: 4089 diff changeset	25	(This form is useful with the classical reasoner)
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4686 diff changeset	26	Goal "!!x::'a::order. x = y ==> x <= y";
4600 e3e7e901ce6c New theorem order_eq_refl paulson parents: 4089 diff changeset	27	by (etac ssubst 1);
e3e7e901ce6c New theorem order_eq_refl paulson parents: 4089 diff changeset	28	by (rtac order_refl 1);
e3e7e901ce6c New theorem order_eq_refl paulson parents: 4089 diff changeset	29	qed "order_eq_refl";
e3e7e901ce6c New theorem order_eq_refl paulson parents: 4089 diff changeset	30
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4686 diff changeset	31	Goal "~ x < (x::'a::order)";
4089 96fba19bcbe2 isatool fixclasimp; wenzelm parents: 2935 diff changeset	32	by (simp_tac (simpset() addsimps [order_less_le]) 1);
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: 1465 diff changeset	33	qed "order_less_irrefl";
450c9b682a92 New class "order" and accompanying changes. nipkow parents: 1465 diff changeset	34	AddIffs [order_less_irrefl];
450c9b682a92 New class "order" and accompanying changes. nipkow parents: 1465 diff changeset	35
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4686 diff changeset	36	Goal "(x::'a::order) <= y = (x < y \| x = y)";
4089 96fba19bcbe2 isatool fixclasimp; wenzelm parents: 2935 diff changeset	37	by (simp_tac (simpset() addsimps [order_less_le]) 1);
2935 998cb95fdd43 Yet more fast_tac->blast_tac, and other tidying paulson parents: 2608 diff changeset	38	by (Blast_tac 1);
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: 1465 diff changeset	39	qed "order_le_less";
450c9b682a92 New class "order" and accompanying changes. nipkow parents: 1465 diff changeset	40
450c9b682a92 New class "order" and accompanying changes. nipkow parents: 1465 diff changeset	41	( min )
450c9b682a92 New class "order" and accompanying changes. nipkow parents: 1465 diff changeset	42
5143 b94cd208f073 Removal of leading "\!\!..." from most Goal commands paulson parents: 5132 diff changeset	43	val prems = Goalw [min_def] "(!!x. least <= x) ==> min least x = least";
b94cd208f073 Removal of leading "\!\!..." from most Goal commands paulson parents: 5132 diff changeset	44	by (simp_tac (simpset() addsimps prems) 1);
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: 1465 diff changeset	45	qed "min_leastL";
450c9b682a92 New class "order" and accompanying changes. nipkow parents: 1465 diff changeset	46
5316 7a8975451a89 even more tidying of Goal commands paulson parents: 5143 diff changeset	47	val prems = Goalw [min_def]
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: 1465 diff changeset	48	"(!!x::'a::order. least <= x) ==> min x least = least";
2935 998cb95fdd43 Yet more fast_tac->blast_tac, and other tidying paulson parents: 2608 diff changeset	49	by (cut_facts_tac prems 1);
998cb95fdd43 Yet more fast_tac->blast_tac, and other tidying paulson parents: 2608 diff changeset	50	by (Asm_simp_tac 1);
4089 96fba19bcbe2 isatool fixclasimp; wenzelm parents: 2935 diff changeset	51	by (blast_tac (claset() addIs [order_antisym]) 1);
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: 1465 diff changeset	52	qed "min_leastR";
4640 ac6cf9f18653 Congruence rules use == in premises now. nipkow parents: 4600 diff changeset	53
ac6cf9f18653 Congruence rules use == in premises now. nipkow parents: 4600 diff changeset	54
ac6cf9f18653 Congruence rules use == in premises now. nipkow parents: 4600 diff changeset	55	section "Linear/Total Orders";
ac6cf9f18653 Congruence rules use == in premises now. nipkow parents: 4600 diff changeset	56
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4686 diff changeset	57	Goal "!!x::'a::linorder. x<y \| x=y \| y<x";
4640 ac6cf9f18653 Congruence rules use == in premises now. nipkow parents: 4600 diff changeset	58	by (simp_tac (simpset() addsimps [order_less_le]) 1);
5132 24f992a25adc isatool expandshort; wenzelm parents: 5069 diff changeset	59	by (cut_facts_tac [linorder_linear] 1);
4640 ac6cf9f18653 Congruence rules use == in premises now. nipkow parents: 4600 diff changeset	60	by (Blast_tac 1);
ac6cf9f18653 Congruence rules use == in premises now. nipkow parents: 4600 diff changeset	61	qed "linorder_less_linear";
ac6cf9f18653 Congruence rules use == in premises now. nipkow parents: 4600 diff changeset	62
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4686 diff changeset	63	Goalw [max_def] "!!z::'a::linorder. (z <= max x y) = (z <= x \| z <= y)";
4686 74a12e86b20b Removed `addsplits [expand_if]' nipkow parents: 4640 diff changeset	64	by (Simp_tac 1);
5132 24f992a25adc isatool expandshort; wenzelm parents: 5069 diff changeset	65	by (cut_facts_tac [linorder_linear] 1);
4640 ac6cf9f18653 Congruence rules use == in premises now. nipkow parents: 4600 diff changeset	66	by (blast_tac (claset() addIs [order_trans]) 1);
ac6cf9f18653 Congruence rules use == in premises now. nipkow parents: 4600 diff changeset	67	qed "le_max_iff_disj";
ac6cf9f18653 Congruence rules use == in premises now. nipkow parents: 4600 diff changeset	68
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4686 diff changeset	69	Goalw [max_def] "!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)";
4686 74a12e86b20b Removed `addsplits [expand_if]' nipkow parents: 4640 diff changeset	70	by (Simp_tac 1);
5132 24f992a25adc isatool expandshort; wenzelm parents: 5069 diff changeset	71	by (cut_facts_tac [linorder_linear] 1);
4640 ac6cf9f18653 Congruence rules use == in premises now. nipkow parents: 4600 diff changeset	72	by (blast_tac (claset() addIs [order_trans]) 1);
ac6cf9f18653 Congruence rules use == in premises now. nipkow parents: 4600 diff changeset	73	qed "max_le_iff_conj";
ac6cf9f18653 Congruence rules use == in premises now. nipkow parents: 4600 diff changeset	74
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4686 diff changeset	75	Goalw [min_def] "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)";
4686 74a12e86b20b Removed `addsplits [expand_if]' nipkow parents: 4640 diff changeset	76	by (Simp_tac 1);
5132 24f992a25adc isatool expandshort; wenzelm parents: 5069 diff changeset	77	by (cut_facts_tac [linorder_linear] 1);
4640 ac6cf9f18653 Congruence rules use == in premises now. nipkow parents: 4600 diff changeset	78	by (blast_tac (claset() addIs [order_trans]) 1);
ac6cf9f18653 Congruence rules use == in premises now. nipkow parents: 4600 diff changeset	79	qed "le_min_iff_conj";
ac6cf9f18653 Congruence rules use == in premises now. nipkow parents: 4600 diff changeset	80
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4686 diff changeset	81	Goalw [min_def] "!!z::'a::linorder. (min x y <= z) = (x <= z \| y <= z)";
4686 74a12e86b20b Removed `addsplits [expand_if]' nipkow parents: 4640 diff changeset	82	by (Simp_tac 1);
5132 24f992a25adc isatool expandshort; wenzelm parents: 5069 diff changeset	83	by (cut_facts_tac [linorder_linear] 1);
4640 ac6cf9f18653 Congruence rules use == in premises now. nipkow parents: 4600 diff changeset	84	by (blast_tac (claset() addIs [order_trans]) 1);
ac6cf9f18653 Congruence rules use == in premises now. nipkow parents: 4600 diff changeset	85	qed "min_le_iff_disj";
ac6cf9f18653 Congruence rules use == in premises now. nipkow parents: 4600 diff changeset	86
ac6cf9f18653 Congruence rules use == in premises now. nipkow parents: 4600 diff changeset	87

author	oheimb
	Wed, 09 Sep 1998 17:14:19 +0200
changeset 5442	e60b8698ab15
parent 5316	7a8975451a89
child 5449	d853d1ac85a3
permissions	-rw-r--r--