author  wenzelm 
Fri, 01 Dec 2000 19:43:06 +0100  
changeset 10569  e8346dad78e1 
parent 10279  b223a9a3350e 
child 10729  1b3350c4ee92 
permissions  rwrr 
5094  1 
(* Title: HOL/Tools/inductive_package.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Stefan Berghofer, TU Muenchen 

5 
Copyright 1994 University of Cambridge 

9598  6 
1998 TU Muenchen 
5094  7 

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

10 
Features: 

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

13 
* mutually recursive definitions 

14 
* definitions involving arbitrary monotone operators 

15 
* automatically proves introduction and elimination rules 

5094  16 

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

5094  19 

20 
Introduction rules have the form 

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

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

24 
ti, t are any terms 

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

26 

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

5094  29 
*) 
30 

31 
signature INDUCTIVE_PACKAGE = 

32 
sig 

6424  33 
val quiet_mode: bool ref 
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

34 
val unify_consts: Sign.sg > term list > term list > term list * term list 
9116
9df44b5c610b
get_inductive now returns None instead of raising an exception.
berghofe
parents:
9072
diff
changeset

35 
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

36 
{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

37 
intrs: thm list, mk_cases: string > thm, mono: thm, unfold: thm}) option 
6437  38 
val print_inductives: theory > unit 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

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

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

41 
val get_monos: theory > thm list 
6424  42 
val add_inductive_i: bool > bool > bstring > bool > bool > bool > term list > 
6521  43 
theory attribute list > ((bstring * term) * theory attribute list) list > 
44 
thm list > thm list > theory > theory * 

6424  45 
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm, 
6437  46 
intrs: thm list, mk_cases: string > thm, mono: thm, unfold: thm} 
6521  47 
val add_inductive: bool > bool > string list > Args.src list > 
48 
((bstring * string) * Args.src list) list > (xstring * Args.src list) list > 

49 
(xstring * Args.src list) list > theory > theory * 

6424  50 
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm, 
6437  51 
intrs: thm list, mk_cases: string > thm, mono: thm, unfold: thm} 
9598  52 
val inductive_cases: ((bstring * Args.src list) * string list) * Comment.text 
7107  53 
> theory > theory 
9598  54 
val inductive_cases_i: ((bstring * theory attribute list) * term list) * Comment.text 
7107  55 
> theory > theory 
6437  56 
val setup: (theory > theory) list 
5094  57 
end; 
58 

6424  59 
structure InductivePackage: INDUCTIVE_PACKAGE = 
5094  60 
struct 
61 

9598  62 

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

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

64 

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

65 
(* data kind 'HOL/inductive' *) 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

66 

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

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

68 
{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

69 
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

70 

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

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

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

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

74 
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

75 

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

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

77 
val copy = I; 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

78 
val prep_ext = I; 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

79 
fun merge ((tab1, monos1), (tab2, monos2)) = (Symtab.merge (K true) (tab1, tab2), 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

80 
Library.generic_merge Thm.eq_thm I I monos1 monos2); 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

81 

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

82 
fun print sg (tab, monos) = 
8720  83 
[Pretty.strs ("(co)inductives:" :: map #1 (Sign.cond_extern_table sg Sign.constK tab)), 
10008  84 
Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_sg sg) monos)] 
8720  85 
> Pretty.chunks > Pretty.writeln; 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

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

87 

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

88 
structure InductiveData = TheoryDataFun(InductiveArgs); 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

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

90 

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

91 

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

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

93 

9116
9df44b5c610b
get_inductive now returns None instead of raising an exception.
berghofe
parents:
9072
diff
changeset

94 
fun get_inductive thy name = Symtab.lookup (fst (InductiveData.get thy), name); 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

95 

9598  96 
fun the_inductive thy name = 
97 
(case get_inductive thy name of 

98 
None => error ("Unknown (co)inductive set " ^ quote name) 

99 
 Some info => info); 

100 

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

101 
fun put_inductives names info thy = 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

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

103 
fun upd ((tab, monos), name) = (Symtab.update_new ((name, info), tab), monos); 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

104 
val tab_monos = foldl upd (InductiveData.get thy, names) 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

105 
handle Symtab.DUP name => error ("Duplicate definition of (co)inductive set " ^ quote name); 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

106 
in InductiveData.put tab_monos thy end; 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

107 

8277  108 

7710
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 
(** monotonicity rules **) 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

111 

9831  112 
val get_monos = #2 o InductiveData.get; 
113 
fun map_monos f = InductiveData.map (Library.apsnd f); 

8277  114 

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

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

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

117 
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

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

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

