src/HOL/Import/HOL4Setup.thy
 author wenzelm Sat, 08 Oct 2005 22:39:39 +0200 changeset 17801 30cbd2685e73 parent 17322 781abf7011e6 child 19064 bf19cc5a7899 permissions -rw-r--r--
uses susp.ML, lazy_seq.ML, lazy_scan.ML;
```
(*  Title:      HOL/Import/HOL4Setup.thy
ID:         \$Id\$
Author:     Sebastian Skalberg (TU Muenchen)
*)

theory HOL4Setup imports MakeEqual
uses "susp.ML" "lazy_seq.ML" "lazy_scan.ML"
("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import_package.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"
ONTO    :: "('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"

lemma INFINITY_AX: "EX (f::ind \<Rightarrow> ind). (inj f & ~(surj f))"
proof (rule exI,safe)
show "inj Suc_Rep"
by (rule inj_Suc_Rep)
next
assume "surj Suc_Rep"
hence "ALL y. EX x. y = Suc_Rep x"
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)"
have ed: "TYPE_DEFINITION P Rep"
fix x y
assume "Rep x = Rep y"
from td have "x = Abs (Rep x)"
by auto
also have "Abs (Rep x) = Abs (Rep y)"
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"
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_package.ML"

setup ImportPackage.setup

end
```