isabelle: src/Tools/Code_Generator.thy@b6a77cffc231 (annotated)

30929 d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy haftmann parents: diff changeset	1	(* Title: Tools/Code_Generator.thy
d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy haftmann parents: diff changeset	2	Author: Florian Haftmann, TU Muenchen
d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy haftmann parents: diff changeset	3	*)
d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy haftmann parents: diff changeset	4
d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy haftmann parents: diff changeset	5	header {* Loading the code generator modules *}
d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy haftmann parents: diff changeset	6
d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy haftmann parents: diff changeset	7	theory Code_Generator
33820 082d9bc6992d load ML directly into theory Code_Generator (quickcheck also requires this); wenzelm parents: 33561 diff changeset	8	imports Pure
30929 d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy haftmann parents: diff changeset	9	uses
37818 dd65033fed78 load cache_io before code generator; moved adhoc-overloading to generic tools haftmann parents: 37442 diff changeset	10	"~~/src/Tools/cache_io.ML"
39323 ce5c6a8b0359 start renaming "Auto_Counterexample" to "Auto_Tools"; blanchet parents: 38970 diff changeset	11	"~~/src/Tools/auto_tools.ML"
33889 4328de748fb2 some rearangement of load order to keep preferences adjacent -- slightly fragile; wenzelm parents: 33820 diff changeset	12	"~~/src/Tools/auto_solve.ML"
4328de748fb2 some rearangement of load order to keep preferences adjacent -- slightly fragile; wenzelm parents: 33820 diff changeset	13	"~~/src/Tools/quickcheck.ML"
30929 d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy haftmann parents: diff changeset	14	"~~/src/Tools/value.ML"
31775 2b04504fcb69 uniformly capitialized names for subdirectories haftmann parents: 31125 diff changeset	15	"~~/src/Tools/Code/code_preproc.ML"
2b04504fcb69 uniformly capitialized names for subdirectories haftmann parents: 31125 diff changeset	16	"~~/src/Tools/Code/code_thingol.ML"
37442 037ee7b712b2 added code_simp infrastructure haftmann parents: 34968 diff changeset	17	"~~/src/Tools/Code/code_simp.ML"
31775 2b04504fcb69 uniformly capitialized names for subdirectories haftmann parents: 31125 diff changeset	18	"~~/src/Tools/Code/code_printer.ML"
2b04504fcb69 uniformly capitialized names for subdirectories haftmann parents: 31125 diff changeset	19	"~~/src/Tools/Code/code_target.ML"
38970 53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML haftmann parents: 37818 diff changeset	20	"~~/src/Tools/Code/code_namespace.ML"
31775 2b04504fcb69 uniformly capitialized names for subdirectories haftmann parents: 31125 diff changeset	21	"~~/src/Tools/Code/code_ml.ML"
2b04504fcb69 uniformly capitialized names for subdirectories haftmann parents: 31125 diff changeset	22	"~~/src/Tools/Code/code_haskell.ML"
34294 19c1fd52d6c9 a primitive scala serializer haftmann parents: 34028 diff changeset	23	"~~/src/Tools/Code/code_scala.ML"
39421 b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	24	("~~/src/Tools/Code/code_runtime.ML")
30929 d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy haftmann parents: diff changeset	25	"~~/src/Tools/nbe.ML"
d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy haftmann parents: diff changeset	26	begin
d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy haftmann parents: diff changeset	27
39421 b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	28	code_datatype "TYPE('a\<Colon>{})"
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	29
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	30	definition holds :: "prop" where
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	31	"holds \<equiv> ((\<lambda>x::prop. x) \<equiv> (\<lambda>x. x))"
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	32
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	33	lemma holds: "PROP holds"
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	34	by (unfold holds_def) (rule reflexive)
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	35
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	36	code_datatype holds
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	37
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	38	lemma implies_code [code]:
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	39	"(PROP holds \<Longrightarrow> PROP P) \<equiv> PROP P"
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	40	"(PROP P \<Longrightarrow> PROP holds) \<equiv> PROP holds"
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	41	proof -
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	42	show "(PROP holds \<Longrightarrow> PROP P) \<equiv> PROP P"
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	43	proof
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	44	assume "PROP holds \<Longrightarrow> PROP P"
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	45	then show "PROP P" using holds .
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	46	next
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	47	assume "PROP P"
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	48	then show "PROP P" .
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	49	qed
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	50	next
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	51	show "(PROP P \<Longrightarrow> PROP holds) \<equiv> PROP holds"
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	52	by rule (rule holds)+
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	53	qed
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	54
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	55	use "~~/src/Tools/Code/code_runtime.ML"
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	56
30929 d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy haftmann parents: diff changeset	57	setup {*
39329 0a85f960ac50 make Auto Solve part of the "Auto Tools" blanchet parents: 39323 diff changeset	58	Auto_Solve.setup
0a85f960ac50 make Auto Solve part of the "Auto Tools" blanchet parents: 39323 diff changeset	59	#> Code_Preproc.setup
37442 037ee7b712b2 added code_simp infrastructure haftmann parents: 34968 diff changeset	60	#> Code_Simp.setup
31125 80218ee73167 transferred code generator preprocessor into separate module haftmann parents: 31036 diff changeset	61	#> Code_ML.setup
30929 d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy haftmann parents: diff changeset	62	#> Code_Haskell.setup
34294 19c1fd52d6c9 a primitive scala serializer haftmann parents: 34028 diff changeset	63	#> Code_Scala.setup
39401 887f4218a39a code_eval renamed to code_runtime haftmann parents: 39329 diff changeset	64	#> Code_Runtime.setup
30929 d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy haftmann parents: diff changeset	65	#> Nbe.setup
34968 ceeffca32eb0 tuned structure; moved non-related quickcheck.setup to Code_Generator.thy haftmann parents: 34294 diff changeset	66	#> Quickcheck.setup
30929 d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy haftmann parents: diff changeset	67	*}
d9343c0aac11 code generator bootstrap theory src/Tools/Code_Generator.thy haftmann parents: diff changeset	68
39421 b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	69	hide_const (open) holds
b6a77cffc231 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy haftmann parents: 39401 diff changeset	70
33561 ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck; blanchet parents: 31775 diff changeset	71	end

author	haftmann
	Wed, 15 Sep 2010 16:47:31 +0200
changeset 39421	b6a77cffc231
parent 39401	887f4218a39a
child 39423	9969401e1fb8
permissions	-rw-r--r--