1(* ========================================================================= * 2 * * 3 * Coinductive Definitions * 4 * * 5 * ========================================================================= *) 6 7structure CoIndDefLib :> CoIndDefLib = 8struct 9 10open HolKernel boolLib liteLib InductiveDefinition IndDefLib 11 12val ERR = mk_HOL_ERR "CoIndDefLib" 13 14(* Prove definitions work for non-schematic relations with canonical rules. *) 15 16fun derive_canon_coinductive_relations pclauses = 17 let val (vargs, bodies) = split(map strip_forall pclauses) 18 val swap_fn = fn (x, y) => (y, x) 19 val bodies = map mk_imp (map swap_fn (map dest_imp bodies)) 20 val pclauses = map list_mk_forall (zip vargs bodies) 21 val closed = list_mk_conj pclauses 22 val (ants, concs) = split (map dest_imp bodies) 23 val rels = map (repeat rator) ants 24 val avoids = all_vars closed 25 val rels' = variants avoids rels 26 val prime_fn = subst (map2 (curry op |->) rels rels' ) 27 val closed' = prime_fn closed 28 29 (* definition theorems *) 30 fun mk_def arg ant = 31 mk_eq(repeat rator ant, 32 list_mk_abs(arg,list_mk_exists(rels', 33 mk_conj(prime_fn ant, closed')))) 34 val deftms = map2 mk_def vargs ants 35 val defthms = map2 HALF_BETA_EXPAND vargs (map ASSUME deftms) 36 37 (* coinductive theorems *) 38 fun rm_exists_left th = 39 let val ant = fst (dest_imp (concl th)) 40 val (vars, conj) = strip_exists ant 41 val ex_fn = fn (v, t) => EXISTS(mk_exists(v, concl t), v) t 42 val ex = foldl ex_fn (ASSUME conj) (rev vars) 43 val th1 = PROVE_HYP ex (UNDISCH th) 44 val (c1, c2) = dest_conj conj 45 val th2 = CONJ (ASSUME c1) (ASSUME c2) 46 in DISCH c1 (PROVE_HYP th2 th1) 47 end 48 49 fun mk_coind args th = 50 let val th = snd(EQ_IMP_RULE(SPEC_ALL th)) 51 in GENL args (rm_exists_left th) 52 end 53 val coindthms = map2 mk_coind vargs defthms 54 val coindthmr = end_itlist CONJ coindthms 55 val coindthm = GENL rels'(DISCH closed' coindthmr) 56 57 (* mono theorems *) 58 val mants = map2 (fn a => fn t => 59 list_mk_forall(a,mk_imp(prime_fn t, t))) vargs concs 60 val monotm = mk_imp(concl coindthmr, list_mk_conj mants) 61 val monothm = ASSUME(list_mk_forall(rels,list_mk_forall(rels',monotm))) 62 val closthm = ASSUME closed' 63 val monothms = CONJUNCTS 64 (MP (SPEC_ALL monothm) (MP (SPECL rels' coindthm) closthm)) 65 val closthms = CONJUNCTS closthm 66 67 (* rules *) 68 fun intro_exists_left th = 69 let val conj1 = fst (dest_imp (concl th)) 70 val conj = mk_conj(conj1, closed') 71 val A = CONJUNCT1(ASSUME conj); 72 val B = CONJUNCT2(ASSUME conj); 73 val step1 = PROVE_HYP A (UNDISCH th); 74 val step2 = PROVE_HYP B step1; 75 val ex_fn = fn (v, (t1, t2)) => 76 (mk_exists(v, t1), CHOOSE(v, ASSUME (mk_exists(v, t1))) t2) 77 in foldl ex_fn (conj, step2) (rev rels') 78 end 79 80 fun prove_rule mth (cth,dth) = 81 let val (avs, bod) = strip_forall(concl mth) 82 val th1 = IMP_TRANS (SPECL avs cth) (SPECL avs mth) 83 val (ex, th1') = intro_exists_left th1 84 val th2 = DISCH ex th1' 85 val th3 = IMP_TRANS (fst(EQ_IMP_RULE(SPECL avs dth))) th2 86 in GENL avs th3 87 end 88 val ruvalhms = map2 prove_rule monothms (zip closthms defthms) 89 val ruvalhm = end_itlist CONJ ruvalhms 90 91 (* cases *) 92 val dtms = map2 (curry list_mk_abs) vargs concs 93 val double_fn = subst (map2 (curry op |->) rels dtms) 94 fun mk_unbetas tm dtm = 95 let val (avs,bod) = strip_forall tm 96 val (il,r) = dest_comb bod 97 val (i,l) = dest_comb il 98 val bth = RIGHT_BETAS avs (REFL dtm) 99 val munb = AP_THM (AP_TERM i bth) l 100 val iunb = AP_THM (AP_TERM i bth) (double_fn r) 101 val junb = AP_TERM (mk_comb(i,l)) bth 102 val quantify = itlist MK_FORALL avs 103 in (quantify junb,(quantify iunb,quantify munb)) 104 end 105 val unths = map2 mk_unbetas pclauses dtms 106 val irthm = EQ_MP (SYM(end_itlist MK_CONJ (map fst unths))) ruvalhm 107 val mrthm = MP (SPECL rels (SPECL dtms monothm)) irthm 108 val imrth = EQ_MP 109 (SYM(end_itlist MK_CONJ (map (fst o snd) unths))) mrthm 110 val ifthm = MP (SPECL dtms coindthm) imrth 111 val fthm = EQ_MP (end_itlist MK_CONJ (map (snd o snd) unths)) ifthm 112 fun mk_case th1 th2 = 113 let val avs = fst(strip_forall(concl th1)) 114 in GENL avs (IMP_ANTISYM_RULE (SPEC_ALL th2) (SPEC_ALL th1)) 115 end 116 val casethm = end_itlist CONJ 117 (map2 mk_case (CONJUNCTS fthm) (CONJUNCTS ruvalhm)) 118 in CONJ fthm (CONJ coindthm casethm) 119 end 120 handle e => raise (wrap_exn "CoIndDefLib" 121 "derive_canon_coinductive_relations"e); 122 123 124 125(* General case for nonschematic relations; monotonicity & defn hyps. *) 126 127fun derive_nonschematic_coinductive_relations tm = 128 let val clauses = strip_conj tm 129 val canonthm = canonicalize_clauses clauses 130 val canonthm' = SYM canonthm 131 val pclosed = rand(concl canonthm) 132 val pclauses = strip_conj pclosed 133 val rawthm = derive_canon_coinductive_relations pclauses 134 val (ruvalhm,otherthms) = CONJ_PAIR rawthm 135 val (indthm,casethm) = CONJ_PAIR otherthms 136 val ruvalhm' = EQ_MP canonthm' ruvalhm 137 and indthm' = CONV_RULE (ONCE_DEPTH_CONV (REWR_CONV canonthm')) indthm 138 in CONJ ruvalhm' (CONJ indthm' casethm) 139 end 140 handle e => raise (wrap_exn "CoIndDefLib" 141 "derive_nonschematic_coinductive_relations" e); 142 143 144fun new_coinductive_definition monoset stem (tm,clocs) = 145 let val clauses = strip_conj tm 146 val (clauses',fvs) = unschematize_clauses clauses 147 val _ = check_definition fvs clocs (list_mk_conj clauses') 148 val th0 = derive_nonschematic_coinductive_relations 149 (check_definition fvs clocs (list_mk_conj clauses')) 150 val th1 = prove_monotonicity_hyps monoset th0 151 val th2 = generalize_schematic_variables fvs th1 152 val th3 = make_definitions stem th2 153 val avs = fst(strip_forall(concl th3)) 154 val (r,ic) = CONJ_PAIR(SPECL avs th3) 155 val (i,c) = CONJ_PAIR ic 156 in (GENL avs r, GENL avs i, GENL avs c) 157 end 158 handle e => raise wrap_exn "CoIndDefLib" "new_coinductive_definition" e; 159 160 161(* ------------------------------------------------------------------------- *) 162 163fun save_theorems name (rules, coind, strong_ind, cases) = let 164in 165 save_thm(name^"_rules", rules); 166 save_thm(name^"_coind", coind); 167 (* save_thm(name^"_strongind", strong_ind);*) 168 save_thm(name^"_cases", cases); 169 (* export_rule_induction (name ^ "_strongind") *) 170 () 171end 172 173fun derive_strong_coinduction (rules, coind) = ((* TODO *)) 174 175(* ------------------------------------------------------------------------- ) 176( Entrypoints: *) 177 178fun Hol_mono_coreln name monoset tm = let 179 val _ = Lexis.ok_sml_identifier (name ^ !boolLib.def_suffix) orelse 180 raise ERR "Hol_mono_coreln" 181 ("Bad name for definition: "^ Lib.mlquote name^ 182 " (use xHol_coreln to specify a better)") 183 val (rules, coind, cases) = new_coinductive_definition monoset name tm 184 val strong_ind = derive_strong_coinduction (rules, coind) 185in 186 save_theorems name (rules, coind, strong_ind, cases); 187 (rules, coind, cases) 188end 189handle e => raise (wrap_exn "CoIndDefLib" "Hol_mono_coreln" e); 190 191fun xHol_coreln name q = 192 Hol_mono_coreln name (!IndDefLib.the_monoset) (IndDefLib.term_of q) 193 194fun Hol_coreln q = let 195 val parse = IndDefLib.term_of 196 |> trace ("syntax_error", 0) 197 |> trace ("show_typecheck_errors", 0) 198 val def as (def_t, _) = parse q 199 val name = IndDefLib.name_from_def def_t 200in 201 Hol_mono_coreln name (!IndDefLib.the_monoset) def 202end handle e => Raise (wrap_exn "CoIndDefLib" "Hol_coreln" e); 203 204 205end (* CoIndDefLib *) 206