author  wenzelm 
Sat, 21 Jan 2006 23:02:14 +0100  
changeset 18728  6790126ab5f6 
parent 18708  4b3dadb4fe33 
child 18787  5784fe1b5657 
permissions  rwrr 
5094  1 
(* Title: HOL/Tools/inductive_package.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

10735  4 
Author: Stefan Berghofer, TU Muenchen 
5 
Author: Markus Wenzel, TU Muenchen 

5094  6 

6424  7 
(Co)Inductive Definition module for HOL. 
5094  8 

9 
Features: 

6424  10 
* least or greatest fixedpoints 
11 
* userspecified product and sum constructions 

12 
* mutually recursive definitions 

13 
* definitions involving arbitrary monotone operators 

14 
* automatically proves introduction and elimination rules 

5094  15 

6424  16 
The recursive sets must *already* be declared as constants in the 
17 
current theory! 

5094  18 

19 
Introduction rules have the form 

8316
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

20 
[ ti:M(Sj), ..., P(x), ... ] ==> t: Sk 
5094  21 
where M is some monotone operator (usually the identity) 
22 
P(x) is any side condition on the free variables 

23 
ti, t are any terms 

24 
Sj, Sk are two of the sets being defined in mutual recursion 

25 

6424  26 
Sums are used only for mutual recursion. Products are used only to 
27 
derive "streamlined" induction rules for relations. 

5094  28 
*) 
29 

30 
signature INDUCTIVE_PACKAGE = 

31 
sig 

6424  32 
val quiet_mode: bool ref 
13626
282fbabec862
Fixed bug involving inductive definitions having equalities in the premises,
paulson
parents:
13197
diff
changeset

33 
val trace: bool ref 
16432  34 
val unify_consts: theory > term list > term list > term list * term list 
10988
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

35 
val split_rule_vars: term list > thm > thm 
9116
9df44b5c610b
get_inductive now returns None instead of raising an exception.
berghofe
parents:
9072
diff
changeset

36 
val get_inductive: theory > string > ({names: string list, coind: bool} * 
9df44b5c610b
get_inductive now returns None instead of raising an exception.
berghofe
parents:
9072
diff
changeset

37 
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm, 
9df44b5c610b
get_inductive now returns None instead of raising an exception.
berghofe
parents:
9072
diff
changeset

38 
intrs: thm list, mk_cases: string > thm, mono: thm, unfold: thm}) option 
12400  39 
val the_mk_cases: theory > string > string > thm 
6437  40 
val print_inductives: theory > unit 
18728  41 
val mono_add: attribute 
42 
val mono_del: attribute 

7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

43 
val get_monos: theory > thm list 
10910
058775a575db
export inductive_forall_name, inductive_forall_def, rulify;
wenzelm
parents:
10804
diff
changeset

44 
val inductive_forall_name: string 
058775a575db
export inductive_forall_name, inductive_forall_def, rulify;
wenzelm
parents:
10804
diff
changeset

45 
val inductive_forall_def: thm 
058775a575db
export inductive_forall_name, inductive_forall_def, rulify;
wenzelm
parents:
10804
diff
changeset

46 
val rulify: thm > thm 
15703  47 
val inductive_cases: ((bstring * Attrib.src list) * string list) list > theory > theory 
18728  48 
val inductive_cases_i: ((bstring * attribute list) * term list) list > theory > theory 
6424  49 
val add_inductive_i: bool > bool > bstring > bool > bool > bool > term list > 
18728  50 
((bstring * term) * attribute list) list > thm list > theory > theory * 
6424  51 
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm, 
6437  52 
intrs: thm list, mk_cases: string > thm, mono: thm, unfold: thm} 
11628  53 
val add_inductive: bool > bool > string list > 
15703  54 
((bstring * string) * Attrib.src list) list > (thmref * Attrib.src list) list > 
12180  55 
theory > theory * 
6424  56 
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm, 
6437  57 
intrs: thm list, mk_cases: string > thm, mono: thm, unfold: thm} 
18708  58 
val setup: theory > theory 
5094  59 
end; 
60 

6424  61 
structure InductivePackage: INDUCTIVE_PACKAGE = 
5094  62 
struct 
63 

9598  64 

10729  65 
(** theory context references **) 
66 

15525  67 
val mono_name = "Orderings.mono"; 
17010
5abc26872268
changed reference to Lfp.lfp to FixedPint.lfp, ditto for gfp
avigad
parents:
16975
diff
changeset

68 
val gfp_name = "FixedPoint.gfp"; 
5abc26872268
changed reference to Lfp.lfp to FixedPint.lfp, ditto for gfp
avigad
parents:
16975
diff
changeset

69 
val lfp_name = "FixedPoint.lfp"; 
12259  70 
val vimage_name = "Set.vimage"; 
10735  71 
val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (Thm.concl_of vimageD); 
72 

11991  73 
val inductive_forall_name = "HOL.induct_forall"; 
74 
val inductive_forall_def = thm "induct_forall_def"; 

75 
val inductive_conj_name = "HOL.induct_conj"; 

76 
val inductive_conj_def = thm "induct_conj_def"; 

77 
val inductive_conj = thms "induct_conj"; 

78 
val inductive_atomize = thms "induct_atomize"; 

18463  79 
val inductive_rulify = thms "induct_rulify"; 
80 
val inductive_rulify_fallback = thms "induct_rulify_fallback"; 

10729  81 

82 

83 

10735  84 
(** theory data **) 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

85 

bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

86 
type inductive_info = 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

87 
{names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm, 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

88 
induct: thm, intrs: thm list, mk_cases: string > thm, mono: thm, unfold: thm}; 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

89 

16432  90 
structure InductiveData = TheoryDataFun 
91 
(struct 

7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

92 
val name = "HOL/inductive"; 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

93 
type T = inductive_info Symtab.table * thm list; 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

94 

bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

95 
val empty = (Symtab.empty, []); 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

96 
val copy = I; 
16432  97 
val extend = I; 
98 
fun merge _ ((tab1, monos1), (tab2, monos2)) = 

11502  99 
(Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2)); 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

100 

16432  101 
fun print thy (tab, monos) = 
16364  102 
[Pretty.strs ("(co)inductives:" :: 
16432  103 
map #1 (NameSpace.extern_table (Sign.const_space thy, tab))), 
104 
Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_sg thy) monos)] 

