1 (* ========================================================================= *)
2 (* Definition by primitive recursion and other tools for inductive types. *)
4 (* John Harrison, University of Cambridge Computer Laboratory *)
6 (* (c) Copyright, University of Cambridge 1998 *)
7 (* (c) Copyright, John Harrison 1998-2007 *)
8 (* ========================================================================= *)
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 (* ------------------------------------------------------------------------- *)
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
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)
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
46 let avs,bod = strip_forall t in
47 let l,r = dest_eq bod in
48 let fn,args = strip_comb l in
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
75 let l,r = dest_eq t in
76 MP (INST [r,l] (DISCH t th)) (REFL r) in
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);;
91 (* ------------------------------------------------------------------------- *)
92 (* Version that defines function(s). *)
93 (* ------------------------------------------------------------------------- *)
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
101 try let th = tryfind (find_redefinition tm) (!the_recursive_definitions) in
102 warn true "Benign redefinition of recursive function"; th
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;;