author  wenzelm 
Sat, 21 Jan 2006 23:02:14 +0100  
changeset 18728  6790126ab5f6 
parent 18708  4b3dadb4fe33 
child 18977  f24c416a4814 
permissions  rwrr 
11658  1 
(* Title: Pure/Isar/induct_attrib.ML 
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

3 
Author: Markus Wenzel, TU Muenchen 
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

4 

e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

5 
Declaration of rules for cases and induction. 
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

6 
*) 
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

7 

e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

8 
signature INDUCT_ATTRIB = 
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

9 
sig 
11730  10 
val vars_of: term > term list 
18637  11 
val dest_rules: Context.generic > 
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

12 
{type_cases: (string * thm) list, set_cases: (string * thm) list, 
18210  13 
type_induct: (string * thm) list, set_induct: (string * thm) list, 
14 
type_coinduct: (string * thm) list, set_coinduct: (string * thm) list} 

18637  15 
val print_rules: Context.generic > unit 
11730  16 
val lookup_casesT : Proof.context > string > thm option 
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

17 
val lookup_casesS : Proof.context > string > thm option 
11730  18 
val lookup_inductT : Proof.context > string > thm option 
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

19 
val lookup_inductS : Proof.context > string > thm option 
18210  20 
val lookup_coinductT : Proof.context > string > thm option 
21 
val lookup_coinductS : Proof.context > string > thm option 

11730  22 
val find_casesT: Proof.context > typ > thm list 
18226  23 
val find_casesS: Proof.context > term > thm list 
11730  24 
val find_inductT: Proof.context > typ > thm list 
18226  25 
val find_inductS: Proof.context > term > thm list 
18210  26 
val find_coinductT: Proof.context > typ > thm list 
18226  27 
val find_coinductS: Proof.context > term > thm list 
18728  28 
val cases_type: string > attribute 
29 
val cases_set: string > attribute 

30 
val induct_type: string > attribute 

31 
val induct_set: string > attribute 

32 
val coinduct_type: string > attribute 

33 
val coinduct_set: string > attribute 

11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

34 
val casesN: string 
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

35 
val inductN: string 
18210  36 
val coinductN: string 
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

37 
val typeN: string 
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

38 
val setN: string 
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

39 
end; 
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

40 

e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

41 
structure InductAttrib: INDUCT_ATTRIB = 
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

42 
struct 
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

43 

e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

44 

11730  45 
(** misc utils **) 
46 

47 
(* encode_type  for indexing purposes *) 

48 

49 
fun encode_type (Type (c, Ts)) = Term.list_comb (Const (c, dummyT), map encode_type Ts) 

50 
 encode_type (TFree (a, _)) = Free (a, dummyT) 

51 
 encode_type (TVar (a, _)) = Var (a, dummyT); 

52 

53 

54 
(* variables  ordered lefttoright, preferring right *) 

55 

18210  56 
fun vars_of tm = 
57 
Term.fold_aterms (fn (t as Var _) => cons t  _ => I) tm [] 

58 
> Library.distinct 

59 
> rev; 

11730  60 

18210  61 
local 
11730  62 

63 
val mk_var = encode_type o #2 o Term.dest_Var; 

64 

18210  65 
fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle Empty => 
66 
raise THM ("No variables in conclusion of rule", 0, [thm]); 

67 

11730  68 
in 
69 

18210  70 
fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle Empty => 
71 
raise THM ("No variables in major premise of rule", 0, [thm]); 

11730  72 

18210  73 
val left_var_concl = concl_var hd; 
74 
val right_var_concl = concl_var List.last; 

11730  75 

76 
end; 

77 

78 

79 

18637  80 
(** induct data **) 
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

81 

e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

82 
(* rules *) 
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

83 

e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

84 
type rules = (string * thm) NetRules.T; 
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

85 

12381  86 
val init_rules = 
13105
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
12381
diff
changeset

87 
NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso 
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
12381
diff
changeset

88 
Drule.eq_thm_prop (th1, th2)); 
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

89 

17184  90 
fun lookup_rule (rs: rules) = AList.lookup (op =) (NetRules.rules rs); 
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

91 

18637  92 
fun pretty_rules ctxt kind rs = 
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

93 
let val thms = map snd (NetRules.rules rs) 
18637  94 
in Pretty.big_list kind (map (ProofContext.pretty_thm ctxt) thms) end; 
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

95 

e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

96 

18637  97 
(* context data *) 
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

98 

18637  99 
fun dest ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) = 
100 
{type_cases = NetRules.rules casesT, 

101 
set_cases = NetRules.rules casesS, 

102 
type_induct = NetRules.rules inductT, 

103 
set_induct = NetRules.rules inductS, 

104 
type_coinduct = NetRules.rules coinductT, 

105 
set_coinduct = NetRules.rules coinductS}; 

106 

107 
structure Induct = GenericDataFun 

108 
( 

18210  109 
val name = "Isar/induct"; 
110 
type T = (rules * rules) * (rules * rules) * (rules * rules); 

11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

111 

11730  112 
val empty = 
18210  113 
((init_rules (left_var_prem o #2), init_rules (Thm.major_prem_of o #2)), 
114 
(init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)), 

115 
(init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2))); 

18637  116 

16424  117 
val extend = I; 
18637  118 

18210  119 
fun merge _ (((casesT1, casesS1), (inductT1, inductS1), (coinductT1, coinductS1)), 
120 
((casesT2, casesS2), (inductT2, inductS2), (coinductT2, coinductS2))) = 

11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

121 
((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)), 
18210  122 
(NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)), 
123 
(NetRules.merge (coinductT1, coinductT2), NetRules.merge (coinductS1, coinductS2))); 