8720  105 
> Pretty.chunks > Pretty.writeln; 
16432  106 
end); 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

107 

bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

108 
val print_inductives = InductiveData.print; 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

109 

bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

110 

bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

111 
(* get and put data *) 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

112 

17412  113 
val get_inductive = Symtab.lookup o #1 o InductiveData.get; 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

114 

9598  115 
fun the_inductive thy name = 
116 
(case get_inductive thy name of 

15531  117 
NONE => error ("Unknown (co)inductive set " ^ quote name) 
118 
 SOME info => info); 

9598  119 

12400  120 
val the_mk_cases = (#mk_cases o #2) oo the_inductive; 
121 

18222  122 
fun put_inductives names info = InductiveData.map (apfst (fn tab => 
123 
fold (fn name => Symtab.update_new (name, info)) names tab 

124 
handle Symtab.DUP dup => error ("Duplicate definition of (co)inductive set " ^ quote dup))); 

7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

125 

8277  126 

7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

127 

bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

128 
(** monotonicity rules **) 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

129 

9831  130 
val get_monos = #2 o InductiveData.get; 
18728  131 
val map_monos = Context.map_theory o InductiveData.map o Library.apsnd; 
8277  132 

7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

133 
fun mk_mono thm = 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

134 
let 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

135 
fun eq2mono thm' = [standard (thm' RS (thm' RS eq_to_mono))] @ 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

136 
(case concl_of thm of 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

137 
(_ $ (_ $ (Const ("Not", _) $ _) $ _)) => [] 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

138 
 _ => [standard (thm' RS (thm' RS eq_to_mono2))]); 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

139 
val concl = concl_of thm 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

140 
in 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

141 
if Logic.is_equals concl then 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

142 
eq2mono (thm RS meta_eq_to_obj_eq) 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

143 
else if can (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl then 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

144 
eq2mono thm 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

145 
else [thm] 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

146 
end; 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

147 

8634  148 

149 
(* attributes *) 

7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

150 

18728  151 
val mono_add = Thm.declaration_attribute (map_monos o Drule.add_rules o mk_mono); 
152 
val mono_del = Thm.declaration_attribute (map_monos o Drule.del_rules o mk_mono); 

7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

153 

bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

154 

7107  155 

10735  156 
(** misc utilities **) 
6424  157 

5662  158 
val quiet_mode = ref false; 
13626
282fbabec862
Fixed bug involving inductive definitions having equalities in the premises,
paulson
parents:
13197
diff
changeset

159 
val trace = ref false; (*for debugging*) 
10735  160 
fun message s = if ! quiet_mode then () else writeln s; 
161 
fun clean_message s = if ! quick_and_dirty then () else message s; 

5662  162 

6424  163 
fun coind_prefix true = "co" 
164 
 coind_prefix false = ""; 

165 

166 

10735  167 
(*the following code ensures that each recursive set always has the 
168 
same type in all introduction rules*) 

16432  169 
fun unify_consts thy cs intr_ts = 
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

170 
(let 
16861  171 
val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c  _ => I); 
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

172 
fun varify (t, (i, ts)) = 
16876  173 
let val t' = map_term_types (Logic.incr_tvar (i + 1)) (#1 (Type.varify (t, []))) 
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

174 
in (maxidx_of_term t', t'::ts) end; 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

175 
val (i, cs') = foldr varify (~1, []) cs; 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

176 
val (i', intr_ts') = foldr varify (i, []) intr_ts; 
16861  177 
val rec_consts = fold add_term_consts_2 cs' []; 
178 
val intr_consts = fold add_term_consts_2 intr_ts' []; 

16934  179 
fun unify (cname, cT) = 
15570  180 
let val consts = map snd (List.filter (fn c => fst c = cname) intr_consts) 
16934  181 
in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end; 
182 
val (env, _) = fold unify rec_consts (Vartab.empty, i'); 

16287  183 
val subst = Type.freeze o map_term_types (Envir.norm_type env) 
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

184 

75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

185 
in (map subst cs', map subst intr_ts') 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

186 
end) handle Type.TUNIFY => 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

187 
(warning "Occurrences of recursive constant have nonunifiable types"; (cs, intr_ts)); 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

188 

75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

189 

10735  190 
(*make injections used in mutually recursive definitions*) 
5094  191 
fun mk_inj cs sumT c x = 
192 
let 

193 
fun mk_inj' T n i = 

194 
if n = 1 then x else 

195 
let val n2 = n div 2; 

196 
val Type (_, [T1, T2]) = T 

197 
in 

198 
if i <= n2 then 

15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
15032
diff
changeset

199 
Const ("Sum_Type.Inl", T1 > T) $ (mk_inj' T1 n2 i) 
5094  200 
else 
15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
15032
diff
changeset

201 
Const ("Sum_Type.Inr", T2 > T) $ (mk_inj' T2 (n  n2) (i  n2)) 
5094  202 
end 
203 
in mk_inj' sumT (length cs) (1 + find_index_eq c cs) 

204 
end; 

205 

10735  206 
(*make "vimage" terms for selecting out components of mutually rec.def*) 
5094  207 
fun mk_vimage cs sumT t c = if length cs < 2 then t else 
208 
let 

209 
val cT = HOLogic.dest_setT (fastype_of c); 

210 
val vimageT = [cT > sumT, HOLogic.mk_setT sumT] > HOLogic.mk_setT cT 

211 
in 

212 
Const (vimage_name, vimageT) $ 

213 
Abs ("y", cT, mk_inj cs sumT c (Bound 0)) $ t 

214 
end; 

215 

10988
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

216 
(** proper splitting **) 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

217 

e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

218 
fun prod_factors p (Const ("Pair", _) $ t $ u) = 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

219 
p :: prod_factors (1::p) t @ prod_factors (2::p) u 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

220 
 prod_factors p _ = []; 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

221 

17485  222 
fun mg_prod_factors ts (t $ u) fs = if t mem ts then 
10988
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

223 
let val f = prod_factors [] u 
17325  224 
in AList.update (op =) (t, f inter (AList.lookup (op =) fs t) > the_default f) fs end 
17485  225 
else mg_prod_factors ts u (mg_prod_factors ts t fs) 
226 
 mg_prod_factors ts (Abs (_, _, t)) fs = mg_prod_factors ts t fs 

227 
 mg_prod_factors ts _ fs = fs; 

10988
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

228 

e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

229 
fun prodT_factors p ps (T as Type ("*", [T1, T2])) = 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

230 
if p mem ps then prodT_factors (1::p) ps T1 @ prodT_factors (2::p) ps T2 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

231 
else [T] 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

232 
 prodT_factors _ _ T = [T]; 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

233 

e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

234 
fun ap_split p ps (Type ("*", [T1, T2])) T3 u = 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

235 
if p mem ps then HOLogic.split_const (T1, T2, T3) $ 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

236 
Abs ("v", T1, ap_split (2::p) ps T2 T3 (ap_split (1::p) ps T1 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

237 
(prodT_factors (2::p) ps T2 > T3) (incr_boundvars 1 u) $ Bound 0)) 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

238 
else u 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

239 
 ap_split _ _ _ _ u = u; 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

240 

e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

241 
fun mk_tuple p ps (Type ("*", [T1, T2])) (tms as t::_) = 
17985  242 
if p mem ps then HOLogic.mk_prod (mk_tuple (1::p) ps T1 tms, 
15570  243 
mk_tuple (2::p) ps T2 (Library.drop (length (prodT_factors (1::p) ps T1), tms))) 
10988
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

244 
else t 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

245 
 mk_tuple _ _ _ (t::_) = t; 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

246 

e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

247 
fun split_rule_var' ((t as Var (v, Type ("fun", [T1, T2])), ps), rl) = 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

248 
let val T' = prodT_factors [] ps T1 > T2 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

249 
val newt = ap_split [] ps T1 T2 (Var (v, T')) 
16432  250 
val cterm = Thm.cterm_of (Thm.theory_of_thm rl) 
10988
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

251 
in 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

252 
instantiate ([], [(cterm t, cterm newt)]) rl 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

253 
end 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

254 
 split_rule_var' (_, rl) = rl; 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

255 

e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

256 
val remove_split = rewrite_rule [split_conv RS eq_reflection]; 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

257 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

258 
fun split_rule_vars vs rl = standard (remove_split (foldr split_rule_var' 
17485  259 
rl (mg_prod_factors vs (Thm.prop_of rl) []))); 
10988
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

260 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

261 
fun split_rule vs rl = standard (remove_split (foldr split_rule_var' 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

262 
rl (List.mapPartial (fn (t as Var ((a, _), _)) => 
17485  263 
Option.map (pair t) (AList.lookup (op =) vs a)) (term_vars (Thm.prop_of rl))))); 
6424  264 

265 

10729  266 
(** process rules **) 
267 

268 
local 

5094  269 

16432  270 
fun err_in_rule thy name t msg = 
271 
error (cat_lines ["Illformed introduction rule " ^ quote name, 

272 
Sign.string_of_term thy t, msg]); 

10729  273 

16432  274 
fun err_in_prem thy name t p msg = 
275 
error (cat_lines ["Illformed premise", Sign.string_of_term thy p, 

276 
"in introduction rule " ^ quote name, Sign.string_of_term thy t, msg]); 

5094  277 

10729  278 
val bad_concl = "Conclusion of introduction rule must have form \"t : S_i\""; 
279 

17985  280 
val all_not_allowed = 
11358
416ea5c009f5
now checks for leading metaquantifiers and complains, instead of
paulson
parents:
11036
diff
changeset

281 
"Introduction rule must not have a leading \"!!\" quantifier"; 
416ea5c009f5
now checks for leading metaquantifiers and complains, instead of
paulson
parents:
11036
diff
changeset

282 

16432  283 
fun atomize_term thy = MetaSimplifier.rewrite_term thy inductive_atomize []; 
10729  284 

285 
in 

5094  286 

16432  287 
fun check_rule thy cs ((name, rule), att) = 
10729  288 
let 
289 
val concl = Logic.strip_imp_concl rule; 

290 
val prems = Logic.strip_imp_prems rule; 

16432  291 
val aprems = map (atomize_term thy) prems; 
10729  292 
val arule = Logic.list_implies (aprems, concl); 
5094  293 

10729  294 
fun check_prem (prem, aprem) = 
295 
if can HOLogic.dest_Trueprop aprem then () 

16432  296 
else err_in_prem thy name rule prem "Nonatomic premise"; 
10729  297 
in 
11358
416ea5c009f5
now checks for leading metaquantifiers and complains, instead of
paulson
parents:
11036
diff
changeset

298 
(case concl of 
416ea5c009f5
now checks for leading metaquantifiers and complains, instead of
paulson
parents:
11036
diff
changeset

299 
Const ("Trueprop", _) $ (Const ("op :", _) $ t $ u) => 
10729  300 
if u mem cs then 
301 
if exists (Logic.occs o rpair t) cs then 

16432  302 
err_in_rule thy name rule "Recursion term on left of member symbol" 
15570  303 
else List.app check_prem (prems ~~ aprems) 
16432  304 
else err_in_rule thy name rule bad_concl 
305 
 Const ("all", _) $ _ => err_in_rule thy name rule all_not_allowed 

306 
 _ => err_in_rule thy name rule bad_concl); 

10729  307 
((name, arule), att) 
308 
end; 

5094  309 

18222  310 
val rulify = (* FIXME norm_hhf *) 
311 
hol_simplify inductive_conj 

18463  312 
#> hol_simplify inductive_rulify 
313 
#> hol_simplify inductive_rulify_fallback 

18222  314 
#> standard; 
10729  315 

316 
end; 

317 

5094  318 

6424  319 

10735  320 
(** properties of (co)inductive sets **) 
5094  321 

10735  322 
(* elimination rules *) 
5094  323 

8375  324 
fun mk_elims cs cTs params intr_ts intr_names = 
5094  325 
let 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

326 
val used = foldr add_term_names [] intr_ts; 
5094  327 
val [aname, pname] = variantlist (["a", "P"], used); 
328 
val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT)); 

329 

330 
fun dest_intr r = 

331 
let val Const ("op :", _) $ t $ u = 

332 
HOLogic.dest_Trueprop (Logic.strip_imp_concl r) 

333 
in (u, t, Logic.strip_imp_prems r) end; 

334 

8380  335 
val intrs = map dest_intr intr_ts ~~ intr_names; 
5094  336 

337 
fun mk_elim (c, T) = 

338 
let 

339 
val a = Free (aname, T); 

340 

341 
fun mk_elim_prem (_, t, ts) = 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

342 
list_all_free (map dest_Free ((foldr add_term_frees [] (t::ts)) \\ params), 
5094  343 
Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P)); 
15570  344 
val c_intrs = (List.filter (equal c o #1 o #1) intrs); 
5094  345 
in 
8375  346 
(Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) :: 
347 
map mk_elim_prem (map #1 c_intrs), P), map #2 c_intrs) 

5094  348 
end 
349 
in 

350 
map mk_elim (cs ~~ cTs) 

351 
end; 

9598  352 

6424  353 

10735  354 
(* premises and conclusions of induction rules *) 
5094  355 

356 
fun mk_indrule cs cTs params intr_ts = 

357 
let 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

358 
val used = foldr add_term_names [] intr_ts; 
5094  359 

360 
(* predicates for induction rule *) 

361 

362 
val preds = map Free (variantlist (if length cs < 2 then ["P"] else 

363 
map (fn i => "P" ^ string_of_int i) (1 upto length cs), used) ~~ 

364 
map (fn T => T > HOLogic.boolT) cTs); 

365 

366 
(* transform an introduction rule into a premise for induction rule *) 

367 

368 
fun mk_ind_prem r = 

369 
let 

370 
val frees = map dest_Free ((add_term_frees (r, [])) \\ params); 

371 

17485  372 
val pred_of = AList.lookup (op aconv) (cs ~~ preds); 
5094  373 

7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

374 
fun subst (s as ((m as Const ("op :", T)) $ t $ u)) = 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

375 
(case pred_of u of 
15531  376 
NONE => (m $ fst (subst t) $ fst (subst u), NONE) 
377 
 SOME P => (HOLogic.mk_binop inductive_conj_name (s, P $ t), SOME (s, P $ t))) 

7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

378 
 subst s = 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

379 
(case pred_of s of 
15531  380 
SOME P => (HOLogic.mk_binop "op Int" 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

381 
(s, HOLogic.Collect_const (HOLogic.dest_setT 
15531  382 
(fastype_of s)) $ P), NONE) 
383 
 NONE => (case s of 

384 
(t $ u) => (fst (subst t) $ fst (subst u), NONE) 

385 
 (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), NONE) 

386 
 _ => (s, NONE))); 

7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

387 

bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

388 
fun mk_prem (s, prems) = (case subst s of 
15531  389 
(_, SOME (t, u)) => t :: u :: prems 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

390 
 (t, _) => t :: prems); 
9598  391 

5094  392 
val Const ("op :", _) $ t $ u = 
393 
HOLogic.dest_Trueprop (Logic.strip_imp_concl r) 

394 

395 
in list_all_free (frees, 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

396 
Logic.list_implies (map HOLogic.mk_Trueprop (foldr mk_prem 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

397 
[] (map HOLogic.dest_Trueprop (Logic.strip_imp_prems r))), 
15570  398 
HOLogic.mk_Trueprop (valOf (pred_of u) $ t))) 
5094  399 
end; 
400 

401 
val ind_prems = map mk_ind_prem intr_ts; 

13626
282fbabec862
Fixed bug involving inductive definitions having equalities in the premises,
paulson
parents:
13197
diff
changeset

402 

17485  403 
val factors = Library.fold (mg_prod_factors preds) ind_prems []; 
5094  404 

405 
(* make conclusions for induction rules *) 

406 

407 
fun mk_ind_concl ((c, P), (ts, x)) = 

408 
let val T = HOLogic.dest_setT (fastype_of c); 

17485  409 
val ps = AList.lookup (op =) factors P > the_default []; 
10988
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

410 
val Ts = prodT_factors [] ps T; 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

411 
val (frees, x') = foldr (fn (T', (fs, s)) => 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

412 
((Free (s, T'))::fs, Symbol.bump_string s)) ([], x) Ts; 
10988
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

413 
val tuple = mk_tuple [] ps T frees; 
5094  414 
in ((HOLogic.mk_binop "op >" 
415 
(HOLogic.mk_mem (tuple, c), P $ tuple))::ts, x') 

416 
end; 

417 

7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

418 
val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

419 
(fst (foldr mk_ind_concl ([], "xa") (cs ~~ preds)))) 
5094  420 

10988
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

421 
in (preds, ind_prems, mutual_ind_concl, 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

422 
map (apfst (fst o dest_Free)) factors) 
5094  423 
end; 
424 

6424  425 

10735  426 
(* prepare cases and induct rules *) 
8316
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

427 

18222  428 
fun add_cases_induct no_elim no_induct coind names elims induct = 
8316
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

429 
let 
18330  430 
fun cases_spec name elim thy = 
9405  431 
thy 
18463  432 
> Theory.parent_path 
9405  433 
> Theory.add_path (Sign.base_name name) 
18728  434 
> PureThy.add_thms [(("cases", elim), [InductAttrib.cases_set name])] > snd 
18463  435 
> Theory.restore_naming thy; 
18330  436 
val cases_specs = if no_elim then [] else map2 cases_spec names elims; 
8316
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

437 

18728  438 
val induct_att = if coind then InductAttrib.coinduct_set else InductAttrib.induct_set; 
18222  439 
val induct_specs = 
18463  440 
if no_induct then I 
441 
else 

442 
let 

443 
val rules = names ~~ map (ProjectRule.project induct) (1 upto length names); 

444 
val inducts = map (RuleCases.save induct o standard o #2) rules; 

445 
in 

446 
PureThy.add_thms (rules > map (fn (name, th) => 

447 
(("", th), [RuleCases.consumes 1, induct_att name]))) #> snd #> 

448 
PureThy.add_thmss 

449 
[((coind_prefix coind ^ "inducts", inducts), [RuleCases.consumes 1])] #> snd 

450 
end; 

451 
in Library.apply cases_specs #> induct_specs end; 

8316
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

452 

74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

453 

74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

454 

10735  455 
(** proofs for (co)inductive sets **) 
6424  456 

10735  457 
(* prove monotonicity  NOT subject to quick_and_dirty! *) 
5094  458 

459 
fun prove_mono setT fp_fun monos thy = 

10735  460 
(message " Proving monotonicity ..."; 
17985  461 
standard (Goal.prove thy [] [] (*NO quick_and_dirty here!*) 
462 
(HOLogic.mk_Trueprop 

463 
(Const (mono_name, (setT > setT) > HOLogic.boolT) $ fp_fun)) 

464 
(fn _ => EVERY [rtac monoI 1, 

465 
REPEAT (ares_tac (List.concat (map mk_mono monos) @ get_monos thy) 1)]))); 

5094  466 

6424  467 

10735  468 
(* prove introduction rules *) 
5094  469 

12180  470 
fun prove_intrs coind mono fp_def intr_ts rec_sets_defs thy = 
5094  471 
let 
10735  472 
val _ = clean_message " Proving the introduction rules ..."; 
5094  473 

13657
c1637d60a846
Now applies standard' to "unfold" theorem (due to flexflex constraints).
berghofe
parents:
13626
diff
changeset

474 
val unfold = standard' (mono RS (fp_def RS 
10186  475 
(if coind then def_gfp_unfold else def_lfp_unfold))); 
5094  476 

477 
fun select_disj 1 1 = [] 

478 
 select_disj _ 1 = [rtac disjI1] 

479 
 select_disj n i = (rtac disjI2)::(select_disj (n  1) (i  1)); 

480 

17985  481 
val intrs = (1 upto (length intr_ts) ~~ intr_ts) > map (fn (i, intr) => 
18222  482 
rulify (SkipProof.prove thy [] [] intr (fn _ => EVERY 
17985  483 
[rewrite_goals_tac rec_sets_defs, 
484 
stac unfold 1, 

485 
REPEAT (resolve_tac [vimageI2, CollectI] 1), 

486 
(*Now 12 subgoals: the disjunction, perhaps equality.*) 

487 
EVERY1 (select_disj (length intr_ts) i), 

488 
(*Not ares_tac, since refl must be tried before any equality assumptions; 

489 
backtracking may occur if the premises have extra variables!*) 

490 
DEPTH_SOLVE_1 (resolve_tac [refl, exI, conjI] 1 APPEND assume_tac 1), 

491 
(*Now solve the equations like Inl 0 = Inl ?b2*) 

18222  492 
REPEAT (rtac refl 1)]))) 
5094  493 

494 
in (intrs, unfold) end; 

495 

6424  496 

10735  497 
(* prove elimination rules *) 
5094  498 

8375  499 
fun prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy = 
5094  500 
let 
10735  501 
val _ = clean_message " Proving the elimination rules ..."; 
5094  502 

7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

503 
val rules1 = [CollectE, disjE, make_elim vimageD, exE]; 
10735  504 
val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ map make_elim [Inl_inject, Inr_inject]; 
8375  505 
in 
11005  506 
mk_elims cs cTs params intr_ts intr_names > map (fn (t, cases) => 
17985  507 
SkipProof.prove thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t) 
508 
(fn prems => EVERY 

11005  509 
[cut_facts_tac [hd prems] 1, 
17985  510 
rewrite_goals_tac rec_sets_defs, 
11005  511 
dtac (unfold RS subst) 1, 
512 
REPEAT (FIRSTGOAL (eresolve_tac rules1)), 

513 
REPEAT (FIRSTGOAL (eresolve_tac rules2)), 

17985  514 
EVERY (map (fn prem => 
515 
DEPTH_SOLVE_1 (ares_tac [rewrite_rule rec_sets_defs prem, conjI] 1)) (tl prems))]) 

11005  516 
> rulify 
517 
> RuleCases.name cases) 

8375  518 
end; 
5094  519 

6424  520 

10735  521 
(* derivation of simplified elimination rules *) 
5094  522 

11682
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

523 
local 
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

524 

7107  525 
(*cprop should have the form t:Si where Si is an inductive set*) 
11682
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

526 
val mk_cases_err = "mk_cases: proposition not of form \"t : S_i\""; 
9598  527 

11682
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

528 
(*delete needless equality assumptions*) 
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

529 
val refl_thin = prove_goal HOL.thy "!!P. a = a ==> P ==> P" (fn _ => [assume_tac 1]); 
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

530 
val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, Pair_inject]; 
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

531 
val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls; 
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

532 

d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

533 
fun simp_case_tac solved ss i = 
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

534 
EVERY' [elim_tac, asm_full_simp_tac ss, elim_tac, REPEAT o bound_hyp_subst_tac] i 
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

535 
THEN_MAYBE (if solved then no_tac else all_tac); 
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

536 

d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

537 
in 
9598  538 

539 
fun mk_cases_i elims ss cprop = 

7107  540 
let 
541 
val prem = Thm.assume cprop; 

11682
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

542 
val tac = ALLGOALS (simp_case_tac false ss) THEN prune_params_tac; 
9298  543 
fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic tac (prem RS rl)); 
7107  544 
in 
545 
(case get_first (try mk_elim) elims of 

15531  546 
SOME r => r 
547 
 NONE => error (Pretty.string_of (Pretty.block 

9598  548 
[Pretty.str mk_cases_err, Pretty.fbrk, Display.pretty_cterm cprop]))) 
7107  549 
end; 
550 

6141  551 
fun mk_cases elims s = 
16432  552 
mk_cases_i elims (simpset()) (Thm.read_cterm (Thm.theory_of_thm (hd elims)) (s, propT)); 
9598  553 

554 
fun smart_mk_cases thy ss cprop = 

555 
let 

556 
val c = #1 (Term.dest_Const (Term.head_of (#2 (HOLogic.dest_mem (HOLogic.dest_Trueprop 

557 
(Logic.strip_imp_concl (Thm.term_of cprop))))))) handle TERM _ => error mk_cases_err; 

