author  berghofe 
Tue, 05 Oct 1999 15:23:22 +0200  
changeset 7710  bf8cb3fc5d64 
parent 7349  228b711ad68c 
child 7798  42e94b618f34 
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 

6 
1998 TU Muenchen 

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 

21 
[ ti:M(Sj), ..., P(x), ... ] ==> t: Sk ] 

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 
6437  35 
val get_inductive: theory > string > 
36 
{names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm, 

37 
induct: thm, intrs: thm list, mk_cases: string > thm, mono: thm, unfold: thm} 

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} 
7107  52 
val inductive_cases: (((bstring * Args.src list) * xstring) * string list) * Comment.text 
53 
> theory > theory 

54 
val inductive_cases_i: (((bstring * theory attribute list) * string) * term list) * Comment.text 

55 
> theory > theory 

6437  56 
val setup: (theory > theory) list 
5094  57 
end; 
58 

6424  59 
structure InductivePackage: INDUCTIVE_PACKAGE = 
5094  60 
struct 
61 

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

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

63 

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

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

65 

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

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

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

68 
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

69 

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

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

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

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

73 
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

74 

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

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

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

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

78 
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

79 
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

80 

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

81 
fun print sg (tab, monos) = 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

82 
(Pretty.writeln (Pretty.strs ("(co)inductives:" :: 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

83 
map #1 (Sign.cond_extern_table sg Sign.constK tab))); 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

84 
Pretty.writeln (Pretty.big_list "monotonicity rules:" (map Display.pretty_thm monos))); 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

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

86 

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

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

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

89 

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

92 

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

93 
fun get_inductive thy name = 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

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

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

96 
 None => error ("Unknown (co)inductive set " ^ quote name)); 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

97 

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

98 
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

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

100 
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

101 
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

102 
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

103 
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

104 

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

105 
val get_monos = snd o InductiveData.get; 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

106 

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

107 
fun put_monos thms thy = InductiveData.put (fst (InductiveData.get thy), thms) thy; 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

108 

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

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

110 

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

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

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

113 
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

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

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

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

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

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

119 
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

120 
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

121 
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

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

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

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

125 

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

126 
(* mono add/del *) 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

127 

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

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

129 

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

130 
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

131 

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

132 
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

133 
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

134 

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

135 
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

136 

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

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

138 

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

139 
val mono_add_global = mk_att map_rules_global add_mono; 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

140 
val mono_del_global = mk_att map_rules_global del_mono; 
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 
end; 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

143 

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

144 

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

145 
(* concrete syntax *) 
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 monoN = "mono"; 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

148 
val addN = "add"; 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

149 
val delN = "del"; 
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 
fun mono_att add del = 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

152 
Attrib.syntax (Scan.lift (Args.$$$ addN >> K add  Args.$$$ delN >> K del  Scan.succeed add)); 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

153 

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

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

155 
(mono_att mono_add_global mono_del_global, mono_att Attrib.undef_local_attribute Attrib.undef_local_attribute); 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

156 

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

157 

7107  158 

6424  159 
(** utilities **) 
160 

161 
(* messages *) 

162 

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

165 

6424  166 
fun coind_prefix true = "co" 
167 
 coind_prefix false = ""; 

168 

169 

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

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

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

172 

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

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

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

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

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

177 
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

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

179 
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

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

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

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

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

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

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

186 
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

187 
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

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

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

190 
val (env, _) = foldl unify (([], i'), rec_consts); 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

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

192 
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

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

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

195 

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

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

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

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

199 

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

200 

6424  201 
(* misc *) 
202 

5094  203 
val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (concl_of vimageD); 
204 

205 
(*Delete needless equality assumptions*) 

206 
val refl_thin = prove_goal HOL.thy "!!P. [ a=a; P ] ==> P" 

207 
(fn _ => [assume_tac 1]); 

208 

209 
(*For simplifying the elimination rule*) 

5120
f7f5442c934a
Removed disjE from list of rules used to simplify elimination
berghofe
parents:
5108
diff
changeset

210 
val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, Pair_inject]; 
5094  211 

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

5094  214 

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

216 

217 
fun mk_inj cs sumT c x = 

218 
let 

219 
fun mk_inj' T n i = 

220 
if n = 1 then x else 

221 
let val n2 = n div 2; 

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

223 
in 

224 
if i <= n2 then 

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

226 
else 

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

228 
end 

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

230 
end; 

231 

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

233 

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

235 
let 

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

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

238 
in 

239 
Const (vimage_name, vimageT) $ 

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

241 
end; 

242 

6424  243 

244 

245 
(** wellformedness checks **) 

5094  246 

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

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

249 

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

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

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

253 

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

255 
\ ' t : S_i '"; 

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

256 
val msg2 = "Nonatomic premise"; 
5094  257 
val msg3 = "Recursion term on left of member symbol"; 
258 

259 
fun check_rule sign cs r = 

260 
let 

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

261 
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

262 
else err_in_prem sign r prem msg2; 
5094  263 

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

264 
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

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

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

267 
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

268 
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

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

270 
seq check_prem (Logic.strip_imp_prems r) 
5094  271 
else err_in_rule sign r msg1 
272 
 _ => err_in_rule sign r msg1) 

273 
end; 

274 

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

275 
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

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

277 
 None => error (msg ^ Sign.string_of_term sign t)); 
