author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 1461  6bcb44e4d6e5 
child 2033  639de962ded4 
permissions  rwrr 
1461  1 
(* Title: ZF/intr_elim.ML 
0  2 
ID: $Id$ 
1461  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
516  4 
Copyright 1994 University of Cambridge 
0  5 

6 
Introduction/elimination rule module  for Inductive/Coinductive Definitions 

7 
*) 

8 

1461  9 
signature INDUCTIVE_ARG = (** Description of a (co)inductive def **) 
0  10 
sig 
516  11 
val thy : theory (*new theory with inductive defs*) 
1461  12 
val monos : thm list (*monotonicity of each M operator*) 
13 
val con_defs : thm list (*definitions of the constructors*) 

14 
val type_intrs : thm list (*typechecking intro rules*) 

15 
val type_elims : thm list (*typechecking elim rules*) 

0  16 
end; 
17 

1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
909
diff
changeset

18 

1461  19 
signature INDUCTIVE_I = (** Terms read from the theory section **) 
516  20 
sig 
1461  21 
val rec_tms : term list (*the recursive sets*) 
22 
val dom_sum : term (*their common domain*) 

23 
val intr_tms : term list (*terms for the introduction rules*) 

516  24 
end; 
25 

0  26 
signature INTR_ELIM = 
27 
sig 

516  28 
val thy : theory (*copy of input theory*) 
1461  29 
val defs : thm list (*definitions made in thy*) 
30 
val bnd_mono : thm (*monotonicity for the lfp definition*) 

31 
val dom_subset : thm (*inclusion of recursive set in dom*) 

32 
val intrs : thm list (*introduction rules*) 

33 
val elim : thm (*case analysis theorem*) 

34 
val mk_cases : thm list > string > thm (*generates case theorems*) 

1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
909
diff
changeset

35 
end; 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
909
diff
changeset

36 

1461  37 
signature INTR_ELIM_AUX = (** Used to make induction rules **) 
1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
909
diff
changeset

38 
sig 
1461  39 
val raw_induct : thm (*raw induction rule from Fp.induct*) 
40 
val rec_names : string list (*names of recursive sets*) 

0  41 
end; 
42 

516  43 
(*prove intr/elim rules for a fixedpoint definition*) 
44 
functor Intr_elim_Fun 

45 
(structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end 

1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
909
diff
changeset

46 
and Fp: FP and Pr : PR and Su : SU) 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
909
diff
changeset

47 
: sig include INTR_ELIM INTR_ELIM_AUX end = 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
909
diff
changeset

48 
let 
0  49 

1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
909
diff
changeset

