author  wenzelm 
Mon, 28 Feb 2000 13:39:45 +0100  
changeset 8312  b470bc28b59d 
parent 8307  6600c6e53111 
child 8316  74639e19eca0 
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 

8277  105 

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

108 

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

111 

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

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

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

114 
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

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

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

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

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

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

120 
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

121 
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

122 
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

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

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

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

126 

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

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

128 

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

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

130 

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

131 
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

132 

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

133 
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

134 
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

135 

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

136 
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

137 

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

138 
in 
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 
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

141 
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

142 

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

143 
end; 
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 

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

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

147 

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

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

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

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

151 

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

152 
fun mono_att add del = 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

153 
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

154 

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

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

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

157 

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

158 

7107  159 

6424  160 
(** utilities **) 
161 

162 
(* messages *) 

163 

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

166 

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

169 

170 

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

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

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

173 

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

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

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

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

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

178 
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

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

180 
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

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

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

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

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

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

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

187 
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

188 
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

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

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

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

192 
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

193 
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

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

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

196 

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

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

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

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

200 

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

201 

6424  202 
(* misc *) 
203 

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

206 
(*Delete needless equality assumptions*) 

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

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

209 

210 
(*For simplifying the elimination rule*) 

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

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

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

5094  215 

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

217 

218 
fun mk_inj cs sumT c x = 

219 
let 

220 
fun mk_inj' T n i = 

221 
if n = 1 then x else 

222 
let val n2 = n div 2; 

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

224 
in 

225 
if i <= n2 then 

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

227 
else 

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

229 
end 

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

231 
end; 

232 

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

234 

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

236 
let 

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

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

239 
in 

240 
Const (vimage_name, vimageT) $ 

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

242 
end; 

243 

6424  244 

245 

246 
(** wellformedness checks **) 

5094  247 

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

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

250 

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

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

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

254 

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

256 
\ ' t : S_i '"; 

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

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

260 
fun check_rule sign cs r = 

261 
let 

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

262 
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

263 
else err_in_prem sign r prem msg2; 
5094  264 

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

265 
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

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

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

268 
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

269 
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

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

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

274 
end; 

275 

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

276 
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

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

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

6424  280 

5094  281 

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

284 
(** elimination rules **) 

5094  285 

286 
fun mk_elims cs cTs params intr_ts = 

287 
let 

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

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

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

291 

292 
fun dest_intr r = 

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

294 
HOLogic.dest_Trueprop (Logic.strip_imp_concl r) 

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

296 

297 
val intrs = map dest_intr intr_ts; 

298 

299 
fun mk_elim (c, T) = 

300 
let 

301 
val a = Free (aname, T); 

302 

303 
fun mk_elim_prem (_, t, ts) = 

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

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

306 
in 

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

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

309 
end 

310 
in 

311 
map mk_elim (cs ~~ cTs) 

312 
end; 

313 

6424  314 

315 

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

5094  317 

318 
fun mk_indrule cs cTs params intr_ts = 

319 
let 

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

321 

322 
(* predicates for induction rule *) 

323 

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

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

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

327 

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

329 

330 
fun mk_ind_prem r = 

331 
let 

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

333 

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

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

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

336 
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

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

338 
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

339 
 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

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

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

342 
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

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

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

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

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

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

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

349 

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

350 
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

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

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

353 

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

356 

357 
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

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

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

363 
val ind_prems = map mk_ind_prem intr_ts; 

364 

365 
(* make conclusions for induction rules *) 

366 

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

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

369 
val Ts = HOLogic.prodT_factors T; 

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

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

372 
val tuple = HOLogic.mk_tuple T frees; 