558 
val (_, {elims, ...}) = the_inductive thy c; 

559 
in mk_cases_i elims ss cprop end; 

7107  560 

11682
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

561 
end; 
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

562 

7107  563 

564 
(* inductive_cases(_i) *) 

565 

12609  566 
fun gen_inductive_cases prep_att prep_prop args thy = 
9598  567 
let 
16432  568 
val cert_prop = Thm.cterm_of thy o prep_prop (ProofContext.init thy); 
12609  569 
val mk_cases = smart_mk_cases thy (Simplifier.simpset_of thy) o cert_prop; 
570 

12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12798
diff
changeset

571 
val facts = args > map (fn ((a, atts), props) => 
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12798
diff
changeset

572 
((a, map (prep_att thy) atts), map (Thm.no_attributes o single o mk_cases) props)); 
18418
bf448d999b7e
rearranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18377
diff
changeset

573 
in thy > IsarThy.theorems_i Drule.lemmaK facts > snd end; 
5094  574 

18728  575 
val inductive_cases = gen_inductive_cases Attrib.attribute ProofContext.read_prop; 
12172  576 
val inductive_cases_i = gen_inductive_cases (K I) ProofContext.cert_prop; 
7107  577 

6424  578 

9598  579 
(* mk_cases_meth *) 
580 

