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