author  berghofe 
Wed, 07 Feb 2007 17:58:50 +0100  
changeset 22275  51411098e49b 
parent 22102  a89ef7144729 
child 22422  ee19cdb07528 
permissions  rwrr 
5094  1 
(* Title: HOL/Tools/inductive_package.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

4 
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen 
5094  5 

6424  6 
(Co)Inductive Definition module for HOL. 
5094  7 

8 
Features: 

6424  9 
* least or greatest fixedpoints 
10 
* mutually recursive definitions 

11 
* definitions involving arbitrary monotone operators 

12 
* automatically proves introduction and elimination rules 

5094  13 

14 
Introduction rules have the form 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

15 
[ M Pj ti, ..., Q x, ... ] ==> Pk t 
5094  16 
where M is some monotone operator (usually the identity) 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

17 
Q x is any side condition on the free variables 
5094  18 
ti, t are any terms 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

19 
Pj, Pk are two of the predicates being defined in mutual recursion 
5094  20 
*) 
21 

22 
signature INDUCTIVE_PACKAGE = 

23 
sig 

6424  24 
val quiet_mode: bool ref 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

25 
type inductive_result 
21526
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

26 
val morph_result: morphism > inductive_result > inductive_result 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

27 
type inductive_info 
21526
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

28 
val the_inductive: Proof.context > string > inductive_info 
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

29 
val print_inductives: Proof.context > unit 
18728  30 
val mono_add: attribute 
31 
val mono_del: attribute 

21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

32 
val get_monos: Proof.context > thm list 
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

33 
val mk_cases: Proof.context > term > thm 
10910
058775a575db
export inductive_forall_name, inductive_forall_def, rulify;
wenzelm
parents:
10804
diff
changeset

34 
val inductive_forall_name: string 
058775a575db
export inductive_forall_name, inductive_forall_def, rulify;
wenzelm
parents:
10804
diff
changeset

35 
val inductive_forall_def: thm 
058775a575db
export inductive_forall_name, inductive_forall_def, rulify;
wenzelm
parents:
10804
diff
changeset

36 
val rulify: thm > thm 
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

37 
val inductive_cases: ((bstring * Attrib.src list) * string list) list > 
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

38 
Proof.context > thm list list * local_theory 
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

39 
val inductive_cases_i: ((bstring * Attrib.src list) * term list) list > 
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

40 
Proof.context > thm list list * local_theory 
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

41 
val add_inductive_i: bool > bstring > bool > bool > bool > 
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

42 
(string * typ option * mixfix) list > 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

43 
(string * typ option) list > ((bstring * Attrib.src list) * term) list > thm list > 
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

44 
local_theory > inductive_result * local_theory 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

45 
val add_inductive: bool > bool > (string * string option * mixfix) list > 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

46 
(string * string option * mixfix) list > 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

47 
((bstring * Attrib.src list) * string) list > (thmref * Attrib.src list) list > 
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

48 
local_theory > inductive_result * local_theory 
21526
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

49 
val add_inductive_global: bool > bstring > bool > bool > bool > 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

50 
(string * typ option * mixfix) list > (string * typ option) list > 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

51 
((bstring * Attrib.src list) * term) list > thm list > theory > inductive_result * theory 
18708  52 
val setup: theory > theory 
5094  53 
end; 
54 

6424  55 
structure InductivePackage: INDUCTIVE_PACKAGE = 
5094  56 
struct 
57 

9598  58 

10729  59 
(** theory context references **) 
60 

15525  61 
val mono_name = "Orderings.mono"; 
17010
5abc26872268
changed reference to Lfp.lfp to FixedPint.lfp, ditto for gfp
avigad
parents:
16975
diff
changeset

62 
val gfp_name = "FixedPoint.gfp"; 
5abc26872268
changed reference to Lfp.lfp to FixedPint.lfp, ditto for gfp
avigad
parents:
16975
diff
changeset

63 
val lfp_name = "FixedPoint.lfp"; 
10735  64 

11991  65 
val inductive_forall_name = "HOL.induct_forall"; 
66 
val inductive_forall_def = thm "induct_forall_def"; 

67 
val inductive_conj_name = "HOL.induct_conj"; 

68 
val inductive_conj_def = thm "induct_conj_def"; 

69 
val inductive_conj = thms "induct_conj"; 

70 
val inductive_atomize = thms "induct_atomize"; 

18463  71 
val inductive_rulify = thms "induct_rulify"; 
72 
val inductive_rulify_fallback = thms "induct_rulify_fallback"; 

10729  73 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

74 
val notTrueE = TrueI RSN (2, notE); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

75 
val notFalseI = Seq.hd (atac 1 notI); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

76 
val simp_thms' = map (fn s => mk_meta_eq (the (find_first 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

77 
(equal (term_of (read_cterm HOL.thy (s, propT))) o prop_of) simp_thms))) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

78 
["(~True) = False", "(~False) = True", 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

79 
"(True > ?P) = ?P", "(False > ?P) = True", 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

80 
"(?P & True) = ?P", "(True & ?P) = ?P"]; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

81 

10729  82 

83 

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

85 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

86 
type inductive_result = 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

87 
{preds: term list, defs: thm list, elims: thm list, raw_induct: thm, 
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

88 
induct: thm, intrs: thm list, mono: thm, unfold: thm}; 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

89 

21526
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

90 
fun morph_result phi {preds, defs, elims, raw_induct: thm, induct, intrs, mono, unfold} = 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

91 
let 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

92 
val term = Morphism.term phi; 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

93 
val thm = Morphism.thm phi; 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

94 
val fact = Morphism.fact phi; 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

95 
in 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

96 
{preds = map term preds, defs = fact defs, elims = fact elims, raw_induct = thm raw_induct, 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

97 
induct = thm induct, intrs = fact intrs, mono = thm mono, unfold = thm unfold} 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

98 
end; 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

99 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

100 
type inductive_info = 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

101 
{names: string list, coind: bool} * inductive_result; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

102 

63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

103 
structure InductiveData = GenericDataFun 
16432  104 
(struct 
21526
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

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

106 
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

107 

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

108 
val empty = (Symtab.empty, []); 
16432  109 
val extend = I; 
110 
fun merge _ ((tab1, monos1), (tab2, monos2)) = 

11502  111 
(Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2)); 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

112 

21526
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

113 
fun print context (tab, monos) = 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

114 
let 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

115 
val ctxt = Context.proof_of context; 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

116 
val space = Consts.space_of (ProofContext.consts_of ctxt); 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

117 
in 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