581 
fun mk_cases_meth (ctxt, raw_props) = 

582 
let 

583 
val thy = ProofContext.theory_of ctxt; 

15032  584 
val ss = local_simpset_of ctxt; 
16432  585 
val cprops = map (Thm.cterm_of thy o ProofContext.read_prop ctxt) raw_props; 
10743  586 
in Method.erule 0 (map (smart_mk_cases thy ss) cprops) end; 
9598  587 

588 
val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name)); 

589 

590 

10735  591 
(* prove induction rule *) 
5094  592 

593 
fun prove_indrule cs cTs sumT rec_const params intr_ts mono 

594 
fp_def rec_sets_defs thy = 

595 
let 

10735  596 
val _ = clean_message " Proving the induction rule ..."; 
5094  597 

12922  598 
val sum_case_rewrites = 
16432  599 
(if Context.theory_name thy = "Datatype" then 
16486  600 
PureThy.get_thms thy (Name "sum.cases") 
16432  601 
else 
602 
(case ThyInfo.lookup_theory "Datatype" of 

603 
NONE => [] 

16975  604 
 SOME thy' => 
605 
if Theory.subthy (thy', thy) then 

606 
PureThy.get_thms thy' (Name "sum.cases") 

607 
else [])) 

16432  608 
> map mk_meta_eq; 
7293  609 

10988
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

610 
val (preds, ind_prems, mutual_ind_concl, factors) = 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

611 
mk_indrule cs cTs params intr_ts; 
5094  612 

13626
282fbabec862
Fixed bug involving inductive definitions having equalities in the premises,
paulson
parents:
13197
diff
changeset

613 
val dummy = if !trace then 
17985  614 
(writeln "ind_prems = "; 
615 
List.app (writeln o Sign.string_of_term thy) ind_prems) 

616 
else (); 

13626
282fbabec862
Fixed bug involving inductive definitions having equalities in the premises,
paulson
parents:
13197
diff
changeset

617 

5094  618 
(* make predicate for instantiation of abstract induction rule *) 
619 

620 
fun mk_ind_pred _ [P] = P 

621 
 mk_ind_pred T Ps = 

622 
let val n = (length Ps) div 2; 

623 
val Type (_, [T1, T2]) = T 

7293  624 
in Const ("Datatype.sum.sum_case", 
5094  625 
[T1 > HOLogic.boolT, T2 > HOLogic.boolT, T] > HOLogic.boolT) $ 
15570  626 
mk_ind_pred T1 (Library.take (n, Ps)) $ mk_ind_pred T2 (Library.drop (n, Ps)) 
5094  627 
end; 
628 

629 
val ind_pred = mk_ind_pred sumT preds; 

630 

631 
val ind_concl = HOLogic.mk_Trueprop 

632 
(HOLogic.all_const sumT $ Abs ("x", sumT, HOLogic.mk_binop "op >" 

633 
(HOLogic.mk_mem (Bound 0, rec_const), ind_pred $ Bound 0))); 

634 

635 
(* simplification rules for vimage and Collect *) 

636 

637 
val vimage_simps = if length cs < 2 then [] else 

17985  638 
map (fn c => standard (SkipProof.prove thy [] [] 
5094  639 
(HOLogic.mk_Trueprop (HOLogic.mk_eq 
640 
(mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c, 

641 
HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $ 

17985  642 
List.nth (preds, find_index_eq c cs)))) 
643 
(fn _ => EVERY 

644 
[rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, rtac refl 1]))) cs; 

5094  645 

13626
282fbabec862
Fixed bug involving inductive definitions having equalities in the premises,
paulson
parents:
13197
diff
changeset

646 
val raw_fp_induct = (mono RS (fp_def RS def_lfp_induct)); 
282fbabec862
Fixed bug involving inductive definitions having equalities in the premises,
paulson
parents:
13197
diff
changeset

647 

282fbabec862
Fixed bug involving inductive definitions having equalities in the premises,
paulson
parents:
13197
diff
changeset

648 
val dummy = if !trace then 
17985  649 
(writeln "raw_fp_induct = "; print_thm raw_fp_induct) 
650 
else (); 

13626
282fbabec862
Fixed bug involving inductive definitions having equalities in the premises,
paulson
parents:
13197
diff
changeset

651 

17985  652 
val induct = standard (SkipProof.prove thy [] ind_prems ind_concl 
653 
(fn prems => EVERY 

654 
[rewrite_goals_tac [inductive_conj_def], 

655 
rtac (impI RS allI) 1, 

13626
282fbabec862
Fixed bug involving inductive definitions having equalities in the premises,
paulson
parents:
13197
diff
changeset

656 
DETERM (etac raw_fp_induct 1), 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

657 
rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)), 
5094  658 
fold_goals_tac rec_sets_defs, 
659 
(*This CollectE and disjE separates out the introduction rules*) 

7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

660 
REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE, exE])), 
5094  661 
(*Now break down the individual cases. No disjE here in case 
662 
some premise involves disjunction.*) 

