Theory Import_Setup

(*  Title:      HOL/Import/Import_Setup.thy
    Author:     Cezary Kaliszyk, University of Innsbruck
    Author:     Alexander Krauss, QAware GmbH
*)

section ‹Importer machinery and required theorems›

theory Import_Setup
imports Main
keywords "import_type_map" "import_const_map" "import_file" :: thy_decl
begin

ML_file ‹import_data.ML›

lemma light_ex_imp_nonempty:
  "P t ⟹ ∃x. x ∈ Collect P"
  by auto

lemma typedef_hol2hollight:
  assumes a: "type_definition Rep Abs (Collect P)"
  shows "Abs (Rep a) = a ∧ P r = (Rep (Abs r) = r)"
  by (metis type_definition.Rep_inverse type_definition.Abs_inverse
      type_definition.Rep a mem_Collect_eq)

lemma ext2:
  "(⋀x. f x = g x) ⟹ f = g"
  by auto

ML_file ‹import_rule.ML›

end