1(*---------------------------------------------------------------------------*)
2(*  DEFCHOOSE (sname, cname,``!x1 ... xn. ?z. M[x1,...,xn,z]``)              *)
3(*   returns                                                                 *)
4(*                                                                           *)
5(*    |- !x1...xn z. M[x1,...,xn,z] ==> M[x1,...,xn,cname x1...xn]           *)
6(*                                                                           *)
7(* where cname on the rhs of the implication is a constant. This theorem is  *)
8(* stored in the current theory under sname. So this rule is just            *)
9(* Skolemization exactly as done in FOL, where the Skolem fn. can't be       *)
10(* expressed as a first class citizen, as it can be in HOL.                  *)
11(*---------------------------------------------------------------------------*)
12
13fun DEFCHOOSE (store_name,const_name,tm) = 
14 let val (V,body) = strip_forall tm
15     val (z,M) = dest_exists body
16     val zname = fst(dest_var z)
17     val tm1 = mk_exists (z,M)
18     val th0 = GSYM RIGHT_EXISTS_IMP_THM
19     val th1 = SPEC tm1 th0
20     val th2 = BETA_RULE (ISPEC (mk_abs(z,M)) th1)
21     val th3 = EQ_MP th2 (DISCH_ALL (ASSUME tm1))
22     val th4 = GENL V th3
23     val th5 = Ho_Rewrite.REWRITE_RULE[SKOLEM_THM] th4
24     val th6 = Ho_Rewrite.REWRITE_RULE[GSYM LEFT_FORALL_IMP_THM] th5
25     val fvar = mk_var(const_name,snd(dest_var(fst(dest_exists(concl th6)))))
26     val th7a = GEN_ALPHA_CONV fvar (concl th6)
27     val th7 = EQ_MP th7a th6
28 in
29   new_specification(store_name, [const_name], th6)
30 end
31 handle e => raise wrap_exn "" "DEFCHOOSE" e;
32
33
34(*---------------------------------------------------------------------------*)
35(*  MINCHOOSE (sname, cname,``!x1 ... xn. ?z. M[x1,...,xn,z]``)              *)
36(*   returns                                                                 *)
37(*                                                                           *)
38(*    |- !x1...xn z. M[x1,...,xn,z] ==>                                      *)
39(*                   M[x1,...,xn,cname x1...xn] /\                           *)
40(*                   !m. M[x1,...,xn,m] ==> cname x1...xn <= m               *)
41(*                                                                           *)
42(* where cname in the theorem is a constant. This theorem is stored in the   *)
43(* current theory under sname. Thus this rule is a form of the               *)
44(* well-ordering property.                                                   *)
45(*---------------------------------------------------------------------------*)
46
47val WOP_THM = Q.prove
48(`!P. (?n. P n) ==> ?min. P min /\ !k. P k ==> min <= k`,
49 METIS_TAC [arithmeticTheory.WOP,DECIDE ``~(m<n) ==> n<=m``]);
50
51fun MINCHOOSE (store_name,const_name,tm) = 
52 let val (V,body) = strip_forall tm
53     val P = snd(dest_comb body)
54     val wop_thm = BETA_RULE(SPEC P WOP_THM)
55     val min_term = snd(dest_imp (concl wop_thm))
56     val min_term_pred = snd(dest_comb min_term)
57     val th1 = BETA_RULE(GSYM (ISPECL [body,min_term_pred] RIGHT_EXISTS_IMP_THM))
58     val th2 = EQ_MP th1 wop_thm
59     val th3 = GENL V th2
60     val th4 = Ho_Rewrite.REWRITE_RULE[SKOLEM_THM] th3
61     val th5 = Ho_Rewrite.REWRITE_RULE[GSYM LEFT_FORALL_IMP_THM] th4
62 in
63  new_specification(store_name, [const_name], th5)
64 end
65 handle e => raise wrap_exn "" "MINCHOOSE" e;
66