# HG changeset patch
# User haftmann
# Date 1330815801 -3600
# Node ID b778cc5396013b261e7d1a87ff53683401e3cba2
# Parent  9696218b02fea24dfc3ea7b386548c4f8626ea6a
actually add "the" Importer theory

diff -r 9696218b02fe -r b778cc539601 src/HOL/Import/Importer.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/Importer.thy	Sun Mar 04 00:03:21 2012 +0100
@@ -0,0 +1,239 @@
+(*  Title:      HOL/Import/Importer.thy
+    Author:     Sebastian Skalberg, TU Muenchen
+*)
+
+theory Importer
+imports Main
+uses "shuffler.ML" ("import_rews.ML") ("proof_kernel.ML") ("replay.ML") ("import.ML") ("import_syntax.ML")
+begin
+
+setup Shuffler.setup
+
+lemma conj_norm [shuffle_rule]: "(A & B ==> PROP C) == ([| A ; B |] ==> PROP C)"
+proof
+  assume "A & B ==> PROP C" A B
+  thus "PROP C"
+    by auto
+next
+  assume "[| A; B |] ==> PROP C" "A & B"
+  thus "PROP C"
+    by auto
+qed
+
+lemma imp_norm [shuffle_rule]: "(Trueprop (A --> B)) == (A ==> B)"
+proof
+  assume "A --> B" A
+  thus B ..
+next
+  assume "A ==> B"
+  thus "A --> B"
+    by auto
+qed
+
+lemma all_norm [shuffle_rule]: "(Trueprop (ALL x. P x)) == (!!x. P x)"
+proof
+  fix x
+  assume "ALL x. P x"
+  thus "P x" ..
+next
+  assume "!!x. P x"
+  thus "ALL x. P x"
+    ..
+qed
+
+lemma ex_norm [shuffle_rule]: "(EX x. P x ==> PROP Q) == (!!x. P x ==> PROP Q)"
+proof
+  fix x
+  assume ex: "EX x. P x ==> PROP Q"
+  assume "P x"
+  hence "EX x. P x" ..
+  with ex show "PROP Q" .
+next
+  assume allx: "!!x. P x ==> PROP Q"
+  assume "EX x. P x"
+  hence p: "P (SOME x. P x)"
+    ..
+  from allx
+  have "P (SOME x. P x) ==> PROP Q"
+    .
+  with p
+  show "PROP Q"
+    by auto
+qed
+
+lemma eq_norm [shuffle_rule]: "Trueprop (t = u) == (t == u)"
+proof
+  assume "t = u"
+  thus "t == u" by simp
+next
+  assume "t == u"
+  thus "t = u"
+    by simp
+qed
+
+section {* General Setup *}
+
+lemma eq_imp: "P = Q \<Longrightarrow> P \<longrightarrow> Q"
+  by auto
+
+lemma HOLallI: "(!! bogus. P bogus) \<Longrightarrow> (ALL bogus. P bogus)"
+proof -
+  assume "!! bogus. P bogus"
+  thus "ALL x. P x"
+    ..
+qed
+
+consts
+  ONE_ONE :: "('a => 'b) => bool"
+
+defs
+  ONE_ONE_DEF: "ONE_ONE f == ALL x y. f x = f y --> x = y"
+
+lemma ONE_ONE_rew: "ONE_ONE f = inj_on f UNIV"
+  by (simp add: ONE_ONE_DEF inj_on_def)
+
+lemma INFINITY_AX: "EX (f::ind \<Rightarrow> ind). (inj f & ~(surj f))"
+proof (rule exI,safe)
+  show "inj Suc_Rep"
+    by (rule injI) (rule Suc_Rep_inject)
+next
+  assume "surj Suc_Rep"
+  hence "ALL y. EX x. y = Suc_Rep x"
+    by (simp add: surj_def)
+  hence "EX x. Zero_Rep = Suc_Rep x"
+    by (rule spec)
+  thus False
+  proof (rule exE)
+    fix x
+    assume "Zero_Rep = Suc_Rep x"
+    hence "Suc_Rep x = Zero_Rep"
+      ..
+    with Suc_Rep_not_Zero_Rep
+    show False
+      ..
+  qed
+qed
+
+lemma EXISTS_DEF: "Ex P = P (Eps P)"
+proof (rule iffI)
+  assume "Ex P"
+  thus "P (Eps P)"
+    ..
+next
+  assume "P (Eps P)"
+  thus "Ex P"
+    ..
+qed
+
+consts
+  TYPE_DEFINITION :: "('a => bool) => ('b => 'a) => bool"
+
+defs
+  TYPE_DEFINITION: "TYPE_DEFINITION p rep == ((ALL x y. (rep x = rep y) --> (x = y)) & (ALL x. (p x = (EX y. x = rep y))))"
+
+lemma ex_imp_nonempty: "Ex P ==> EX x. x : (Collect P)"
+  by simp
+
+lemma light_ex_imp_nonempty: "P t ==> EX x. x : (Collect P)"
+proof -
+  assume "P t"
+  hence "EX x. P x"
+    ..
+  thus ?thesis
+    by (rule ex_imp_nonempty)
+qed
+
+lemma light_imp_as: "[| Q --> P; P --> Q |] ==> P = Q"
+  by blast
+
+lemma typedef_hol2hol4:
+  assumes a: "type_definition (Rep::'a=>'b) Abs (Collect P)"
+  shows "EX rep. TYPE_DEFINITION P (rep::'a=>'b)"
+proof -
+  from a
+  have td: "(ALL x. P (Rep x)) & (ALL x. Abs (Rep x) = x) & (ALL y. P y \<longrightarrow> Rep (Abs y) = y)"
+    by (simp add: type_definition_def)
+  have ed: "TYPE_DEFINITION P Rep"
+  proof (auto simp add: TYPE_DEFINITION)
+    fix x y
+    assume b: "Rep x = Rep y"
+    from td have "x = Abs (Rep x)"
+      by auto
+    also have "Abs (Rep x) = Abs (Rep y)"
+      by (simp add: b)
+    also from td have "Abs (Rep y) = y"
+      by auto
+    finally show "x = y" .
+  next
+    fix x
+    assume "P x"
+    with td
+    have "Rep (Abs x) = x"
+      by auto
+    hence "x = Rep (Abs x)"
+      ..
+    thus "EX y. x = Rep y"
+      ..
+  next
+    fix y
+    from td
+    show "P (Rep y)"
+      by auto
+  qed
+  show ?thesis
+    apply (rule exI [of _ Rep])
+    apply (rule ed)
+    .
+qed
+
+lemma typedef_hol2hollight:
+  assumes a: "type_definition (Rep::'a=>'b) Abs (Collect P)"
+  shows "(Abs (Rep a) = a) & (P r = (Rep (Abs r) = r))"
+proof
+  from a
+  show "Abs (Rep a) = a"
+    by (rule type_definition.Rep_inverse)
+next
+  show "P r = (Rep (Abs r) = r)"
+  proof
+    assume "P r"
+    hence "r \<in> (Collect P)"
+      by simp
+    with a
+    show "Rep (Abs r) = r"
+      by (rule type_definition.Abs_inverse)
+  next
+    assume ra: "Rep (Abs r) = r"
+    from a
+    have "Rep (Abs r) \<in> (Collect P)"
+      by (rule type_definition.Rep)
+    thus "P r"
+      by (simp add: ra)
+  qed
+qed
+
+lemma termspec_help: "[| Ex P ; c == Eps P |] ==> P c"
+  apply simp
+  apply (rule someI_ex)
+  .
+
+lemma typedef_helper: "EX x. P x \<Longrightarrow> EX x. x \<in> (Collect P)"
+  by simp
+
+use "import_rews.ML"
+
+setup importer_setup
+parse_ast_translation smarter_trueprop_parsing
+
+use "proof_kernel.ML"
+use "replay.ML"
+use "import.ML"
+
+setup Import.setup
+
+use "import_syntax.ML"
+
+ML {* Importer_Import_Syntax.setup() *}
+
+end
+