|
1 (* Title: HOL/intr_elim.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1994 University of Cambridge |
|
5 |
|
6 Introduction/elimination rule module -- for Inductive/Coinductive Definitions |
|
7 *) |
|
8 |
|
9 signature INDUCTIVE_ARG = (** Description of a (co)inductive def **) |
|
10 sig |
|
11 val thy : theory (*new theory with inductive defs*) |
|
12 val monos : thm list (*monotonicity of each M operator*) |
|
13 val con_defs : thm list (*definitions of the constructors*) |
|
14 end; |
|
15 |
|
16 (*internal items*) |
|
17 signature INDUCTIVE_I = |
|
18 sig |
|
19 val rec_tms : term list (*the recursive sets*) |
|
20 val intr_tms : term list (*terms for the introduction rules*) |
|
21 end; |
|
22 |
|
23 signature INTR_ELIM = |
|
24 sig |
|
25 val thy : theory (*copy of input theory*) |
|
26 val defs : thm list (*definitions made in thy*) |
|
27 val mono : thm (*monotonicity for the lfp definition*) |
|
28 val unfold : thm (*fixed-point equation*) |
|
29 val intrs : thm list (*introduction rules*) |
|
30 val elim : thm (*case analysis theorem*) |
|
31 val raw_induct : thm (*raw induction rule from Fp.induct*) |
|
32 val mk_cases : thm list -> string -> thm (*generates case theorems*) |
|
33 val rec_names : string list (*names of recursive sets*) |
|
34 end; |
|
35 |
|
36 (*prove intr/elim rules for a fixedpoint definition*) |
|
37 functor Intr_elim_Fun |
|
38 (structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end |
|
39 and Fp: FP) : INTR_ELIM = |
|
40 struct |
|
41 open Logic Inductive Ind_Syntax; |
|
42 |
|
43 val rec_names = map (#1 o dest_Const o head_of) rec_tms; |
|
44 val big_rec_name = space_implode "_" rec_names; |
|
45 |
|
46 val _ = deny (big_rec_name mem map ! (stamps_of_thy thy)) |
|
47 ("Definition " ^ big_rec_name ^ |
|
48 " would clash with the theory of the same name!"); |
|
49 |
|
50 (*fetch fp definitions from the theory*) |
|
51 val big_rec_def::part_rec_defs = |
|
52 map (get_def thy) |
|
53 (case rec_names of [_] => rec_names | _ => big_rec_name::rec_names); |
|
54 |
|
55 |
|
56 val sign = sign_of thy; |
|
57 |
|
58 (********) |
|
59 val _ = writeln " Proving monotonicity..."; |
|
60 |
|
61 val Const("==",_) $ _ $ (Const(_,fpT) $ fp_abs) = |
|
62 big_rec_def |> rep_thm |> #prop |> unvarify; |
|
63 |
|
64 (*For the type of the argument of mono*) |
|
65 val [monoT] = binder_types fpT; |
|
66 |
|
67 val mono = |
|
68 prove_goalw_cterm [] |
|
69 (cterm_of sign (mk_tprop (Const("mono", monoT-->boolT) $ fp_abs))) |
|
70 (fn _ => |
|
71 [rtac monoI 1, |
|
72 REPEAT (ares_tac (basic_monos @ monos) 1)]); |
|
73 |
|
74 val unfold = standard (mono RS (big_rec_def RS Fp.Tarski)); |
|
75 |
|
76 (********) |
|
77 val _ = writeln " Proving the introduction rules..."; |
|
78 |
|
79 fun intro_tacsf disjIn prems = |
|
80 [(*insert prems and underlying sets*) |
|
81 cut_facts_tac prems 1, |
|
82 rtac (unfold RS ssubst) 1, |
|
83 REPEAT (resolve_tac [Part_eqI,CollectI] 1), |
|
84 (*Now 1-2 subgoals: the disjunction, perhaps equality.*) |
|
85 rtac disjIn 1, |
|
86 REPEAT (ares_tac [refl,exI,conjI] 1)]; |
|
87 |
|
88 (*combines disjI1 and disjI2 to access the corresponding nested disjunct...*) |
|
89 val mk_disj_rls = |
|
90 let fun f rl = rl RS disjI1 |
|
91 and g rl = rl RS disjI2 |
|
92 in accesses_bal(f, g, asm_rl) end; |
|
93 |
|
94 val intrs = map (uncurry (prove_goalw_cterm part_rec_defs)) |
|
95 (map (cterm_of sign) intr_tms ~~ |
|
96 map intro_tacsf (mk_disj_rls(length intr_tms))); |
|
97 |
|
98 (********) |
|
99 val _ = writeln " Proving the elimination rule..."; |
|
100 |
|
101 (*Includes rules for Suc and Pair since they are common constructions*) |
|
102 val elim_rls = [asm_rl, FalseE, Suc_neq_Zero, Zero_neq_Suc, |
|
103 make_elim Suc_inject, |
|
104 refl_thin, conjE, exE, disjE]; |
|
105 |
|
106 (*Breaks down logical connectives in the monotonic function*) |
|
107 val basic_elim_tac = |
|
108 REPEAT (SOMEGOAL (eresolve_tac (elim_rls@sumprod_free_SEs) |
|
109 ORELSE' bound_hyp_subst_tac)) |
|
110 THEN prune_params_tac; |
|
111 |
|
112 val elim = rule_by_tactic basic_elim_tac (unfold RS equals_CollectD); |
|
113 |
|
114 (*Applies freeness of the given constructors, which *must* be unfolded by |
|
115 the given defs. Cannot simply use the local con_defs because con_defs=[] |
|
116 for inference systems. *) |
|
117 fun con_elim_tac defs = |
|
118 rewrite_goals_tac defs THEN basic_elim_tac THEN fold_tac defs; |
|
119 |
|
120 (*String s should have the form t:Si where Si is an inductive set*) |
|
121 fun mk_cases defs s = |
|
122 rule_by_tactic (con_elim_tac defs) |
|
123 (assume_read thy s RS elim); |
|
124 |
|
125 val defs = big_rec_def::part_rec_defs; |
|
126 |
|
127 val raw_induct = standard ([big_rec_def, mono] MRS Fp.induct); |
|
128 end; |
|
129 |