120 
 _ => [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

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

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

123 
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

124 
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

125 
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

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

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

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

129 

8634  130 

131 
(* attributes *) 

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

132 

9831  133 
fun mono_add_global (thy, thm) = (map_monos (Drule.add_rules (mk_mono thm)) thy, thm); 
134 
fun mono_del_global (thy, thm) = (map_monos (Drule.del_rules (mk_mono thm)) thy, thm); 

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

135 

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

136 
val mono_attr = 
8634  137 
(Attrib.add_del_args mono_add_global mono_del_global, 
138 
Attrib.add_del_args Attrib.undef_local_attribute Attrib.undef_local_attribute); 

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

139 

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

140 

7107  141 

6424  142 
(** utilities **) 
143 

144 
(* messages *) 

145 

5662  146 
val quiet_mode = ref false; 
147 
fun message s = if !quiet_mode then () else writeln s; 

148 

6424  149 
fun coind_prefix true = "co" 
150 
 coind_prefix false = ""; 

151 

152 

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

153 
(* the following code ensures that each recursive set *) 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

154 
(* always has the same type in all introduction rules *) 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

155 

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

156 
fun unify_consts sign cs intr_ts = 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

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

158 
val {tsig, ...} = Sign.rep_sg sign; 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

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

160 
foldl_aterms (fn (cs, Const c) => c ins cs  (cs, _) => cs); 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

161 
fun varify (t, (i, ts)) = 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

162 
let val t' = map_term_types (incr_tvar (i + 1)) (Type.varify (t, [])) 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

163 
in (maxidx_of_term t', t'::ts) end; 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

164 
val (i, cs') = foldr varify (cs, (~1, [])); 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

165 
val (i', intr_ts') = foldr varify (intr_ts, (i, [])); 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

166 
val rec_consts = foldl add_term_consts_2 ([], cs'); 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

167 
val intr_consts = foldl add_term_consts_2 ([], intr_ts'); 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

168 
fun unify (env, (cname, cT)) = 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

169 
let val consts = map snd (filter (fn c => fst c = cname) intr_consts) 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

170 
in foldl (fn ((env', j'), Tp) => (Type.unify tsig j' env' Tp)) 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

171 
(env, (replicate (length consts) cT) ~~ consts) 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

172 
end; 
8410
5902c02fa122
Type.unify now uses Vartab instead of association lists.
berghofe
parents:
8401
diff
changeset

173 
val (env, _) = foldl unify ((Vartab.empty, i'), rec_consts); 
5902c02fa122
Type.unify now uses Vartab instead of association lists.
berghofe
parents:
8401
diff
changeset

174 
fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars_Vartab env T 
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

175 
in if T = T' then T else typ_subst_TVars_2 env T' end; 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

176 
val subst = fst o Type.freeze_thaw o 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

177 
(map_term_types (typ_subst_TVars_2 env)) 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

178 

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

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

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

181 
(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

182 

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

183 

6424  184 
(* misc *) 
185 

5094  186 
val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (concl_of vimageD); 
187 

10212  188 
val vimage_name = Sign.intern_const (Theory.sign_of Inverse_Image.thy) "vimage"; 
6394  189 
val mono_name = Sign.intern_const (Theory.sign_of Ord.thy) "mono"; 
5094  190 

191 
(* make injections needed in mutually recursive definitions *) 

192 

193 
fun mk_inj cs sumT c x = 

194 
let 

195 
fun mk_inj' T n i = 

196 
if n = 1 then x else 

197 
let val n2 = n div 2; 

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

199 
in 

200 
if i <= n2 then 

201 
Const ("Inl", T1 > T) $ (mk_inj' T1 n2 i) 

202 
else 

203 
Const ("Inr", T2 > T) $ (mk_inj' T2 (n  n2) (i  n2)) 

204 
end 

205 
in mk_inj' sumT (length cs) (1 + find_index_eq c cs) 

206 
end; 

207 

208 
(* make "vimage" terms for selecting out components of mutually rec.def. *) 

209 

210 
fun mk_vimage cs sumT t c = if length cs < 2 then t else 

211 
let 

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

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

214 
in 

215 
Const (vimage_name, vimageT) $ 

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

217 
end; 

218 

6424  219 

220 

221 
(** wellformedness checks **) 

5094  222 

223 
fun err_in_rule sign t msg = error ("Illformed introduction rule\n" ^ 

224 
(Sign.string_of_term sign t) ^ "\n" ^ msg); 

225 

226 
fun err_in_prem sign t p msg = error ("Illformed premise\n" ^ 

227 
(Sign.string_of_term sign p) ^ "\nin introduction rule\n" ^ 

228 
(Sign.string_of_term sign t) ^ "\n" ^ msg); 

229 

230 
val msg1 = "Conclusion of introduction rule must have form\ 

231 
\ ' t : S_i '"; 

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

232 
val msg2 = "Nonatomic premise"; 
5094  233 
val msg3 = "Recursion term on left of member symbol"; 
234 

235 
fun check_rule sign cs r = 

236 
let 

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

237 
fun check_prem prem = if can HOLogic.dest_Trueprop prem then () 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

238 
else err_in_prem sign r prem msg2; 
5094  239 

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

240 
in (case HOLogic.dest_Trueprop (Logic.strip_imp_concl r) of 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

241 
(Const ("op :", _) $ t $ u) => 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

242 
if u mem cs then 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

243 
if exists (Logic.occs o (rpair t)) cs then 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

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

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

246 
seq check_prem (Logic.strip_imp_prems r) 
5094  247 
else err_in_rule sign r msg1 
248 
 _ => err_in_rule sign r msg1) 

249 
end; 

250 

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

251 
fun try' f msg sign t = (case (try f t) of 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

252 
Some x => x 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

253 
 None => error (msg ^ Sign.string_of_term sign t)); 
5094  254 

6424  255 

5094  256 

6424  257 
(*** properties of (co)inductive sets ***) 
258 

259 
(** elimination rules **) 

5094  260 

8375  261 
fun mk_elims cs cTs params intr_ts intr_names = 
5094  262 
let 
263 
val used = foldr add_term_names (intr_ts, []); 

264 
val [aname, pname] = variantlist (["a", "P"], used); 

265 
val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT)); 

266 

267 
fun dest_intr r = 

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

269 
HOLogic.dest_Trueprop (Logic.strip_imp_concl r) 

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

271 

8380  272 
val intrs = map dest_intr intr_ts ~~ intr_names; 
5094  273 

274 
fun mk_elim (c, T) = 

275 
let 

276 
val a = Free (aname, T); 

277 

278 
fun mk_elim_prem (_, t, ts) = 

279 
list_all_free (map dest_Free ((foldr add_term_frees (t::ts, [])) \\ params), 

280 
Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P)); 

8375  281 
val c_intrs = (filter (equal c o #1 o #1) intrs); 
5094  282 
in 
8375  283 
(Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) :: 
284 
map mk_elim_prem (map #1 c_intrs), P), map #2 c_intrs) 

5094  285 
end 
286 
in 

287 
map mk_elim (cs ~~ cTs) 

288 
end; 

9598  289 

6424  290 

291 

292 
(** premises and conclusions of induction rules **) 

5094  293 

294 
fun mk_indrule cs cTs params intr_ts = 

295 
let 

296 
val used = foldr add_term_names (intr_ts, []); 

297 

298 
(* predicates for induction rule *) 

299 

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

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

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

303 

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

305 

306 
fun mk_ind_prem r = 

307 
let 

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

309 

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

310 
val pred_of = curry (Library.gen_assoc (op aconv)) (cs ~~ preds); 
5094  311 

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

312 
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

313 
(case pred_of u of 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

314 
None => (m $ fst (subst t) $ fst (subst u), None) 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

315 
 Some P => (HOLogic.conj $ s $ (P $ t), Some (s, P $ t))) 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

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

317 
(case pred_of s of 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

318 
Some P => (HOLogic.mk_binop "op Int" 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

319 
(s, HOLogic.Collect_const (HOLogic.dest_setT 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

320 
(fastype_of s)) $ P), None) 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

321 
 None => (case s of 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

322 
(t $ u) => (fst (subst t) $ fst (subst u), None) 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

323 
 (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), None) 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

324 
 _ => (s, None))); 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

325 

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

326 
fun mk_prem (s, prems) = (case subst s of 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

327 
(_, Some (t, u)) => t :: u :: prems 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

328 
 (t, _) => t :: prems); 
9598  329 

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

332 

333 
in list_all_free (frees, 

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

334 
Logic.list_implies (map HOLogic.mk_Trueprop (foldr mk_prem 
5094  335 
(map HOLogic.dest_Trueprop (Logic.strip_imp_prems r), [])), 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

336 
HOLogic.mk_Trueprop (the (pred_of u) $ t))) 
5094  337 
end; 
338 

339 
val ind_prems = map mk_ind_prem intr_ts; 

340 

341 
(* make conclusions for induction rules *) 

342 

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

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

345 
val Ts = HOLogic.prodT_factors T; 

346 
val (frees, x') = foldr (fn (T', (fs, s)) => 

347 
((Free (s, T'))::fs, bump_string s)) (Ts, ([], x)); 

348 
val tuple = HOLogic.mk_tuple T frees; 

349 
in ((HOLogic.mk_binop "op >" 

350 
(HOLogic.mk_mem (tuple, c), P $ tuple))::ts, x') 

351 
end; 

352 

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

353 
val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj 
5094  354 
(fst (foldr mk_ind_concl (cs ~~ preds, ([], "xa"))))) 
355 

356 
in (preds, ind_prems, mutual_ind_concl) 

357 
end; 

358 

6424  359 

5094  360 

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

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

362 

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

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

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

365 
HH ==> (x1:A1 > P1 x1) & ... & (xn:An > Pn xn) 
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

366 
into ith projection: 
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

367 
xi:Ai ==> HH ==> Pi xi 
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

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

369 

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

370 
fun project_rules [name] rule = [(name, rule)] 
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

371 
 project_rules names mutual_rule = 
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

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

373 
val n = length names; 
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

374 
fun proj i = 
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

375 
(if i < n then (fn th => th RS conjunct1) else I) 
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

376 
(Library.funpow (i  1) (fn th => th RS conjunct2) mutual_rule) 
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

377 
RS mp > Thm.permute_prems 0 ~1 > Drule.standard; 
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

378 
in names ~~ map proj (1 upto n) end; 
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

379 

8375  380 
fun add_cases_induct no_elim no_ind names elims induct induct_cases = 
8316
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

381 
let 
9405  382 
fun cases_spec (name, elim) thy = 
383 
thy 

384 
> Theory.add_path (Sign.base_name name) 

10279  385 
> (#1 o PureThy.add_thms [(("cases", elim), [InductAttrib.cases_set_global name])]) 
9405  386 
> Theory.parent_path; 
8375  387 
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

388 

9405  389 
fun induct_spec (name, th) = (#1 o PureThy.add_thms 
10279  390 
[(("", th), [RuleCases.case_names induct_cases, InductAttrib.induct_set_global name])]); 
8401  391 
val induct_specs = if no_ind then [] else map induct_spec (project_rules names induct); 
9405  392 
in Library.apply (cases_specs @ induct_specs) end; 
8316
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

393 

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

394 

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

395 

6424  396 
(*** proofs for (co)inductive sets ***) 
397 

398 
(** prove monotonicity **) 

5094  399 

400 
fun prove_mono setT fp_fun monos thy = 

401 
let 

6427  402 
val _ = message " Proving monotonicity ..."; 
5094  403 

6394  404 
val mono = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop 
5094  405 
(Const (mono_name, (setT > setT) > HOLogic.boolT) $ fp_fun))) 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

406 
(fn _ => [rtac monoI 1, REPEAT (ares_tac (get_monos thy @ flat (map mk_mono monos)) 1)]) 
5094  407 

408 
in mono end; 

409 

6424  410 

411 

412 
(** prove introduction rules **) 

5094  413 

414 
fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy = 

415 
let 

6427  416 
val _ = message " Proving the introduction rules ..."; 
5094  417 

418 
val unfold = standard (mono RS (fp_def RS 

10186  419 
(if coind then def_gfp_unfold else def_lfp_unfold))); 
5094  420 

421 
fun select_disj 1 1 = [] 

422 
 select_disj _ 1 = [rtac disjI1] 

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

424 

425 
val intrs = map (fn (i, intr) => prove_goalw_cterm rec_sets_defs 

6394  426 
(cterm_of (Theory.sign_of thy) intr) (fn prems => 
5094  427 
[(*insert prems and underlying sets*) 
428 
cut_facts_tac prems 1, 

429 
stac unfold 1, 

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

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

432 
EVERY1 (select_disj (length intr_ts) i), 

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

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

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

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

437 
rewrite_goals_tac con_defs, 

438 
REPEAT (rtac refl 1)])) (1 upto (length intr_ts) ~~ intr_ts) 

439 

440 
in (intrs, unfold) end; 

441 

6424  442 

443 

444 
(** prove elimination rules **) 

5094  445 

8375  446 
fun prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy = 
5094  447 
let 
6427  448 
val _ = message " Proving the elimination rules ..."; 
5094  449 

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

450 
val rules1 = [CollectE, disjE, make_elim vimageD, exE]; 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

451 
val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ 
5094  452 
map make_elim [Inl_inject, Inr_inject]; 
8375  453 
in 
454 
map (fn (t, cases) => prove_goalw_cterm rec_sets_defs 

6394  455 
(cterm_of (Theory.sign_of thy) t) (fn prems => 
5094  456 
[cut_facts_tac [hd prems] 1, 
457 
dtac (unfold RS subst) 1, 

458 
REPEAT (FIRSTGOAL (eresolve_tac rules1)), 

459 
REPEAT (FIRSTGOAL (eresolve_tac rules2)), 

460 
EVERY (map (fn prem => 

8375  461 
DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))]) 
462 
> RuleCases.name cases) 

463 
(mk_elims cs cTs params intr_ts intr_names) 

464 
end; 

5094  465 

6424  466 

5094  467 
(** derivation of simplified elimination rules **) 
468 

469 
(*Applies freeness of the given constructors, which *must* be unfolded by 

9598  470 
the given defs. Cannot simply use the local con_defs because con_defs=[] 
5094  471 
for inference systems. 
472 
*) 

473 

7107  474 
(*cprop should have the form t:Si where Si is an inductive set*) 
9598  475 

476 
val mk_cases_err = "mk_cases: proposition not of form 't : S_i'"; 

477 

478 
fun mk_cases_i elims ss cprop = 

7107  479 
let 
480 
val prem = Thm.assume cprop; 

9598  481 
val tac = ALLGOALS (InductMethod.simp_case_tac false ss) THEN prune_params_tac; 
9298  482 
fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic tac (prem RS rl)); 
7107  483 
in 
484 
(case get_first (try mk_elim) elims of 

485 
Some r => r 

486 
 None => error (Pretty.string_of (Pretty.block 

9598  487 
[Pretty.str mk_cases_err, Pretty.fbrk, Display.pretty_cterm cprop]))) 
7107  488 
end; 
489 

6141  490 
fun mk_cases elims s = 
9598  491 
mk_cases_i elims (simpset()) (Thm.read_cterm (Thm.sign_of_thm (hd elims)) (s, propT)); 
492 

493 
fun smart_mk_cases thy ss cprop = 

494 
let 

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

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

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

498 
in mk_cases_i elims ss cprop end; 

7107  499 

500 

501 
(* inductive_cases(_i) *) 

502 

503 
fun gen_inductive_cases prep_att prep_const prep_prop 

9598  504 
(((name, raw_atts), raw_props), comment) thy = 
505 
let 

506 
val ss = Simplifier.simpset_of thy; 

507 
val sign = Theory.sign_of thy; 

508 
val cprops = map (Thm.cterm_of sign o prep_prop (ProofContext.init thy)) raw_props; 

509 
val atts = map (prep_att thy) raw_atts; 

510 
val thms = map (smart_mk_cases thy ss) cprops; 

511 
in thy > IsarThy.have_theorems_i [(((name, atts), map Thm.no_attributes thms), comment)] end; 

5094  512 

7107  513 
val inductive_cases = 
514 
gen_inductive_cases Attrib.global_attribute Sign.intern_const ProofContext.read_prop; 

515 

516 
val inductive_cases_i = gen_inductive_cases (K I) (K I) ProofContext.cert_prop; 

517 

6424  518 

9598  519 
(* mk_cases_meth *) 
520 

521 
fun mk_cases_meth (ctxt, raw_props) = 

522 
let 

523 
val thy = ProofContext.theory_of ctxt; 

524 
val ss = Simplifier.get_local_simpset ctxt; 

525 
val cprops = map (Thm.cterm_of (Theory.sign_of thy) o ProofContext.read_prop ctxt) raw_props; 

526 
in Method.erule (map (smart_mk_cases thy ss) cprops) end; 

527 

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

529 

530 

6424  531 

532 
(** prove induction rule **) 

5094  533 

534 
fun prove_indrule cs cTs sumT rec_const params intr_ts mono 

535 
fp_def rec_sets_defs thy = 

536 
let 

6427  537 
val _ = message " Proving the induction rule ..."; 
5094  538 

6394  539 
val sign = Theory.sign_of thy; 
5094  540 

7293  541 
val sum_case_rewrites = (case ThyInfo.lookup_theory "Datatype" of 
542 
None => [] 

543 
 Some thy' => map mk_meta_eq (PureThy.get_thms thy' "sum.cases")); 

544 

5094  545 
val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts; 
546 

547 
(* make predicate for instantiation of abstract induction rule *) 

548 

549 
fun mk_ind_pred _ [P] = P 

550 
 mk_ind_pred T Ps = 

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

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

7293  553 
in Const ("Datatype.sum.sum_case", 
5094  554 
[T1 > HOLogic.boolT, T2 > HOLogic.boolT, T] > HOLogic.boolT) $ 
555 
mk_ind_pred T1 (take (n, Ps)) $ mk_ind_pred T2 (drop (n, Ps)) 

556 
end; 

557 

558 
val ind_pred = mk_ind_pred sumT preds; 

559 

560 
val ind_concl = HOLogic.mk_Trueprop 

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

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

563 

564 
(* simplification rules for vimage and Collect *) 

565 

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

567 
map (fn c => prove_goalw_cterm [] (cterm_of sign 

568 
(HOLogic.mk_Trueprop (HOLogic.mk_eq 

569 
(mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c, 

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

571 
nth_elem (find_index_eq c cs, preds))))) 

7293  572 
(fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, 
5094  573 
rtac refl 1])) cs; 
574 

575 
val induct = prove_goalw_cterm [] (cterm_of sign 

576 
(Logic.list_implies (ind_prems, ind_concl))) (fn prems => 

577 
[rtac (impI RS allI) 1, 

10202  578 
DETERM (etac (mono RS (fp_def RS def_lfp_induct)) 1), 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

579 
rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)), 
5094  580 
fold_goals_tac rec_sets_defs, 
581 
(*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

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

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

585 
REPEAT (FIRSTGOAL (etac conjE ORELSE' hyp_subst_tac)), 
7293  586 
rewrite_goals_tac sum_case_rewrites, 
5094  587 
EVERY (map (fn prem => 
5149  588 
DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]); 
5094  589 

590 
val lemma = prove_goalw_cterm rec_sets_defs (cterm_of sign 

591 
(Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems => 

592 
[cut_facts_tac prems 1, 

593 
REPEAT (EVERY 

594 
[REPEAT (resolve_tac [conjI, impI] 1), 

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

7293  596 
rewrite_goals_tac sum_case_rewrites, 
5094  597 
atac 1])]) 
598 

599 
in standard (split_rule (induct RS lemma)) 

600 
end; 

601 

6424  602 

603 

604 
(*** specification of (co)inductive sets ****) 

605 

606 
(** definitional introduction of (co)inductive sets **) 

5094  607 

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

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

609 
params paramTs cTs cnames = 
5094  610 
let 
611 
val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs; 

612 
val setT = HOLogic.mk_setT sumT; 

613 

6394  614 
val fp_name = if coind then Sign.intern_const (Theory.sign_of Gfp.thy) "gfp" 
615 
else Sign.intern_const (Theory.sign_of Lfp.thy) "lfp"; 

5094  616 

5149  617 
val used = foldr add_term_names (intr_ts, []); 
618 
val [sname, xname] = variantlist (["S", "x"], used); 

619 

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

622 
(* is transformed into *) 

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

624 

625 
fun transform_rule r = 

626 
let 

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

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

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

632 

633 
in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P)) 

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

634 
(frees, foldr1 HOLogic.mk_conj 
5149  635 
(((HOLogic.eq_const sumT) $ Free (xname, sumT) $ (mk_inj cs sumT u t)):: 
5094  636 
(map (subst o HOLogic.dest_Trueprop) 
637 
(Logic.strip_imp_prems r)))) 

638 
end 

639 

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

641 

5149  642 
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

643 
absfree (xname, sumT, foldr1 HOLogic.mk_disj (map transform_rule intr_ts))); 
5094  644 

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

646 

647 
val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name; 

6394  648 
val full_rec_name = Sign.full_name (Theory.sign_of thy) rec_name; 
5094  649 

650 
val rec_const = list_comb 

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

652 

653 
val fp_def_term = Logic.mk_equals (rec_const, 

654 
Const (fp_name, (setT > setT) > setT) $ fp_fun) 

655 

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

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

658 

8433  659 
val (thy', [fp_def :: rec_sets_defs]) = 
660 
thy 

661 
> (if declare_consts then 

662 
Theory.add_consts_i (map (fn (c, n) => 

663 
(n, paramTs > fastype_of c, NoSyn)) (cs ~~ cnames)) 

664 
else I) 

665 
> (if length cs < 2 then I 

666 
else Theory.add_consts_i [(rec_name, paramTs > setT, NoSyn)]) 

667 
> Theory.add_path rec_name 

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

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

670 
val mono = prove_mono setT fp_fun monos thy' 
5094  671 

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

672 
in 
9598  673 
(thy', mono, fp_def, rec_sets_defs, rec_const, sumT) 
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

674 
end; 
5094  675 

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

676 
fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs 
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

677 
atts intros monos con_defs thy params paramTs cTs cnames induct_cases = 
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

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

679 
val _ = if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^ 
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

680 
commas_quote cnames) else (); 
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

681 

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

682 
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

683 

9939  684 
val (thy1, mono, fp_def, rec_sets_defs, rec_const, sumT) = 
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

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

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

687 

5094  688 
val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts con_defs 
9939  689 
rec_sets_defs thy1; 
5094  690 
val elims = if no_elim then [] else 
9939  691 
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

692 
val raw_induct = if no_ind then Drule.asm_rl else 
5094  693 
if coind then standard (rule_by_tactic 
5553  694 
(rewrite_tac [mk_meta_eq vimage_Un] THEN 
5094  695 
fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct))) 
696 
else 

697 
prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def 

9939  698 
rec_sets_defs thy1; 
5108  699 
val induct = if coind orelse no_ind orelse length cs > 1 then raw_induct 
5094  700 
else standard (raw_induct RSN (2, rev_mp)); 
701 

9939  702 
val (thy2, intrs') = 
703 
thy1 > PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts); 

704 
val (thy3, [intrs'']) = 

705 
thy2 

706 
> PureThy.add_thmss [(("intros", intrs'), atts)] 

8433  707 
>> (if no_elim then I else #1 o PureThy.add_thmss [(("elims", elims), [])]) 
708 
>> (if no_ind then I else #1 o PureThy.add_thms 

8401  709 
[((coind_prefix coind ^ "induct", induct), [RuleCases.case_names induct_cases])]) 
8433  710 
>> Theory.parent_path; 
9939  711 
val elims' = if no_elim then elims else PureThy.get_thms thy3 "elims"; (* FIXME improve *) 
712 
val induct' = if no_ind then induct else PureThy.get_thm thy3 (coind_prefix coind ^ "induct"); (* FIXME improve *) 

713 
in (thy3, 

5094  714 
{defs = fp_def::rec_sets_defs, 
715 
mono = mono, 

716 
unfold = unfold, 

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

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

719 
mk_cases = mk_cases elims', 
5094  720 
raw_induct = raw_induct, 
7798
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7710
diff
changeset

721 
induct = induct'}) 
5094  722 
end; 
723 

6424  724 

725 

726 
(** axiomatic introduction of (co)inductive sets **) 

5094  727 

728 
fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs 

8401  729 
atts intros monos con_defs thy params paramTs cTs cnames induct_cases = 
5094  730 
let 
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

731 
val _ = message (coind_prefix coind ^ "inductive set(s) " ^ commas_quote cnames); 
5094  732 

6424  733 
val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros); 
9939  734 
val (thy1, _, fp_def, rec_sets_defs, _, _) = 
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

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

736 
params paramTs cTs cnames; 
8375  737 
val (elim_ts, elim_cases) = Library.split_list (mk_elims cs cTs params intr_ts intr_names); 
5094  738 
val (_, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts; 
739 
val ind_t = Logic.list_implies (ind_prems, mutual_ind_concl); 

9598  740 

9939  741 
val (thy2, [intrs, raw_elims]) = 
742 
thy1 

743 
> (PureThy.add_axiomss_i o map Thm.no_attributes) 

744 
[("raw_intros", intr_ts), ("raw_elims", elim_ts)] 

9598  745 
>> (if coind then I else 
8433  746 
#1 o PureThy.add_axioms_i [(("raw_induct", ind_t), [apsnd (standard o split_rule)])]); 
5094  747 

9598  748 
val elims = map2 (fn (th, cases) => RuleCases.name cases th) (raw_elims, elim_cases); 
9939  749 
val raw_induct = if coind then Drule.asm_rl else PureThy.get_thm thy2 "raw_induct"; 
5094  750 
val induct = if coind orelse length cs > 1 then raw_induct 
751 
else standard (raw_induct RSN (2, rev_mp)); 

752 

9939  753 
val (thy3, intrs') = 
754 
thy2 > PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts); 

755 
val (thy4, [intrs'', elims']) = 

756 
thy3 

757 
> PureThy.add_thmss [(("intros", intrs'), atts), (("elims", elims), [])] 

8433  758 
>> (if coind then I 
759 
else #1 o PureThy.add_thms [(("induct", induct), [RuleCases.case_names induct_cases])]) 

760 
>> Theory.parent_path; 

9939  761 
val induct' = if coind then raw_induct else PureThy.get_thm thy4 "induct"; 
762 
in (thy4, 

9235  763 
{defs = fp_def :: rec_sets_defs, 
8312
b470bc28b59d
add_cases_induct: accomodate no_elim and no_ind flags;
wenzelm
parents:
8307
diff
changeset

764 
mono = Drule.asm_rl, 
b470bc28b59d
add_cases_induct: accomodate no_elim and no_ind flags;
wenzelm
parents:
8307
diff
changeset

765 
unfold = Drule.asm_rl, 
9939  766 
intrs = intrs'', 
8433  767 
elims = elims', 
768 
mk_cases = mk_cases elims', 

5094  769 
raw_induct = raw_induct, 
7798
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7710
diff
changeset

770 
induct = induct'}) 
5094  771 
end; 
772 

6424  773 

774 

775 
(** introduction of (co)inductive sets **) 

5094  776 

777 
fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs 

6521  778 
atts intros monos con_defs thy = 
5094  779 
let 
6424  780 
val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions"); 
6394  781 
val sign = Theory.sign_of thy; 
5094  782 

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

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

785 
val paramTs = map (try' (snd o dest_Free) "Parameter in recursive\ 

786 
\ component is not a free variable: " sign) params; 

787 

788 
val cTs = map (try' (HOLogic.dest_setT o fastype_of) 

789 
"Recursive component not of type set: " sign) cs; 

790 

6437  791 
val full_cnames = map (try' (fst o dest_Const o head_of) 
5094  792 
"Recursive set not previously declared as constant: " sign) cs; 
6437  793 
val cnames = map Sign.base_name full_cnames; 
5094  794 

6424  795 
val _ = seq (check_rule sign cs o snd o fst) intros; 
8401  796 
val induct_cases = map (#1 o #1) intros; 
6437  797 

9405  798 
val (thy1, result as {elims, induct, ...}) = 
10569  799 
(if ! quick_and_dirty andalso not coind (* FIXME *) then add_ind_axm else add_ind_def) 
6521  800 
verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos 
8401  801 
con_defs thy params paramTs cTs cnames induct_cases; 
8307  802 
val thy2 = thy1 
803 
> put_inductives full_cnames ({names = full_cnames, coind = coind}, result) 

9405  804 
> add_cases_induct no_elim (no_ind orelse coind) full_cnames elims induct induct_cases; 
6437  805 
in (thy2, result) end; 
5094  806 

6424  807 

5094  808 

6424  809 
(** external interface **) 
810 

6521  811 
fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy = 
5094  812 
let 
6394  813 
val sign = Theory.sign_of thy; 
8100  814 
val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termT) c_strings; 
6424  815 

6521  816 
val atts = map (Attrib.global_attribute thy) srcs; 
6424  817 
val intr_names = map (fst o fst) intro_srcs; 
9405  818 
fun read_rule s = Thm.read_cterm sign (s, propT) 
819 
handle ERROR => error ("The error(s) above occurred for " ^ s); 

820 
val intr_ts = map (Thm.term_of o read_rule o snd o fst) intro_srcs; 

6424  821 
val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs; 
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

822 
val (cs', intr_ts') = unify_consts sign cs intr_ts; 
5094  823 

6424  824 
val ((thy', con_defs), monos) = thy 
825 
> IsarThy.apply_theorems raw_monos 

826 
> apfst (IsarThy.apply_theorems raw_con_defs); 

827 
in 

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

828 
add_inductive_i verbose false "" coind false false cs' 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

829 
atts ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy' 
5094  830 
end; 
831 

6424  832 

833 

6437  834 
(** package setup **) 
835 

836 
(* setup theory *) 

837 

8634  838 
val setup = 
839 
[InductiveData.init, 

9625  840 
Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args, 
9598  841 
"dynamic case analysis on sets")], 
9893  842 
Attrib.add_attributes [("mono", mono_attr, "declaration of monotonicity rule")]]; 
6437  843 

844 

845 
(* outer syntax *) 

6424  846 

6723  847 
local structure P = OuterParse and K = OuterSyntax.Keyword in 
6424  848 

6521  849 
fun mk_ind coind (((sets, (atts, intrs)), monos), con_defs) = 
6723  850 
#1 o add_inductive true coind sets atts (map P.triple_swap intrs) monos con_defs; 
6424  851 

852 
fun ind_decl coind = 

6729  853 
(Scan.repeat1 P.term  P.marg_comment)  
9598  854 
(P.$$$ "intros"  
7152  855 
P.!!! (P.opt_attribs  Scan.repeat1 (P.opt_thm_name ":"  P.prop  P.marg_comment)))  
6729  856 
Scan.optional (P.$$$ "monos"  P.!!! P.xthms1  P.marg_comment) []  
857 
Scan.optional (P.$$$ "con_defs"  P.!!! P.xthms1  P.marg_comment) [] 

6424  858 
>> (Toplevel.theory o mk_ind coind); 
859 

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

862 

863 
val coinductiveP = 

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

6424  865 

7107  866 

867 
val ind_cases = 

9625  868 
P.opt_thm_name ":"  Scan.repeat1 P.prop  P.marg_comment 
7107  869 
>> (Toplevel.theory o inductive_cases); 
870 

871 
val inductive_casesP = 

9804  872 
OuterSyntax.command "inductive_cases" 
9598  873 
"create simplified instances of elimination rules (improper)" K.thy_script ind_cases; 
7107  874 

9643  875 
val _ = OuterSyntax.add_keywords ["intros", "monos", "con_defs"]; 
7107  876 
val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP]; 
6424  877 

5094  878 
end; 
6424  879 

880 

881 
end; 