author  wenzelm 
Thu, 17 Aug 2000 10:37:33 +0200  
changeset 9625  77506775481e 
parent 9598  65ee72db0236 
child 9643  c94db1a96f4e 
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)), 
84 
Pretty.big_list "monotonicity rules:" (map Display.pretty_thm monos)] 

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 

8277  112 
val get_monos = snd o InductiveData.get; 
113 
fun put_monos thms thy = InductiveData.put (fst (InductiveData.get thy), thms) thy; 

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 

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

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

134 

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

135 
fun map_rules_global f thy = put_monos (f (get_monos thy)) thy; 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

136 

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

137 
fun add_mono thm rules = Library.gen_union Thm.eq_thm (mk_mono thm, rules); 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

138 
fun del_mono thm rules = Library.gen_rems Thm.eq_thm (rules, mk_mono thm); 
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 
fun mk_att f g (x, thm) = (f (g thm) x, thm); 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

141 

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

142 
in 
8634  143 
val mono_add_global = mk_att map_rules_global add_mono; 
144 
val mono_del_global = mk_att map_rules_global del_mono; 

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

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

146 

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

147 
val mono_attr = 
8634  148 
(Attrib.add_del_args mono_add_global mono_del_global, 
149 
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

150 

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

151 

7107  152 

6424  153 
(** utilities **) 
154 

155 
(* messages *) 

156 

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

159 

6424  160 
fun coind_prefix true = "co" 
161 
 coind_prefix false = ""; 

162 

163 

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

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

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

166 

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

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

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

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

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

171 
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

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

173 
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

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

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

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

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

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

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

180 
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

181 
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

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

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

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

185 
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

186 
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

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

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

189 

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

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

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

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

193 

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

194 

6424  195 
(* misc *) 
196 

5094  197 
val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (concl_of vimageD); 
198 

6394  199 
val vimage_name = Sign.intern_const (Theory.sign_of Vimage.thy) "op ``"; 
200 
val mono_name = Sign.intern_const (Theory.sign_of Ord.thy) "mono"; 

5094  201 

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

203 

204 
fun mk_inj cs sumT c x = 

205 
let 

206 
fun mk_inj' T n i = 

207 
if n = 1 then x else 

208 
let val n2 = n div 2; 

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

210 
in 

211 
if i <= n2 then 

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

213 
else 

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

215 
end 

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

217 
end; 

218 

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

220 

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

222 
let 

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

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

225 
in 

226 
Const (vimage_name, vimageT) $ 

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

228 
end; 

229 

6424  230 

231 

232 
(** wellformedness checks **) 

5094  233 

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

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

236 

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

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

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

240 

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

242 
\ ' t : S_i '"; 

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

243 
val msg2 = "Nonatomic premise"; 
5094  244 
val msg3 = "Recursion term on left of member symbol"; 
245 

246 
fun check_rule sign cs r = 

247 
let 

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

248 
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

249 
else err_in_prem sign r prem msg2; 
5094  250 

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

251 
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

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

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

254 
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

255 
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

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

257 
seq check_prem (Logic.strip_imp_prems r) 
5094  258 
else err_in_rule sign r msg1 
259 
 _ => err_in_rule sign r msg1) 

260 
end; 

261 

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

262 
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

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

264 
 None => error (msg ^ Sign.string_of_term sign t)); 
5094  265 

6424  266 

5094  267 

6424  268 
(*** properties of (co)inductive sets ***) 
269 

270 
(** elimination rules **) 

5094  271 

8375  272 
fun mk_elims cs cTs params intr_ts intr_names = 
5094  273 
let 
274 
val used = foldr add_term_names (intr_ts, []); 

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

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

277 

278 
fun dest_intr r = 

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

280 
HOLogic.dest_Trueprop (Logic.strip_imp_concl r) 

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

282 

8380  283 
val intrs = map dest_intr intr_ts ~~ intr_names; 
5094  284 

285 
fun mk_elim (c, T) = 

286 
let 

287 
val a = Free (aname, T); 

288 

289 
fun mk_elim_prem (_, t, ts) = 

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

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