50 
val rec_names = map (#1 o dest_Const o head_of) Inductive.rec_tms; 
0  51 
val big_rec_name = space_implode "_" rec_names; 
52 

1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
909
diff
changeset

53 
val _ = deny (big_rec_name mem map ! (stamps_of_thy Inductive.thy)) 
578
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
543
diff
changeset

54 
("Definition " ^ big_rec_name ^ 
1461  55 
" would clash with the theory of the same name!"); 
578
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
543
diff
changeset

56 

516  57 
(*fetch fp definitions from the theory*) 
58 
val big_rec_def::part_rec_defs = 

1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
909
diff
changeset

59 
map (get_def Inductive.thy) 
516  60 
(case rec_names of [_] => rec_names  _ => big_rec_name::rec_names); 
0  61 

62 

1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
909
diff
changeset

63 
val sign = sign_of Inductive.thy; 
0  64 

65 
(********) 

516  66 
val _ = writeln " Proving monotonicity..."; 
67 

68 
val Const("==",_) $ _ $ (_ $ dom_sum $ fp_abs) = 

543
e961b2092869
ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents:
516
diff
changeset

69 
big_rec_def > rep_thm > #prop > Logic.unvarify; 
0  70 

71 
val bnd_mono = 

543
e961b2092869
ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents:
516
diff
changeset

72 
prove_goalw_cterm [] 
1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
909
diff
changeset

73 
(cterm_of sign (Ind_Syntax.mk_tprop (Fp.bnd_mono $ dom_sum $ fp_abs))) 
543
e961b2092869
ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents:
516
diff
changeset

74 
(fn _ => 
0  75 
[rtac (Collect_subset RS bnd_monoI) 1, 
1461  76 
REPEAT (ares_tac (basic_monos @ Inductive.monos) 1)]); 
0  77 

78 
val dom_subset = standard (big_rec_def RS Fp.subs); 

79 

726
d703d1a1a2af
ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents:
652
diff
changeset

80 
val unfold = standard ([big_rec_def, bnd_mono] MRS Fp.Tarski); 
0  81 

82 
(********) 

516  83 
val _ = writeln " Proving the introduction rules..."; 
0  84 

726
d703d1a1a2af
ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents:
652
diff
changeset

85 
(*Mutual recursion? Helps to derive subset rules for the individual sets.*) 
d703d1a1a2af
ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents:
652
diff
changeset

86 
val Part_trans = 
d703d1a1a2af
ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents:
652
diff
changeset

87 
case rec_names of 
d703d1a1a2af
ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents:
652
diff
changeset

88 
[_] => asm_rl 
d703d1a1a2af
ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents:
652
diff
changeset

89 
 _ => standard (Part_subset RS subset_trans); 
d703d1a1a2af
ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents:
652
diff
changeset

90 

d703d1a1a2af
ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents:
652
diff
changeset

91 
(*To typecheck recursive occurrences of the inductive sets, possibly 
d703d1a1a2af
ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents:
652
diff
changeset

92 
enclosed in some monotonic operator M.*) 
d703d1a1a2af
ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents:
652
diff
changeset

93 
val rec_typechecks = 
1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
909
diff
changeset

94 
[dom_subset] RL (asm_rl :: ([Part_trans] RL Inductive.monos)) RL [subsetD]; 
0  95 

96 
(*Typechecking is hardest aspect of proof; 

97 
disjIn selects the correct disjunct after unfolding*) 

98 
fun intro_tacsf disjIn prems = 

99 
[(*insert prems and underlying sets*) 

55  100 
cut_facts_tac prems 1, 
726
d703d1a1a2af
ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents:
652
diff
changeset

101 
DETERM (rtac (unfold RS ssubst) 1), 
0  102 
REPEAT (resolve_tac [Part_eqI,CollectI] 1), 
103 
(*Now 23 subgoals: typechecking, the disjunction, perhaps equality.*) 

104 
rtac disjIn 2, 

634
8a5f6961250f
{HOL,ZF}/intr_elim/intro_tacsf: now calls DEPTH_SOLVE_1 instead of REPEAT to
lcp
parents:
590
diff
changeset

105 
(*Not ares_tac, since refl must be tried before any equality assumptions; 
8a5f6961250f
{HOL,ZF}/intr_elim/intro_tacsf: now calls DEPTH_SOLVE_1 instead of REPEAT to
lcp
parents:
590
diff
changeset

106 
backtracking may occur if the premises have extra variables!*) 
8a5f6961250f
{HOL,ZF}/intr_elim/intro_tacsf: now calls DEPTH_SOLVE_1 instead of REPEAT to
lcp
parents:
590
diff
changeset

107 
DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 2 ORELSE assume_tac 2), 
578
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
543
diff
changeset

108 
(*Now solve the equations like Tcons(a,f) = Inl(?b4)*) 
1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
909
diff
changeset

109 
rewrite_goals_tac Inductive.con_defs, 
0  110 
REPEAT (rtac refl 2), 
578
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding without
lcp
parents:
543
diff
changeset

111 
(*Typechecking; this can fail*) 
516  112 
REPEAT (FIRSTGOAL ( dresolve_tac rec_typechecks 
1461  113 
ORELSE' eresolve_tac (asm_rl::PartE::SigmaE2:: 
114 
Inductive.type_elims) 

115 
ORELSE' hyp_subst_tac)), 

1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
909
diff
changeset

116 
DEPTH_SOLVE (swap_res_tac (SigmaI::subsetI::Inductive.type_intrs) 1)]; 
0  117 

118 
(*combines disjI1 and disjI2 to access the corresponding nested disjunct...*) 

119 
val mk_disj_rls = 

120 
let fun f rl = rl RS disjI1 

1461  121 
and g rl = rl RS disjI2 
0  122 
in accesses_bal(f, g, asm_rl) end; 
123 

543
e961b2092869
ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp
parents:
516
diff
changeset

124 
val intrs = map (uncurry (prove_goalw_cterm part_rec_defs)) 
1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
909
diff
changeset

125 
(map (cterm_of sign) Inductive.intr_tms ~~ 
1461  126 
map intro_tacsf (mk_disj_rls(length Inductive.intr_tms))); 
0  127 

128 
(********) 

516  129 
val _ = writeln " Proving the elimination rule..."; 
0  130 

131 
(*Breaks down logical connectives in the monotonic function*) 

132 
val basic_elim_tac = 

1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
909
diff
changeset

133 
REPEAT (SOMEGOAL (eresolve_tac (Ind_Syntax.elim_rls @ Su.free_SEs) 
1461  134 
ORELSE' bound_hyp_subst_tac)) 
726
d703d1a1a2af
ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents:
652
diff
changeset

135 
THEN prune_params_tac 
d703d1a1a2af
ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents:
652
diff
changeset

136 
(*Mutual recursion: collapse references to Part(D,h)*) 
d703d1a1a2af
ZF/intr_elim/elim: now "folds" definitions of the mutually recursive sets!
lcp
parents:
652
diff
changeset

137 
THEN fold_tac part_rec_defs; 
0  138 

1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
909
diff
changeset

139 
in 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
909
diff
changeset

140 
struct 
1427  141 
val thy = Inductive.thy 
142 
and defs = big_rec_def :: part_rec_defs 

143 
and bnd_mono = bnd_mono 

1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
909
diff
changeset

144 
and dom_subset = dom_subset 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
909
diff
changeset

145 
and intrs = intrs; 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
909
diff
changeset

146 

f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
909
diff
changeset

147 
val elim = rule_by_tactic basic_elim_tac 
1461  148 
(unfold RS Ind_Syntax.equals_CollectD); 
0  149 

1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
909
diff
changeset

150 
(*Applies freeness of the given constructors, which *must* be unfolded by 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
909
diff
changeset

151 
the given defs. Cannot simply use the local con_defs because 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
909
diff
changeset

152 
con_defs=[] for inference systems. 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
909
diff
changeset

153 
String s should have the form t:Si where Si is an inductive set*) 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
909
diff
changeset

154 
fun mk_cases defs s = 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
909
diff
changeset

155 
rule_by_tactic (rewrite_goals_tac defs THEN 
1461  156 
basic_elim_tac THEN 
157 
fold_tac defs) 

158 
(assume_read Inductive.thy s RS elim); 

0  159 

1427  160 
val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct) 
161 
and rec_names = rec_names 

1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
909
diff
changeset

162 
end 
516  163 
end; 
0  164 