isabelle: src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy@2f45f4abf0a9 (annotated)

51161 6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51139 diff changeset	1
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51139 diff changeset	2	(* Author: Ondrej Kuncar, TU Muenchen *)
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51139 diff changeset	3
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 63134 diff changeset	4	section \<open>Pervasive test of code generator\<close>
48624 9b71daba4ec7 add testing file for RBT_Set kuncar parents: diff changeset	5
51161 6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51139 diff changeset	6	theory Generate_Efficient_Datastructures
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51139 diff changeset	7	imports
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51139 diff changeset	8	Candidates
51599 1559e9266280 optionalized very specific code setup for multisets haftmann parents: 51161 diff changeset	9	"~~/src/HOL/Library/DAList_Multiset"
51161 6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51139 diff changeset	10	"~~/src/HOL/Library/RBT_Mapping"
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51139 diff changeset	11	"~~/src/HOL/Library/RBT_Set"
48624 9b71daba4ec7 add testing file for RBT_Set kuncar parents: diff changeset	12	begin
9b71daba4ec7 add testing file for RBT_Set kuncar parents: diff changeset	13
64786 340db65fd2c1 reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings haftmann parents: 63965 diff changeset	14	text \<open>
340db65fd2c1 reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings haftmann parents: 63965 diff changeset	15	The following code equations have to be deleted because they use
340db65fd2c1 reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings haftmann parents: 63965 diff changeset	16	lists to implement sets in the code generetor.
340db65fd2c1 reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings haftmann parents: 63965 diff changeset	17	\<close>
51116 0dac0158b8d4 implement code generation for finite, card, op = and op <= for sets always via finite_UNIV and card_UNIV, as fragile rewrites based on sorts are hard to find and debug Andreas Lochbihler parents: 50996 diff changeset	18
64786 340db65fd2c1 reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings haftmann parents: 63965 diff changeset	19	declare [[code drop:
340db65fd2c1 reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings haftmann parents: 63965 diff changeset	20	Sup_pred_inst.Sup_pred
340db65fd2c1 reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings haftmann parents: 63965 diff changeset	21	Inf_pred_inst.Inf_pred
340db65fd2c1 reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings haftmann parents: 63965 diff changeset	22	pred_of_set
340db65fd2c1 reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings haftmann parents: 63965 diff changeset	23	Wellfounded.acc
340db65fd2c1 reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings haftmann parents: 63965 diff changeset	24	Cardinality.card'
340db65fd2c1 reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings haftmann parents: 63965 diff changeset	25	Cardinality.finite'
340db65fd2c1 reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings haftmann parents: 63965 diff changeset	26	Cardinality.subset'
340db65fd2c1 reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings haftmann parents: 63965 diff changeset	27	Cardinality.eq_set
64850 fc9265882329 gcd/lcm on finite sets haftmann parents: 64786 diff changeset	28	Gcd_fin
fc9265882329 gcd/lcm on finite sets haftmann parents: 64786 diff changeset	29	Lcm_fin
64786 340db65fd2c1 reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings haftmann parents: 63965 diff changeset	30	"Gcd :: nat set \<Rightarrow> nat"
340db65fd2c1 reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings haftmann parents: 63965 diff changeset	31	"Lcm :: nat set \<Rightarrow> nat"
340db65fd2c1 reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings haftmann parents: 63965 diff changeset	32	"Gcd :: int set \<Rightarrow> int"
340db65fd2c1 reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings haftmann parents: 63965 diff changeset	33	"Lcm :: int set \<Rightarrow> int"
340db65fd2c1 reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings haftmann parents: 63965 diff changeset	34	"Gcd :: _ poly set \<Rightarrow> _"
340db65fd2c1 reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings haftmann parents: 63965 diff changeset	35	"Lcm :: _ poly set \<Rightarrow> _"
340db65fd2c1 reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings haftmann parents: 63965 diff changeset	36	Euclidean_Algorithm.Gcd
340db65fd2c1 reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings haftmann parents: 63965 diff changeset	37	Euclidean_Algorithm.Lcm
340db65fd2c1 reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings haftmann parents: 63965 diff changeset	38	permutations_of_set
340db65fd2c1 reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings haftmann parents: 63965 diff changeset	39	permutations_of_multiset
340db65fd2c1 reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings haftmann parents: 63965 diff changeset	40	]]
63965 d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations eberlm <eberlm@in.tum.de> parents: 63167 diff changeset	41
48624 9b71daba4ec7 add testing file for RBT_Set kuncar parents: diff changeset	42	(*
9b71daba4ec7 add testing file for RBT_Set kuncar parents: diff changeset	43	If the code generation ends with an exception with the following message:
9b71daba4ec7 add testing file for RBT_Set kuncar parents: diff changeset	44	'"List.set" is not a constructor, on left hand side of equation: ...',
9b71daba4ec7 add testing file for RBT_Set kuncar parents: diff changeset	45	the code equation in question has to be either deleted (like many others in this file)
9b71daba4ec7 add testing file for RBT_Set kuncar parents: diff changeset	46	or implemented for RBT trees.
9b71daba4ec7 add testing file for RBT_Set kuncar parents: diff changeset	47	*)
9b71daba4ec7 add testing file for RBT_Set kuncar parents: diff changeset	48
65919 b6d458915f1b obsolete special case haftmann parents: 64850 diff changeset	49	export_code _ checking SML OCaml? Haskell? Scala
48624 9b71daba4ec7 add testing file for RBT_Set kuncar parents: diff changeset	50
9b71daba4ec7 add testing file for RBT_Set kuncar parents: diff changeset	51	end

author	haftmann
	Mon, 05 Jun 2017 15:59:45 +0200
changeset 66014	2f45f4abf0a9
parent 65919	b6d458915f1b
child 66016	39d9a59d8d94
permissions	-rw-r--r--