isabelle: src/HOL/Codegenerator_Test/Candidates.thy@cd945dc13bec (annotated)

31378 d1cbf6393964 tuned code generator test theories haftmann parents: 30446 diff changeset	1
d1cbf6393964 tuned code generator test theories haftmann parents: 30446 diff changeset	2	(* Author: Florian Haftmann, TU Muenchen *)
21917 12b8fde1f9c0 added haftmann parents: diff changeset	3
58889 5b7a9633cfa8 modernized header uniformly as section; wenzelm parents: 58740 diff changeset	4	section {* A huge collection of equations to generate code from *}
21917 12b8fde1f9c0 added haftmann parents: diff changeset	5
37695 71e84a203c19 introduced distinct session HOL-Codegenerator_Test haftmann parents: 37407 diff changeset	6	theory Candidates
21917 12b8fde1f9c0 added haftmann parents: diff changeset	7	imports
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27103 diff changeset	8	Complex_Main
51160 599ff65b85e2 systematic conversions between nat and nibble/char; haftmann parents: 49077 diff changeset	9	"~~/src/HOL/Library/Library"
51161 6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51160 diff changeset	10	"~~/src/HOL/Library/Sublist_Order"
51173 3cbb4e95a565 Sieve of Eratosthenes haftmann parents: 51161 diff changeset	11	"~~/src/HOL/Number_Theory/Eratosthenes"
35303 816e48d60b13 added Dlist haftmann parents: 33500 diff changeset	12	"~~/src/HOL/ex/Records"
21917 12b8fde1f9c0 added haftmann parents: diff changeset	13	begin
12b8fde1f9c0 added haftmann parents: diff changeset	14
59484 a130ae7a9398 slightly more standard code setup for String.literal, with explicit special case in predicate compiler haftmann parents: 58889 diff changeset	15	setup \<open>
a130ae7a9398 slightly more standard code setup for String.literal, with explicit special case in predicate compiler haftmann parents: 58889 diff changeset	16	let
a130ae7a9398 slightly more standard code setup for String.literal, with explicit special case in predicate compiler haftmann parents: 58889 diff changeset	17	val tycos = (#log_types o Type.rep_tsig o Sign.tsig_of) @{theory};
a130ae7a9398 slightly more standard code setup for String.literal, with explicit special case in predicate compiler haftmann parents: 58889 diff changeset	18	val consts = map_filter (try (curry (Axclass.param_of_inst @{theory})
a130ae7a9398 slightly more standard code setup for String.literal, with explicit special case in predicate compiler haftmann parents: 58889 diff changeset	19	@{const_name "Quickcheck_Narrowing.partial_term_of"})) tycos;
a130ae7a9398 slightly more standard code setup for String.literal, with explicit special case in predicate compiler haftmann parents: 58889 diff changeset	20	in fold Code.del_eqns consts end
a130ae7a9398 slightly more standard code setup for String.literal, with explicit special case in predicate compiler haftmann parents: 58889 diff changeset	21	\<close> -- \<open>drop technical stuff from @{text Quickcheck_Narrowing} which is tailored towards Haskell\<close>
a130ae7a9398 slightly more standard code setup for String.literal, with explicit special case in predicate compiler haftmann parents: 58889 diff changeset	22
51161 6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51160 diff changeset	23	inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51160 diff changeset	24	where
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51160 diff changeset	25	empty: "sublist [] xs"
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51160 diff changeset	26	\| drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)"
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51160 diff changeset	27	\| take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)"
33500 22e5725be1f3 added predicate example haftmann parents: 33356 diff changeset	28
22e5725be1f3 added predicate example haftmann parents: 33356 diff changeset	29	code_pred sublist .
22e5725be1f3 added predicate example haftmann parents: 33356 diff changeset	30
51161 6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51160 diff changeset	31	code_reserved SML upto -- {* avoid popular infix *}
31378 d1cbf6393964 tuned code generator test theories haftmann parents: 30446 diff changeset	32
21917 12b8fde1f9c0 added haftmann parents: diff changeset	33	end

author	paulson <lp15@cam.ac.uk>
	Tue, 17 Mar 2015 15:11:25 +0000
changeset 59733	cd945dc13bec
parent 59731	7fccaeec22f0
child 59842	9fda99b3d5ee
permissions	-rw-r--r--