# HG changeset patch
# User haftmann
# Date 1330814962 -3600
# Node ID bdf9a78d46cff57aa18947a9cc3e18bfa0dd55e5
# Parent  81e5ec0a3cd0d1bf21dcfda5d861c1dc9f37c534
dropped dead theories

diff -r 81e5ec0a3cd0 -r bdf9a78d46cf src/HOL/Import/HOL4Setup.thy
--- a/src/HOL/Import/HOL4Setup.thy	Sat Mar 03 23:43:21 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,169 +0,0 @@
-(*  Title:      HOL/Import/HOL4Setup.thy
-    Author:     Sebastian Skalberg (TU Muenchen)
-*)
-
-theory HOL4Setup imports MakeEqual
-  uses ("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import.ML") begin
-
-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 "hol4rews.ML"
-
-setup hol4_setup
-parse_ast_translation smarter_trueprop_parsing
-
-use "proof_kernel.ML"
-use "replay.ML"
-use "import.ML"
-
-setup Import.setup
-
-end
-
diff -r 81e5ec0a3cd0 -r bdf9a78d46cf src/HOL/Import/HOL4Syntax.thy
--- a/src/HOL/Import/HOL4Syntax.thy	Sat Mar 03 23:43:21 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-(*  Title:      HOL/Import/HOL4Syntax.thy
-    Author:     Sebastian Skalberg, TU Muenchen
-*)
-
-theory HOL4Syntax
-imports HOL4Setup
-uses "import_syntax.ML"
-begin
-
-ML {* HOL4ImportSyntax.setup() *}
-
-end