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