118 
[Pretty.strs ("(co)inductives:" :: map #1 (NameSpace.extern_table (space, tab))), 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

119 
Pretty.big_list "monotonicity rules:" (map (ProofContext.pretty_thm ctxt) monos)] 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

120 
> Pretty.chunks > Pretty.writeln 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

121 
end; 
16432  122 
end); 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

123 

21526
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

124 
val get_inductives = InductiveData.get o Context.Proof; 
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

125 
val print_inductives = InductiveData.print o Context.Proof; 
7710
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 

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

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

129 

21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

130 
fun the_inductive ctxt name = 
21526
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

131 
(case Symtab.lookup (#1 (get_inductives ctxt)) name of 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

132 
NONE => error ("Unknown (co)inductive predicate " ^ quote name) 
15531  133 
 SOME info => info); 
9598  134 

18222  135 
fun put_inductives names info = InductiveData.map (apfst (fn tab => 
136 
fold (fn name => Symtab.update_new (name, info)) names tab 

21526
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

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

138 

8277  139 

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

140 

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

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

142 

21526
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

143 
val get_monos = #2 o get_inductives; 
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

144 
val map_monos = InductiveData.map o apsnd; 
8277  145 

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

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

147 
let 
22275
51411098e49b
 Improved handling of monotonicity rules involving <=
berghofe
parents:
22102
diff
changeset

148 
val concl = concl_of thm; 
51411098e49b
 Improved handling of monotonicity rules involving <=
berghofe
parents:
22102
diff
changeset

149 
fun eq2mono thm' = [thm' RS (thm' RS eq_to_mono)] @ 
51411098e49b
 Improved handling of monotonicity rules involving <=
berghofe
parents:
22102
diff
changeset

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

151 
(_ $ (_ $ (Const ("Not", _) $ _) $ _)) => [] 
22275
51411098e49b
 Improved handling of monotonicity rules involving <=
berghofe
parents:
22102
diff
changeset

152 
 _ => [thm' RS (thm' RS eq_to_mono2)]); 
51411098e49b
 Improved handling of monotonicity rules involving <=
berghofe
parents:
22102
diff
changeset

153 
fun dest_less_concl thm = dest_less_concl (thm RS le_funD) 
51411098e49b
 Improved handling of monotonicity rules involving <=
berghofe
parents:
22102
diff
changeset

154 
handle THM _ => thm RS le_boolD 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

155 
in 
22275
51411098e49b
 Improved handling of monotonicity rules involving <=
berghofe
parents:
22102
diff
changeset

156 
case concl of 
51411098e49b
 Improved handling of monotonicity rules involving <=
berghofe
parents:
22102
diff
changeset

157 
Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq) 
51411098e49b
 Improved handling of monotonicity rules involving <=
berghofe
parents:
22102
diff
changeset

158 
 _ $ (Const ("op =", _) $ _ $ _) => eq2mono thm 
51411098e49b
 Improved handling of monotonicity rules involving <=
berghofe
parents:
22102
diff
changeset

159 
 _ $ (Const ("Orderings.less_eq", _) $ _ $ _) => 
51411098e49b
 Improved handling of monotonicity rules involving <=
berghofe
parents:
22102
diff
changeset

160 
[dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL 
51411098e49b
 Improved handling of monotonicity rules involving <=
berghofe
parents:
22102
diff
changeset

161 
(resolve_tac [le_funI, le_boolI'])) thm))] 
51411098e49b
 Improved handling of monotonicity rules involving <=
berghofe
parents:
22102
diff
changeset

162 
 _ => [thm] 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

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

164 

21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

165 
val mono_add = Thm.declaration_attribute (map_monos o fold Drule.add_rule o mk_mono); 
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

166 
val mono_del = Thm.declaration_attribute (map_monos o fold Drule.del_rule o mk_mono); 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

167 

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

168 

7107  169 

10735  170 
(** misc utilities **) 
6424  171 

5662  172 
val quiet_mode = ref false; 
10735  173 
fun message s = if ! quiet_mode then () else writeln s; 
174 
fun clean_message s = if ! quick_and_dirty then () else message s; 

5662  175 

21433  176 
val note_theorems = LocalTheory.notes Thm.theoremK; 
177 
val note_theorem = LocalTheory.note Thm.theoremK; 

178 

6424  179 
fun coind_prefix true = "co" 
180 
 coind_prefix false = ""; 

181 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

182 
fun log b m n = if m >= n then 0 else 1 + log b (b * m) n; 
6424  183 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

184 
fun make_bool_args f g [] i = [] 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

185 
 make_bool_args f g (x :: xs) i = 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

186 
(if i mod 2 = 0 then f x else g x) :: make_bool_args f g xs (i div 2); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

187 

63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

188 
fun make_bool_args' xs = 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

189 
make_bool_args (K HOLogic.false_const) (K HOLogic.true_const) xs; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

190 

63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

191 
fun find_arg T x [] = sys_error "find_arg" 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

192 
 find_arg T x ((p as (_, (SOME _, _))) :: ps) = 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

193 
apsnd (cons p) (find_arg T x ps) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

194 
 find_arg T x ((p as (U, (NONE, y))) :: ps) = 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

195 
if T = U then (y, (U, (SOME x, y)) :: ps) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

196 
else apsnd (cons p) (find_arg T x ps); 
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

197 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

198 
fun make_args Ts xs = 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

199 
map (fn (T, (NONE, ())) => Const ("arbitrary", T)  (_, (SOME t, ())) => t) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

200 
(fold (fn (t, T) => snd o find_arg T t) xs (map (rpair (NONE, ())) Ts)); 
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

201 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

202 
fun make_args' Ts xs Us = 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

203 
fst (fold_map (fn T => find_arg T ()) Us (Ts ~~ map (pair NONE) xs)); 
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

204 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

205 
fun dest_predicate cs params t = 
5094  206 
let 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

207 
val k = length params; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

208 
val (c, ts) = strip_comb t; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

209 
val (xs, ys) = chop k ts; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

210 
val i = find_index_eq c cs; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

211 
in 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

212 
if xs = params andalso i >= 0 then 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

213 
SOME (c, i, ys, chop (length ys) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

214 
(List.drop (binder_types (fastype_of c), k))) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

215 
else NONE 
5094  216 
end; 
217 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

218 
fun mk_names a 0 = [] 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

219 
 mk_names a 1 = [a] 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

220 
 mk_names a n = map (fn i => a ^ string_of_int i) (1 upto n); 
10988
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

221 

6424  222 

223 

10729  224 
(** process rules **) 
225 

226 
local 

5094  227 

16432  228 
fun err_in_rule thy name t msg = 
229 
error (cat_lines ["Illformed introduction rule " ^ quote name, 

230 
Sign.string_of_term thy t, msg]); 

10729  231 

16432  232 
fun err_in_prem thy name t p msg = 
233 
error (cat_lines ["Illformed premise", Sign.string_of_term thy p, 

234 
"in introduction rule " ^ quote name, Sign.string_of_term thy t, msg]); 

5094  235 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

236 
val bad_concl = "Conclusion of introduction rule must be an inductive predicate"; 
10729  237 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

238 
val bad_ind_occ = "Inductive predicate occurs in argument of inductive predicate"; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

239 

63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

240 
val bad_app = "Inductive predicate must be applied to parameter(s) "; 
11358
416ea5c009f5
now checks for leading metaquantifiers and complains, instead of
paulson
parents:
11036
diff
changeset

241 

16432  242 
fun atomize_term thy = MetaSimplifier.rewrite_term thy inductive_atomize []; 
10729  243 

244 
in 

5094  245 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

246 
fun check_rule thy cs params ((name, att), rule) = 
10729  247 
let 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

248 
val params' = Term.variant_frees rule (Logic.strip_params rule); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

249 
val frees = rev (map Free params'); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

250 
val concl = subst_bounds (frees, Logic.strip_assums_concl rule); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

251 
val prems = map (curry subst_bounds frees) (Logic.strip_assums_hyp rule); 
16432  252 
val aprems = map (atomize_term thy) prems; 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

253 
val arule = list_all_free (params', Logic.list_implies (aprems, concl)); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

254 

63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

255 
fun check_ind err t = case dest_predicate cs params t of 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

256 
NONE => err (bad_app ^ 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

257 
commas (map (Sign.string_of_term thy) params)) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

258 
 SOME (_, _, ys, _) => 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

259 
if exists (fn c => exists (fn t => Logic.occs (c, t)) ys) cs 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

260 
then err bad_ind_occ else (); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

261 

63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

262 
fun check_prem' prem t = 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

263 
if head_of t mem cs then 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

264 
check_ind (err_in_prem thy name rule prem) t 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

265 
else (case t of 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

266 
Abs (_, _, t) => check_prem' prem t 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

267 
 t $ u => (check_prem' prem t; check_prem' prem u) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

268 
 _ => ()); 
5094  269 

10729  270 
fun check_prem (prem, aprem) = 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

271 
if can HOLogic.dest_Trueprop aprem then check_prem' prem prem 
16432  272 
else err_in_prem thy name rule prem "Nonatomic premise"; 
10729  273 
in 
11358
416ea5c009f5
now checks for leading metaquantifiers and complains, instead of
paulson
parents:
11036
diff
changeset

274 
(case concl of 
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

275 
Const ("Trueprop", _) $ t => 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

276 
if head_of t mem cs then 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

277 
(check_ind (err_in_rule thy name rule) t; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

278 
List.app check_prem (prems ~~ aprems)) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

279 
else err_in_rule thy name rule bad_concl 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

280 
 _ => err_in_rule thy name rule bad_concl); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

281 
((name, att), arule) 
10729  282 
end; 
5094  283 

18222  284 
val rulify = (* FIXME norm_hhf *) 
285 
hol_simplify inductive_conj 

18463  286 
#> hol_simplify inductive_rulify 
287 
#> hol_simplify inductive_rulify_fallback 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

288 
(*#> standard*); 
10729  289 

290 
end; 

291 

5094  292 

6424  293 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

294 
(** proofs for (co)inductive predicates **) 
6424  295 

10735  296 
(* prove monotonicity  NOT subject to quick_and_dirty! *) 
5094  297 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

298 
fun prove_mono predT fp_fun monos ctxt = 
10735  299 
(message " Proving monotonicity ..."; 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

300 
Goal.prove ctxt [] [] (*NO quick_and_dirty here!*) 
17985  301 
(HOLogic.mk_Trueprop 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

302 
(Const (mono_name, (predT > predT) > HOLogic.boolT) $ fp_fun)) 
17985  303 
(fn _ => EVERY [rtac monoI 1, 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

304 
REPEAT (resolve_tac [le_funI, le_boolI'] 1), 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

305 
REPEAT (FIRST 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

306 
[atac 1, 
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

307 
resolve_tac (List.concat (map mk_mono monos) @ get_monos ctxt) 1, 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

308 
etac le_funE 1, dtac le_boolD 1])])); 
5094  309 

6424  310 

10735  311 
(* prove introduction rules *) 
5094  312 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

313 
fun prove_intrs coind mono fp_def k intr_ts rec_preds_defs ctxt = 
5094  314 
let 
10735  315 
val _ = clean_message " Proving the introduction rules ..."; 
5094  316 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

317 
val unfold = funpow k (fn th => th RS fun_cong) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

318 
(mono RS (fp_def RS 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

319 
(if coind then def_gfp_unfold else def_lfp_unfold))); 
5094  320 

321 
fun select_disj 1 1 = [] 

322 
 select_disj _ 1 = [rtac disjI1] 

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

324 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

325 
val rules = [refl, TrueI, notFalseI, exI, conjI]; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

326 

63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

327 
val intrs = map_index (fn (i, intr) => 
20047  328 
rulify (SkipProof.prove ctxt [] [] intr (fn _ => EVERY 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

329 
[rewrite_goals_tac rec_preds_defs, 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

330 
rtac (unfold RS iffD2) 1, 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

331 
EVERY1 (select_disj (length intr_ts) (i + 1)), 
17985  332 
(*Not ares_tac, since refl must be tried before any equality assumptions; 
333 
backtracking may occur if the premises have extra variables!*) 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

334 
DEPTH_SOLVE_1 (resolve_tac rules 1 APPEND assume_tac 1)]))) intr_ts 
5094  335 

336 
in (intrs, unfold) end; 

337 

6424  338 

10735  339 
(* prove elimination rules *) 
5094  340 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

341 
fun prove_elims cs params intr_ts intr_names unfold rec_preds_defs ctxt = 
5094  342 
let 
10735  343 
val _ = clean_message " Proving the elimination rules ..."; 
5094  344 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

345 
val ([pname], ctxt') = Variable.variant_fixes ["P"] ctxt; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

346 
val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT)); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

347 

63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

348 
fun dest_intr r = 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

349 
(the (dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r))), 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

350 
Logic.strip_assums_hyp r, Logic.strip_params r); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

351 

63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

352 
val intrs = map dest_intr intr_ts ~~ intr_names; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

353 

63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

354 
val rules1 = [disjE, exE, FalseE]; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

355 
val rules2 = [conjE, FalseE, notTrueE]; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

356 

63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

357 
fun prove_elim c = 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

358 
let 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

359 
val Ts = List.drop (binder_types (fastype_of c), length params); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

360 
val (anames, ctxt'') = Variable.variant_fixes (mk_names "a" (length Ts)) ctxt'; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

361 
val frees = map Free (anames ~~ Ts); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

362 

63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

363 
fun mk_elim_prem ((_, _, us, _), ts, params') = 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

364 
list_all (params', 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

365 
Logic.list_implies (map (HOLogic.mk_Trueprop o HOLogic.mk_eq) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

366 
(frees ~~ us) @ ts, P)); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

367 
val c_intrs = (List.filter (equal c o #1 o #1 o #1) intrs); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

368 
val prems = HOLogic.mk_Trueprop (list_comb (c, params @ frees)) :: 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

369 
map mk_elim_prem (map #1 c_intrs) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

370 
in 
21048
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

371 
(SkipProof.prove ctxt'' [] prems P 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

372 
(fn {prems, ...} => EVERY 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

373 
[cut_facts_tac [hd prems] 1, 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

374 
rewrite_goals_tac rec_preds_defs, 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

375 
dtac (unfold RS iffD1) 1, 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

376 
REPEAT (FIRSTGOAL (eresolve_tac rules1)), 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

377 
REPEAT (FIRSTGOAL (eresolve_tac rules2)), 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

378 
EVERY (map (fn prem => 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

379 
DEPTH_SOLVE_1 (ares_tac [rewrite_rule rec_preds_defs prem, conjI] 1)) (tl prems))]) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

380 
> rulify 
21048
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

381 
> singleton (ProofContext.export ctxt'' ctxt), 
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

382 
map #2 c_intrs) 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

383 
end 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

384 

63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

385 
in map prove_elim cs end; 
5094  386 

6424  387 

10735  388 
(* derivation of simplified elimination rules *) 
5094  389 

11682
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

390 
local 
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

391 

d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

392 
(*delete needless equality assumptions*) 
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

393 
val refl_thin = prove_goal HOL.thy "!!P. a = a ==> P ==> P" (fn _ => [assume_tac 1]); 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

394 
val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE]; 
11682
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

395 
val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls; 
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

396 

d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

397 
fun simp_case_tac solved ss i = 
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

398 
EVERY' [elim_tac, asm_full_simp_tac ss, elim_tac, REPEAT o bound_hyp_subst_tac] i 
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

399 
THEN_MAYBE (if solved then no_tac else all_tac); (* FIXME !? *) 
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

400 

11682
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

401 
in 
9598  402 

21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

403 
fun mk_cases ctxt prop = 
7107  404 
let 
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

405 
val thy = ProofContext.theory_of ctxt; 
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

406 
val ss = Simplifier.local_simpset_of ctxt; 
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

407 

21526
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

408 
fun err msg = 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

409 
error (Pretty.string_of (Pretty.block 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

410 
[Pretty.str msg, Pretty.fbrk, ProofContext.pretty_term ctxt prop])); 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

411 

1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

412 
val P = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop) handle TERM _ => 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

413 
err "Objectlogic proposition expected"; 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

414 
val c = Term.head_name_of P; 
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

415 
val (_, {elims, ...}) = the_inductive ctxt c; 
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

416 

7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

417 
val cprop = Thm.cterm_of thy prop; 
11682
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

418 
val tac = ALLGOALS (simp_case_tac false ss) THEN prune_params_tac; 
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

419 
fun mk_elim rl = 
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

420 
Thm.implies_intr cprop (Tactic.rule_by_tactic tac (Thm.assume cprop RS rl)) 
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

421 
> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt); 
7107  422 
in 
423 
(case get_first (try mk_elim) elims of 

15531  424 
SOME r => r 
21526
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

425 
 NONE => err "Proposition not an inductive predicate:") 
7107  426 
end; 
427 

11682
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

428 
end; 
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

429 

7107  430 

21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

431 
(* inductive_cases *) 
7107  432 

21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

433 
fun gen_inductive_cases prep_att prep_prop args lthy = 
9598  434 
let 
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

435 
val thy = ProofContext.theory_of lthy; 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12798
diff
changeset

436 
val facts = args > map (fn ((a, atts), props) => 
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

437 
((a, map (prep_att thy) atts), 
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

438 
map (Thm.no_attributes o single o mk_cases lthy o prep_prop lthy) props)); 
21433  439 
in lthy > note_theorems facts >> map snd end; 
5094  440 

21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

441 
val inductive_cases = gen_inductive_cases Attrib.intern_src ProofContext.read_prop; 
12172  442 
val inductive_cases_i = gen_inductive_cases (K I) ProofContext.cert_prop; 
7107  443 

6424  444 

22275
51411098e49b
 Improved handling of monotonicity rules involving <=
berghofe
parents:
22102
diff
changeset

445 
fun ind_cases src = Method.syntax (Scan.lift (Scan.repeat1 Args.name  
51411098e49b
 Improved handling of monotonicity rules involving <=
berghofe
parents:
22102
diff
changeset

446 
Scan.optional (Args.$$$ "for"  Scan.repeat1 Args.name) [])) src 
51411098e49b
 Improved handling of monotonicity rules involving <=
berghofe
parents:
22102
diff
changeset

447 
#> (fn ((raw_props, fixes), ctxt) => 
51411098e49b
 Improved handling of monotonicity rules involving <=
berghofe
parents:
22102
diff
changeset

448 
let 
51411098e49b
 Improved handling of monotonicity rules involving <=
berghofe
parents:
22102
diff
changeset

449 
val (_, ctxt') = Variable.add_fixes fixes ctxt; 
51411098e49b
 Improved handling of monotonicity rules involving <=
berghofe
parents:
22102
diff
changeset

450 
val props = map (ProofContext.read_prop ctxt') raw_props; 
51411098e49b
 Improved handling of monotonicity rules involving <=
berghofe
parents:
22102
diff
changeset

451 
val ctxt'' = fold Variable.declare_term props ctxt'; 
51411098e49b
 Improved handling of monotonicity rules involving <=
berghofe
parents:
22102
diff
changeset

452 
val rules = ProofContext.export ctxt'' ctxt (map (mk_cases ctxt'') props) 
51411098e49b
 Improved handling of monotonicity rules involving <=
berghofe
parents:
22102
diff
changeset

453 
in Method.erule 0 rules end); 
9598  454 

455 

456 

10735  457 
(* prove induction rule *) 
5094  458 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

459 
fun prove_indrule cs argTs bs xs rec_const params intr_ts mono 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

460 
fp_def rec_preds_defs ctxt = 
5094  461 
let 
10735  462 
val _ = clean_message " Proving the induction rule ..."; 
20047  463 
val thy = ProofContext.theory_of ctxt; 
5094  464 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

465 
(* predicates for induction rule *) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

466 

63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

467 
val (pnames, ctxt') = Variable.variant_fixes (mk_names "P" (length cs)) ctxt; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

468 
val preds = map Free (pnames ~~ 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

469 
map (fn c => List.drop (binder_types (fastype_of c), length params) > 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

470 
HOLogic.boolT) cs); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

471 

63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

472 
(* transform an introduction rule into a premise for induction rule *) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

473 

63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

474 
fun mk_ind_prem r = 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

475 
let 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

476 
fun subst s = (case dest_predicate cs params s of 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

477 
SOME (_, i, ys, (_, Ts)) => 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

478 
let 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

479 
val k = length Ts; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

480 
val bs = map Bound (k  1 downto 0); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

481 
val P = list_comb (List.nth (preds, i), ys @ bs); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

482 
val Q = list_abs (mk_names "x" k ~~ Ts, 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

483 
HOLogic.mk_binop inductive_conj_name (list_comb (s, bs), P)) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

484 
in (Q, case Ts of [] => SOME (s, P)  _ => NONE) end 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

485 
 NONE => (case s of 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

486 
(t $ u) => (fst (subst t) $ fst (subst u), NONE) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

487 
 (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), NONE) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

488 
 _ => (s, NONE))); 
7293  489 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

490 
fun mk_prem (s, prems) = (case subst s of 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

491 
(_, SOME (t, u)) => t :: u :: prems 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

492 
 (t, _) => t :: prems); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

493 

63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

494 
val SOME (_, i, ys, _) = dest_predicate cs params 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

495 
(HOLogic.dest_Trueprop (Logic.strip_assums_concl r)) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

496 

63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

497 
in list_all_free (Logic.strip_params r, 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

498 
Logic.list_implies (map HOLogic.mk_Trueprop (foldr mk_prem 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

499 
[] (map HOLogic.dest_Trueprop (Logic.strip_assums_hyp r))), 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

500 
HOLogic.mk_Trueprop (list_comb (List.nth (preds, i), ys)))) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

501 
end; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

502 

63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

503 
val ind_prems = map mk_ind_prem intr_ts; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

504 

21526
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

505 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

506 
(* make conclusions for induction rules *) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

507 

63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

508 
val Tss = map (binder_types o fastype_of) preds; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

509 
val (xnames, ctxt'') = 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

510 
Variable.variant_fixes (mk_names "x" (length (flat Tss))) ctxt'; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

511 
val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

512 
(map (fn (((xnames, Ts), c), P) => 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

513 
let val frees = map Free (xnames ~~ Ts) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

514 
in HOLogic.mk_imp 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

515 
(list_comb (c, params @ frees), list_comb (P, frees)) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

516 
end) (unflat Tss xnames ~~ Tss ~~ cs ~~ preds))); 
5094  517 

13626
282fbabec862
Fixed bug involving inductive definitions having equalities in the premises,
paulson
parents:
13197
diff
changeset

518 

5094  519 
(* make predicate for instantiation of abstract induction rule *) 
520 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

521 
val ind_pred = fold_rev lambda (bs @ xs) (foldr1 HOLogic.mk_conj 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

522 
(map_index (fn (i, P) => foldr HOLogic.mk_imp 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

523 
(list_comb (P, make_args' argTs xs (binder_types (fastype_of P)))) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

524 
(make_bool_args HOLogic.mk_not I bs i)) preds)); 
5094  525 

526 
val ind_concl = HOLogic.mk_Trueprop 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

527 
(HOLogic.mk_binrel "Orderings.less_eq" (rec_const, ind_pred)); 
5094  528 

13626
282fbabec862
Fixed bug involving inductive definitions having equalities in the premises,
paulson
parents:
13197
diff
changeset

529 
val raw_fp_induct = (mono RS (fp_def RS def_lfp_induct)); 
282fbabec862
Fixed bug involving inductive definitions having equalities in the premises,
paulson
parents:
13197
diff
changeset

530 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

531 
val induct = SkipProof.prove ctxt'' [] ind_prems ind_concl 
20248  532 
(fn {prems, ...} => EVERY 
17985  533 
[rewrite_goals_tac [inductive_conj_def], 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

534 
DETERM (rtac raw_fp_induct 1), 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

535 
REPEAT (resolve_tac [le_funI, le_boolI] 1), 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

536 
rewrite_goals_tac (map mk_meta_eq [meet_fun_eq, meet_bool_eq] @ simp_thms'), 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

537 
(*This disjE separates out the introduction rules*) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

538 
REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])), 
5094  539 
(*Now break down the individual cases. No disjE here in case 
540 
some premise involves disjunction.*) 

13747
bf308fcfd08e
Better treatment of equality in premises of inductive definitions. Less
paulson
parents:
13709
diff
changeset

541 
REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac)), 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

542 
REPEAT (FIRSTGOAL 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

543 
(resolve_tac [conjI, impI] ORELSE' (etac notE THEN' atac))), 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

544 
EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

545 
(inductive_conj_def :: rec_preds_defs) prem, conjI, refl] 1)) prems)]); 
5094  546 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

547 
val lemma = SkipProof.prove ctxt'' [] [] 
17985  548 
(Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn _ => EVERY 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

549 
[rewrite_goals_tac rec_preds_defs, 
5094  550 
REPEAT (EVERY 
551 
[REPEAT (resolve_tac [conjI, impI] 1), 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

552 
REPEAT (eresolve_tac [le_funE, le_boolE] 1), 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

553 
atac 1, 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

554 
rewrite_goals_tac simp_thms', 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

555 
atac 1])]) 
5094  556 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

557 
in singleton (ProofContext.export ctxt'' ctxt) (induct RS lemma) end; 
5094  558 

6424  559 

560 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

561 
(** specification of (co)inductive predicates **) 
10729  562 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

563 
fun mk_ind_def alt_name coind cs intr_ts monos 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

564 
params cnames_syn ctxt = 
5094  565 
let 
10735  566 
val fp_name = if coind then gfp_name else lfp_name; 
5094  567 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

568 
val argTs = fold (fn c => fn Ts => Ts @ 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

569 
(List.drop (binder_types (fastype_of c), length params) \\ Ts)) cs []; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

570 
val k = log 2 1 (length cs); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

571 
val predT = replicate k HOLogic.boolT > argTs > HOLogic.boolT; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

572 
val p :: xs = map Free (Variable.variant_frees ctxt intr_ts 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

573 
(("p", predT) :: (mk_names "x" (length argTs) ~~ argTs))); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

574 
val bs = map Free (Variable.variant_frees ctxt (p :: xs @ intr_ts) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

575 
(map (rpair HOLogic.boolT) (mk_names "b" k))); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

576 

63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

577 
fun subst t = (case dest_predicate cs params t of 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

578 
SOME (_, i, ts, (Ts, Us)) => 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

579 
let val zs = map Bound (length Us  1 downto 0) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

580 
in 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

581 
list_abs (map (pair "z") Us, list_comb (p, 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

582 
make_bool_args' bs i @ make_args argTs ((ts ~~ Ts) @ (zs ~~ Us)))) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

583 
end 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

584 
 NONE => (case t of 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

585 
t1 $ t2 => subst t1 $ subst t2 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

586 
 Abs (x, T, u) => Abs (x, T, subst u) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

587 
 _ => t)); 
5149  588 

5094  589 
(* transform an introduction rule into a conjunction *) 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

590 
(* [ p_i t; ... ] ==> p_j u *) 
5094  591 
(* is transformed into *) 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

592 
(* b_j & x_j = u & p b_j t & ... *) 
5094  593 

594 
fun transform_rule r = 

595 
let 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

596 
val SOME (_, i, ts, (Ts, _)) = dest_predicate cs params 
21048
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

597 
(HOLogic.dest_Trueprop (Logic.strip_assums_concl r)); 
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

598 
val ps = make_bool_args HOLogic.mk_not I bs i @ 
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

599 
map HOLogic.mk_eq (make_args' argTs xs Ts ~~ ts) @ 
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

600 
map (subst o HOLogic.dest_Trueprop) 
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

601 
(Logic.strip_assums_hyp r) 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

602 
in foldr (fn ((x, T), P) => HOLogic.exists_const T $ (Abs (x, T, P))) 
21048
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

603 
(if null ps then HOLogic.true_const else foldr1 HOLogic.mk_conj ps) 
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

604 
(Logic.strip_params r) 
5094  605 
end 
606 

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

608 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

609 
val fp_fun = fold_rev lambda (p :: bs @ xs) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

610 
(if null intr_ts then HOLogic.false_const 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

611 
else foldr1 HOLogic.mk_disj (map transform_rule intr_ts)); 
5094  612 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

613 
(* add definiton of recursive predicates to theory *) 
5094  614 

14235
281295a1bbaa
Fixed bug in mk_ind_def that caused the inductive definition package to
berghofe
parents:
13747
diff
changeset

615 
val rec_name = if alt_name = "" then 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

616 
space_implode "_" (map fst cnames_syn) else alt_name; 
5094  617 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

618 
val ((rec_const, (_, fp_def)), ctxt') = ctxt > 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

619 
Variable.add_fixes (map (fst o dest_Free) params) > snd > 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

620 
fold Variable.declare_term intr_ts > 
21433  621 
LocalTheory.def Thm.internalK 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

622 
((rec_name, case cnames_syn of [(_, syn)] => syn  _ => NoSyn), 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

623 
(("", []), fold_rev lambda params 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

624 
(Const (fp_name, (predT > predT) > predT) $ fp_fun))); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

625 
val fp_def' = Simplifier.rewrite (HOL_basic_ss addsimps [fp_def]) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

626 
(cterm_of (ProofContext.theory_of ctxt') (list_comb (rec_const, params))); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

627 
val specs = if length cs < 2 then [] else 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

628 
map_index (fn (i, (name_mx, c)) => 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

629 
let 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

630 
val Ts = List.drop (binder_types (fastype_of c), length params); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

631 
val xs = map Free (Variable.variant_frees ctxt intr_ts 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

632 
(mk_names "x" (length Ts) ~~ Ts)) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

633 
in 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

634 
(name_mx, (("", []), fold_rev lambda (params @ xs) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

635 
(list_comb (rec_const, params @ make_bool_args' bs i @ 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

636 
make_args argTs (xs ~~ Ts))))) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

637 
end) (cnames_syn ~~ cs); 
21433  638 
val (consts_defs, ctxt'') = fold_map (LocalTheory.def Thm.internalK) specs ctxt'; 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

639 
val preds = (case cs of [_] => [rec_const]  _ => map #1 consts_defs); 
5094  640 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

641 
val mono = prove_mono predT fp_fun monos ctxt'' 
5094  642 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

643 
in (ctxt'', rec_name, mono, fp_def', map (#2 o #2) consts_defs, 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

644 
list_comb (rec_const, params), preds, argTs, bs, xs) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

645 
end; 
5094  646 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

647 
fun add_ind_def verbose alt_name coind no_elim no_ind cs 
21048
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

648 
intros monos params cnames_syn ctxt = 
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

649 
let 
10735  650 
val _ = 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

651 
if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^ 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

652 
commas_quote (map fst cnames_syn)) else (); 
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

653 

21526
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

654 
val cnames = map (Sign.full_name (ProofContext.theory_of ctxt) o #1) cnames_syn; (* FIXME *) 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

655 
val ((intr_names, intr_atts), intr_ts) = apfst split_list (split_list intros); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

656 

63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

657 
val (ctxt1, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds, 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

658 
argTs, bs, xs) = mk_ind_def alt_name coind cs intr_ts 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

659 
monos params cnames_syn ctxt; 
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

660 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

661 
val (intrs, unfold) = prove_intrs coind mono fp_def (length bs + length xs) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

662 
intr_ts rec_preds_defs ctxt1; 
21048
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

663 
val elims = if no_elim then [] else 
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

664 
cnames ~~ map (apfst (singleton (ProofContext.export ctxt1 ctxt))) 
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

665 
(prove_elims cs params intr_ts intr_names unfold rec_preds_defs ctxt1); 
21766
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

666 
val raw_induct = zero_var_indexes (singleton (ProofContext.export ctxt1 ctxt) 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

667 
(if no_ind then Drule.asm_rl else 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

668 
if coind then ObjectLogic.rulify (rule_by_tactic 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

669 
(rewrite_tac [le_fun_def, le_bool_def] THEN 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

670 
fold_tac rec_preds_defs) (mono RS (fp_def RS def_coinduct))) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

671 
else 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

672 
prove_indrule cs argTs bs xs rec_const params intr_ts mono fp_def 
21766
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

673 
rec_preds_defs ctxt1)); 
21048
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

674 
val induct_cases = map (#1 o #1) intros; 
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

675 
val ind_case_names = RuleCases.case_names induct_cases; 
12165  676 
val induct = 
18222  677 
if coind then 
678 
(raw_induct, [RuleCases.case_names [rec_name], 

18234  679 
RuleCases.case_conclusion (rec_name, induct_cases), 
18222  680 
RuleCases.consumes 1]) 
681 
else if no_ind orelse length cs > 1 then 

21048
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

682 
(raw_induct, [ind_case_names, RuleCases.consumes 0]) 
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

683 
else (raw_induct RSN (2, rev_mp), [ind_case_names, RuleCases.consumes 1]); 
5094  684 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

685 
val (intrs', ctxt2) = 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

686 
ctxt1 > 
21433  687 
note_theorems 
21390
b3a9d8a83dea
replaced NameSpace.append by NameSpace.qualified, which handles empty names as expected;
wenzelm
parents:
21367
diff
changeset

688 
(map (NameSpace.qualified rec_name) intr_names ~~ 
21048
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

689 
intr_atts ~~ 
21658  690 
map (fn th => [([th], [Attrib.internal (K (ContextRules.intro_query NONE))])]) 
21465
2d3f477118c2
more careful declaration of "intros" as Pure.intro;
wenzelm
parents:
21433
diff
changeset

691 
(ProofContext.export ctxt1 ctxt intrs)) >> 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

692 
map (hd o snd); (* FIXME? *) 
21048
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

693 
val (((_, elims'), (_, [induct'])), ctxt3) = 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

694 
ctxt2 > 
21465
2d3f477118c2
more careful declaration of "intros" as Pure.intro;
wenzelm
parents:
21433
diff
changeset

695 
note_theorem ((NameSpace.qualified rec_name "intros", []), intrs') >> 
21048
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

696 
fold_map (fn (name, (elim, cases)) => 
21433  697 
note_theorem ((NameSpace.qualified (Sign.base_name name) "cases", 
21658  698 
[Attrib.internal (K (RuleCases.case_names cases)), 
699 
Attrib.internal (K (RuleCases.consumes 1)), 

700 
Attrib.internal (K (InductAttrib.cases_set name)), 

701 
Attrib.internal (K (ContextRules.elim_query NONE))]), [elim]) #> 

21048
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

702 
apfst (hd o snd)) elims >> 
21433  703 
note_theorem ((NameSpace.qualified rec_name (coind_prefix coind ^ "induct"), 
21658  704 
map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]); 
21048
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

705 

e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

706 
val induct_att = if coind then InductAttrib.coinduct_set else InductAttrib.induct_set; 
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

707 
val ctxt4 = if no_ind then ctxt3 else 
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

708 
let val inducts = cnames ~~ ProjectRule.projects ctxt (1 upto length cnames) induct' 
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

709 
in 
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

710 
ctxt3 > 
21508  711 
note_theorems [((NameSpace.qualified rec_name (coind_prefix coind ^ "inducts"), []), 
712 
inducts > map (fn (name, th) => ([th], 

21658  713 
[Attrib.internal (K ind_case_names), 
714 
Attrib.internal (K (RuleCases.consumes 1)), 

715 
Attrib.internal (K (induct_att name))])))] > snd 

21048
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

716 
end; 
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

717 

21526
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

718 
val names = map #1 cnames_syn; 
21048
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

719 
val result = 
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

720 
{preds = preds, 
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

721 
defs = fp_def :: rec_preds_defs, 
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

722 
mono = singleton (ProofContext.export ctxt1 ctxt) mono, 
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

723 
unfold = singleton (ProofContext.export ctxt1 ctxt) unfold, 
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

724 
intrs = intrs', 
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

725 
elims = elims', 
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

726 
raw_induct = rulify raw_induct, 
21526
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

727 
induct = induct'}; 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

728 
val target_result = morph_result (LocalTheory.target_morphism ctxt4) result; 
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

729 

21526
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

730 
val ctxt5 = ctxt4 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

731 
> Context.proof_map (put_inductives names ({names = names, coind = coind}, result)) 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

732 
> LocalTheory.declaration (fn phi => 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

733 
let 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

734 
val names' = map (LocalTheory.target_name ctxt4 o Morphism.name phi) names; 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

735 
val result' = morph_result phi target_result; 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

736 
in put_inductives names' ({names = names', coind = coind}, result') end); 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

737 
in (result, ctxt5) end; 
5094  738 

6424  739 

10735  740 
(* external interfaces *) 
5094  741 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

742 
fun add_inductive_i verbose alt_name coind no_elim no_ind cnames_syn pnames pre_intros monos ctxt = 
5094  743 
let 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

744 
val thy = ProofContext.theory_of ctxt; 
6424  745 
val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions"); 
5094  746 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

747 
val frees = fold (Term.add_frees o snd) pre_intros []; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

748 
fun type_of s = (case AList.lookup op = frees s of 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

749 
NONE => error ("No such variable: " ^ s)  SOME T => T); 
5094  750 

21766
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

751 
fun is_abbrev ((name, atts), t) = 
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

752 
can (Logic.strip_assums_concl #> Logic.dest_equals) t andalso 
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

753 
(name = "" andalso null atts orelse 
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

754 
error "Abbreviations may not have names or attributes"); 
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

755 

3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

756 
fun expand_atom tab (t as Free xT) = 
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

757 
the_default t (AList.lookup op = tab xT) 
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

758 
 expand_atom tab t = t; 
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

759 
fun expand [] r = r 
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

760 
 expand tab r = Envir.beta_norm (Term.map_aterms (expand_atom tab) r); 
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

761 

3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

762 
val (_, ctxt') = Variable.add_fixes (map #1 cnames_syn) ctxt; 
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

763 

3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

764 
fun prep_abbrevs [] abbrevs' abbrevs'' = (rev abbrevs', rev abbrevs'') 
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

765 
 prep_abbrevs ((_, abbrev) :: abbrevs) abbrevs' abbrevs'' = 
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

766 
let val ((s, T), t) = 
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

767 
LocalDefs.abs_def (snd (LocalDefs.cert_def ctxt' abbrev)) 
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

768 
in case find_first (equal s o #1) cnames_syn of 
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

769 
NONE => error ("Head of abbreviation " ^ quote s ^ " undeclared") 
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

770 
 SOME (_, _, mx) => prep_abbrevs abbrevs 
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

771 
(((s, T), expand abbrevs' t) :: abbrevs') 
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

772 
(((s, mx), expand abbrevs' t) :: abbrevs'') (* FIXME: do not expand *) 
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

773 
end; 
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

774 

3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

775 
val (abbrevs, pre_intros') = List.partition is_abbrev pre_intros; 
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

776 
val (abbrevs', abbrevs'') = prep_abbrevs abbrevs [] []; 
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

777 
val _ = (case gen_inter (op = o apsnd fst) 
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

778 
(fold (Term.add_frees o snd) abbrevs' [], abbrevs') of 
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

779 
[] => () 
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

780 
 xs => error ("Bad abbreviation(s): " ^ commas (map fst xs))); 
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

781 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

782 
val params = map 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

783 
(fn (s, SOME T) => Free (s, T)  (s, NONE) => Free (s, type_of s)) pnames; 
21766
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

784 
val cnames_syn' = filter_out (fn (s, _, _) => 
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

785 
exists (equal s o fst o fst) abbrevs') cnames_syn; 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

786 
val cs = map 
21766
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

787 
(fn (s, SOME T, _) => Free (s, T)  (s, NONE, _) => Free (s, type_of s)) cnames_syn'; 
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

788 
val cnames_syn'' = map (fn (s, _, mx) => (s, mx)) cnames_syn'; 
5094  789 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

790 
fun close_rule (x, r) = (x, list_all_free (rev (fold_aterms 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

791 
(fn t as Free (v as (s, _)) => 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

792 
if Variable.is_fixed ctxt s orelse member op = cs t orelse 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

793 
member op = params t then I else insert op = v 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

794 
 _ => I) r []), r)); 
5094  795 

21766
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

796 
val intros = map (apsnd (expand abbrevs') #> 
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

797 
check_rule thy cs params #> close_rule) pre_intros'; 
21048
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

798 
in 
21766
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

799 
ctxt > 
21048
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

800 
add_ind_def verbose alt_name coind no_elim no_ind cs intros monos 
21766
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

801 
params cnames_syn'' > 
21793  802 
fold (snd oo LocalTheory.abbrev Syntax.default_mode) abbrevs'' 
21048
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

803 
end; 
5094  804 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

805 
fun add_inductive verbose coind cnames_syn pnames_syn intro_srcs raw_monos ctxt = 
5094  806 
let 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

807 
val (_, ctxt') = Specification.read_specification (cnames_syn @ pnames_syn) [] ctxt; 
21766
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

808 
val intrs = map (fn ((name, att), s) => apsnd hd (hd (snd (fst 
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

809 
(Specification.read_specification [] [((name, att), [s])] ctxt')))) 
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

810 
handle ERROR msg => 
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

811 
cat_error msg ("The error(s) above occurred for\n" ^ 
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

812 
(if name = "" then "" else name ^ ": ") ^ s)) intro_srcs; 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

813 
val pnames = map (fn (s, _, _) => 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

814 
(s, SOME (ProofContext.infer_type ctxt' s))) pnames_syn; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

815 
val cnames_syn' = map (fn (s, _, mx) => 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

816 
(s, SOME (ProofContext.infer_type ctxt' s), mx)) cnames_syn; 
21350  817 
val (monos, ctxt'') = LocalTheory.theory_result (IsarCmd.apply_theorems raw_monos) ctxt; 
6424  818 
in 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

819 
add_inductive_i verbose "" coind false false cnames_syn' pnames intrs monos ctxt'' 
5094  820 
end; 
821 

21526
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

822 
fun add_inductive_global verbose alt_name coind no_elim no_ind cnames_syn pnames pre_intros monos = 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

823 
TheoryTarget.init NONE #> 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

824 
add_inductive_i verbose alt_name coind no_elim no_ind cnames_syn pnames pre_intros monos #> 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

825 
(fn (_, lthy) => 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

826 
(#2 (the_inductive (LocalTheory.target_of lthy) 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

827 
(LocalTheory.target_name lthy (#1 (hd cnames_syn)))), 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

828 
ProofContext.theory_of (LocalTheory.exit lthy))); 
6424  829 

830 

6437  831 
(** package setup **) 
832 

833 
(* setup theory *) 

834 

8634  835 
val setup = 
18708  836 
InductiveData.init #> 
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

837 
Method.add_methods [("ind_cases2", ind_cases, (* FIXME "ind_cases" (?) *) 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

838 
"dynamic case analysis on predicates")] #> 
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

839 
Attrib.add_attributes [("mono2", Attrib.add_del_args mono_add mono_del, (* FIXME "mono" *) 
18728  840 
"declaration of monotonicity rule")]; 
6437  841 

842 

843 
(* outer syntax *) 

6424  844 

17057  845 
local structure P = OuterParse and K = OuterKeyword in 
6424  846 

21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

847 
(* FIXME tmp *) 
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

848 
fun flatten_specification specs = specs > maps 
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

849 
(fn (a, (concl, [])) => concl > map 
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

850 
(fn ((b, atts), [B]) => 
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

851 
if a = "" then ((b, atts), B) 
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

852 
else if b = "" then ((a, atts), B) 
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

853 
else error ("Illegal nested case names " ^ quote (NameSpace.append a b)) 
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

854 
 ((b, _), _) => error ("Illegal simultaneous specification " ^ quote b)) 
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

855 
 (a, _) => error ("Illegal local specification parameters for " ^ quote a)); 
6424  856 

857 
fun ind_decl coind = 

22102  858 
P.opt_target  
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

859 
P.fixes  P.for_fixes  
22102  860 
Scan.optional (P.$$$ "where"  P.!!! SpecParse.specification) []  
861 
Scan.optional (P.$$$ "monos"  P.!!! SpecParse.xthms1) [] 

21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

862 
>> (fn ((((loc, preds), params), specs), monos) => 
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

863 
Toplevel.local_theory loc 
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

864 
(fn lthy => lthy 
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

865 
> add_inductive true coind preds params (flatten_specification specs) monos > snd)); 
6424  866 

6723  867 
val inductiveP = 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

868 
OuterSyntax.command "inductive2" "define inductive predicates" K.thy_decl (ind_decl false); 
6723  869 

870 
val coinductiveP = 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

871 
OuterSyntax.command "coinductive2" "define coinductive predicates" K.thy_decl (ind_decl true); 
6424  872 

7107  873 

874 
val inductive_casesP = 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

875 
OuterSyntax.command "inductive_cases2" 
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

876 
"create simplified instances of elimination rules (improper)" K.thy_script 
22102  877 
(P.opt_target  P.and_list1 SpecParse.spec 
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

878 
>> (fn (loc, specs) => Toplevel.local_theory loc (snd o inductive_cases specs))); 
7107  879 

21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

880 
val _ = OuterSyntax.add_keywords ["monos"]; 
7107  881 
val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP]; 
6424  882 

5094  883 
end; 
6424  884 

885 
end; 