5094  278 

6424  279 

5094  280 

6424  281 
(*** properties of (co)inductive sets ***) 
282 

283 
(** elimination rules **) 

5094  284 

285 
fun mk_elims cs cTs params intr_ts = 

286 
let 

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

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

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

290 

291 
fun dest_intr r = 

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

293 
HOLogic.dest_Trueprop (Logic.strip_imp_concl r) 

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

295 

296 
val intrs = map dest_intr intr_ts; 

297 

298 
fun mk_elim (c, T) = 

299 
let 

300 
val a = Free (aname, T); 

301 

302 
fun mk_elim_prem (_, t, ts) = 

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

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

305 
in 

306 
Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) :: 

307 
map mk_elim_prem (filter (equal c o #1) intrs), P) 

308 
end 

309 
in 

310 
map mk_elim (cs ~~ cTs) 

311 
end; 

312 

6424  313 

314 

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

5094  316 

317 
fun mk_indrule cs cTs params intr_ts = 

318 
let 

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

320 

321 
(* predicates for induction rule *) 

322 

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

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

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

326 

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

328 

329 
fun mk_ind_prem r = 

330 
let 

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

332 

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

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

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

335 
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

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

337 
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

338 
 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

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

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

341 
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

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

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

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

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

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

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

348 

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

349 
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

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

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

352 

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

355 

356 
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

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

359 
HOLogic.mk_Trueprop (the (pred_of u) $ t))) 
5094  360 
end; 
361 

362 
val ind_prems = map mk_ind_prem intr_ts; 

363 

364 
(* make conclusions for induction rules *) 

365 

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

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

368 
val Ts = HOLogic.prodT_factors T; 

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

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

371 
val tuple = HOLogic.mk_tuple T frees; 

372 
in ((HOLogic.mk_binop "op >" 

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

374 
end; 

375 

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

376 
val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj 
5094  377 
(fst (foldr mk_ind_concl (cs ~~ preds, ([], "xa"))))) 
378 

379 
in (preds, ind_prems, mutual_ind_concl) 

380 
end; 

381 

6424  382 

5094  383 

6424  384 
(*** proofs for (co)inductive sets ***) 
385 

386 
(** prove monotonicity **) 

5094  387 

388 
fun prove_mono setT fp_fun monos thy = 

389 
let 

6427  390 
val _ = message " Proving monotonicity ..."; 
5094  391 

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

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

396 
in mono end; 

397 

6424  398 

399 

400 
(** prove introduction rules **) 

5094  401 

402 
fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy = 

403 
let 

6427  404 
val _ = message " Proving the introduction rules ..."; 
5094  405 

406 
val unfold = standard (mono RS (fp_def RS 

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

408 

409 
fun select_disj 1 1 = [] 

410 
 select_disj _ 1 = [rtac disjI1] 

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

412 

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

6394  414 
(cterm_of (Theory.sign_of thy) intr) (fn prems => 
5094  415 
[(*insert prems and underlying sets*) 
416 
cut_facts_tac prems 1, 

417 
stac unfold 1, 

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

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

420 
EVERY1 (select_disj (length intr_ts) i), 

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

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

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

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

425 
rewrite_goals_tac con_defs, 

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

427 

428 
in (intrs, unfold) end; 

429 

6424  430 

431 

432 
(** prove elimination rules **) 

5094  433 

434 
fun prove_elims cs cTs params intr_ts unfold rec_sets_defs thy = 

435 
let 

6427  436 
val _ = message " Proving the elimination rules ..."; 
5094  437 

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

438 
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

439 
val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ 
5094  440 
map make_elim [Inl_inject, Inr_inject]; 
441 

442 
val elims = map (fn t => prove_goalw_cterm rec_sets_defs 

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

446 
REPEAT (FIRSTGOAL (eresolve_tac rules1)), 

447 
REPEAT (FIRSTGOAL (eresolve_tac rules2)), 

448 
EVERY (map (fn prem => 

5149  449 
DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))])) 
5094  450 
(mk_elims cs cTs params intr_ts) 
451 

452 
in elims end; 

453 

6424  454 

5094  455 
(** derivation of simplified elimination rules **) 
456 

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

458 
the given defs. Cannot simply use the local con_defs because con_defs=[] 

459 
for inference systems. 

460 
*) 

6141  461 
fun con_elim_tac ss = 
5094  462 
let val elim_tac = REPEAT o (eresolve_tac elim_rls) 
463 
in ALLGOALS(EVERY'[elim_tac, 

6141  464 
asm_full_simp_tac ss, 
465 
elim_tac, 

466 
REPEAT o bound_hyp_subst_tac]) 

5094  467 
THEN prune_params_tac 
468 
end; 

469 

7107  470 
(*cprop should have the form t:Si where Si is an inductive set*) 
471 
fun mk_cases_i elims ss cprop = 

472 
let 

473 
val prem = Thm.assume cprop; 

474 
fun mk_elim rl = standard (rule_by_tactic (con_elim_tac ss) (prem RS rl)); 

475 
in 

476 
(case get_first (try mk_elim) elims of 

477 
Some r => r 

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

479 
[Pretty.str "mk_cases: proposition not of form 't : S_i'", Pretty.fbrk, 

480 
Display.pretty_cterm cprop]))) 

