isabelle: src/HOL/Library/multiset_simprocs.ML@d0053e582dd9 (annotated)

63793 e68a0b651eb5 add_mset constructor in multisets fleury <Mathias.Fleury@mpi-inf.mpg.de> parents: diff changeset	1	(* Author: Mathias Fleury, MPII
e68a0b651eb5 add_mset constructor in multisets fleury <Mathias.Fleury@mpi-inf.mpg.de> parents: diff changeset	2
e68a0b651eb5 add_mset constructor in multisets fleury <Mathias.Fleury@mpi-inf.mpg.de> parents: diff changeset	3
e68a0b651eb5 add_mset constructor in multisets fleury <Mathias.Fleury@mpi-inf.mpg.de> parents: diff changeset	4	Simprocs for multisets, based on Larry Paulson's simprocs for
e68a0b651eb5 add_mset constructor in multisets fleury <Mathias.Fleury@mpi-inf.mpg.de> parents: diff changeset	5	natural numbers and numerals.
e68a0b651eb5 add_mset constructor in multisets fleury <Mathias.Fleury@mpi-inf.mpg.de> parents: diff changeset	6	*)
e68a0b651eb5 add_mset constructor in multisets fleury <Mathias.Fleury@mpi-inf.mpg.de> parents: diff changeset	7
e68a0b651eb5 add_mset constructor in multisets fleury <Mathias.Fleury@mpi-inf.mpg.de> parents: diff changeset	8	signature MULTISET_SIMPROCS =
e68a0b651eb5 add_mset constructor in multisets fleury <Mathias.Fleury@mpi-inf.mpg.de> parents: diff changeset	9	sig
e68a0b651eb5 add_mset constructor in multisets fleury <Mathias.Fleury@mpi-inf.mpg.de> parents: diff changeset	10	val subset_cancel_msets: Proof.context -> cterm -> thm option
e68a0b651eb5 add_mset constructor in multisets fleury <Mathias.Fleury@mpi-inf.mpg.de> parents: diff changeset	11	val subseteq_cancel_msets: Proof.context -> cterm -> thm option
e68a0b651eb5 add_mset constructor in multisets fleury <Mathias.Fleury@mpi-inf.mpg.de> parents: diff changeset	12	end;
e68a0b651eb5 add_mset constructor in multisets fleury <Mathias.Fleury@mpi-inf.mpg.de> parents: diff changeset	13
e68a0b651eb5 add_mset constructor in multisets fleury <Mathias.Fleury@mpi-inf.mpg.de> parents: diff changeset	14	structure Multiset_Simprocs : MULTISET_SIMPROCS =
e68a0b651eb5 add_mset constructor in multisets fleury <Mathias.Fleury@mpi-inf.mpg.de> parents: diff changeset	15	struct
e68a0b651eb5 add_mset constructor in multisets fleury <Mathias.Fleury@mpi-inf.mpg.de> parents: diff changeset	16
65029 00731700e54f cancellation simprocs generalising the multiset simprocs fleury <Mathias.Fleury@mpi-inf.mpg.de> parents: 63793 diff changeset	17	structure Subset_Cancel_Multiset = Cancel_Fun
00731700e54f cancellation simprocs generalising the multiset simprocs fleury <Mathias.Fleury@mpi-inf.mpg.de> parents: 63793 diff changeset	18	(open Cancel_Data
69593 3dda49e08b9d isabelle update -u control_cartouches; wenzelm parents: 65029 diff changeset	19	val mk_bal = HOLogic.mk_binrel \<^const_name>\<open>subset_mset\<close>
3dda49e08b9d isabelle update -u control_cartouches; wenzelm parents: 65029 diff changeset	20	val dest_bal = HOLogic.dest_bin \<^const_name>\<open>subset_mset\<close> dummyT
65029 00731700e54f cancellation simprocs generalising the multiset simprocs fleury <Mathias.Fleury@mpi-inf.mpg.de> parents: 63793 diff changeset	21	val bal_add1 = @{thm mset_subset_add_iff1[unfolded repeat_mset_iterate_add]} RS trans
00731700e54f cancellation simprocs generalising the multiset simprocs fleury <Mathias.Fleury@mpi-inf.mpg.de> parents: 63793 diff changeset	22	val bal_add2 = @{thm mset_subset_add_iff2[unfolded repeat_mset_iterate_add]} RS trans
63793 e68a0b651eb5 add_mset constructor in multisets fleury <Mathias.Fleury@mpi-inf.mpg.de> parents: diff changeset	23	);
e68a0b651eb5 add_mset constructor in multisets fleury <Mathias.Fleury@mpi-inf.mpg.de> parents: diff changeset	24
65029 00731700e54f cancellation simprocs generalising the multiset simprocs fleury <Mathias.Fleury@mpi-inf.mpg.de> parents: 63793 diff changeset	25	structure Subseteq_Cancel_Multiset = Cancel_Fun
00731700e54f cancellation simprocs generalising the multiset simprocs fleury <Mathias.Fleury@mpi-inf.mpg.de> parents: 63793 diff changeset	26	(open Cancel_Data
69593 3dda49e08b9d isabelle update -u control_cartouches; wenzelm parents: 65029 diff changeset	27	val mk_bal = HOLogic.mk_binrel \<^const_name>\<open>subseteq_mset\<close>
3dda49e08b9d isabelle update -u control_cartouches; wenzelm parents: 65029 diff changeset	28	val dest_bal = HOLogic.dest_bin \<^const_name>\<open>subseteq_mset\<close> dummyT
65029 00731700e54f cancellation simprocs generalising the multiset simprocs fleury <Mathias.Fleury@mpi-inf.mpg.de> parents: 63793 diff changeset	29	val bal_add1 = @{thm mset_subseteq_add_iff1[unfolded repeat_mset_iterate_add]} RS trans
00731700e54f cancellation simprocs generalising the multiset simprocs fleury <Mathias.Fleury@mpi-inf.mpg.de> parents: 63793 diff changeset	30	val bal_add2 = @{thm mset_subseteq_add_iff2[unfolded repeat_mset_iterate_add]} RS trans
63793 e68a0b651eb5 add_mset constructor in multisets fleury <Mathias.Fleury@mpi-inf.mpg.de> parents: diff changeset	31	);
e68a0b651eb5 add_mset constructor in multisets fleury <Mathias.Fleury@mpi-inf.mpg.de> parents: diff changeset	32
65029 00731700e54f cancellation simprocs generalising the multiset simprocs fleury <Mathias.Fleury@mpi-inf.mpg.de> parents: 63793 diff changeset	33	val subset_cancel_msets = Subset_Cancel_Multiset.proc;
00731700e54f cancellation simprocs generalising the multiset simprocs fleury <Mathias.Fleury@mpi-inf.mpg.de> parents: 63793 diff changeset	34	val subseteq_cancel_msets = Subseteq_Cancel_Multiset.proc;
63793 e68a0b651eb5 add_mset constructor in multisets fleury <Mathias.Fleury@mpi-inf.mpg.de> parents: diff changeset	35
e68a0b651eb5 add_mset constructor in multisets fleury <Mathias.Fleury@mpi-inf.mpg.de> parents: diff changeset	36	end

author	wenzelm
	Sun, 27 Aug 2023 17:00:03 +0200
changeset 78588	d0053e582dd9
parent 69593	3dda49e08b9d
child 78800	0b3700d31758
permissions	-rw-r--r--