373 
in ((HOLogic.mk_binop "op >" 

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

375 
end; 

376 

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

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

380 
in (preds, ind_prems, mutual_ind_concl) 

381 
end; 

382 

6424  383 

5094  384 

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

387 
(** prove monotonicity **) 

5094  388 

389 
fun prove_mono setT fp_fun monos thy = 

390 
let 

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

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

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

397 
in mono end; 

398 

6424  399 

400 

401 
(** prove introduction rules **) 

5094  402 

403 
fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy = 

404 
let 

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

407 
val unfold = standard (mono RS (fp_def RS 

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

409 

410 
fun select_disj 1 1 = [] 

411 
 select_disj _ 1 = [rtac disjI1] 

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

413 

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

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

418 
stac unfold 1, 

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

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

421 
EVERY1 (select_disj (length intr_ts) i), 

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

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

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

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

426 
rewrite_goals_tac con_defs, 

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

428 

429 
in (intrs, unfold) end; 

430 

6424  431 

432 

433 
(** prove elimination rules **) 

5094  434 

435 
fun prove_elims cs cTs params intr_ts unfold rec_sets_defs thy = 

436 
let 

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

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

439 
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

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

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

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

447 
REPEAT (FIRSTGOAL (eresolve_tac rules1)), 

448 
REPEAT (FIRSTGOAL (eresolve_tac rules2)), 

449 
EVERY (map (fn prem => 

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

453 
in elims end; 

454 

6424  455 

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

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

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

460 
for inference systems. 

461 
*) 

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

6141  465 
asm_full_simp_tac ss, 
466 
elim_tac, 

467 
REPEAT o bound_hyp_subst_tac]) 

5094  468 
THEN prune_params_tac 
469 
end; 

470 

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

473 
let 

474 
val prem = Thm.assume cprop; 

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

476 
in 

477 
(case get_first (try mk_elim) elims of 

478 
Some r => r 

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

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

481 
Display.pretty_cterm cprop]))) 

482 
end; 

483 

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

487 

488 
(* inductive_cases(_i) *) 

489 

490 
fun gen_inductive_cases prep_att prep_const prep_prop 

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

492 
let 

493 
val sign = Theory.sign_of thy; 

494 

495 
val atts = map (prep_att thy) raw_atts; 

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

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

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

499 
in 

500 
thy 

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

5094  502 
end; 
503 

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

506 

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

508 

6424  509 

510 

511 
(** prove induction rule **) 

5094  512 

513 
fun prove_indrule cs cTs sumT rec_const params intr_ts mono 

514 
fp_def rec_sets_defs thy = 

515 
let 

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

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

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

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

523 

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

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

527 

528 
fun mk_ind_pred _ [P] = P 

529 
 mk_ind_pred T Ps = 

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

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

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

535 
end; 

536 

537 
val ind_pred = mk_ind_pred sumT preds; 

538 

539 
val ind_concl = HOLogic.mk_Trueprop 

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

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

542 

543 
(* simplification rules for vimage and Collect *) 

544 

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

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

