isabelle: src/HOL/Import/Import_Setup.thy@cdbc8d92c349 (annotated)

47258 880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	1	(* Title: HOL/Import/Import_Setup.thy
880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	2	Author: Cezary Kaliszyk, University of Innsbruck
880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	3	Author: Alexander Krauss, QAware GmbH
880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	4	*)
880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	5
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 59669 diff changeset	6	section \<open>Importer machinery and required theorems\<close>
47258 880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	7
880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	8	theory Import_Setup
65552 f533820e7248 theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications; wenzelm parents: 63167 diff changeset	9	imports Main
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47258 diff changeset	10	keywords "import_type_map" "import_const_map" "import_file" :: thy_decl
47258 880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	11	begin
880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	12
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 65552 diff changeset	13	ML_file \<open>import_data.ML\<close>
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47258 diff changeset	14
47258 880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	15	lemma light_ex_imp_nonempty:
880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	16	"P t \<Longrightarrow> \<exists>x. x \<in> Collect P"
880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	17	by auto
880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	18
880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	19	lemma typedef_hol2hollight:
880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	20	assumes a: "type_definition Rep Abs (Collect P)"
880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	21	shows "Abs (Rep a) = a \<and> P r = (Rep (Abs r) = r)"
880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	22	by (metis type_definition.Rep_inverse type_definition.Abs_inverse
880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	23	type_definition.Rep a mem_Collect_eq)
880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	24
880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	25	lemma ext2:
880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	26	"(\<And>x. f x = g x) \<Longrightarrow> f = g"
880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	27	by auto
880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	28
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 65552 diff changeset	29	ML_file \<open>import_rule.ML\<close>
47258 880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	30
880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	31	end
880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	32

author	wenzelm
	Thu, 02 May 2019 14:43:19 +0200
changeset 70231	cdbc8d92c349
parent 69605	a96320074298
child 81828	b93e6b458433
permissions	-rw-r--r--