src/HOL/Import/HOL4Setup.thy
changeset 14516 a183dec876ab
child 14620 1be590fd2422
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Import/HOL4Setup.thy	Fri Apr 02 17:37:45 2004 +0200
     1.3 @@ -0,0 +1,166 @@
     1.4 +theory HOL4Setup = MakeEqual
     1.5 +  files ("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import_package.ML"):
     1.6 +
     1.7 +section {* General Setup *}
     1.8 +
     1.9 +lemma eq_imp: "P = Q \<Longrightarrow> P \<longrightarrow> Q"
    1.10 +  by auto
    1.11 +
    1.12 +lemma HOLallI: "(!! bogus. P bogus) \<Longrightarrow> (ALL bogus. P bogus)"
    1.13 +proof -
    1.14 +  assume "!! bogus. P bogus"
    1.15 +  thus "ALL x. P x"
    1.16 +    ..
    1.17 +qed
    1.18 +
    1.19 +consts
    1.20 +  ONE_ONE :: "('a => 'b) => bool"
    1.21 +  ONTO    :: "('a => 'b) => bool"
    1.22 +
    1.23 +defs
    1.24 +  ONE_ONE_DEF: "ONE_ONE f == ALL x y. f x = f y --> x = y"
    1.25 +  ONTO_DEF   : "ONTO f == ALL y. EX x. y = f x"
    1.26 +
    1.27 +lemma ONE_ONE_rew: "ONE_ONE f = inj_on f UNIV"
    1.28 +  by (simp add: ONE_ONE_DEF inj_on_def)
    1.29 +
    1.30 +lemma INFINITY_AX: "EX (f::ind \<Rightarrow> ind). (inj f & ~(ONTO f))"
    1.31 +proof (rule exI,safe)
    1.32 +  show "inj Suc_Rep"
    1.33 +    by (rule inj_Suc_Rep)
    1.34 +next
    1.35 +  assume "ONTO Suc_Rep"
    1.36 +  hence "ALL y. EX x. y = Suc_Rep x"
    1.37 +    by (simp add: ONTO_DEF surj_def)
    1.38 +  hence "EX x. Zero_Rep = Suc_Rep x"
    1.39 +    by (rule spec)
    1.40 +  thus False
    1.41 +  proof (rule exE)
    1.42 +    fix x
    1.43 +    assume "Zero_Rep = Suc_Rep x"
    1.44 +    hence "Suc_Rep x = Zero_Rep"
    1.45 +      ..
    1.46 +    with Suc_Rep_not_Zero_Rep
    1.47 +    show False
    1.48 +      ..
    1.49 +  qed
    1.50 +qed
    1.51 +
    1.52 +lemma EXISTS_DEF: "Ex P = P (Eps P)"
    1.53 +proof (rule iffI)
    1.54 +  assume "Ex P"
    1.55 +  thus "P (Eps P)"
    1.56 +    ..
    1.57 +next
    1.58 +  assume "P (Eps P)"
    1.59 +  thus "Ex P"
    1.60 +    ..
    1.61 +qed
    1.62 +
    1.63 +consts
    1.64 +  TYPE_DEFINITION :: "('a => bool) => ('b => 'a) => bool"
    1.65 +
    1.66 +defs
    1.67 +  TYPE_DEFINITION: "TYPE_DEFINITION p rep == ((ALL x y. (rep x = rep y) --> (x = y)) & (ALL x. (p x = (EX y. x = rep y))))"
    1.68 +
    1.69 +lemma ex_imp_nonempty: "Ex P ==> EX x. x : (Collect P)"
    1.70 +  by simp
    1.71 +
    1.72 +lemma light_ex_imp_nonempty: "P t ==> EX x. x : (Collect P)"
    1.73 +proof -
    1.74 +  assume "P t"
    1.75 +  hence "EX x. P x"
    1.76 +    ..
    1.77 +  thus ?thesis
    1.78 +    by (rule ex_imp_nonempty)
    1.79 +qed
    1.80 +
    1.81 +lemma light_imp_as: "[| Q --> P; P --> Q |] ==> P = Q"
    1.82 +  by blast
    1.83 +
    1.84 +lemma typedef_hol2hol4:
    1.85 +  assumes a: "type_definition (Rep::'a=>'b) Abs (Collect P)"
    1.86 +  shows "EX rep. TYPE_DEFINITION P (rep::'a=>'b)"
    1.87 +proof -
    1.88 +  from a
    1.89 +  have td: "(ALL x. P (Rep x)) & (ALL x. Abs (Rep x) = x) & (ALL y. P y \<longrightarrow> Rep (Abs y) = y)"
    1.90 +    by (simp add: type_definition_def)
    1.91 +  have ed: "TYPE_DEFINITION P Rep"
    1.92 +  proof (auto simp add: TYPE_DEFINITION)
    1.93 +    fix x y
    1.94 +    assume "Rep x = Rep y"
    1.95 +    from td have "x = Abs (Rep x)"
    1.96 +      by auto
    1.97 +    also have "Abs (Rep x) = Abs (Rep y)"
    1.98 +      by (simp add: prems)
    1.99 +    also from td have "Abs (Rep y) = y"
   1.100 +      by auto
   1.101 +    finally show "x = y" .
   1.102 +  next
   1.103 +    fix x
   1.104 +    assume "P x"
   1.105 +    with td
   1.106 +    have "Rep (Abs x) = x"
   1.107 +      by auto
   1.108 +    hence "x = Rep (Abs x)"
   1.109 +      ..
   1.110 +    thus "EX y. x = Rep y"
   1.111 +      ..
   1.112 +  next
   1.113 +    fix y
   1.114 +    from td
   1.115 +    show "P (Rep y)"
   1.116 +      by auto
   1.117 +  qed
   1.118 +  show ?thesis
   1.119 +    apply (rule exI [of _ Rep])
   1.120 +    apply (rule ed)
   1.121 +    .
   1.122 +qed
   1.123 +
   1.124 +lemma typedef_hol2hollight:
   1.125 +  assumes a: "type_definition (Rep::'a=>'b) Abs (Collect P)"
   1.126 +  shows "(Abs (Rep a) = a) & (P r = (Rep (Abs r) = r))"
   1.127 +proof
   1.128 +  from a
   1.129 +  show "Abs (Rep a) = a"
   1.130 +    by (rule type_definition.Rep_inverse)
   1.131 +next
   1.132 +  show "P r = (Rep (Abs r) = r)"
   1.133 +  proof
   1.134 +    assume "P r"
   1.135 +    hence "r \<in> (Collect P)"
   1.136 +      by simp
   1.137 +    with a
   1.138 +    show "Rep (Abs r) = r"
   1.139 +      by (rule type_definition.Abs_inverse)
   1.140 +  next
   1.141 +    assume ra: "Rep (Abs r) = r"
   1.142 +    from a
   1.143 +    have "Rep (Abs r) \<in> (Collect P)"
   1.144 +      by (rule type_definition.Rep)
   1.145 +    thus "P r"
   1.146 +      by (simp add: ra)
   1.147 +  qed
   1.148 +qed
   1.149 +
   1.150 +lemma termspec_help: "[| Ex P ; c == Eps P |] ==> P c"
   1.151 +  apply simp
   1.152 +  apply (rule someI_ex)
   1.153 +  .
   1.154 +
   1.155 +lemma typedef_helper: "EX x. P x \<Longrightarrow> EX x. x \<in> (Collect P)"
   1.156 +  by simp
   1.157 +
   1.158 +use "hol4rews.ML"
   1.159 +
   1.160 +setup hol4_setup
   1.161 +parse_ast_translation smarter_trueprop_parsing
   1.162 +
   1.163 +use "proof_kernel.ML"
   1.164 +use "replay.ML"
   1.165 +use "import_package.ML"
   1.166 +
   1.167 +setup ImportPackage.setup
   1.168 +
   1.169 +end