481 
end; 

482 

6141  483 
fun mk_cases elims s = 
7107  484 
mk_cases_i elims (simpset()) (Thm.read_cterm (Thm.sign_of_thm (hd elims)) (s, propT)); 
485 

486 

487 
(* inductive_cases(_i) *) 

488 

489 
fun gen_inductive_cases prep_att prep_const prep_prop 

490 
((((name, raw_atts), raw_set), raw_props), comment) thy = 

491 
let 

492 
val sign = Theory.sign_of thy; 

493 

494 
val atts = map (prep_att thy) raw_atts; 

495 
val (_, {elims, ...}) = get_inductive thy (prep_const sign raw_set); 

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

497 
val thms = map (mk_cases_i elims (Simplifier.simpset_of thy)) cprops; 

498 
in 

499 
thy 

500 
> IsarThy.have_theorems_i (((name, atts), map Thm.no_attributes thms), comment) 

5094  501 
end; 
502 

7107  503 
val inductive_cases = 
504 
gen_inductive_cases Attrib.global_attribute Sign.intern_const ProofContext.read_prop; 

505 

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

507 

6424  508 

509 

510 
(** prove induction rule **) 

5094  511 

512 
fun prove_indrule cs cTs sumT rec_const params intr_ts mono 

513 
fp_def rec_sets_defs thy = 

514 
let 

6427  515 
val _ = message " Proving the induction rule ..."; 
5094  516 

6394  517 
val sign = Theory.sign_of thy; 
5094  518 

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

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

522 

5094  523 
val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts; 
524 

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

526 

527 
fun mk_ind_pred _ [P] = P 

528 
 mk_ind_pred T Ps = 

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

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

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

534 
end; 

535 

536 
val ind_pred = mk_ind_pred sumT preds; 

537 

538 
val ind_concl = HOLogic.mk_Trueprop 

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

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

541 

542 
(* simplification rules for vimage and Collect *) 

543 

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

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

546 
(HOLogic.mk_Trueprop (HOLogic.mk_eq 

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

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

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

7293  550 
(fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, 
5094  551 
rtac refl 1])) cs; 
552 

553 
val induct = prove_goalw_cterm [] (cterm_of sign 

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

555 
[rtac (impI RS allI) 1, 

556 
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

557 
rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)), 
5094  558 
fold_goals_tac rec_sets_defs, 
559 
(*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

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

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

563 
REPEAT (FIRSTGOAL (etac conjE ORELSE' hyp_subst_tac)), 
7293  564 
rewrite_goals_tac sum_case_rewrites, 
5094  565 
EVERY (map (fn prem => 
5149  566 
DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]); 
5094  567 

568 
val lemma = prove_goalw_cterm rec_sets_defs (cterm_of sign 

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

570 
[cut_facts_tac prems 1, 

571 
REPEAT (EVERY 

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

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

7293  574 
rewrite_goals_tac sum_case_rewrites, 
5094  575 
atac 1])]) 
576 

577 
in standard (split_rule (induct RS lemma)) 

578 
end; 

579 

6424  580 

581 

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

583 

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

5094  585 

586 
fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs 

6521  587 
atts intros monos con_defs thy params paramTs cTs cnames = 
5094  588 
let 
6424  589 
val _ = if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^ 
590 
commas_quote cnames) else (); 

5094  591 

592 
val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs; 

593 
val setT = HOLogic.mk_setT sumT; 

594 

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

5094  597 

6424  598 
val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros); 
599 

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