13747
bf308fcfd08e
Better treatment of equality in premises of inductive definitions. Less
paulson
parents:
13709
diff
changeset

663 
REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac)), 
15416
db69af736ebb
Further fix to a bug (involving equational premises) in inductive definitions
paulson
parents:
15391
diff
changeset

664 
ALLGOALS (simp_tac (HOL_basic_ss addsimps sum_case_rewrites)), 
5094  665 
EVERY (map (fn prem => 
17985  666 
DEPTH_SOLVE_1 (ares_tac [rewrite_rule [inductive_conj_def] prem, conjI, refl] 1)) prems)])); 
5094  667 

17985  668 
val lemma = standard (SkipProof.prove thy [] [] 
669 
(Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn _ => EVERY 

670 
[rewrite_goals_tac rec_sets_defs, 

5094  671 
REPEAT (EVERY 
672 
[REPEAT (resolve_tac [conjI, impI] 1), 

673 
TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1, 

7293  674 
rewrite_goals_tac sum_case_rewrites, 
17985  675 
atac 1])])) 
5094  676 

10988
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

677 
in standard (split_rule factors (induct RS lemma)) end; 
5094  678 

6424  679 

680 

10735  681 
(** specification of (co)inductive sets **) 
5094  682 

10729  683 
fun cond_declare_consts declare_consts cs paramTs cnames = 
684 
if declare_consts then 

