src/HOL/Hilbert_Choice.thy
author wenzelm
Sat Jun 05 13:07:04 2004 +0200 (2004-06-05)
changeset 14872 3f2144aebd76
parent 14760 a08e916f4946
child 15131 c69542757a4d
permissions -rw-r--r--
improved symbolic syntax of Eps: \<some> for mode "epsilon";
     1 (*  Title:      HOL/Hilbert_Choice.thy
     2     ID: $Id$
     3     Author:     Lawrence C Paulson
     4     Copyright   2001  University of Cambridge
     5 *)
     6 
     7 header {* Hilbert's Epsilon-Operator and the Axiom of Choice *}
     8 
     9 theory Hilbert_Choice = NatArith
    10 files ("Tools/meson.ML") ("Tools/specification_package.ML"):
    11 
    12 
    13 subsection {* Hilbert's epsilon *}
    14 
    15 consts
    16   Eps           :: "('a => bool) => 'a"
    17 
    18 syntax (epsilon)
    19   "_Eps"        :: "[pttrn, bool] => 'a"    ("(3\<some>_./ _)" [0, 10] 10)
    20 syntax (HOL)
    21   "_Eps"        :: "[pttrn, bool] => 'a"    ("(3@ _./ _)" [0, 10] 10)
    22 syntax
    23   "_Eps"        :: "[pttrn, bool] => 'a"    ("(3SOME _./ _)" [0, 10] 10)
    24 translations
    25   "SOME x. P" == "Eps (%x. P)"
    26 
    27 print_translation {*
    28 (* to avoid eta-contraction of body *)
    29 [("Eps", fn [Abs abs] =>
    30      let val (x,t) = atomic_abs_tr' abs
    31      in Syntax.const "_Eps" $ x $ t end)]
    32 *}
    33 
    34 axioms
    35   someI: "P (x::'a) ==> P (SOME x. P x)"
    36 
    37 
    38 constdefs
    39   inv :: "('a => 'b) => ('b => 'a)"
    40   "inv(f :: 'a => 'b) == %y. SOME x. f x = y"
    41 
    42   Inv :: "'a set => ('a => 'b) => ('b => 'a)"
    43   "Inv A f == %x. SOME y. y \<in> A & f y = x"
    44 
    45 
    46 subsection {*Hilbert's Epsilon-operator*}
    47 
    48 text{*Easier to apply than @{text someI} if the witness comes from an
    49 existential formula*}
    50 lemma someI_ex [elim?]: "\<exists>x. P x ==> P (SOME x. P x)"
    51 apply (erule exE)
    52 apply (erule someI)
    53 done
    54 
    55 text{*Easier to apply than @{text someI} because the conclusion has only one
    56 occurrence of @{term P}.*}
    57 lemma someI2: "[| P a;  !!x. P x ==> Q x |] ==> Q (SOME x. P x)"
    58 by (blast intro: someI)
    59 
    60 text{*Easier to apply than @{text someI2} if the witness comes from an
    61 existential formula*}
    62 lemma someI2_ex: "[| \<exists>a. P a; !!x. P x ==> Q x |] ==> Q (SOME x. P x)"
    63 by (blast intro: someI2)
    64 
    65 lemma some_equality [intro]:
    66      "[| P a;  !!x. P x ==> x=a |] ==> (SOME x. P x) = a"
    67 by (blast intro: someI2)
    68 
    69 lemma some1_equality: "[| EX!x. P x; P a |] ==> (SOME x. P x) = a"
    70 by (blast intro: some_equality)
    71 
    72 lemma some_eq_ex: "P (SOME x. P x) =  (\<exists>x. P x)"
    73 by (blast intro: someI)
    74 
    75 lemma some_eq_trivial [simp]: "(SOME y. y=x) = x"
    76 apply (rule some_equality)
    77 apply (rule refl, assumption)
    78 done
    79 
    80 lemma some_sym_eq_trivial [simp]: "(SOME y. x=y) = x"
    81 apply (rule some_equality)
    82 apply (rule refl)
    83 apply (erule sym)
    84 done
    85 
    86 
    87 subsection{*Axiom of Choice, Proved Using the Description Operator*}
    88 
    89 text{*Used in @{text "Tools/meson.ML"}*}
    90 lemma choice: "\<forall>x. \<exists>y. Q x y ==> \<exists>f. \<forall>x. Q x (f x)"
    91 by (fast elim: someI)
    92 
    93 lemma bchoice: "\<forall>x\<in>S. \<exists>y. Q x y ==> \<exists>f. \<forall>x\<in>S. Q x (f x)"
    94 by (fast elim: someI)
    95 
    96 
    97 subsection {*Function Inverse*}
    98 
    99 lemma inv_id [simp]: "inv id = id"
   100 by (simp add: inv_def id_def)
   101 
   102 text{*A one-to-one function has an inverse.*}
   103 lemma inv_f_f [simp]: "inj f ==> inv f (f x) = x"
   104 by (simp add: inv_def inj_eq)
   105 
   106 lemma inv_f_eq: "[| inj f;  f x = y |] ==> inv f y = x"
   107 apply (erule subst)
   108 apply (erule inv_f_f)
   109 done
   110 
   111 lemma inj_imp_inv_eq: "[| inj f; \<forall>x. f(g x) = x |] ==> inv f = g"
   112 by (blast intro: ext inv_f_eq)
   113 
   114 text{*But is it useful?*}
   115 lemma inj_transfer:
   116   assumes injf: "inj f" and minor: "!!y. y \<in> range(f) ==> P(inv f y)"
   117   shows "P x"
   118 proof -
   119   have "f x \<in> range f" by auto
   120   hence "P(inv f (f x))" by (rule minor)
   121   thus "P x" by (simp add: inv_f_f [OF injf])
   122 qed
   123 
   124 
   125 lemma inj_iff: "(inj f) = (inv f o f = id)"
   126 apply (simp add: o_def expand_fun_eq)
   127 apply (blast intro: inj_on_inverseI inv_f_f)
   128 done
   129 
   130 lemma inj_imp_surj_inv: "inj f ==> surj (inv f)"
   131 by (blast intro: surjI inv_f_f)
   132 
   133 lemma f_inv_f: "y \<in> range(f) ==> f(inv f y) = y"
   134 apply (simp add: inv_def)
   135 apply (fast intro: someI)
   136 done
   137 
   138 lemma surj_f_inv_f: "surj f ==> f(inv f y) = y"
   139 by (simp add: f_inv_f surj_range)
   140 
   141 lemma inv_injective:
   142   assumes eq: "inv f x = inv f y"
   143       and x: "x: range f"
   144       and y: "y: range f"
   145   shows "x=y"
   146 proof -
   147   have "f (inv f x) = f (inv f y)" using eq by simp
   148   thus ?thesis by (simp add: f_inv_f x y) 
   149 qed
   150 
   151 lemma inj_on_inv: "A <= range(f) ==> inj_on (inv f) A"
   152 by (fast intro: inj_onI elim: inv_injective injD)
   153 
   154 lemma surj_imp_inj_inv: "surj f ==> inj (inv f)"
   155 by (simp add: inj_on_inv surj_range)
   156 
   157 lemma surj_iff: "(surj f) = (f o inv f = id)"
   158 apply (simp add: o_def expand_fun_eq)
   159 apply (blast intro: surjI surj_f_inv_f)
   160 done
   161 
   162 lemma surj_imp_inv_eq: "[| surj f; \<forall>x. g(f x) = x |] ==> inv f = g"
   163 apply (rule ext)
   164 apply (drule_tac x = "inv f x" in spec)
   165 apply (simp add: surj_f_inv_f)
   166 done
   167 
   168 lemma bij_imp_bij_inv: "bij f ==> bij (inv f)"
   169 by (simp add: bij_def inj_imp_surj_inv surj_imp_inj_inv)
   170 
   171 lemma inv_equality: "[| !!x. g (f x) = x;  !!y. f (g y) = y |] ==> inv f = g"
   172 apply (rule ext)
   173 apply (auto simp add: inv_def)
   174 done
   175 
   176 lemma inv_inv_eq: "bij f ==> inv (inv f) = f"
   177 apply (rule inv_equality)
   178 apply (auto simp add: bij_def surj_f_inv_f)
   179 done
   180 
   181 (** bij(inv f) implies little about f.  Consider f::bool=>bool such that
   182     f(True)=f(False)=True.  Then it's consistent with axiom someI that
   183     inv f could be any function at all, including the identity function.
   184     If inv f=id then inv f is a bijection, but inj f, surj(f) and
   185     inv(inv f)=f all fail.
   186 **)
   187 
   188 lemma o_inv_distrib: "[| bij f; bij g |] ==> inv (f o g) = inv g o inv f"
   189 apply (rule inv_equality)
   190 apply (auto simp add: bij_def surj_f_inv_f)
   191 done
   192 
   193 
   194 lemma image_surj_f_inv_f: "surj f ==> f ` (inv f ` A) = A"
   195 by (simp add: image_eq_UN surj_f_inv_f)
   196 
   197 lemma image_inv_f_f: "inj f ==> (inv f) ` (f ` A) = A"
   198 by (simp add: image_eq_UN)
   199 
   200 lemma inv_image_comp: "inj f ==> inv f ` (f`X) = X"
   201 by (auto simp add: image_def)
   202 
   203 lemma bij_image_Collect_eq: "bij f ==> f ` Collect P = {y. P (inv f y)}"
   204 apply auto
   205 apply (force simp add: bij_is_inj)
   206 apply (blast intro: bij_is_surj [THEN surj_f_inv_f, symmetric])
   207 done
   208 
   209 lemma bij_vimage_eq_inv_image: "bij f ==> f -` A = inv f ` A" 
   210 apply (auto simp add: bij_is_surj [THEN surj_f_inv_f])
   211 apply (blast intro: bij_is_inj [THEN inv_f_f, symmetric])
   212 done
   213 
   214 
   215 subsection {*Inverse of a PI-function (restricted domain)*}
   216 
   217 lemma Inv_f_f: "[| inj_on f A;  x \<in> A |] ==> Inv A f (f x) = x"
   218 apply (simp add: Inv_def inj_on_def)
   219 apply (blast intro: someI2)
   220 done
   221 
   222 lemma f_Inv_f: "y \<in> f`A  ==> f (Inv A f y) = y"
   223 apply (simp add: Inv_def)
   224 apply (fast intro: someI2)
   225 done
   226 
   227 lemma Inv_injective:
   228   assumes eq: "Inv A f x = Inv A f y"
   229       and x: "x: f`A"
   230       and y: "y: f`A"
   231   shows "x=y"
   232 proof -
   233   have "f (Inv A f x) = f (Inv A f y)" using eq by simp
   234   thus ?thesis by (simp add: f_Inv_f x y) 
   235 qed
   236 
   237 lemma inj_on_Inv: "B <= f`A ==> inj_on (Inv A f) B"
   238 apply (rule inj_onI)
   239 apply (blast intro: inj_onI dest: Inv_injective injD)
   240 done
   241 
   242 lemma Inv_mem: "[| f ` A = B;  x \<in> B |] ==> Inv A f x \<in> A"
   243 apply (simp add: Inv_def)
   244 apply (fast intro: someI2)
   245 done
   246 
   247 lemma Inv_f_eq: "[| inj_on f A; f x = y; x \<in> A |] ==> Inv A f y = x"
   248   apply (erule subst)
   249   apply (erule Inv_f_f, assumption)
   250   done
   251 
   252 lemma Inv_comp:
   253   "[| inj_on f (g ` A); inj_on g A; x \<in> f ` g ` A |] ==>
   254   Inv A (f o g) x = (Inv A g o Inv (g ` A) f) x"
   255   apply simp
   256   apply (rule Inv_f_eq)
   257     apply (fast intro: comp_inj_on)
   258    apply (simp add: f_Inv_f Inv_mem)
   259   apply (simp add: Inv_mem)
   260   done
   261 
   262 
   263 subsection {*Other Consequences of Hilbert's Epsilon*}
   264 
   265 text {*Hilbert's Epsilon and the @{term split} Operator*}
   266 
   267 text{*Looping simprule*}
   268 lemma split_paired_Eps: "(SOME x. P x) = (SOME (a,b). P(a,b))"
   269 by (simp add: split_Pair_apply)
   270 
   271 lemma Eps_split: "Eps (split P) = (SOME xy. P (fst xy) (snd xy))"
   272 by (simp add: split_def)
   273 
   274 lemma Eps_split_eq [simp]: "(@(x',y'). x = x' & y = y') = (x,y)"
   275 by blast
   276 
   277 
   278 text{*A relation is wellfounded iff it has no infinite descending chain*}
   279 lemma wf_iff_no_infinite_down_chain:
   280   "wf r = (~(\<exists>f. \<forall>i. (f(Suc i),f i) \<in> r))"
   281 apply (simp only: wf_eq_minimal)
   282 apply (rule iffI)
   283  apply (rule notI)
   284  apply (erule exE)
   285  apply (erule_tac x = "{w. \<exists>i. w=f i}" in allE, blast)
   286 apply (erule contrapos_np, simp, clarify)
   287 apply (subgoal_tac "\<forall>n. nat_rec x (%i y. @z. z:Q & (z,y) :r) n \<in> Q")
   288  apply (rule_tac x = "nat_rec x (%i y. @z. z:Q & (z,y) :r)" in exI)
   289  apply (rule allI, simp)
   290  apply (rule someI2_ex, blast, blast)
   291 apply (rule allI)
   292 apply (induct_tac "n", simp_all)
   293 apply (rule someI2_ex, blast+)
   294 done
   295 
   296 text{*A dynamically-scoped fact for TFL *}
   297 lemma tfl_some: "\<forall>P x. P x --> P (Eps P)"
   298   by (blast intro: someI)
   299 
   300 
   301 subsection {* Least value operator *}
   302 
   303 constdefs
   304   LeastM :: "['a => 'b::ord, 'a => bool] => 'a"
   305   "LeastM m P == SOME x. P x & (\<forall>y. P y --> m x <= m y)"
   306 
   307 syntax
   308   "_LeastM" :: "[pttrn, 'a => 'b::ord, bool] => 'a"    ("LEAST _ WRT _. _" [0, 4, 10] 10)
   309 translations
   310   "LEAST x WRT m. P" == "LeastM m (%x. P)"
   311 
   312 lemma LeastMI2:
   313   "P x ==> (!!y. P y ==> m x <= m y)
   314     ==> (!!x. P x ==> \<forall>y. P y --> m x \<le> m y ==> Q x)
   315     ==> Q (LeastM m P)"
   316   apply (simp add: LeastM_def)
   317   apply (rule someI2_ex, blast, blast)
   318   done
   319 
   320 lemma LeastM_equality:
   321   "P k ==> (!!x. P x ==> m k <= m x)
   322     ==> m (LEAST x WRT m. P x) = (m k::'a::order)"
   323   apply (rule LeastMI2, assumption, blast)
   324   apply (blast intro!: order_antisym)
   325   done
   326 
   327 lemma wf_linord_ex_has_least:
   328   "wf r ==> \<forall>x y. ((x,y):r^+) = ((y,x)~:r^*) ==> P k
   329     ==> \<exists>x. P x & (!y. P y --> (m x,m y):r^*)"
   330   apply (drule wf_trancl [THEN wf_eq_minimal [THEN iffD1]])
   331   apply (drule_tac x = "m`Collect P" in spec, force)
   332   done
   333 
   334 lemma ex_has_least_nat:
   335     "P k ==> \<exists>x. P x & (\<forall>y. P y --> m x <= (m y::nat))"
   336   apply (simp only: pred_nat_trancl_eq_le [symmetric])
   337   apply (rule wf_pred_nat [THEN wf_linord_ex_has_least])
   338    apply (simp add: less_eq not_le_iff_less pred_nat_trancl_eq_le, assumption)
   339   done
   340 
   341 lemma LeastM_nat_lemma:
   342     "P k ==> P (LeastM m P) & (\<forall>y. P y --> m (LeastM m P) <= (m y::nat))"
   343   apply (simp add: LeastM_def)
   344   apply (rule someI_ex)
   345   apply (erule ex_has_least_nat)
   346   done
   347 
   348 lemmas LeastM_natI = LeastM_nat_lemma [THEN conjunct1, standard]
   349 
   350 lemma LeastM_nat_le: "P x ==> m (LeastM m P) <= (m x::nat)"
   351 by (rule LeastM_nat_lemma [THEN conjunct2, THEN spec, THEN mp], assumption, assumption)
   352 
   353 
   354 subsection {* Greatest value operator *}
   355 
   356 constdefs
   357   GreatestM :: "['a => 'b::ord, 'a => bool] => 'a"
   358   "GreatestM m P == SOME x. P x & (\<forall>y. P y --> m y <= m x)"
   359 
   360   Greatest :: "('a::ord => bool) => 'a"    (binder "GREATEST " 10)
   361   "Greatest == GreatestM (%x. x)"
   362 
   363 syntax
   364   "_GreatestM" :: "[pttrn, 'a=>'b::ord, bool] => 'a"
   365       ("GREATEST _ WRT _. _" [0, 4, 10] 10)
   366 
   367 translations
   368   "GREATEST x WRT m. P" == "GreatestM m (%x. P)"
   369 
   370 lemma GreatestMI2:
   371   "P x ==> (!!y. P y ==> m y <= m x)
   372     ==> (!!x. P x ==> \<forall>y. P y --> m y \<le> m x ==> Q x)
   373     ==> Q (GreatestM m P)"
   374   apply (simp add: GreatestM_def)
   375   apply (rule someI2_ex, blast, blast)
   376   done
   377 
   378 lemma GreatestM_equality:
   379  "P k ==> (!!x. P x ==> m x <= m k)
   380     ==> m (GREATEST x WRT m. P x) = (m k::'a::order)"
   381   apply (rule_tac m = m in GreatestMI2, assumption, blast)
   382   apply (blast intro!: order_antisym)
   383   done
   384 
   385 lemma Greatest_equality:
   386   "P (k::'a::order) ==> (!!x. P x ==> x <= k) ==> (GREATEST x. P x) = k"
   387   apply (simp add: Greatest_def)
   388   apply (erule GreatestM_equality, blast)
   389   done
   390 
   391 lemma ex_has_greatest_nat_lemma:
   392   "P k ==> \<forall>x. P x --> (\<exists>y. P y & ~ ((m y::nat) <= m x))
   393     ==> \<exists>y. P y & ~ (m y < m k + n)"
   394   apply (induct_tac n, force)
   395   apply (force simp add: le_Suc_eq)
   396   done
   397 
   398 lemma ex_has_greatest_nat:
   399   "P k ==> \<forall>y. P y --> m y < b
   400     ==> \<exists>x. P x & (\<forall>y. P y --> (m y::nat) <= m x)"
   401   apply (rule ccontr)
   402   apply (cut_tac P = P and n = "b - m k" in ex_has_greatest_nat_lemma)
   403     apply (subgoal_tac [3] "m k <= b", auto)
   404   done
   405 
   406 lemma GreatestM_nat_lemma:
   407   "P k ==> \<forall>y. P y --> m y < b
   408     ==> P (GreatestM m P) & (\<forall>y. P y --> (m y::nat) <= m (GreatestM m P))"
   409   apply (simp add: GreatestM_def)
   410   apply (rule someI_ex)
   411   apply (erule ex_has_greatest_nat, assumption)
   412   done
   413 
   414 lemmas GreatestM_natI = GreatestM_nat_lemma [THEN conjunct1, standard]
   415 
   416 lemma GreatestM_nat_le:
   417   "P x ==> \<forall>y. P y --> m y < b
   418     ==> (m x::nat) <= m (GreatestM m P)"
   419   apply (blast dest: GreatestM_nat_lemma [THEN conjunct2, THEN spec])
   420   done
   421 
   422 
   423 text {* \medskip Specialization to @{text GREATEST}. *}
   424 
   425 lemma GreatestI: "P (k::nat) ==> \<forall>y. P y --> y < b ==> P (GREATEST x. P x)"
   426   apply (simp add: Greatest_def)
   427   apply (rule GreatestM_natI, auto)
   428   done
   429 
   430 lemma Greatest_le:
   431     "P x ==> \<forall>y. P y --> y < b ==> (x::nat) <= (GREATEST x. P x)"
   432   apply (simp add: Greatest_def)
   433   apply (rule GreatestM_nat_le, auto)
   434   done
   435 
   436 
   437 subsection {* The Meson proof procedure *}
   438 
   439 subsubsection {* Negation Normal Form *}
   440 
   441 text {* de Morgan laws *}
   442 
   443 lemma meson_not_conjD: "~(P&Q) ==> ~P | ~Q"
   444   and meson_not_disjD: "~(P|Q) ==> ~P & ~Q"
   445   and meson_not_notD: "~~P ==> P"
   446   and meson_not_allD: "!!P. ~(\<forall>x. P(x)) ==> \<exists>x. ~P(x)"
   447   and meson_not_exD: "!!P. ~(\<exists>x. P(x)) ==> \<forall>x. ~P(x)"
   448   by fast+
   449 
   450 text {* Removal of @{text "-->"} and @{text "<->"} (positive and
   451 negative occurrences) *}
   452 
   453 lemma meson_imp_to_disjD: "P-->Q ==> ~P | Q"
   454   and meson_not_impD: "~(P-->Q) ==> P & ~Q"
   455   and meson_iff_to_disjD: "P=Q ==> (~P | Q) & (~Q | P)"
   456   and meson_not_iffD: "~(P=Q) ==> (P | Q) & (~P | ~Q)"
   457     -- {* Much more efficient than @{prop "(P & ~Q) | (Q & ~P)"} for computing CNF *}
   458   by fast+
   459 
   460 
   461 subsubsection {* Pulling out the existential quantifiers *}
   462 
   463 text {* Conjunction *}
   464 
   465 lemma meson_conj_exD1: "!!P Q. (\<exists>x. P(x)) & Q ==> \<exists>x. P(x) & Q"
   466   and meson_conj_exD2: "!!P Q. P & (\<exists>x. Q(x)) ==> \<exists>x. P & Q(x)"
   467   by fast+
   468 
   469 
   470 text {* Disjunction *}
   471 
   472 lemma meson_disj_exD: "!!P Q. (\<exists>x. P(x)) | (\<exists>x. Q(x)) ==> \<exists>x. P(x) | Q(x)"
   473   -- {* DO NOT USE with forall-Skolemization: makes fewer schematic variables!! *}
   474   -- {* With ex-Skolemization, makes fewer Skolem constants *}
   475   and meson_disj_exD1: "!!P Q. (\<exists>x. P(x)) | Q ==> \<exists>x. P(x) | Q"
   476   and meson_disj_exD2: "!!P Q. P | (\<exists>x. Q(x)) ==> \<exists>x. P | Q(x)"
   477   by fast+
   478 
   479 
   480 subsubsection {* Generating clauses for the Meson Proof Procedure *}
   481 
   482 text {* Disjunctions *}
   483 
   484 lemma meson_disj_assoc: "(P|Q)|R ==> P|(Q|R)"
   485   and meson_disj_comm: "P|Q ==> Q|P"
   486   and meson_disj_FalseD1: "False|P ==> P"
   487   and meson_disj_FalseD2: "P|False ==> P"
   488   by fast+
   489 
   490 
   491 subsection{*Lemmas for Meson, the Model Elimination Procedure*}
   492 
   493 
   494 text{* Generation of contrapositives *}
   495 
   496 text{*Inserts negated disjunct after removing the negation; P is a literal.
   497   Model elimination requires assuming the negation of every attempted subgoal,
   498   hence the negated disjuncts.*}
   499 lemma make_neg_rule: "~P|Q ==> ((~P==>P) ==> Q)"
   500 by blast
   501 
   502 text{*Version for Plaisted's "Postive refinement" of the Meson procedure*}
   503 lemma make_refined_neg_rule: "~P|Q ==> (P ==> Q)"
   504 by blast
   505 
   506 text{*@{term P} should be a literal*}
   507 lemma make_pos_rule: "P|Q ==> ((P==>~P) ==> Q)"
   508 by blast
   509 
   510 text{*Versions of @{text make_neg_rule} and @{text make_pos_rule} that don't
   511 insert new assumptions, for ordinary resolution.*}
   512 
   513 lemmas make_neg_rule' = make_refined_neg_rule
   514 
   515 lemma make_pos_rule': "[|P|Q; ~P|] ==> Q"
   516 by blast
   517 
   518 text{* Generation of a goal clause -- put away the final literal *}
   519 
   520 lemma make_neg_goal: "~P ==> ((~P==>P) ==> False)"
   521 by blast
   522 
   523 lemma make_pos_goal: "P ==> ((P==>~P) ==> False)"
   524 by blast
   525 
   526 
   527 subsubsection{* Lemmas for Forward Proof*}
   528 
   529 text{*There is a similarity to congruence rules*}
   530 
   531 (*NOTE: could handle conjunctions (faster?) by
   532     nf(th RS conjunct2) RS (nf(th RS conjunct1) RS conjI) *)
   533 lemma conj_forward: "[| P'&Q';  P' ==> P;  Q' ==> Q |] ==> P&Q"
   534 by blast
   535 
   536 lemma disj_forward: "[| P'|Q';  P' ==> P;  Q' ==> Q |] ==> P|Q"
   537 by blast
   538 
   539 (*Version of @{text disj_forward} for removal of duplicate literals*)
   540 lemma disj_forward2:
   541     "[| P'|Q';  P' ==> P;  [| Q'; P==>False |] ==> Q |] ==> P|Q"
   542 apply blast 
   543 done
   544 
   545 lemma all_forward: "[| \<forall>x. P'(x);  !!x. P'(x) ==> P(x) |] ==> \<forall>x. P(x)"
   546 by blast
   547 
   548 lemma ex_forward: "[| \<exists>x. P'(x);  !!x. P'(x) ==> P(x) |] ==> \<exists>x. P(x)"
   549 by blast
   550 
   551 ML
   552 {*
   553 val inv_def = thm "inv_def";
   554 val Inv_def = thm "Inv_def";
   555 
   556 val someI = thm "someI";
   557 val someI_ex = thm "someI_ex";
   558 val someI2 = thm "someI2";
   559 val someI2_ex = thm "someI2_ex";
   560 val some_equality = thm "some_equality";
   561 val some1_equality = thm "some1_equality";
   562 val some_eq_ex = thm "some_eq_ex";
   563 val some_eq_trivial = thm "some_eq_trivial";
   564 val some_sym_eq_trivial = thm "some_sym_eq_trivial";
   565 val choice = thm "choice";
   566 val bchoice = thm "bchoice";
   567 val inv_id = thm "inv_id";
   568 val inv_f_f = thm "inv_f_f";
   569 val inv_f_eq = thm "inv_f_eq";
   570 val inj_imp_inv_eq = thm "inj_imp_inv_eq";
   571 val inj_transfer = thm "inj_transfer";
   572 val inj_iff = thm "inj_iff";
   573 val inj_imp_surj_inv = thm "inj_imp_surj_inv";
   574 val f_inv_f = thm "f_inv_f";
   575 val surj_f_inv_f = thm "surj_f_inv_f";
   576 val inv_injective = thm "inv_injective";
   577 val inj_on_inv = thm "inj_on_inv";
   578 val surj_imp_inj_inv = thm "surj_imp_inj_inv";
   579 val surj_iff = thm "surj_iff";
   580 val surj_imp_inv_eq = thm "surj_imp_inv_eq";
   581 val bij_imp_bij_inv = thm "bij_imp_bij_inv";
   582 val inv_equality = thm "inv_equality";
   583 val inv_inv_eq = thm "inv_inv_eq";
   584 val o_inv_distrib = thm "o_inv_distrib";
   585 val image_surj_f_inv_f = thm "image_surj_f_inv_f";
   586 val image_inv_f_f = thm "image_inv_f_f";
   587 val inv_image_comp = thm "inv_image_comp";
   588 val bij_image_Collect_eq = thm "bij_image_Collect_eq";
   589 val bij_vimage_eq_inv_image = thm "bij_vimage_eq_inv_image";
   590 val Inv_f_f = thm "Inv_f_f";
   591 val f_Inv_f = thm "f_Inv_f";
   592 val Inv_injective = thm "Inv_injective";
   593 val inj_on_Inv = thm "inj_on_Inv";
   594 val split_paired_Eps = thm "split_paired_Eps";
   595 val Eps_split = thm "Eps_split";
   596 val Eps_split_eq = thm "Eps_split_eq";
   597 val wf_iff_no_infinite_down_chain = thm "wf_iff_no_infinite_down_chain";
   598 val Inv_mem = thm "Inv_mem";
   599 val Inv_f_eq = thm "Inv_f_eq";
   600 val Inv_comp = thm "Inv_comp";
   601 val tfl_some = thm "tfl_some";
   602 val make_neg_rule = thm "make_neg_rule";
   603 val make_refined_neg_rule = thm "make_refined_neg_rule";
   604 val make_pos_rule = thm "make_pos_rule";
   605 val make_neg_rule' = thm "make_neg_rule'";
   606 val make_pos_rule' = thm "make_pos_rule'";
   607 val make_neg_goal = thm "make_neg_goal";
   608 val make_pos_goal = thm "make_pos_goal";
   609 val conj_forward = thm "conj_forward";
   610 val disj_forward = thm "disj_forward";
   611 val disj_forward2 = thm "disj_forward2";
   612 val all_forward = thm "all_forward";
   613 val ex_forward = thm "ex_forward";
   614 *}
   615 
   616 
   617 use "Tools/meson.ML"
   618 setup meson_setup
   619 
   620 use "Tools/specification_package.ML"
   621 
   622 end