602 

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

605 
(* is transformed into *) 

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

607 

608 
fun transform_rule r = 

609 
let 

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

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

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

615 

616 
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

617 
(frees, foldr1 HOLogic.mk_conj 
5149  618 
(((HOLogic.eq_const sumT) $ Free (xname, sumT) $ (mk_inj cs sumT u t)):: 
5094  619 
(map (subst o HOLogic.dest_Trueprop) 
620 
(Logic.strip_imp_prems r)))) 

621 
end 

622 

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

624 

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

626 
absfree (xname, sumT, foldr1 HOLogic.mk_disj (map transform_rule intr_ts))); 
5094  627 

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

629 

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

6394  631 
val full_rec_name = Sign.full_name (Theory.sign_of thy) rec_name; 
5094  632 

633 
val rec_const = list_comb 

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

635 

636 
val fp_def_term = Logic.mk_equals (rec_const, 

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

638 

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

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

641 

642 
val thy' = thy > 

643 
(if declare_consts then 

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

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

646 
else I) > 

647 
(if length cs < 2 then I else 

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

649 
Theory.add_path rec_name > 

650 
PureThy.add_defss_i [(("defs", def_terms), [])]; 

651 

652 
(* get definitions from theory *) 

653 

6424  654 
val fp_def::rec_sets_defs = PureThy.get_thms thy' "defs"; 
5094  655 

656 
(* prove and store theorems *) 

657 

658 
val mono = prove_mono setT fp_fun monos thy'; 

659 
val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts con_defs 

660 
rec_sets_defs thy'; 

661 
val elims = if no_elim then [] else 

662 
prove_elims cs cTs params intr_ts unfold rec_sets_defs thy'; 

663 
val raw_induct = if no_ind then TrueI else 

664 
if coind then standard (rule_by_tactic 

5553  665 
(rewrite_tac [mk_meta_eq vimage_Un] THEN 
5094  666 
fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct))) 
667 
else 

668 
prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def 

669 
rec_sets_defs thy'; 

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

6424  673 
val thy'' = thy' 
6521  674 
> PureThy.add_thmss [(("intrs", intrs), atts)] 
6424  675 
> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts) 
676 
> (if no_elim then I else PureThy.add_thmss [(("elims", elims), [])]) 

677 
> (if no_ind then I else PureThy.add_thms 

678 
[((coind_prefix coind ^ "induct", induct), [])]) 

679 
> Theory.parent_path; 

5094  680 

681 
in (thy'', 

682 
{defs = fp_def::rec_sets_defs, 

683 
mono = mono, 

684 
unfold = unfold, 

685 
intrs = intrs, 

686 
elims = elims, 

687 
mk_cases = mk_cases elims, 

688 
raw_induct = raw_induct, 

689 
induct = induct}) 

690 
end; 

691 

6424  692 

693 

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

5094  695 

696 
fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs 

6521  697 
atts intros monos con_defs thy params paramTs cTs cnames = 
5094  698 
let 
699 
val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name; 

700 

6424  701 
val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros); 
5094  702 
val elim_ts = mk_elims cs cTs params intr_ts; 
703 