14235
281295a1bbaa
Fixed bug in mk_ind_def that caused the inductive definition package to
berghofe
parents:
13747
diff
changeset

685 
Theory.add_consts_i (map (fn (c, n) => (Sign.base_name n, paramTs > fastype_of c, NoSyn)) (cs ~~ cnames)) 
10729  686 
else I; 
687 

12180  688 
fun mk_ind_def declare_consts alt_name coind cs intr_ts monos thy 
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

689 
params paramTs cTs cnames = 
5094  690 
let 
691 
val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs; 

692 
val setT = HOLogic.mk_setT sumT; 

693 

10735  694 
val fp_name = if coind then gfp_name else lfp_name; 
5094  695 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

696 
val used = foldr add_term_names [] intr_ts; 
5149  697 
val [sname, xname] = variantlist (["S", "x"], used); 
698 

5094  699 
(* transform an introduction rule into a conjunction *) 
700 
(* [ t : ... S_i ... ; ... ] ==> u : S_j *) 

701 
(* is transformed into *) 

702 
(* x = Inj_j u & t : ... Inj_i `` S ... & ... *) 

703 

704 
fun transform_rule r = 

705 
let 

706 
val frees = map dest_Free ((add_term_frees (r, [])) \\ params); 

5149  707 
val subst = subst_free 
708 
(cs ~~ (map (mk_vimage cs sumT (Free (sname, setT))) cs)); 