8375  292 
val c_intrs = (filter (equal c o #1 o #1) intrs); 
5094  293 
in 
8375  294 
(Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) :: 
295 
map mk_elim_prem (map #1 c_intrs), P), map #2 c_intrs) 

5094  296 
end 
297 
in 

298 
map mk_elim (cs ~~ cTs) 

299 
end; 

9598  300 

6424  301 

302 

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

5094  304 

305 
fun mk_indrule cs cTs params intr_ts = 

306 
let 

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

308 

309 
(* predicates for induction rule *) 

310 

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

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

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

314 

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

316 

317 
fun mk_ind_prem r = 

318 
let 

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

320 

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

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

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

323 
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

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

325 
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

326 
 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

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

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

329 
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

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

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

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

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

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

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

336 

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

337 
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

338 
(_, 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

339 
 (t, _) => t :: prems); 
9598  340 

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

343 

344 
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

345 
Logic.list_implies (map HOLogic.mk_Trueprop (foldr mk_prem 
5094  346 
(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

347 
HOLogic.mk_Trueprop (the (pred_of u) $ t))) 
5094  348 
end; 
349 

350 
val ind_prems = map mk_ind_prem intr_ts; 

351 

352 
(* make conclusions for induction rules *) 

353 

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

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

356 
val Ts = HOLogic.prodT_factors T; 

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

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

359 
val tuple = HOLogic.mk_tuple T frees; 

360 
in ((HOLogic.mk_binop "op >" 

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

362 
end; 

363 

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

364 
val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj 
5094  365 
(fst (foldr mk_ind_concl (cs ~~ preds, ([], "xa"))))) 
366 

367 
in (preds, ind_prems, mutual_ind_concl) 

368 
end; 

369 

6424  370 

5094  371 

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

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

373 

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

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

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

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

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

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

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

380 

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

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

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

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

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

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

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

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

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

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

390 

8375  391 
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

392 
let 
9405  393 
fun cases_spec (name, elim) thy = 
394 
thy 

395 
> Theory.add_path (Sign.base_name name) 

396 
> (#1 o PureThy.add_thms [(("cases", elim), [InductMethod.cases_set_global name])]) 

397 
> Theory.parent_path; 

8375  398 
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

399 

9405  400 
fun induct_spec (name, th) = (#1 o PureThy.add_thms 
401 
[(("", th), [RuleCases.case_names induct_cases, InductMethod.induct_set_global name])]); 

8401  402 
val induct_specs = if no_ind then [] else map induct_spec (project_rules names induct); 
9405  403 
in Library.apply (cases_specs @ induct_specs) end; 
8316
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

404 

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

405 

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

406 

6424  407 
(*** proofs for (co)inductive sets ***) 
408 

409 
(** prove monotonicity **) 

5094  410 

411 
fun prove_mono setT fp_fun monos thy = 

412 
let 

6427  413 
val _ = message " Proving monotonicity ..."; 
5094  414 

6394  415 
val mono = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop 
5094  416 
(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

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

419 
in mono end; 

420 

6424  421 

422 

423 
(** prove introduction rules **) 

5094  424 

425 
fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy = 

426 
let 

6427  427 
val _ = message " Proving the introduction rules ..."; 
5094  428 

429 
val unfold = standard (mono RS (fp_def RS 

430 
(if coind then def_gfp_Tarski else def_lfp_Tarski))); 

431 

432 
fun select_disj 1 1 = [] 

433 
 select_disj _ 1 = [rtac disjI1] 

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

435 

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

6394  437 
(cterm_of (Theory.sign_of thy) intr) (fn prems => 
5094  438 
[(*insert prems and underlying sets*) 
439 
cut_facts_tac prems 1, 

440 
stac unfold 1, 

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

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

443 
EVERY1 (select_disj (length intr_ts) i), 

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

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

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

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

448 
rewrite_goals_tac con_defs, 

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

450 

451 
in (intrs, unfold) end; 

452 

6424  453 

454 

455 
(** prove elimination rules **) 

5094  456 

8375  457 
fun prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy = 
5094  458 
let 
6427  459 
val _ = message " Proving the elimination rules ..."; 
5094  460 

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

461 
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

462 
val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ 
5094  463 
map make_elim [Inl_inject, Inr_inject]; 
8375  464 
in 
465 
map (fn (t, cases) => prove_goalw_cterm rec_sets_defs 

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

469 
REPEAT (FIRSTGOAL (eresolve_tac rules1)), 

470 
REPEAT (FIRSTGOAL (eresolve_tac rules2)), 

471 
EVERY (map (fn prem => 

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

474 
(mk_elims cs cTs params intr_ts intr_names) 

475 
end; 

5094  476 

6424  477 

5094  478 
(** derivation of simplified elimination rules **) 
479 

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

9598  481 
the given defs. Cannot simply use the local con_defs because con_defs=[] 
5094  482 
for inference systems. 
483 
*) 

484 

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

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

488 

489 
fun mk_cases_i elims ss cprop = 

7107  490 
let 
491 
val prem = Thm.assume cprop; 

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

496 
Some r => r 

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

9598  498 
[Pretty.str mk_cases_err, Pretty.fbrk, Display.pretty_cterm cprop]))) 
7107  499 
end; 
500 

6141  501 
fun mk_cases elims s = 
9598  502 
mk_cases_i elims (simpset()) (Thm.read_cterm (Thm.sign_of_thm (hd elims)) (s, propT)); 
503 

504 
fun smart_mk_cases thy ss cprop = 

505 
let 

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

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

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

509 
in mk_cases_i elims ss cprop end; 

7107  510 

511 

512 
(* inductive_cases(_i) *) 

513 

514 
fun gen_inductive_cases prep_att prep_const prep_prop 

9598  515 
(((name, raw_atts), raw_props), comment) thy = 
516 
let 

517 
val ss = Simplifier.simpset_of thy; 

518 
val sign = Theory.sign_of thy; 

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

520 
val atts = map (prep_att thy) raw_atts; 

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

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

5094  523 

7107  524 
val inductive_cases = 
525 
gen_inductive_cases Attrib.global_attribute Sign.intern_const ProofContext.read_prop; 

526 

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

528 

6424  529 

9598  530 
(* mk_cases_meth *) 
531 

532 
fun mk_cases_meth (ctxt, raw_props) = 

533 
let 

534 
val thy = ProofContext.theory_of ctxt; 

535 
val ss = Simplifier.get_local_simpset ctxt; 

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

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

538 

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

540 

541 

6424  542 

543 
(** prove induction rule **) 

5094  544 

545 
fun prove_indrule cs cTs sumT rec_const params intr_ts mono 

546 
fp_def rec_sets_defs thy = 

547 
let 

6427  548 
val _ = message " Proving the induction rule ..."; 
5094  549 

6394  550 
val sign = Theory.sign_of thy; 
5094  551 

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

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

555 

5094  556 
val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts; 
557 

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

559 

560 
fun mk_ind_pred _ [P] = P 

561 
 mk_ind_pred T Ps = 

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

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

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

567 
end; 

568 

569 
val ind_pred = mk_ind_pred sumT preds; 

570 

571 
val ind_concl = HOLogic.mk_Trueprop 

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

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

574 

575 
(* simplification rules for vimage and Collect *) 

576 

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

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

579 
(HOLogic.mk_Trueprop (HOLogic.mk_eq 

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

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

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

7293  583 
(fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, 
5094  584 
rtac refl 1])) cs; 
585 

586 
val induct = prove_goalw_cterm [] (cterm_of sign 

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

588 
[rtac (impI RS allI) 1, 

589 
DETERM (etac (mono RS (fp_def RS def_induct)) 1), 

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

590 
rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)), 
5094  591 
fold_goals_tac rec_sets_defs, 
592 
(*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

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

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

596 
REPEAT (FIRSTGOAL (etac conjE ORELSE' hyp_subst_tac)), 
7293  597 
rewrite_goals_tac sum_case_rewrites, 
5094  598 
EVERY (map (fn prem => 
5149  599 
DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]); 
5094  600 

601 
val lemma = prove_goalw_cterm rec_sets_defs (cterm_of sign 

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

603 
[cut_facts_tac prems 1, 

604 
REPEAT (EVERY 

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

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

7293  607 
rewrite_goals_tac sum_case_rewrites, 
5094  608 
atac 1])]) 
609 

610 
in standard (split_rule (induct RS lemma)) 

611 
end; 

612 

6424  613 

614 

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

616 

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

5094  618 

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

619 
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

620 
params paramTs cTs cnames = 
5094  621 
let 
622 
val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs; 

623 
val setT = HOLogic.mk_setT sumT; 

624 

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

5094  627 

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

630 

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

633 
(* is transformed into *) 

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

635 

636 
fun transform_rule r = 

637 
let 

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

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

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

643 

644 
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

645 
(frees, foldr1 HOLogic.mk_conj 
5149  646 
(((HOLogic.eq_const sumT) $ Free (xname, sumT) $ (mk_inj cs sumT u t)):: 
5094  647 
(map (subst o HOLogic.dest_Trueprop) 
648 
(Logic.strip_imp_prems r)))) 

649 
end 

650 

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

652 

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

654 
absfree (xname, sumT, foldr1 HOLogic.mk_disj (map transform_rule intr_ts))); 
5094  655 

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

657 

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

6394  659 
val full_rec_name = Sign.full_name (Theory.sign_of thy) rec_name; 
5094  660 

661 
val rec_const = list_comb 

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

663 

664 
val fp_def_term = Logic.mk_equals (rec_const, 

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

666 

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

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

669 

8433  670 
val (thy', [fp_def :: rec_sets_defs]) = 
671 
thy 

672 
> (if declare_consts then 

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

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

675 
else I) 

676 
> (if length cs < 2 then I 

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

678 
> Theory.add_path rec_name 

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

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

681 
val mono = prove_mono setT fp_fun monos thy' 
5094  682 

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

683 
in 
9598  684 
(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

685 
end; 
5094  686 

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

687 
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

688 
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

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

690 
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

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

692 

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

693 
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

694 

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

695 
val (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) = 
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

696 
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

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

698 

5094  699 
val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts con_defs 
700 
rec_sets_defs thy'; 

701 
val elims = if no_elim then [] else 

8375  702 
prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy'; 
8312
b470bc28b59d
add_cases_induct: accomodate no_elim and no_ind flags;
wenzelm
parents:
8307
diff
changeset

703 
val raw_induct = if no_ind then Drule.asm_rl else 
5094  704 
if coind then standard (rule_by_tactic 
5553  705 
(rewrite_tac [mk_meta_eq vimage_Un] THEN 
5094  706 
fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct))) 
707 
else 

708 
prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def 

709 
rec_sets_defs thy'; 

5108  710 
val induct = if coind orelse no_ind orelse length cs > 1 then raw_induct 
5094  711 
else standard (raw_induct RSN (2, rev_mp)); 
712 

8433  713 
val (thy'', [intrs']) = 
714 
thy' 

9598  715 
> PureThy.add_thmss [(("intros", intrs), atts)] 
8433  716 
>> (#1 o PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts)) 
717 
>> (if no_elim then I else #1 o PureThy.add_thmss [(("elims", elims), [])]) 

718 
>> (if no_ind then I else #1 o PureThy.add_thms 

8401  719 
[((coind_prefix coind ^ "induct", induct), [RuleCases.case_names induct_cases])]) 
8433  720 
>> Theory.parent_path; 
8312
b470bc28b59d
add_cases_induct: accomodate no_elim and no_ind flags;
wenzelm
parents:
8307
diff
changeset

721 
val elims' = if no_elim then elims else PureThy.get_thms thy'' "elims"; (* FIXME improve *) 
b470bc28b59d
add_cases_induct: accomodate no_elim and no_ind flags;
wenzelm
parents:
8307
diff
changeset

722 
val induct' = if no_ind then induct else PureThy.get_thm thy'' (coind_prefix coind ^ "induct"); (* FIXME improve *) 
5094  723 
in (thy'', 
724 
{defs = fp_def::rec_sets_defs, 

725 
mono = mono, 

726 
unfold = unfold, 

7798
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7710
diff
changeset

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

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

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

731 
induct = induct'}) 
5094  732 
end; 
733 

6424  734 

735 

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

5094  737 

738 
fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs 

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

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

6424  743 
val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros); 
9235  744 
val (thy', _, fp_def, rec_sets_defs, _, _) = 
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

745 
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

746 
params paramTs cTs cnames; 
8375  747 
val (elim_ts, elim_cases) = Library.split_list (mk_elims cs cTs params intr_ts intr_names); 
5094  748 
val (_, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts; 
749 
val ind_t = Logic.list_implies (ind_prems, mutual_ind_concl); 

9598  750 

751 
val (thy'', [intrs, raw_elims]) = 

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

752 
thy' 
9598  753 
> PureThy.add_axiomss_i [(("intros", intr_ts), atts), (("raw_elims", elim_ts), [])] 
754 
>> (if coind then I else 

8433  755 
#1 o PureThy.add_axioms_i [(("raw_induct", ind_t), [apsnd (standard o split_rule)])]); 
5094  756 

9598  757 
val elims = map2 (fn (th, cases) => RuleCases.name cases th) (raw_elims, elim_cases); 
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

758 
val raw_induct = if coind then Drule.asm_rl else PureThy.get_thm thy'' "raw_induct"; 
5094  759 
val induct = if coind orelse length cs > 1 then raw_induct 
760 
else standard (raw_induct RSN (2, rev_mp)); 

761 

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

762 
val (thy''', ([elims'], intrs')) = 
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

763 
thy'' 
8375  764 
> PureThy.add_thmss [(("elims", elims), [])] 
8433  765 
>> (if coind then I 
766 
else #1 o PureThy.add_thms [(("induct", induct), [RuleCases.case_names induct_cases])]) 

767 
>>> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts) 

768 
>> Theory.parent_path; 

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

769 
val induct' = if coind then raw_induct else PureThy.get_thm thy''' "induct"; 
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

770 
in (thy''', 
9235  771 
{defs = fp_def :: rec_sets_defs, 
8312
b470bc28b59d
add_cases_induct: accomodate no_elim and no_ind flags;
wenzelm
parents:
8307
diff
changeset

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

773 
unfold = Drule.asm_rl, 
8433  774 
intrs = intrs', 
775 
elims = elims', 

776 
mk_cases = mk_cases elims', 

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

778 
induct = induct'}) 
5094  779 
end; 
780 

6424  781 

782 

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

5094  784 

785 
fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs 

6521  786 
atts intros monos con_defs thy = 
5094  787 
let 
6424  788 
val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions"); 
6394  789 
val sign = Theory.sign_of thy; 
5094  790 

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

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

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

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

795 

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

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

798 

6437  799 
val full_cnames = map (try' (fst o dest_Const o head_of) 
5094  800 
"Recursive set not previously declared as constant: " sign) cs; 
6437  801 
val cnames = map Sign.base_name full_cnames; 
5094  802 

6424  803 
val _ = seq (check_rule sign cs o snd o fst) intros; 
8401  804 
val induct_cases = map (#1 o #1) intros; 
6437  805 

9405  806 
val (thy1, result as {elims, induct, ...}) = 
6437  807 
(if ! quick_and_dirty then add_ind_axm else add_ind_def) 
6521  808 
verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos 
8401  809 
con_defs thy params paramTs cTs cnames induct_cases; 
8307  810 
val thy2 = thy1 
811 
> put_inductives full_cnames ({names = full_cnames, coind = coind}, result) 

9405  812 
> add_cases_induct no_elim (no_ind orelse coind) full_cnames elims induct induct_cases; 
6437  813 
in (thy2, result) end; 
5094  814 

6424  815 

5094  816 

6424  817 
(** external interface **) 
818 

6521  819 
fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy = 
5094  820 
let 
6394  821 
val sign = Theory.sign_of thy; 
8100  822 
val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termT) c_strings; 
6424  823 

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

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

6424  829 
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

830 
val (cs', intr_ts') = unify_consts sign cs intr_ts; 
5094  831 

6424  832 
val ((thy', con_defs), monos) = thy 
833 
> IsarThy.apply_theorems raw_monos 

834 
> apfst (IsarThy.apply_theorems raw_con_defs); 

835 
in 

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

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

837 
atts ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy' 
5094  838 
end; 
839 

6424  840 

841 

6437  842 
(** package setup **) 
843 

844 
(* setup theory *) 

845 

8634  846 
val setup = 
847 
[InductiveData.init, 

9625  848 
Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args, 
9598  849 
"dynamic case analysis on sets")], 
8634  850 
Attrib.add_attributes [("mono", mono_attr, "monotonicity rule")]]; 
6437  851 

852 

853 
(* outer syntax *) 

6424  854 

6723  855 
local structure P = OuterParse and K = OuterSyntax.Keyword in 
6424  856 

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

860 
fun ind_decl coind = 

6729  861 
(Scan.repeat1 P.term  P.marg_comment)  
9598  862 
(P.$$$ "intros"  
7152  863 
P.!!! (P.opt_attribs  Scan.repeat1 (P.opt_thm_name ":"  P.prop  P.marg_comment)))  
6729  864 
Scan.optional (P.$$$ "monos"  P.!!! P.xthms1  P.marg_comment) []  
865 
Scan.optional (P.$$$ "con_defs"  P.!!! P.xthms1  P.marg_comment) [] 

6424  866 
>> (Toplevel.theory o mk_ind coind); 
867 

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

870 

871 
val coinductiveP = 

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

6424  873 

7107  874 

875 
val ind_cases = 

9625  876 
P.opt_thm_name ":"  Scan.repeat1 P.prop  P.marg_comment 
7107  877 
>> (Toplevel.theory o inductive_cases); 
878 

879 
val inductive_casesP = 

9598  880 
OuterSyntax.improper_command "inductive_cases" 
881 
"create simplified instances of elimination rules (improper)" K.thy_script ind_cases; 

7107  882 

9598  883 
val _ = OuterSyntax.add_keywords ["intros", "monos", "con_defs", "of"]; 
7107  884 
val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP]; 
6424  885 

5094  886 
end; 
6424  887 

888 

889 
end; 