isabelle: src/HOL/Induct/MultisetOrder.thy@50be659d4222 (annotated)

9660 80d14ea0e200 turned into new-style theory; wenzelm parents: 9017 diff changeset	1	(* Title: HOL/Induct/MultisetOrder.thy
8916 433843c1b454 multisets are partially ordered paulson parents: diff changeset	2	ID: $Id$
433843c1b454 multisets are partially ordered paulson parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
433843c1b454 multisets are partially ordered paulson parents: diff changeset	4	Copyright 2000 University of Cambridge
433843c1b454 multisets are partially ordered paulson parents: diff changeset	5
9660 80d14ea0e200 turned into new-style theory; wenzelm parents: 9017 diff changeset	6	Multisets are partially ordered.
8916 433843c1b454 multisets are partially ordered paulson parents: diff changeset	7	*)
433843c1b454 multisets are partially ordered paulson parents: diff changeset	8
9660 80d14ea0e200 turned into new-style theory; wenzelm parents: 9017 diff changeset	9	theory MultisetOrder = Multiset:
8916 433843c1b454 multisets are partially ordered paulson parents: diff changeset	10
433843c1b454 multisets are partially ordered paulson parents: diff changeset	11	instance multiset :: (order) order
9660 80d14ea0e200 turned into new-style theory; wenzelm parents: 9017 diff changeset	12	apply intro_classes
80d14ea0e200 turned into new-style theory; wenzelm parents: 9017 diff changeset	13	apply (rule mult_le_refl)
80d14ea0e200 turned into new-style theory; wenzelm parents: 9017 diff changeset	14	apply (erule mult_le_trans)
80d14ea0e200 turned into new-style theory; wenzelm parents: 9017 diff changeset	15	apply assumption
80d14ea0e200 turned into new-style theory; wenzelm parents: 9017 diff changeset	16	apply (erule mult_le_antisym)
80d14ea0e200 turned into new-style theory; wenzelm parents: 9017 diff changeset	17	apply assumption
80d14ea0e200 turned into new-style theory; wenzelm parents: 9017 diff changeset	18	apply (rule mult_less_le)
80d14ea0e200 turned into new-style theory; wenzelm parents: 9017 diff changeset	19	done
8916 433843c1b454 multisets are partially ordered paulson parents: diff changeset	20
9660 80d14ea0e200 turned into new-style theory; wenzelm parents: 9017 diff changeset	21	instance multiset :: ("term") plus_ac0
80d14ea0e200 turned into new-style theory; wenzelm parents: 9017 diff changeset	22	apply intro_classes
80d14ea0e200 turned into new-style theory; wenzelm parents: 9017 diff changeset	23	apply (rule union_commute)
80d14ea0e200 turned into new-style theory; wenzelm parents: 9017 diff changeset	24	apply (rule union_assoc)
80d14ea0e200 turned into new-style theory; wenzelm parents: 9017 diff changeset	25	apply simp
80d14ea0e200 turned into new-style theory; wenzelm parents: 9017 diff changeset	26	done
80d14ea0e200 turned into new-style theory; wenzelm parents: 9017 diff changeset	27
8916 433843c1b454 multisets are partially ordered paulson parents: diff changeset	28	end

author	wenzelm
	Fri, 06 Oct 2000 17:35:58 +0200
changeset 10168	50be659d4222
parent 9660	80d14ea0e200
permissions	-rw-r--r--