5094  709 
val Const ("op :", _) $ t $ u = 
710 
HOLogic.dest_Trueprop (Logic.strip_imp_concl r) 

711 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

712 
in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P)) 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

713 
(foldr1 HOLogic.mk_conj 
5149  714 
(((HOLogic.eq_const sumT) $ Free (xname, sumT) $ (mk_inj cs sumT u t)):: 
5094  715 
(map (subst o HOLogic.dest_Trueprop) 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

716 
(Logic.strip_imp_prems r)))) frees 
5094  717 
end 
718 

719 
(* make a disjunction of all introduction rules *) 

720 

5149  721 
val fp_fun = absfree (sname, setT, (HOLogic.Collect_const sumT) $ 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

722 
absfree (xname, sumT, foldr1 HOLogic.mk_disj (map transform_rule intr_ts))); 
5094  723 

724 
(* add definiton of recursive sets to theory *) 

725 

14235
281295a1bbaa
Fixed bug in mk_ind_def that caused the inductive definition package to
berghofe
parents:
13747
diff
changeset

726 
val rec_name = if alt_name = "" then 
281295a1bbaa
Fixed bug in mk_ind_def that caused the inductive definition package to
berghofe
parents:
13747
diff
changeset

727 
space_implode "_" (map Sign.base_name cnames) else alt_name; 
281295a1bbaa
Fixed bug in mk_ind_def that caused the inductive definition package to
berghofe
parents:
13747
diff
changeset

728 
val full_rec_name = if length cs < 2 then hd cnames 
16432  729 
else Sign.full_name thy rec_name; 
5094  730 

731 
val rec_const = list_comb 

732 
(Const (full_rec_name, paramTs > setT), params); 

733 

734 
val fp_def_term = Logic.mk_equals (rec_const, 

10735  735 
Const (fp_name, (setT > setT) > setT) $ fp_fun); 
5094  736 

737 
val def_terms = fp_def_term :: (if length cs < 2 then [] else 

738 
map (fn c => Logic.mk_equals (c, mk_vimage cs sumT rec_const c)) cs); 

739 

18358  740 
val ([fp_def :: rec_sets_defs], thy') = 
8433  741 
thy 
10729  742 
> cond_declare_consts declare_consts cs paramTs cnames 
8433  743 
> (if length cs < 2 then I 
744 
else Theory.add_consts_i [(rec_name, paramTs > setT, NoSyn)]) 

745 
> Theory.add_path rec_name 

9315  746 
> PureThy.add_defss_i false [(("defs", def_terms), [])]; 
5094  747 

9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

748 
val mono = prove_mono setT fp_fun monos thy' 
5094  749 

18222  750 
in (thy', rec_name, mono, fp_def, rec_sets_defs, rec_const, sumT) end; 
5094  751 

9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

752 
fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs 
12180  753 
intros monos thy params paramTs cTs cnames induct_cases = 
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

754 
let 
10735  755 
val _ = 
756 
if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^ 

14235
281295a1bbaa
Fixed bug in mk_ind_def that caused the inductive definition package to
berghofe
parents:
13747
diff
changeset

757 
commas_quote (map Sign.base_name cnames)) else (); 
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

758 

a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

759 
val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros); 
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

760 

18222  761 
val (thy1, rec_name, mono, fp_def, rec_sets_defs, rec_const, sumT) = 
12180  762 
mk_ind_def declare_consts alt_name coind cs intr_ts monos thy 
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

763 
params paramTs cTs cnames; 
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

764 

12180  765 
val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts rec_sets_defs thy1; 
5094  766 
val elims = if no_elim then [] else 
9939  767 
prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy1; 
8312
b470bc28b59d
add_cases_induct: accomodate no_elim and no_ind flags;
wenzelm
parents:
8307
diff
changeset

768 
val raw_induct = if no_ind then Drule.asm_rl else 
5094  769 
if coind then standard (rule_by_tactic 
5553  770 
(rewrite_tac [mk_meta_eq vimage_Un] THEN 
5094  771 
fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct))) 
772 
else 

773 
prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def 

9939  774 
rec_sets_defs thy1; 
12165  775 
val induct = 
18222  776 
if coind then 
777 
(raw_induct, [RuleCases.case_names [rec_name], 

18234  778 
RuleCases.case_conclusion (rec_name, induct_cases), 
18222  779 
RuleCases.consumes 1]) 
780 
else if no_ind orelse length cs > 1 then 

781 
(raw_induct, [RuleCases.case_names induct_cases, RuleCases.consumes 0]) 

782 
else (raw_induct RSN (2, rev_mp), [RuleCases.case_names induct_cases, RuleCases.consumes 1]); 

5094  783 

18377  784 
val (intrs', thy2) = 
785 
thy1 

786 
> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts); 

