isabelle: src/HOL/Import/Generate-HOL/GenHOL4Real.thy@89a17197cb98 (annotated)

14620 1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import. skalberg parents: 14516 diff changeset	1	(* Title: HOL/Import/Generate-HOL/GenHOL4Real.thy
1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import. skalberg parents: 14516 diff changeset	2	Author: Sebastian Skalberg (TU Muenchen)
1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import. skalberg parents: 14516 diff changeset	3	*)
1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import. skalberg parents: 14516 diff changeset	4
16417 9bc16273c2d4 migrated theory headers to new format haftmann parents: 15647 diff changeset	5	theory GenHOL4Real imports GenHOL4Base begin
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	6
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	7	import_segment "hol4";
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	8
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	9	setup_dump "../HOL" "HOL4Real";
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	10
17566 484ff733f29c new header syntax; wenzelm parents: 16417 diff changeset	11	append_dump "theory HOL4Real imports HOL4Base begin";
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	12
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	13	import_theory realax;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	14
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	15	type_maps
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	16	real > RealDef.real;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	17
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	18	const_maps
44740 a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44064 diff changeset	19	real_0 > Groups.zero_class.zero :: real
a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44064 diff changeset	20	real_1 > Groups.one_class.one :: real
a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44064 diff changeset	21	real_neg > Groups.uminus_class.uminus :: "real \<Rightarrow> real"
a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44064 diff changeset	22	inv > Fields.inverse_class.inverse :: "real \<Rightarrow> real"
a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44064 diff changeset	23	real_add > Groups.plus_class.plus :: "real \<Rightarrow> real \<Rightarrow> real"
a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44064 diff changeset	24	real_sub > Groups.minus_class.minus :: "real \<Rightarrow> real \<Rightarrow> real"
a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44064 diff changeset	25	real_mul > Groups.times_class.times :: "real \<Rightarrow> real \<Rightarrow> real"
a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44064 diff changeset	26	real_div > Fields.inverse_class.divide :: "real \<Rightarrow> real \<Rightarrow> real"
a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44064 diff changeset	27	real_lt > Orderings.ord_class.less :: "real \<Rightarrow> real \<Rightarrow> bool"
a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44064 diff changeset	28	mk_real > HOL.undefined (* Otherwise proof_import_concl fails *)
a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44064 diff changeset	29	dest_real > HOL.undefined
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	30
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	31	ignore_thms
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	32	real_TY_DEF
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	33	real_tybij
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	34	real_0
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	35	real_1
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	36	real_neg
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	37	real_inv
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	38	real_add
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	39	real_mul
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	40	real_lt
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	41	real_of_hreal
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	42	hreal_of_real
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	43	REAL_ISO_EQ
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	44	REAL_POS
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	45	SUP_ALLPOS_LEMMA1
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	46	SUP_ALLPOS_LEMMA2
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	47	SUP_ALLPOS_LEMMA3
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	48	SUP_ALLPOS_LEMMA4;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	49
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	50	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	51
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	52	import_theory real;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	53
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	54	const_maps
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	55	real_gt > HOL4Compat.real_gt
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	56	real_ge > HOL4Compat.real_ge
44740 a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44064 diff changeset	57	real_lte > Orderings.ord_class.less_eq :: "real \<Rightarrow> real \<Rightarrow> bool"
a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44064 diff changeset	58	real_sub > Groups.minus_class.minus :: "real \<Rightarrow> real \<Rightarrow> real"
a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44064 diff changeset	59	"/" > Fields.inverse_class.divide :: "real \<Rightarrow> real \<Rightarrow> real"
a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44064 diff changeset	60	pow > Power.power_class.power :: "real \<Rightarrow> nat \<Rightarrow> real"
a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44064 diff changeset	61	abs > Groups.abs_class.abs :: "real => real"
15647 b1f486a9c56b Updated import configuration. skalberg parents: 14620 diff changeset	62	real_of_num > RealDef.real :: "nat => real";
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	63
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	64	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	65
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	66	import_theory topology;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	67	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	68
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	69	import_theory nets;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	70	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	71
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	72	import_theory seq;
17694 b7870c2bd7df mapped "-->" to "hol4-->" obua parents: 17566 diff changeset	73	const_renames
b7870c2bd7df mapped "-->" to "hol4-->" obua parents: 17566 diff changeset	74	"-->" > "hol4-->";
b7870c2bd7df mapped "-->" to "hol4-->" obua parents: 17566 diff changeset	75
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	76	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	77
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	78	import_theory lim;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	79	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	80
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	81	import_theory powser;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	82	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	83
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	84	import_theory transc;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	85	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	86
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	87	import_theory poly;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	88	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	89
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	90	append_dump "end";
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	91
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	92	flush_dump;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	93
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	94	import_segment "";
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	95
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	96	end

author	wenzelm
	Thu, 27 Oct 2011 20:26:38 +0200
changeset 45279	89a17197cb98
parent 44740	a2940bc24bad
child 46780	ab4f3f765f91
permissions	-rw-r--r--