1 (* Title: HOL/intr_elim.ML |
1 (* Title: HOL/intr_elim.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1994 University of Cambridge |
4 Copyright 1994 University of Cambridge |
5 |
5 |
6 Introduction/elimination rule module -- for Inductive/Coinductive Definitions |
6 Introduction/elimination rule module -- for Inductive/Coinductive Definitions |
7 *) |
7 *) |
8 |
8 |
9 signature INDUCTIVE_ARG = (** Description of a (co)inductive def **) |
9 signature INDUCTIVE_ARG = (** Description of a (co)inductive def **) |
10 sig |
10 sig |
11 val thy : theory (*new theory with inductive defs*) |
11 val thy : theory (*new theory with inductive defs*) |
12 val monos : thm list (*monotonicity of each M operator*) |
12 val monos : thm list (*monotonicity of each M operator*) |
13 val con_defs : thm list (*definitions of the constructors*) |
13 val con_defs : thm list (*definitions of the constructors*) |
14 end; |
14 end; |
15 |
15 |
16 |
16 |
17 signature INDUCTIVE_I = (** Terms read from the theory section **) |
17 signature INDUCTIVE_I = (** Terms read from the theory section **) |
18 sig |
18 sig |
19 val rec_tms : term list (*the recursive sets*) |
19 val rec_tms : term list (*the recursive sets*) |
20 val intr_tms : term list (*terms for the introduction rules*) |
20 val intr_tms : term list (*terms for the introduction rules*) |
21 end; |
21 end; |
22 |
22 |
23 signature INTR_ELIM = |
23 signature INTR_ELIM = |
24 sig |
24 sig |
25 val thy : theory (*copy of input theory*) |
25 val thy : theory (*copy of input theory*) |
26 val defs : thm list (*definitions made in thy*) |
26 val defs : thm list (*definitions made in thy*) |
27 val mono : thm (*monotonicity for the lfp definition*) |
27 val mono : thm (*monotonicity for the lfp definition*) |
28 val intrs : thm list (*introduction rules*) |
28 val intrs : thm list (*introduction rules*) |
29 val elim : thm (*case analysis theorem*) |
29 val elim : thm (*case analysis theorem*) |
30 val mk_cases : thm list -> string -> thm (*generates case theorems*) |
30 val mk_cases : thm list -> string -> thm (*generates case theorems*) |
31 end; |
31 end; |
32 |
32 |
33 signature INTR_ELIM_AUX = (** Used to make induction rules **) |
33 signature INTR_ELIM_AUX = (** Used to make induction rules **) |
34 sig |
34 sig |
35 val raw_induct : thm (*raw induction rule from Fp.induct*) |
35 val raw_induct : thm (*raw induction rule from Fp.induct*) |
36 val rec_names : string list (*names of recursive sets*) |
36 val rec_names : string list (*names of recursive sets*) |
37 end; |
37 end; |
38 |
38 |
39 (*prove intr/elim rules for a fixedpoint definition*) |
39 (*prove intr/elim rules for a fixedpoint definition*) |
40 functor Intr_elim_Fun |
40 functor Intr_elim_Fun |
41 (structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end |
41 (structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end |
45 val rec_names = map (#1 o dest_Const o head_of) Inductive.rec_tms; |
45 val rec_names = map (#1 o dest_Const o head_of) Inductive.rec_tms; |
46 val big_rec_name = space_implode "_" rec_names; |
46 val big_rec_name = space_implode "_" rec_names; |
47 |
47 |
48 val _ = deny (big_rec_name mem map ! (stamps_of_thy Inductive.thy)) |
48 val _ = deny (big_rec_name mem map ! (stamps_of_thy Inductive.thy)) |
49 ("Definition " ^ big_rec_name ^ |
49 ("Definition " ^ big_rec_name ^ |
50 " would clash with the theory of the same name!"); |
50 " would clash with the theory of the same name!"); |
51 |
51 |
52 (*fetch fp definitions from the theory*) |
52 (*fetch fp definitions from the theory*) |
53 val big_rec_def::part_rec_defs = |
53 val big_rec_def::part_rec_defs = |
54 map (get_def Inductive.thy) |
54 map (get_def Inductive.thy) |
55 (case rec_names of [_] => rec_names | _ => big_rec_name::rec_names); |
55 (case rec_names of [_] => rec_names | _ => big_rec_name::rec_names); |
67 val [monoT] = binder_types fpT; |
67 val [monoT] = binder_types fpT; |
68 |
68 |
69 val mono = |
69 val mono = |
70 prove_goalw_cterm [] |
70 prove_goalw_cterm [] |
71 (cterm_of sign (Ind_Syntax.mk_Trueprop |
71 (cterm_of sign (Ind_Syntax.mk_Trueprop |
72 (Const("mono", monoT --> Ind_Syntax.boolT) $ fp_abs))) |
72 (Const("mono", monoT --> Ind_Syntax.boolT) $ fp_abs))) |
73 (fn _ => |
73 (fn _ => |
74 [rtac monoI 1, |
74 [rtac monoI 1, |
75 REPEAT (ares_tac (basic_monos @ Inductive.monos) 1)]); |
75 REPEAT (ares_tac (basic_monos @ Inductive.monos) 1)]); |
76 |
76 |
77 val unfold = standard (mono RS (big_rec_def RS Fp.Tarski)); |
77 val unfold = standard (mono RS (big_rec_def RS Fp.Tarski)); |
78 |
78 |
79 (********) |
79 (********) |
80 val _ = writeln " Proving the introduction rules..."; |
80 val _ = writeln " Proving the introduction rules..."; |
95 |
95 |
96 |
96 |
97 (*combines disjI1 and disjI2 to access the corresponding nested disjunct...*) |
97 (*combines disjI1 and disjI2 to access the corresponding nested disjunct...*) |
98 val mk_disj_rls = |
98 val mk_disj_rls = |
99 let fun f rl = rl RS disjI1 |
99 let fun f rl = rl RS disjI1 |
100 and g rl = rl RS disjI2 |
100 and g rl = rl RS disjI2 |
101 in accesses_bal(f, g, asm_rl) end; |
101 in accesses_bal(f, g, asm_rl) end; |
102 |
102 |
103 val intrs = map (uncurry (prove_goalw_cterm part_rec_defs)) |
103 val intrs = map (uncurry (prove_goalw_cterm part_rec_defs)) |
104 (map (cterm_of sign) Inductive.intr_tms ~~ |
104 (map (cterm_of sign) Inductive.intr_tms ~~ |
105 map intro_tacsf (mk_disj_rls(length Inductive.intr_tms))); |
105 map intro_tacsf (mk_disj_rls(length Inductive.intr_tms))); |
106 |
106 |
107 (********) |
107 (********) |
108 val _ = writeln " Proving the elimination rule..."; |
108 val _ = writeln " Proving the elimination rule..."; |
109 |
109 |
110 (*Breaks down logical connectives in the monotonic function*) |
110 (*Breaks down logical connectives in the monotonic function*) |
111 val basic_elim_tac = |
111 val basic_elim_tac = |
112 REPEAT (SOMEGOAL (eresolve_tac (Ind_Syntax.elim_rls @ |
112 REPEAT (SOMEGOAL (eresolve_tac (Ind_Syntax.elim_rls @ |
113 Ind_Syntax.sumprod_free_SEs) |
113 Ind_Syntax.sumprod_free_SEs) |
114 ORELSE' bound_hyp_subst_tac)) |
114 ORELSE' bound_hyp_subst_tac)) |
115 THEN prune_params_tac; |
115 THEN prune_params_tac; |
116 |
116 |
117 (*Applies freeness of the given constructors, which *must* be unfolded by |
117 (*Applies freeness of the given constructors, which *must* be unfolded by |
118 the given defs. Cannot simply use the local con_defs because con_defs=[] |
118 the given defs. Cannot simply use the local con_defs because con_defs=[] |
119 for inference systems. |
119 for inference systems. |
120 fun con_elim_tac defs = |
120 fun con_elim_tac defs = |
121 rewrite_goals_tac defs THEN basic_elim_tac THEN fold_tac defs; |
121 rewrite_goals_tac defs THEN basic_elim_tac THEN fold_tac defs; |
122 *) |
122 *) |
123 fun con_elim_tac simps = |
123 fun con_elim_tac simps = |
124 let val elim_tac = REPEAT o (eresolve_tac (Ind_Syntax.elim_rls @ |
124 let val elim_tac = REPEAT o (eresolve_tac (Ind_Syntax.elim_rls @ |
125 Ind_Syntax.sumprod_free_SEs)) |
125 Ind_Syntax.sumprod_free_SEs)) |
126 in ALLGOALS(EVERY'[elim_tac, |
126 in ALLGOALS(EVERY'[elim_tac, |
127 asm_full_simp_tac (simpset_of "Nat" addsimps simps), |
127 asm_full_simp_tac (simpset_of "Nat" addsimps simps), |
128 elim_tac, |
128 elim_tac, |
129 REPEAT o bound_hyp_subst_tac]) |
129 REPEAT o bound_hyp_subst_tac]) |
130 THEN prune_params_tac |
130 THEN prune_params_tac |
142 (unfold RS Ind_Syntax.equals_CollectD); |
142 (unfold RS Ind_Syntax.equals_CollectD); |
143 |
143 |
144 (*String s should have the form t:Si where Si is an inductive set*) |
144 (*String s should have the form t:Si where Si is an inductive set*) |
145 fun mk_cases defs s = |
145 fun mk_cases defs s = |
146 rule_by_tactic (con_elim_tac defs) |
146 rule_by_tactic (con_elim_tac defs) |
147 (assume_read Inductive.thy s RS elim); |
147 (assume_read Inductive.thy s RS elim); |
148 |
148 |
149 val raw_induct = standard ([big_rec_def, mono] MRS Fp.induct) |
149 val raw_induct = standard ([big_rec_def, mono] MRS Fp.induct) |
150 and rec_names = rec_names |
150 and rec_names = rec_names |
151 end |
151 end |
152 end; |
152 end; |