787 
val (([_, elims'], [induct']), thy3) = 

10735  788 
thy2 
11005  789 
> PureThy.add_thmss 
11628  790 
[(("intros", intrs'), []), 
11005  791 
(("elims", elims), [RuleCases.consumes 1])] 
18377  792 
>> PureThy.add_thms 
18463  793 
[((coind_prefix coind ^ "induct", rulify (#1 induct)), #2 induct)]; 
9939  794 
in (thy3, 
10735  795 
{defs = fp_def :: rec_sets_defs, 
5094  796 
mono = mono, 
797 
unfold = unfold, 

13709  798 
intrs = intrs', 
7798
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7710
diff
changeset

799 
elims = elims', 
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7710
diff
changeset

800 
mk_cases = mk_cases elims', 
10729  801 
raw_induct = rulify raw_induct, 
7798
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7710
diff
changeset

802 
induct = induct'}) 
5094  803 
end; 
804 

6424  805 

10735  806 
(* external interfaces *) 
5094  807 

16432  808 
fun try_term f msg thy t = 
10735  809 
(case Library.try f t of 
15531  810 
SOME x => x 
16432  811 
 NONE => error (msg ^ Sign.string_of_term thy t)); 
5094  812 

12180  813 
fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs pre_intros monos thy = 
5094  814 
let 
6424  815 
val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions"); 
5094  816 

817 
(*parameters should agree for all mutually recursive components*) 

818 
val (_, params) = strip_comb (hd cs); 

10735  819 
val paramTs = map (try_term (snd o dest_Free) "Parameter in recursive\ 
16432  820 
\ component is not a free variable: " thy) params; 
5094  821 

10735  822 
val cTs = map (try_term (HOLogic.dest_setT o fastype_of) 
16432  823 
"Recursive component not of type set: " thy) cs; 
5094  824 

14235
281295a1bbaa
Fixed bug in mk_ind_def that caused the inductive definition package to
berghofe
parents:
13747
diff
changeset

825 
val cnames = map (try_term (fst o dest_Const o head_of) 
16432  826 
"Recursive set not previously declared as constant: " thy) cs; 
5094  827 

16432  828 
val save_thy = thy 
829 
> Theory.copy > cond_declare_consts declare_consts cs paramTs cnames; 

830 
val intros = map (check_rule save_thy cs) pre_intros; 

8401  831 
val induct_cases = map (#1 o #1) intros; 
6437  832 

9405  833 
val (thy1, result as {elims, induct, ...}) = 
11628  834 
add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs intros monos 
12180  835 
thy params paramTs cTs cnames induct_cases; 
8307  836 
val thy2 = thy1 
14235
281295a1bbaa
Fixed bug in mk_ind_def that caused the inductive definition package to
berghofe
parents:
13747
diff
changeset

837 
> put_inductives cnames ({names = cnames, coind = coind}, result) 
18463  838 
> add_cases_induct no_elim no_ind coind cnames elims induct 
839 
> Theory.parent_path; 

6437  840 
in (thy2, result) end; 
5094  841 

12180  842 
fun add_inductive verbose coind c_strings intro_srcs raw_monos thy = 
5094  843 
let 
16975  844 
val cs = map (Sign.read_term thy) c_strings; 
6424  845 

846 
val intr_names = map (fst o fst) intro_srcs; 

16432  847 
fun read_rule s = Thm.read_cterm thy (s, propT) 
18678  848 
handle ERROR msg => cat_error msg ("The error(s) above occurred for " ^ s); 
9405  849 
val intr_ts = map (Thm.term_of o read_rule o snd o fst) intro_srcs; 
18728  850 
val intr_atts = map (map (Attrib.attribute thy) o snd) intro_srcs; 
16432  851 
val (cs', intr_ts') = unify_consts thy cs intr_ts; 
5094  852 

18418
bf448d999b7e
rearranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18377
diff
changeset

853 
val (monos, thy') = thy > IsarThy.apply_theorems raw_monos; 
6424  854 
in 
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

855 
add_inductive_i verbose false "" coind false false cs' 
12180  856 
((intr_names ~~ intr_ts') ~~ intr_atts) monos thy' 
5094  857 
end; 
858 

6424  859 

860 

6437  861 
(** package setup **) 
862 

863 
(* setup theory *) 

864 

8634  865 
val setup = 
18708  866 
InductiveData.init #> 
9625  867 
Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args, 
18708  868 
"dynamic case analysis on sets")] #> 
18728  869 
Attrib.add_attributes [("mono", Attrib.add_del_args mono_add mono_del, 
870 
"declaration of monotonicity rule")]; 

6437  871 

872 

873 
(* outer syntax *) 

6424  874 

17057  875 
local structure P = OuterParse and K = OuterKeyword in 
6424  876 

12180  877 
fun mk_ind coind ((sets, intrs), monos) = 
878 
#1 o add_inductive true coind sets (map P.triple_swap intrs) monos; 

6424  879 

880 
fun ind_decl coind = 

12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12798
diff
changeset

881 
Scan.repeat1 P.term  
9598  882 
(P.$$$ "intros"  
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12798
diff
changeset

883 
P.!!! (Scan.repeat1 (P.opt_thm_name ":"  P.prop)))  
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12798
diff
changeset

884 
Scan.optional (P.$$$ "monos"  P.!!! P.xthms1) [] 
6424  885 
>> (Toplevel.theory o mk_ind coind); 
886 

6723  887 
val inductiveP = 
888 
OuterSyntax.command "inductive" "define inductive sets" K.thy_decl (ind_decl false); 

889 

890 
val coinductiveP = 

891 
OuterSyntax.command "coinductive" "define coinductive sets" K.thy_decl (ind_decl true); 

6424  892 

7107  893 

894 
val ind_cases = 

12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12798
diff
changeset

895 
P.and_list1 (P.opt_thm_name ":"  Scan.repeat1 P.prop) 
7107  896 
>> (Toplevel.theory o inductive_cases); 
897 

898 
val inductive_casesP = 

9804  899 
OuterSyntax.command "inductive_cases" 
9598  900 
"create simplified instances of elimination rules (improper)" K.thy_script ind_cases; 
7107  901 

12180  902 
val _ = OuterSyntax.add_keywords ["intros", "monos"]; 
7107  903 
val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP]; 
6424  904 

5094  905 
end; 
6424  906 

907 
end; 

15705  908 