recursion.ml

   1 (* ========================================================================= *)
   2 (* Definition by primitive recursion and other tools for inductive types.    *)
   3 (*                                                                           *)
   4 (*       John Harrison, University of Cambridge Computer Laboratory          *)
   5 (*                                                                           *)
   6 (*            (c) Copyright, University of Cambridge 1998                    *)
   7 (*              (c) Copyright, John Harrison 1998-2007                       *)
   8 (* ========================================================================= *)
   9
  10 needs "nums.ml";;
  11
  12 (* ------------------------------------------------------------------------- *)
  13 (* Prove existence of recursive function. The inner "raw" version requires   *)
  14 (* exact correspondence with recursion theorem; "canon" requires the         *)
  15 (* PR argument to come first in the arg list; the outer one is more general. *)
  16 (* ------------------------------------------------------------------------- *)
  17
  18 let prove_recursive_functions_exist =
  19   let prove_raw_recursive_functions_exist ax tm =
  20     let rawcls = conjuncts tm in
  21     let spcls = map (snd o strip_forall) rawcls in
  22     let lpats = map (strip_comb o lhand) spcls in
  23     let ufns = itlist (insert o fst) lpats [] in
  24     let axth = SPEC_ALL ax in
  25     let exvs,axbody = strip_exists (concl axth) in
  26     let axcls = conjuncts axbody in
  27     let f = fst o dest_const o repeat rator o rand o
  28             lhand o snd o strip_forall in
  29     let findax = C assoc (map (fun t -> f t,t) axcls) in
  30     let raxs =
  31       map (findax o fst o dest_const o repeat rator o hd o snd) lpats in
  32     let axfns = map (repeat rator o lhand o snd o strip_forall) raxs in
  33     let urfns = map (fun v -> assocd v (setify (zip axfns (map fst lpats))) v)
  34                     exvs in
  35     let axtm = list_mk_exists(exvs,list_mk_conj raxs)
  36     and urtm = list_mk_exists(urfns,tm) in
  37     let insts = term_match [] axtm urtm in
  38     let ixth = INSTANTIATE insts axth in
  39     let ixvs,ixbody = strip_exists (concl ixth) in
  40     let ixtm = subst (zip urfns ixvs) ixbody in
  41     let ixths = CONJUNCTS (ASSUME ixtm) in
  42     let rixths = map (fun t -> find (aconv t o concl) ixths) rawcls in
  43     let rixth = itlist SIMPLE_EXISTS ufns (end_itlist CONJ rixths) in
  44     PROVE_HYP ixth (itlist SIMPLE_CHOOSE urfns rixth) in
  45   let canonize t =
  46     let avs,bod = strip_forall t in
  47     let l,r = dest_eq bod in
  48     let fn,args = strip_comb l in
  49     let rarg = hd args
  50     and vargs = tl args in
  51     let l' = mk_comb(fn,rarg)
  52     and r' = list_mk_abs(vargs,r) in
  53     let fvs = frees rarg in
  54     let def = ASSUME(list_mk_forall(fvs,mk_eq(l',r'))) in
  55     GENL avs (RIGHT_BETAS vargs (SPECL fvs def)) in
  56   let prove_canon_recursive_functions_exist ax tm =
  57     let ths = map canonize (conjuncts tm) in
  58     let atm = list_mk_conj (map (hd o hyp) ths) in
  59     let aths = CONJUNCTS(ASSUME atm) in
  60     let rth = end_itlist CONJ (map2 PROVE_HYP aths ths) in
  61     let eth = prove_raw_recursive_functions_exist ax atm in
  62     let evs = fst(strip_exists(concl eth)) in
  63     PROVE_HYP eth (itlist SIMPLE_CHOOSE evs (itlist SIMPLE_EXISTS evs rth)) in
  64   let reshuffle fn args acc =
  65     let args' = uncurry (C (@)) (partition is_var args) in
  66     if args = args' then acc else
  67     let gvs = map (genvar o type_of) args in
  68     let gvs' = map (C assoc (zip args gvs)) args' in
  69     let lty = itlist (mk_fun_ty o type_of) gvs'
  70               (funpow (length gvs) (hd o tl o snd o dest_type) (type_of fn)) in
  71     let fn' = genvar lty in
  72     let def = mk_eq(fn,list_mk_abs(gvs,list_mk_comb(fn',gvs'))) in
  73     (ASSUME def)::acc
  74   and scrub_def t th =
  75     let l,r = dest_eq t in
  76     MP (INST [r,l] (DISCH t th)) (REFL r) in
  77   fun ax tm ->
  78     let rawcls = conjuncts tm in
  79     let spcls = map (snd o strip_forall) rawcls in
  80     let lpats = map (strip_comb o lhand) spcls in
  81     let ufns = itlist (insert o fst) lpats [] in
  82     let uxargs = map (C assoc lpats) ufns in
  83     let trths = itlist2 reshuffle ufns uxargs [] in
  84     let tth = GEN_REWRITE_CONV REDEPTH_CONV (BETA_THM::trths) tm in
  85     let eth = prove_canon_recursive_functions_exist ax (rand(concl tth)) in
  86     let evs,ebod = strip_exists(concl eth) in
  87     let fth = itlist SIMPLE_EXISTS ufns (EQ_MP (SYM tth) (ASSUME ebod)) in
  88     let gth = itlist scrub_def (map concl trths) fth in
  89     PROVE_HYP eth (itlist SIMPLE_CHOOSE evs gth);;
  90
  91 (* ------------------------------------------------------------------------- *)
  92 (* Version that defines function(s).                                         *)
  93 (* ------------------------------------------------------------------------- *)
  94
  95 let new_recursive_definition =
  96   let the_recursive_definitions = ref [] in
  97   let find_redefinition tm th =
  98     let th' = PART_MATCH I th tm in
  99     ignore(PART_MATCH I th' (concl th)); th' in
 100   fun ax tm ->
 101     try let th = tryfind (find_redefinition tm) (!the_recursive_definitions) in
 102         warn true "Benign redefinition of recursive function"; th
 103     with Failure _ ->
 104     let rawcls = conjuncts tm in
 105     let spcls = map (snd o strip_forall) rawcls in
 106     let lpats = map (strip_comb o lhand) spcls in
 107     let ufns = itlist (insert o fst) lpats [] in
 108     let fvs = map (fun t -> subtract (frees t) ufns) rawcls in
 109     let gcls = map2 (curry list_mk_forall) fvs rawcls in
 110     let eth = prove_recursive_functions_exist ax (list_mk_conj gcls) in
 111     let evs,bod = strip_exists(concl eth) in
 112     let dth = new_specification (map (fst o dest_var) evs) eth in
 113     let dths = map2 SPECL fvs (CONJUNCTS dth) in
 114     let th = end_itlist CONJ dths in
 115     the_recursive_definitions := th::(!the_recursive_definitions); th;;