11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

124 

18637  125 
fun print generic ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) = 
126 
let val ctxt = Context.proof_of generic in 

127 
[pretty_rules ctxt "coinduct type:" coinductT, 

128 
pretty_rules ctxt "coinduct set:" coinductS, 

129 
pretty_rules ctxt "induct type:" inductT, 

130 
pretty_rules ctxt "induct set:" inductS, 

131 
pretty_rules ctxt "cases type:" casesT, 

132 
pretty_rules ctxt "cases set:" casesS] 

133 
> Pretty.chunks > Pretty.writeln 

134 
end 

135 
); 

11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

136 

18708  137 
val _ = Context.add_setup Induct.init; 
18637  138 
val print_rules = Induct.print; 
139 
val dest_rules = dest o Induct.get; 

11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

140 

18637  141 
val get_local = Induct.get o Context.Proof; 
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

142 

e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

143 

e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

144 
(* access rules *) 
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

145 

18637  146 
val lookup_casesT = lookup_rule o #1 o #1 o get_local; 
147 
val lookup_casesS = lookup_rule o #2 o #1 o get_local; 

148 
val lookup_inductT = lookup_rule o #1 o #2 o get_local; 

149 
val lookup_inductS = lookup_rule o #2 o #2 o get_local; 

150 
val lookup_coinductT = lookup_rule o #1 o #3 o get_local; 

151 
val lookup_coinductS = lookup_rule o #2 o #3 o get_local; 

11730  152 

11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

153 

11730  154 
fun find_rules which how ctxt x = 
18637  155 
map snd (NetRules.retrieve (which (get_local ctxt)) (how x)); 
11730  156 

157 
val find_casesT = find_rules (#1 o #1) encode_type; 

18226  158 
val find_casesS = find_rules (#2 o #1) I; 
11730  159 
val find_inductT = find_rules (#1 o #2) encode_type; 
18226  160 
val find_inductS = find_rules (#2 o #2) I; 
18210  161 
val find_coinductT = find_rules (#1 o #3) encode_type; 
18226  162 
val find_coinductS = find_rules (#2 o #3) I; 
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

163 

e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

164 

e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

165 

e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

166 
(** attributes **) 
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

167 

e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

168 
local 
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

169 

18637  170 
fun mk_att f g name arg = 
171 
let val (x, thm) = g arg in (Induct.map (f (name, thm)) x, thm) end; 

11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

172 

18210  173 
fun map1 f (x, y, z) = (f x, y, z); 
174 
fun map2 f (x, y, z) = (x, f y, z); 

175 
fun map3 f (x, y, z) = (x, y, f z); 

176 

177 
fun add_casesT rule x = map1 (apfst (NetRules.insert rule)) x; 

178 
fun add_casesS rule x = map1 (apsnd (NetRules.insert rule)) x; 

179 
fun add_inductT rule x = map2 (apfst (NetRules.insert rule)) x; 

180 
fun add_inductS rule x = map2 (apsnd (NetRules.insert rule)) x; 

181 
fun add_coinductT rule x = map3 (apfst (NetRules.insert rule)) x; 

182 
fun add_coinductS rule x = map3 (apsnd (NetRules.insert rule)) x; 

11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

183 

e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

184 
fun consumes0 x = RuleCases.consumes_default 0 x; 
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

185 
fun consumes1 x = RuleCases.consumes_default 1 x; 
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

186 

e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

187 
in 
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

188 

18637  189 
val cases_type = mk_att add_casesT consumes0; 
190 
val cases_set = mk_att add_casesS consumes1; 

191 
val induct_type = mk_att add_inductT consumes0; 

192 
val induct_set = mk_att add_inductS consumes1; 

193 
val coinduct_type = mk_att add_coinductT consumes0; 

194 
val coinduct_set = mk_att add_coinductS consumes1; 

11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

195 

e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

196 
end; 
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

197 

e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

198 

18637  199 

11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

200 
(** concrete syntax **) 
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

201 

e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

202 
val casesN = "cases"; 
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

203 
val inductN = "induct"; 
18210  204 
val coinductN = "coinduct"; 
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

205 

e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

206 
val typeN = "type"; 
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

207 
val setN = "set"; 
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

208 

e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

209 
local 
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

210 

15703  211 
fun spec k arg = 
212 
Scan.lift (Args.$$$ k  Args.colon)  arg  

213 
Scan.lift (Args.$$$ k) >> K ""; 

11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

214 

18637  215 
fun attrib add_type add_set = 
216 
Attrib.syntax (spec typeN Args.tyname >> add_type  spec setN Args.const >> add_set); 

11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

217 

e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

218 
in 
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

219 

18637  220 
val cases_att = attrib cases_type cases_set; 
221 
val induct_att = attrib induct_type induct_set; 

222 
val coinduct_att = attrib coinduct_type coinduct_set; 

18210  223 

11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

224 
end; 
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

225 

15801  226 
val _ = Context.add_setup 
18708  227 
(Attrib.add_attributes 
18728  228 
[(casesN, cases_att, "declaration of cases rule for type or set"), 
229 
(inductN, induct_att, "declaration of induction rule for type or set"), 

230 
(coinductN, coinduct_att, "declaration of coinduction rule for type or set")]); 

11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

231 

e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset

232 
end; 