547 
(HOLogic.mk_Trueprop (HOLogic.mk_eq 

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

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

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

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

554 
val induct = prove_goalw_cterm [] (cterm_of sign 

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

556 
[rtac (impI RS allI) 1, 

557 
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

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

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

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

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

569 
val lemma = prove_goalw_cterm rec_sets_defs (cterm_of sign 

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

571 
[cut_facts_tac prems 1, 

572 
REPEAT (EVERY 

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

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

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

578 
in standard (split_rule (induct RS lemma)) 

579 
end; 

580 

6424  581 

582 

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

584 

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

5094  586 

587 
fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs 

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

5094  592 

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

594 
val setT = HOLogic.mk_setT sumT; 

595 

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

5094  598 

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

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

603 

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

606 
(* is transformed into *) 

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

608 

609 
fun transform_rule r = 

610 
let 

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

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

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

616 

617 
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

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

622 
end 

623 

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

625 

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

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

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

630 

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

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

634 
val rec_const = list_comb 

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

636 

637 
val fp_def_term = Logic.mk_equals (rec_const, 

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

639 

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

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

642 

643 
val thy' = thy > 

644 
(if declare_consts then 

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

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

647 
else I) > 

648 
(if length cs < 2 then I else 

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

650 
Theory.add_path rec_name > 

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

652 

653 
(* get definitions from theory *) 

654 

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

657 
(* prove and store theorems *) 

658 

659 
val mono = prove_mono setT fp_fun monos thy'; 

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

661 
rec_sets_defs thy'; 

662 
val elims = if no_elim then [] else 

663 
prove_elims cs cTs params intr_ts unfold rec_sets_defs thy'; 

8312
b470bc28b59d
add_cases_induct: accomodate no_elim and no_ind flags;
wenzelm
parents:
8307
diff
changeset

664 
val raw_induct = if no_ind then Drule.asm_rl else 
5094  665 
if coind then standard (rule_by_tactic 
5553  666 
(rewrite_tac [mk_meta_eq vimage_Un] THEN 
5094  667 
fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct))) 
668 
else 

669 
prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def 

670 
rec_sets_defs thy'; 

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

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

678 
> (if no_ind then I else PureThy.add_thms 

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

680 
> Theory.parent_path; 

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

681 
val intrs' = PureThy.get_thms thy'' "intrs"; 
8312
b470bc28b59d
add_cases_induct: accomodate no_elim and no_ind flags;
wenzelm
parents:
8307
diff
changeset

682 
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

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

686 
mono = mono, 

687 
unfold = unfold, 

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

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

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

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

692 
induct = induct'}) 
5094  693 
end; 
694 

6424  695 

696 

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

5094  698 

699 
fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs 

6521  700 
atts intros monos con_defs thy params paramTs cTs cnames = 
5094  701 
let 
702 
val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name; 

703 

6424  704 
val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros); 
5094  705 
val elim_ts = mk_elims cs cTs params intr_ts; 
706 

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

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

709 

6424  710 
val thy' = thy 
711 
> (if declare_consts then 

712 
Theory.add_consts_i 

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

714 
else I) 

715 
> Theory.add_path rec_name 

6521  716 
> 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

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

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

6424  720 
val intrs = PureThy.get_thms thy' "intrs"; 
721 
val elims = PureThy.get_thms thy' "elims"; 

8312
b470bc28b59d
add_cases_induct: accomodate no_elim and no_ind flags;
wenzelm
parents:
8307
diff
changeset

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

725 

6424  726 
val thy'' = 
727 
thy' 

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

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

730 
> Theory.parent_path; 

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

731 
val induct' = if coind then raw_induct else PureThy.get_thm thy'' "induct"; 
5094  732 
in (thy'', 
733 
{defs = [], 

8312
b470bc28b59d
add_cases_induct: accomodate no_elim and no_ind flags;
wenzelm
parents:
8307
diff
changeset

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

735 
unfold = Drule.asm_rl, 
5094  736 
intrs = intrs, 
737 
elims = elims, 

738 
mk_cases = mk_cases elims, 

739 
raw_induct = raw_induct, 

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

740 
induct = induct'}) 
5094  741 
end; 
742 

6424  743 

744 

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

5094  746 

8312
b470bc28b59d
add_cases_induct: accomodate no_elim and no_ind flags;
wenzelm
parents:
8307
diff
changeset

747 
fun add_cases_induct no_elim no_ind names elims induct = 
b470bc28b59d
add_cases_induct: accomodate no_elim and no_ind flags;
wenzelm
parents:
8307
diff
changeset

748 
let 
b470bc28b59d
add_cases_induct: accomodate no_elim and no_ind flags;
wenzelm
parents:
8307
diff
changeset

749 
val cases_specs = 
b470bc28b59d
add_cases_induct: accomodate no_elim and no_ind flags;
wenzelm
parents:
8307
diff
changeset

750 
if no_elim then [] 
b470bc28b59d
add_cases_induct: accomodate no_elim and no_ind flags;
wenzelm
parents:
8307
diff
changeset

751 
else map2 (fn (name, elim) => (("", elim), [InductMethod.cases_set_global name])) 
b470bc28b59d
add_cases_induct: accomodate no_elim and no_ind flags;
wenzelm
parents:
8307
diff
changeset

752 
(names, elims); 
b470bc28b59d
add_cases_induct: accomodate no_elim and no_ind flags;
wenzelm
parents:
8307
diff
changeset

753 
val induct_specs = 
b470bc28b59d
add_cases_induct: accomodate no_elim and no_ind flags;
wenzelm
parents:
8307
diff
changeset

754 
if no_ind then [] 
b470bc28b59d
add_cases_induct: accomodate no_elim and no_ind flags;
wenzelm
parents:
8307
diff
changeset

755 
else map (fn name => (("", induct), [InductMethod.induct_set_global name])) names; 
b470bc28b59d
add_cases_induct: accomodate no_elim and no_ind flags;
wenzelm
parents:
8307
diff
changeset

756 
in PureThy.add_thms (cases_specs @ induct_specs) end; 
8307  757 

758 

5094  759 
fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs 
6521  760 
atts intros monos con_defs thy = 
5094  761 
let 
6424  762 
val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions"); 
6394  763 
val sign = Theory.sign_of thy; 
5094  764 

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

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

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

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

769 

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

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

772 

6437  773 
val full_cnames = map (try' (fst o dest_Const o head_of) 
5094  774 
"Recursive set not previously declared as constant: " sign) cs; 
6437  775 
val cnames = map Sign.base_name full_cnames; 
5094  776 

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

779 
val (thy1, result) = 

780 
(if ! quick_and_dirty then add_ind_axm else add_ind_def) 

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

8312
b470bc28b59d
add_cases_induct: accomodate no_elim and no_ind flags;
wenzelm
parents:
8307
diff
changeset

785 
> add_cases_induct no_elim no_ind full_cnames (#elims result) (#induct result); 
6437  786 
in (thy2, result) end; 
5094  787 

6424  788 

5094  789 

6424  790 
(** external interface **) 
791 

6521  792 
fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy = 
5094  793 
let 
6394  794 
val sign = Theory.sign_of thy; 
8100  795 
val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termT) c_strings; 
6424  796 

6521  797 
val atts = map (Attrib.global_attribute thy) srcs; 
6424  798 
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

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

801 
val (cs', intr_ts') = unify_consts sign cs intr_ts; 
5094  802 

6424  803 
val ((thy', con_defs), monos) = thy 
804 
> IsarThy.apply_theorems raw_monos 

805 
> apfst (IsarThy.apply_theorems raw_con_defs); 

806 
in 

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

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

808 
atts ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy' 
5094  809 
end; 
810 

6424  811 

812 

6437  813 
(** package setup **) 
814 

815 
(* setup theory *) 

816 

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

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

818 
Attrib.add_attributes [(monoN, mono_attr, "monotonicity rule")]]; 
6437  819 

820 

821 
(* outer syntax *) 

6424  822 

6723  823 
local structure P = OuterParse and K = OuterSyntax.Keyword in 
6424  824 

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

828 
fun ind_decl coind = 

6729  829 
(Scan.repeat1 P.term  P.marg_comment)  
830 
(P.$$$ "intrs"  

7152  831 
P.!!! (P.opt_attribs  Scan.repeat1 (P.opt_thm_name ":"  P.prop  P.marg_comment)))  
6729  832 
Scan.optional (P.$$$ "monos"  P.!!! P.xthms1  P.marg_comment) []  
833 
Scan.optional (P.$$$ "con_defs"  P.!!! P.xthms1  P.marg_comment) [] 

6424  834 
>> (Toplevel.theory o mk_ind coind); 
835 

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

838 

839 
val coinductiveP = 

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

6424  841 

7107  842 

843 
val ind_cases = 

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

845 
>> (Toplevel.theory o inductive_cases); 

846 

847 
val inductive_casesP = 

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

849 
K.thy_decl ind_cases; 

850 

6424  851 
val _ = OuterSyntax.add_keywords ["intrs", "monos", "con_defs"]; 
7107  852 
val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP]; 
6424  853 

5094  854 
end; 
6424  855 

856 

857 
end; 