src/HOL/Import/Import_Setup.thy
changeset 47258 880e587eee9f
child 48891 c0eafbd55de3
equal deleted inserted replaced
47244:a7f85074c169 47258:880e587eee9f
       
     1 (*  Title:      HOL/Import/Import_Setup.thy
       
     2     Author:     Cezary Kaliszyk, University of Innsbruck
       
     3     Author:     Alexander Krauss, QAware GmbH
       
     4 *)
       
     5 
       
     6 header {* Importer machinery and required theorems *}
       
     7 
       
     8 theory Import_Setup
       
     9 imports "~~/src/HOL/Parity" "~~/src/HOL/Fact"
       
    10 keywords
       
    11     "import_type_map" :: thy_decl and "import_const_map" :: thy_decl and
       
    12     "import_file" :: thy_decl
       
    13 uses "import_data.ML" ("import_rule.ML")
       
    14 begin
       
    15 
       
    16 lemma light_ex_imp_nonempty:
       
    17   "P t \<Longrightarrow> \<exists>x. x \<in> Collect P"
       
    18   by auto
       
    19 
       
    20 lemma typedef_hol2hollight:
       
    21   assumes a: "type_definition Rep Abs (Collect P)"
       
    22   shows "Abs (Rep a) = a \<and> P r = (Rep (Abs r) = r)"
       
    23   by (metis type_definition.Rep_inverse type_definition.Abs_inverse
       
    24       type_definition.Rep a mem_Collect_eq)
       
    25 
       
    26 lemma ext2:
       
    27   "(\<And>x. f x = g x) \<Longrightarrow> f = g"
       
    28   by auto
       
    29 
       
    30 use "import_rule.ML"
       
    31 
       
    32 end
       
    33