704 
val (_, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts; 

705 
val ind_t = Logic.list_implies (ind_prems, mutual_ind_concl); 

706 

6424  707 
val thy' = thy 
708 
> (if declare_consts then 

709 
Theory.add_consts_i 

710 
(map (fn (c, n) => (n, paramTs > fastype_of c, NoSyn)) (cs ~~ cnames)) 

711 
else I) 

712 
> Theory.add_path rec_name 

6521  713 
> PureThy.add_axiomss_i [(("intrs", intr_ts), atts), (("elims", elim_ts), [])] 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

714 
> (if coind then I else 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

715 
PureThy.add_axioms_i [(("raw_induct", ind_t), [apsnd (standard o split_rule)])]); 
5094  716 

6424  717 
val intrs = PureThy.get_thms thy' "intrs"; 
718 
val elims = PureThy.get_thms thy' "elims"; 

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

719 
val raw_induct = if coind then TrueI else PureThy.get_thm thy' "raw_induct"; 
5094  720 
val induct = if coind orelse length cs > 1 then raw_induct 
721 
else standard (raw_induct RSN (2, rev_mp)); 

722 

6424  723 
val thy'' = 
724 
thy' 

725 
> (if coind then I else PureThy.add_thms [(("induct", induct), [])]) 

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

727 
> Theory.parent_path; 

5094  728 
in (thy'', 
729 
{defs = [], 

730 
mono = TrueI, 

731 
unfold = TrueI, 

732 
intrs = intrs, 

733 
elims = elims, 

734 
mk_cases = mk_cases elims, 

735 
raw_induct = raw_induct, 

736 
induct = induct}) 

737 
end; 

738 

6424  739 

740 

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

5094  742 

743 
fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs 

6521  744 
atts intros monos con_defs thy = 
5094  745 
let 
6424  746 
val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions"); 
6394  747 
val sign = Theory.sign_of thy; 
5094  748 

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

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

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

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

753 

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

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

756 

6437  757 
val full_cnames = map (try' (fst o dest_Const o head_of) 
5094  758 
"Recursive set not previously declared as constant: " sign) cs; 
6437  759 
val cnames = map Sign.base_name full_cnames; 
5094  760 

6424  761 
val _ = seq (check_rule sign cs o snd o fst) intros; 
6437  762 

763 
val (thy1, result) = 

764 
(if ! quick_and_dirty then add_ind_axm else add_ind_def) 

6521  765 
verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos 
6437  766 
con_defs thy params paramTs cTs cnames; 
767 
val thy2 = thy1 > put_inductives full_cnames ({names = full_cnames, coind = coind}, result); 

768 
in (thy2, result) end; 

5094  769 

6424  770 

5094  771 

6424  772 
(** external interface **) 
773 

6521  774 
fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy = 
5094  775 
let 
6394  776 
val sign = Theory.sign_of thy; 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

777 
val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termTVar) c_strings; 
6424  778 

6521  779 
val atts = map (Attrib.global_attribute thy) srcs; 
6424  780 
val intr_names = map (fst o fst) intro_srcs; 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

781 
val intr_ts = map (term_of o Thm.read_cterm sign o rpair propT o snd o fst) intro_srcs; 
6424  782 
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

783 
val (cs', intr_ts') = unify_consts sign cs intr_ts; 
5094  784 

6424  785 
val ((thy', con_defs), monos) = thy 
786 
> IsarThy.apply_theorems raw_monos 

787 
> apfst (IsarThy.apply_theorems raw_con_defs); 

788 
in 

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

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

790 
atts ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy' 
5094  791 
end; 
792 

6424  793 

794 

6437  795 
(** package setup **) 
796 

797 
(* setup theory *) 

798 

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

799 
val setup = [InductiveData.init, 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

800 
Attrib.add_attributes [(monoN, mono_attr, "monotonicity rule")]]; 
6437  801 

802 

803 
(* outer syntax *) 

6424  804 

6723  805 
local structure P = OuterParse and K = OuterSyntax.Keyword in 
6424  806 

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

810 
fun ind_decl coind = 

6729  811 
(Scan.repeat1 P.term  P.marg_comment)  
812 
(P.$$$ "intrs"  

7152  813 
P.!!! (P.opt_attribs  Scan.repeat1 (P.opt_thm_name ":"  P.prop  P.marg_comment)))  
6729  814 
Scan.optional (P.$$$ "monos"  P.!!! P.xthms1  P.marg_comment) []  
815 
Scan.optional (P.$$$ "con_defs"  P.!!! P.xthms1  P.marg_comment) [] 

6424  816 
>> (Toplevel.theory o mk_ind coind); 
817 

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

820 

821 
val coinductiveP = 

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

6424  823 

7107  824 

825 
val ind_cases = 

826 
P.opt_thm_name "="  P.xname  P.$$$ ":"  Scan.repeat1 P.prop  P.marg_comment 

827 
>> (Toplevel.theory o inductive_cases); 

828 

829 
val inductive_casesP = 

830 
OuterSyntax.command "inductive_cases" "create simplified instances of elimination rules" 

831 
K.thy_decl ind_cases; 

832 

6424  833 
val _ = OuterSyntax.add_keywords ["intrs", "monos", "con_defs"]; 
7107  834 
val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP]; 
6424  835 

5094  836 
end; 
6424  837 

838 

839 
end; 