author | wenzelm |
Thu, 17 Aug 2000 21:07:25 +0200 | |
changeset 9643 | c94db1a96f4e |
parent 9625 | 77506775481e |
child 9804 | ee0c337327cf |
permissions | -rw-r--r-- |
5094 | 1 |
(* Title: HOL/Tools/inductive_package.ML |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Stefan Berghofer, TU Muenchen |
|
5 |
Copyright 1994 University of Cambridge |
|
9598 | 6 |
1998 TU Muenchen |
5094 | 7 |
|
6424 | 8 |
(Co)Inductive Definition module for HOL. |
5094 | 9 |
|
10 |
Features: |
|
6424 | 11 |
* least or greatest fixedpoints |
12 |
* user-specified product and sum constructions |
|
13 |
* mutually recursive definitions |
|
14 |
* definitions involving arbitrary monotone operators |
|
15 |
* automatically proves introduction and elimination rules |
|
5094 | 16 |
|
6424 | 17 |
The recursive sets must *already* be declared as constants in the |
18 |
current theory! |
|
5094 | 19 |
|
20 |
Introduction rules have the form |
|
8316
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset
|
21 |
[| ti:M(Sj), ..., P(x), ... |] ==> t: Sk |
5094 | 22 |
where M is some monotone operator (usually the identity) |
23 |
P(x) is any side condition on the free variables |
|
24 |
ti, t are any terms |
|
25 |
Sj, Sk are two of the sets being defined in mutual recursion |
|
26 |
||
6424 | 27 |
Sums are used only for mutual recursion. Products are used only to |
28 |
derive "streamlined" induction rules for relations. |
|
5094 | 29 |
*) |
30 |
||
31 |
signature INDUCTIVE_PACKAGE = |
|
32 |
sig |
|
6424 | 33 |
val quiet_mode: bool ref |
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
34 |
val unify_consts: Sign.sg -> term list -> term list -> term list * term list |
9116
9df44b5c610b
get_inductive now returns None instead of raising an exception.
berghofe
parents:
9072
diff
changeset
|
35 |
val get_inductive: theory -> string -> ({names: string list, coind: bool} * |
9df44b5c610b
get_inductive now returns None instead of raising an exception.
berghofe
parents:
9072
diff
changeset
|
36 |
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm, |
9df44b5c610b
get_inductive now returns None instead of raising an exception.
berghofe
parents:
9072
diff
changeset
|
37 |
intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}) option |
6437 | 38 |
val print_inductives: theory -> unit |
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
39 |
val mono_add_global: theory attribute |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
40 |
val mono_del_global: theory attribute |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
41 |
val get_monos: theory -> thm list |
6424 | 42 |
val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list -> |
6521 | 43 |
theory attribute list -> ((bstring * term) * theory attribute list) list -> |
44 |
thm list -> thm list -> theory -> theory * |
|
6424 | 45 |
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm, |
6437 | 46 |
intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm} |
6521 | 47 |
val add_inductive: bool -> bool -> string list -> Args.src list -> |
48 |
((bstring * string) * Args.src list) list -> (xstring * Args.src list) list -> |
|
49 |
(xstring * Args.src list) list -> theory -> theory * |
|
6424 | 50 |
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm, |
6437 | 51 |
intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm} |
9598 | 52 |
val inductive_cases: ((bstring * Args.src list) * string list) * Comment.text |
7107 | 53 |
-> theory -> theory |
9598 | 54 |
val inductive_cases_i: ((bstring * theory attribute list) * term list) * Comment.text |
7107 | 55 |
-> theory -> theory |
6437 | 56 |
val setup: (theory -> theory) list |
5094 | 57 |
end; |
58 |
||
6424 | 59 |
structure InductivePackage: INDUCTIVE_PACKAGE = |
5094 | 60 |
struct |
61 |
||
9598 | 62 |
|
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
63 |
(*** theory data ***) |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
64 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
65 |
(* data kind 'HOL/inductive' *) |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
66 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
67 |
type inductive_info = |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
68 |
{names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm, |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
69 |
induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}; |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
70 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
71 |
structure InductiveArgs = |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
72 |
struct |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
73 |
val name = "HOL/inductive"; |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
74 |
type T = inductive_info Symtab.table * thm list; |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
75 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
76 |
val empty = (Symtab.empty, []); |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
77 |
val copy = I; |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
78 |
val prep_ext = I; |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
79 |
fun merge ((tab1, monos1), (tab2, monos2)) = (Symtab.merge (K true) (tab1, tab2), |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
80 |
Library.generic_merge Thm.eq_thm I I monos1 monos2); |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
81 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
82 |
fun print sg (tab, monos) = |
8720 | 83 |
[Pretty.strs ("(co)inductives:" :: map #1 (Sign.cond_extern_table sg Sign.constK tab)), |
84 |
Pretty.big_list "monotonicity rules:" (map Display.pretty_thm monos)] |
|
85 |
|> Pretty.chunks |> Pretty.writeln; |
|
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
86 |
end; |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
87 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
88 |
structure InductiveData = TheoryDataFun(InductiveArgs); |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
89 |
val print_inductives = InductiveData.print; |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
90 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
91 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
92 |
(* get and put data *) |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
93 |
|
9116
9df44b5c610b
get_inductive now returns None instead of raising an exception.
berghofe
parents:
9072
diff
changeset
|
94 |
fun get_inductive thy name = Symtab.lookup (fst (InductiveData.get thy), name); |
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
95 |
|
9598 | 96 |
fun the_inductive thy name = |
97 |
(case get_inductive thy name of |
|
98 |
None => error ("Unknown (co)inductive set " ^ quote name) |
|
99 |
| Some info => info); |
|
100 |
||
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
101 |
fun put_inductives names info thy = |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
102 |
let |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
103 |
fun upd ((tab, monos), name) = (Symtab.update_new ((name, info), tab), monos); |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
104 |
val tab_monos = foldl upd (InductiveData.get thy, names) |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
105 |
handle Symtab.DUP name => error ("Duplicate definition of (co)inductive set " ^ quote name); |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
106 |
in InductiveData.put tab_monos thy end; |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
107 |
|
8277 | 108 |
|
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
109 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
110 |
(** monotonicity rules **) |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
111 |
|
8277 | 112 |
val get_monos = snd o InductiveData.get; |
113 |
fun put_monos thms thy = InductiveData.put (fst (InductiveData.get thy), thms) thy; |
|
114 |
||
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
115 |
fun mk_mono thm = |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
116 |
let |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
117 |
fun eq2mono thm' = [standard (thm' RS (thm' RS eq_to_mono))] @ |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
118 |
(case concl_of thm of |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
119 |
(_ $ (_ $ (Const ("Not", _) $ _) $ _)) => [] |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
120 |
| _ => [standard (thm' RS (thm' RS eq_to_mono2))]); |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
121 |
val concl = concl_of thm |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
122 |
in |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
123 |
if Logic.is_equals concl then |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
124 |
eq2mono (thm RS meta_eq_to_obj_eq) |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
125 |
else if can (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl then |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
126 |
eq2mono thm |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
127 |
else [thm] |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
128 |
end; |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
129 |
|
8634 | 130 |
|
131 |
(* attributes *) |
|
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
132 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
133 |
local |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
134 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
135 |
fun map_rules_global f thy = put_monos (f (get_monos thy)) thy; |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
136 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
137 |
fun add_mono thm rules = Library.gen_union Thm.eq_thm (mk_mono thm, rules); |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
138 |
fun del_mono thm rules = Library.gen_rems Thm.eq_thm (rules, mk_mono thm); |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
139 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
140 |
fun mk_att f g (x, thm) = (f (g thm) x, thm); |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
141 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
142 |
in |
8634 | 143 |
val mono_add_global = mk_att map_rules_global add_mono; |
144 |
val mono_del_global = mk_att map_rules_global del_mono; |
|
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
145 |
end; |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
146 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
147 |
val mono_attr = |
8634 | 148 |
(Attrib.add_del_args mono_add_global mono_del_global, |
149 |
Attrib.add_del_args Attrib.undef_local_attribute Attrib.undef_local_attribute); |
|
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
150 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
151 |
|
7107 | 152 |
|
6424 | 153 |
(** utilities **) |
154 |
||
155 |
(* messages *) |
|
156 |
||
5662 | 157 |
val quiet_mode = ref false; |
158 |
fun message s = if !quiet_mode then () else writeln s; |
|
159 |
||
6424 | 160 |
fun coind_prefix true = "co" |
161 |
| coind_prefix false = ""; |
|
162 |
||
163 |
||
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
164 |
(* the following code ensures that each recursive set *) |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
165 |
(* always has the same type in all introduction rules *) |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
166 |
|
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
167 |
fun unify_consts sign cs intr_ts = |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
168 |
(let |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
169 |
val {tsig, ...} = Sign.rep_sg sign; |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
170 |
val add_term_consts_2 = |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
171 |
foldl_aterms (fn (cs, Const c) => c ins cs | (cs, _) => cs); |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
172 |
fun varify (t, (i, ts)) = |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
173 |
let val t' = map_term_types (incr_tvar (i + 1)) (Type.varify (t, [])) |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
174 |
in (maxidx_of_term t', t'::ts) end; |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
175 |
val (i, cs') = foldr varify (cs, (~1, [])); |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
176 |
val (i', intr_ts') = foldr varify (intr_ts, (i, [])); |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
177 |
val rec_consts = foldl add_term_consts_2 ([], cs'); |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
178 |
val intr_consts = foldl add_term_consts_2 ([], intr_ts'); |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
179 |
fun unify (env, (cname, cT)) = |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
180 |
let val consts = map snd (filter (fn c => fst c = cname) intr_consts) |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
181 |
in foldl (fn ((env', j'), Tp) => (Type.unify tsig j' env' Tp)) |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
182 |
(env, (replicate (length consts) cT) ~~ consts) |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
183 |
end; |
8410
5902c02fa122
Type.unify now uses Vartab instead of association lists.
berghofe
parents:
8401
diff
changeset
|
184 |
val (env, _) = foldl unify ((Vartab.empty, i'), rec_consts); |
5902c02fa122
Type.unify now uses Vartab instead of association lists.
berghofe
parents:
8401
diff
changeset
|
185 |
fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars_Vartab env T |
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
186 |
in if T = T' then T else typ_subst_TVars_2 env T' end; |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
187 |
val subst = fst o Type.freeze_thaw o |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
188 |
(map_term_types (typ_subst_TVars_2 env)) |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
189 |
|
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
190 |
in (map subst cs', map subst intr_ts') |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
191 |
end) handle Type.TUNIFY => |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
192 |
(warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts)); |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
193 |
|
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
194 |
|
6424 | 195 |
(* misc *) |
196 |
||
5094 | 197 |
val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (concl_of vimageD); |
198 |
||
6394 | 199 |
val vimage_name = Sign.intern_const (Theory.sign_of Vimage.thy) "op -``"; |
200 |
val mono_name = Sign.intern_const (Theory.sign_of Ord.thy) "mono"; |
|
5094 | 201 |
|
202 |
(* make injections needed in mutually recursive definitions *) |
|
203 |
||
204 |
fun mk_inj cs sumT c x = |
|
205 |
let |
|
206 |
fun mk_inj' T n i = |
|
207 |
if n = 1 then x else |
|
208 |
let val n2 = n div 2; |
|
209 |
val Type (_, [T1, T2]) = T |
|
210 |
in |
|
211 |
if i <= n2 then |
|
212 |
Const ("Inl", T1 --> T) $ (mk_inj' T1 n2 i) |
|
213 |
else |
|
214 |
Const ("Inr", T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2)) |
|
215 |
end |
|
216 |
in mk_inj' sumT (length cs) (1 + find_index_eq c cs) |
|
217 |
end; |
|
218 |
||
219 |
(* make "vimage" terms for selecting out components of mutually rec.def. *) |
|
220 |
||
221 |
fun mk_vimage cs sumT t c = if length cs < 2 then t else |
|
222 |
let |
|
223 |
val cT = HOLogic.dest_setT (fastype_of c); |
|
224 |
val vimageT = [cT --> sumT, HOLogic.mk_setT sumT] ---> HOLogic.mk_setT cT |
|
225 |
in |
|
226 |
Const (vimage_name, vimageT) $ |
|
227 |
Abs ("y", cT, mk_inj cs sumT c (Bound 0)) $ t |
|
228 |
end; |
|
229 |
||
6424 | 230 |
|
231 |
||
232 |
(** well-formedness checks **) |
|
5094 | 233 |
|
234 |
fun err_in_rule sign t msg = error ("Ill-formed introduction rule\n" ^ |
|
235 |
(Sign.string_of_term sign t) ^ "\n" ^ msg); |
|
236 |
||
237 |
fun err_in_prem sign t p msg = error ("Ill-formed premise\n" ^ |
|
238 |
(Sign.string_of_term sign p) ^ "\nin introduction rule\n" ^ |
|
239 |
(Sign.string_of_term sign t) ^ "\n" ^ msg); |
|
240 |
||
241 |
val msg1 = "Conclusion of introduction rule must have form\ |
|
242 |
\ ' t : S_i '"; |
|
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
243 |
val msg2 = "Non-atomic premise"; |
5094 | 244 |
val msg3 = "Recursion term on left of member symbol"; |
245 |
||
246 |
fun check_rule sign cs r = |
|
247 |
let |
|
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
248 |
fun check_prem prem = if can HOLogic.dest_Trueprop prem then () |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
249 |
else err_in_prem sign r prem msg2; |
5094 | 250 |
|
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
251 |
in (case HOLogic.dest_Trueprop (Logic.strip_imp_concl r) of |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
252 |
(Const ("op :", _) $ t $ u) => |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
253 |
if u mem cs then |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
254 |
if exists (Logic.occs o (rpair t)) cs then |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
255 |
err_in_rule sign r msg3 |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
256 |
else |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
257 |
seq check_prem (Logic.strip_imp_prems r) |
5094 | 258 |
else err_in_rule sign r msg1 |
259 |
| _ => err_in_rule sign r msg1) |
|
260 |
end; |
|
261 |
||
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
262 |
fun try' f msg sign t = (case (try f t) of |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
263 |
Some x => x |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
264 |
| None => error (msg ^ Sign.string_of_term sign t)); |
5094 | 265 |
|
6424 | 266 |
|
5094 | 267 |
|
6424 | 268 |
(*** properties of (co)inductive sets ***) |
269 |
||
270 |
(** elimination rules **) |
|
5094 | 271 |
|
8375 | 272 |
fun mk_elims cs cTs params intr_ts intr_names = |
5094 | 273 |
let |
274 |
val used = foldr add_term_names (intr_ts, []); |
|
275 |
val [aname, pname] = variantlist (["a", "P"], used); |
|
276 |
val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT)); |
|
277 |
||
278 |
fun dest_intr r = |
|
279 |
let val Const ("op :", _) $ t $ u = |
|
280 |
HOLogic.dest_Trueprop (Logic.strip_imp_concl r) |
|
281 |
in (u, t, Logic.strip_imp_prems r) end; |
|
282 |
||
8380 | 283 |
val intrs = map dest_intr intr_ts ~~ intr_names; |
5094 | 284 |
|
285 |
fun mk_elim (c, T) = |
|
286 |
let |
|
287 |
val a = Free (aname, T); |
|
288 |
||
289 |
fun mk_elim_prem (_, t, ts) = |
|
290 |
list_all_free (map dest_Free ((foldr add_term_frees (t::ts, [])) \\ params), |
|
291 |
Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P)); |
|
8375 | 292 |
val c_intrs = (filter (equal c o #1 o #1) intrs); |
5094 | 293 |
in |
8375 | 294 |
(Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) :: |
295 |
map mk_elim_prem (map #1 c_intrs), P), map #2 c_intrs) |
|
5094 | 296 |
end |
297 |
in |
|
298 |
map mk_elim (cs ~~ cTs) |
|
299 |
end; |
|
9598 | 300 |
|
6424 | 301 |
|
302 |
||
303 |
(** premises and conclusions of induction rules **) |
|
5094 | 304 |
|
305 |
fun mk_indrule cs cTs params intr_ts = |
|
306 |
let |
|
307 |
val used = foldr add_term_names (intr_ts, []); |
|
308 |
||
309 |
(* predicates for induction rule *) |
|
310 |
||
311 |
val preds = map Free (variantlist (if length cs < 2 then ["P"] else |
|
312 |
map (fn i => "P" ^ string_of_int i) (1 upto length cs), used) ~~ |
|
313 |
map (fn T => T --> HOLogic.boolT) cTs); |
|
314 |
||
315 |
(* transform an introduction rule into a premise for induction rule *) |
|
316 |
||
317 |
fun mk_ind_prem r = |
|
318 |
let |
|
319 |
val frees = map dest_Free ((add_term_frees (r, [])) \\ params); |
|
320 |
||
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
321 |
val pred_of = curry (Library.gen_assoc (op aconv)) (cs ~~ preds); |
5094 | 322 |
|
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
323 |
fun subst (s as ((m as Const ("op :", T)) $ t $ u)) = |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
324 |
(case pred_of u of |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
325 |
None => (m $ fst (subst t) $ fst (subst u), None) |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
326 |
| Some P => (HOLogic.conj $ s $ (P $ t), Some (s, P $ t))) |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
327 |
| subst s = |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
328 |
(case pred_of s of |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
329 |
Some P => (HOLogic.mk_binop "op Int" |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
330 |
(s, HOLogic.Collect_const (HOLogic.dest_setT |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
331 |
(fastype_of s)) $ P), None) |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
332 |
| None => (case s of |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
333 |
(t $ u) => (fst (subst t) $ fst (subst u), None) |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
334 |
| (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), None) |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
335 |
| _ => (s, None))); |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
336 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
337 |
fun mk_prem (s, prems) = (case subst s of |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
338 |
(_, Some (t, u)) => t :: u :: prems |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
339 |
| (t, _) => t :: prems); |
9598 | 340 |
|
5094 | 341 |
val Const ("op :", _) $ t $ u = |
342 |
HOLogic.dest_Trueprop (Logic.strip_imp_concl r) |
|
343 |
||
344 |
in list_all_free (frees, |
|
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
345 |
Logic.list_implies (map HOLogic.mk_Trueprop (foldr mk_prem |
5094 | 346 |
(map HOLogic.dest_Trueprop (Logic.strip_imp_prems r), [])), |
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
347 |
HOLogic.mk_Trueprop (the (pred_of u) $ t))) |
5094 | 348 |
end; |
349 |
||
350 |
val ind_prems = map mk_ind_prem intr_ts; |
|
351 |
||
352 |
(* make conclusions for induction rules *) |
|
353 |
||
354 |
fun mk_ind_concl ((c, P), (ts, x)) = |
|
355 |
let val T = HOLogic.dest_setT (fastype_of c); |
|
356 |
val Ts = HOLogic.prodT_factors T; |
|
357 |
val (frees, x') = foldr (fn (T', (fs, s)) => |
|
358 |
((Free (s, T'))::fs, bump_string s)) (Ts, ([], x)); |
|
359 |
val tuple = HOLogic.mk_tuple T frees; |
|
360 |
in ((HOLogic.mk_binop "op -->" |
|
361 |
(HOLogic.mk_mem (tuple, c), P $ tuple))::ts, x') |
|
362 |
end; |
|
363 |
||
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
364 |
val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
5094 | 365 |
(fst (foldr mk_ind_concl (cs ~~ preds, ([], "xa"))))) |
366 |
||
367 |
in (preds, ind_prems, mutual_ind_concl) |
|
368 |
end; |
|
369 |
||
6424 | 370 |
|
5094 | 371 |
|
8316
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset
|
372 |
(** prepare cases and induct rules **) |
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset
|
373 |
|
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset
|
374 |
(* |
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset
|
375 |
transform mutual rule: |
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset
|
376 |
HH ==> (x1:A1 --> P1 x1) & ... & (xn:An --> Pn xn) |
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset
|
377 |
into i-th projection: |
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset
|
378 |
xi:Ai ==> HH ==> Pi xi |
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset
|
379 |
*) |
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset
|
380 |
|
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset
|
381 |
fun project_rules [name] rule = [(name, rule)] |
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset
|
382 |
| project_rules names mutual_rule = |
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset
|
383 |
let |
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset
|
384 |
val n = length names; |
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset
|
385 |
fun proj i = |
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset
|
386 |
(if i < n then (fn th => th RS conjunct1) else I) |
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset
|
387 |
(Library.funpow (i - 1) (fn th => th RS conjunct2) mutual_rule) |
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset
|
388 |
RS mp |> Thm.permute_prems 0 ~1 |> Drule.standard; |
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset
|
389 |
in names ~~ map proj (1 upto n) end; |
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset
|
390 |
|
8375 | 391 |
fun add_cases_induct no_elim no_ind names elims induct induct_cases = |
8316
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset
|
392 |
let |
9405 | 393 |
fun cases_spec (name, elim) thy = |
394 |
thy |
|
395 |
|> Theory.add_path (Sign.base_name name) |
|
396 |
|> (#1 o PureThy.add_thms [(("cases", elim), [InductMethod.cases_set_global name])]) |
|
397 |
|> Theory.parent_path; |
|
8375 | 398 |
val cases_specs = if no_elim then [] else map2 cases_spec (names, elims); |
8316
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset
|
399 |
|
9405 | 400 |
fun induct_spec (name, th) = (#1 o PureThy.add_thms |
401 |
[(("", th), [RuleCases.case_names induct_cases, InductMethod.induct_set_global name])]); |
|
8401 | 402 |
val induct_specs = if no_ind then [] else map induct_spec (project_rules names induct); |
9405 | 403 |
in Library.apply (cases_specs @ induct_specs) end; |
8316
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset
|
404 |
|
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset
|
405 |
|
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset
|
406 |
|
6424 | 407 |
(*** proofs for (co)inductive sets ***) |
408 |
||
409 |
(** prove monotonicity **) |
|
5094 | 410 |
|
411 |
fun prove_mono setT fp_fun monos thy = |
|
412 |
let |
|
6427 | 413 |
val _ = message " Proving monotonicity ..."; |
5094 | 414 |
|
6394 | 415 |
val mono = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop |
5094 | 416 |
(Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun))) |
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
417 |
(fn _ => [rtac monoI 1, REPEAT (ares_tac (get_monos thy @ flat (map mk_mono monos)) 1)]) |
5094 | 418 |
|
419 |
in mono end; |
|
420 |
||
6424 | 421 |
|
422 |
||
423 |
(** prove introduction rules **) |
|
5094 | 424 |
|
425 |
fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy = |
|
426 |
let |
|
6427 | 427 |
val _ = message " Proving the introduction rules ..."; |
5094 | 428 |
|
429 |
val unfold = standard (mono RS (fp_def RS |
|
430 |
(if coind then def_gfp_Tarski else def_lfp_Tarski))); |
|
431 |
||
432 |
fun select_disj 1 1 = [] |
|
433 |
| select_disj _ 1 = [rtac disjI1] |
|
434 |
| select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1)); |
|
435 |
||
436 |
val intrs = map (fn (i, intr) => prove_goalw_cterm rec_sets_defs |
|
6394 | 437 |
(cterm_of (Theory.sign_of thy) intr) (fn prems => |
5094 | 438 |
[(*insert prems and underlying sets*) |
439 |
cut_facts_tac prems 1, |
|
440 |
stac unfold 1, |
|
441 |
REPEAT (resolve_tac [vimageI2, CollectI] 1), |
|
442 |
(*Now 1-2 subgoals: the disjunction, perhaps equality.*) |
|
443 |
EVERY1 (select_disj (length intr_ts) i), |
|
444 |
(*Not ares_tac, since refl must be tried before any equality assumptions; |
|
445 |
backtracking may occur if the premises have extra variables!*) |
|
446 |
DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 1 APPEND assume_tac 1), |
|
447 |
(*Now solve the equations like Inl 0 = Inl ?b2*) |
|
448 |
rewrite_goals_tac con_defs, |
|
449 |
REPEAT (rtac refl 1)])) (1 upto (length intr_ts) ~~ intr_ts) |
|
450 |
||
451 |
in (intrs, unfold) end; |
|
452 |
||
6424 | 453 |
|
454 |
||
455 |
(** prove elimination rules **) |
|
5094 | 456 |
|
8375 | 457 |
fun prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy = |
5094 | 458 |
let |
6427 | 459 |
val _ = message " Proving the elimination rules ..."; |
5094 | 460 |
|
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
461 |
val rules1 = [CollectE, disjE, make_elim vimageD, exE]; |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
462 |
val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ |
5094 | 463 |
map make_elim [Inl_inject, Inr_inject]; |
8375 | 464 |
in |
465 |
map (fn (t, cases) => prove_goalw_cterm rec_sets_defs |
|
6394 | 466 |
(cterm_of (Theory.sign_of thy) t) (fn prems => |
5094 | 467 |
[cut_facts_tac [hd prems] 1, |
468 |
dtac (unfold RS subst) 1, |
|
469 |
REPEAT (FIRSTGOAL (eresolve_tac rules1)), |
|
470 |
REPEAT (FIRSTGOAL (eresolve_tac rules2)), |
|
471 |
EVERY (map (fn prem => |
|
8375 | 472 |
DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))]) |
473 |
|> RuleCases.name cases) |
|
474 |
(mk_elims cs cTs params intr_ts intr_names) |
|
475 |
end; |
|
5094 | 476 |
|
6424 | 477 |
|
5094 | 478 |
(** derivation of simplified elimination rules **) |
479 |
||
480 |
(*Applies freeness of the given constructors, which *must* be unfolded by |
|
9598 | 481 |
the given defs. Cannot simply use the local con_defs because con_defs=[] |
5094 | 482 |
for inference systems. |
483 |
*) |
|
484 |
||
7107 | 485 |
(*cprop should have the form t:Si where Si is an inductive set*) |
9598 | 486 |
|
487 |
val mk_cases_err = "mk_cases: proposition not of form 't : S_i'"; |
|
488 |
||
489 |
fun mk_cases_i elims ss cprop = |
|
7107 | 490 |
let |
491 |
val prem = Thm.assume cprop; |
|
9598 | 492 |
val tac = ALLGOALS (InductMethod.simp_case_tac false ss) THEN prune_params_tac; |
9298 | 493 |
fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic tac (prem RS rl)); |
7107 | 494 |
in |
495 |
(case get_first (try mk_elim) elims of |
|
496 |
Some r => r |
|
497 |
| None => error (Pretty.string_of (Pretty.block |
|
9598 | 498 |
[Pretty.str mk_cases_err, Pretty.fbrk, Display.pretty_cterm cprop]))) |
7107 | 499 |
end; |
500 |
||
6141 | 501 |
fun mk_cases elims s = |
9598 | 502 |
mk_cases_i elims (simpset()) (Thm.read_cterm (Thm.sign_of_thm (hd elims)) (s, propT)); |
503 |
||
504 |
fun smart_mk_cases thy ss cprop = |
|
505 |
let |
|
506 |
val c = #1 (Term.dest_Const (Term.head_of (#2 (HOLogic.dest_mem (HOLogic.dest_Trueprop |
|
507 |
(Logic.strip_imp_concl (Thm.term_of cprop))))))) handle TERM _ => error mk_cases_err; |
|
508 |
val (_, {elims, ...}) = the_inductive thy c; |
|
509 |
in mk_cases_i elims ss cprop end; |
|
7107 | 510 |
|
511 |
||
512 |
(* inductive_cases(_i) *) |
|
513 |
||
514 |
fun gen_inductive_cases prep_att prep_const prep_prop |
|
9598 | 515 |
(((name, raw_atts), raw_props), comment) thy = |
516 |
let |
|
517 |
val ss = Simplifier.simpset_of thy; |
|
518 |
val sign = Theory.sign_of thy; |
|
519 |
val cprops = map (Thm.cterm_of sign o prep_prop (ProofContext.init thy)) raw_props; |
|
520 |
val atts = map (prep_att thy) raw_atts; |
|
521 |
val thms = map (smart_mk_cases thy ss) cprops; |
|
522 |
in thy |> IsarThy.have_theorems_i [(((name, atts), map Thm.no_attributes thms), comment)] end; |
|
5094 | 523 |
|
7107 | 524 |
val inductive_cases = |
525 |
gen_inductive_cases Attrib.global_attribute Sign.intern_const ProofContext.read_prop; |
|
526 |
||
527 |
val inductive_cases_i = gen_inductive_cases (K I) (K I) ProofContext.cert_prop; |
|
528 |
||
6424 | 529 |
|
9598 | 530 |
(* mk_cases_meth *) |
531 |
||
532 |
fun mk_cases_meth (ctxt, raw_props) = |
|
533 |
let |
|
534 |
val thy = ProofContext.theory_of ctxt; |
|
535 |
val ss = Simplifier.get_local_simpset ctxt; |
|
536 |
val cprops = map (Thm.cterm_of (Theory.sign_of thy) o ProofContext.read_prop ctxt) raw_props; |
|
537 |
in Method.erule (map (smart_mk_cases thy ss) cprops) end; |
|
538 |
||
539 |
val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name)); |
|
540 |
||
541 |
||
6424 | 542 |
|
543 |
(** prove induction rule **) |
|
5094 | 544 |
|
545 |
fun prove_indrule cs cTs sumT rec_const params intr_ts mono |
|
546 |
fp_def rec_sets_defs thy = |
|
547 |
let |
|
6427 | 548 |
val _ = message " Proving the induction rule ..."; |
5094 | 549 |
|
6394 | 550 |
val sign = Theory.sign_of thy; |
5094 | 551 |
|
7293 | 552 |
val sum_case_rewrites = (case ThyInfo.lookup_theory "Datatype" of |
553 |
None => [] |
|
554 |
| Some thy' => map mk_meta_eq (PureThy.get_thms thy' "sum.cases")); |
|
555 |
||
5094 | 556 |
val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts; |
557 |
||
558 |
(* make predicate for instantiation of abstract induction rule *) |
|
559 |
||
560 |
fun mk_ind_pred _ [P] = P |
|
561 |
| mk_ind_pred T Ps = |
|
562 |
let val n = (length Ps) div 2; |
|
563 |
val Type (_, [T1, T2]) = T |
|
7293 | 564 |
in Const ("Datatype.sum.sum_case", |
5094 | 565 |
[T1 --> HOLogic.boolT, T2 --> HOLogic.boolT, T] ---> HOLogic.boolT) $ |
566 |
mk_ind_pred T1 (take (n, Ps)) $ mk_ind_pred T2 (drop (n, Ps)) |
|
567 |
end; |
|
568 |
||
569 |
val ind_pred = mk_ind_pred sumT preds; |
|
570 |
||
571 |
val ind_concl = HOLogic.mk_Trueprop |
|
572 |
(HOLogic.all_const sumT $ Abs ("x", sumT, HOLogic.mk_binop "op -->" |
|
573 |
(HOLogic.mk_mem (Bound 0, rec_const), ind_pred $ Bound 0))); |
|
574 |
||
575 |
(* simplification rules for vimage and Collect *) |
|
576 |
||
577 |
val vimage_simps = if length cs < 2 then [] else |
|
578 |
map (fn c => prove_goalw_cterm [] (cterm_of sign |
|
579 |
(HOLogic.mk_Trueprop (HOLogic.mk_eq |
|
580 |
(mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c, |
|
581 |
HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $ |
|
582 |
nth_elem (find_index_eq c cs, preds))))) |
|
7293 | 583 |
(fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, |
5094 | 584 |
rtac refl 1])) cs; |
585 |
||
586 |
val induct = prove_goalw_cterm [] (cterm_of sign |
|
587 |
(Logic.list_implies (ind_prems, ind_concl))) (fn prems => |
|
588 |
[rtac (impI RS allI) 1, |
|
589 |
DETERM (etac (mono RS (fp_def RS def_induct)) 1), |
|
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
590 |
rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)), |
5094 | 591 |
fold_goals_tac rec_sets_defs, |
592 |
(*This CollectE and disjE separates out the introduction rules*) |
|
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
593 |
REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE, exE])), |
5094 | 594 |
(*Now break down the individual cases. No disjE here in case |
595 |
some premise involves disjunction.*) |
|
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
596 |
REPEAT (FIRSTGOAL (etac conjE ORELSE' hyp_subst_tac)), |
7293 | 597 |
rewrite_goals_tac sum_case_rewrites, |
5094 | 598 |
EVERY (map (fn prem => |
5149 | 599 |
DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]); |
5094 | 600 |
|
601 |
val lemma = prove_goalw_cterm rec_sets_defs (cterm_of sign |
|
602 |
(Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems => |
|
603 |
[cut_facts_tac prems 1, |
|
604 |
REPEAT (EVERY |
|
605 |
[REPEAT (resolve_tac [conjI, impI] 1), |
|
606 |
TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1, |
|
7293 | 607 |
rewrite_goals_tac sum_case_rewrites, |
5094 | 608 |
atac 1])]) |
609 |
||
610 |
in standard (split_rule (induct RS lemma)) |
|
611 |
end; |
|
612 |
||
6424 | 613 |
|
614 |
||
615 |
(*** specification of (co)inductive sets ****) |
|
616 |
||
617 |
(** definitional introduction of (co)inductive sets **) |
|
5094 | 618 |
|
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset
|
619 |
fun mk_ind_def declare_consts alt_name coind cs intr_ts monos con_defs thy |
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset
|
620 |
params paramTs cTs cnames = |
5094 | 621 |
let |
622 |
val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs; |
|
623 |
val setT = HOLogic.mk_setT sumT; |
|
624 |
||
6394 | 625 |
val fp_name = if coind then Sign.intern_const (Theory.sign_of Gfp.thy) "gfp" |
626 |
else Sign.intern_const (Theory.sign_of Lfp.thy) "lfp"; |
|
5094 | 627 |
|
5149 | 628 |
val used = foldr add_term_names (intr_ts, []); |
629 |
val [sname, xname] = variantlist (["S", "x"], used); |
|
630 |
||
5094 | 631 |
(* transform an introduction rule into a conjunction *) |
632 |
(* [| t : ... S_i ... ; ... |] ==> u : S_j *) |
|
633 |
(* is transformed into *) |
|
634 |
(* x = Inj_j u & t : ... Inj_i -`` S ... & ... *) |
|
635 |
||
636 |
fun transform_rule r = |
|
637 |
let |
|
638 |
val frees = map dest_Free ((add_term_frees (r, [])) \\ params); |
|
5149 | 639 |
val subst = subst_free |
640 |
(cs ~~ (map (mk_vimage cs sumT (Free (sname, setT))) cs)); |
|
5094 | 641 |
val Const ("op :", _) $ t $ u = |
642 |
HOLogic.dest_Trueprop (Logic.strip_imp_concl r) |
|
643 |
||
644 |
in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P)) |
|
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
645 |
(frees, foldr1 HOLogic.mk_conj |
5149 | 646 |
(((HOLogic.eq_const sumT) $ Free (xname, sumT) $ (mk_inj cs sumT u t)):: |
5094 | 647 |
(map (subst o HOLogic.dest_Trueprop) |
648 |
(Logic.strip_imp_prems r)))) |
|
649 |
end |
|
650 |
||
651 |
(* make a disjunction of all introduction rules *) |
|
652 |
||
5149 | 653 |
val fp_fun = absfree (sname, setT, (HOLogic.Collect_const sumT) $ |
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
654 |
absfree (xname, sumT, foldr1 HOLogic.mk_disj (map transform_rule intr_ts))); |
5094 | 655 |
|
656 |
(* add definiton of recursive sets to theory *) |
|
657 |
||
658 |
val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name; |
|
6394 | 659 |
val full_rec_name = Sign.full_name (Theory.sign_of thy) rec_name; |
5094 | 660 |
|
661 |
val rec_const = list_comb |
|
662 |
(Const (full_rec_name, paramTs ---> setT), params); |
|
663 |
||
664 |
val fp_def_term = Logic.mk_equals (rec_const, |
|
665 |
Const (fp_name, (setT --> setT) --> setT) $ fp_fun) |
|
666 |
||
667 |
val def_terms = fp_def_term :: (if length cs < 2 then [] else |
|
668 |
map (fn c => Logic.mk_equals (c, mk_vimage cs sumT rec_const c)) cs); |
|
669 |
||
8433 | 670 |
val (thy', [fp_def :: rec_sets_defs]) = |
671 |
thy |
|
672 |
|> (if declare_consts then |
|
673 |
Theory.add_consts_i (map (fn (c, n) => |
|
674 |
(n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames)) |
|
675 |
else I) |
|
676 |
|> (if length cs < 2 then I |
|
677 |
else Theory.add_consts_i [(rec_name, paramTs ---> setT, NoSyn)]) |
|
678 |
|> Theory.add_path rec_name |
|
9315 | 679 |
|> PureThy.add_defss_i false [(("defs", def_terms), [])]; |
5094 | 680 |
|
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset
|
681 |
val mono = prove_mono setT fp_fun monos thy' |
5094 | 682 |
|
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset
|
683 |
in |
9598 | 684 |
(thy', mono, fp_def, rec_sets_defs, rec_const, sumT) |
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset
|
685 |
end; |
5094 | 686 |
|
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset
|
687 |
fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs |
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset
|
688 |
atts intros monos con_defs thy params paramTs cTs cnames induct_cases = |
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset
|
689 |
let |
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset
|
690 |
val _ = if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^ |
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset
|
691 |
commas_quote cnames) else (); |
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset
|
692 |
|
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset
|
693 |
val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros); |
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset
|
694 |
|
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset
|
695 |
val (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) = |
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset
|
696 |
mk_ind_def declare_consts alt_name coind cs intr_ts monos con_defs thy |
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset
|
697 |
params paramTs cTs cnames; |
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset
|
698 |
|
5094 | 699 |
val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts con_defs |
700 |
rec_sets_defs thy'; |
|
701 |
val elims = if no_elim then [] else |
|
8375 | 702 |
prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy'; |
8312
b470bc28b59d
add_cases_induct: accomodate no_elim and no_ind flags;
wenzelm
parents:
8307
diff
changeset
|
703 |
val raw_induct = if no_ind then Drule.asm_rl else |
5094 | 704 |
if coind then standard (rule_by_tactic |
5553 | 705 |
(rewrite_tac [mk_meta_eq vimage_Un] THEN |
5094 | 706 |
fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct))) |
707 |
else |
|
708 |
prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def |
|
709 |
rec_sets_defs thy'; |
|
5108 | 710 |
val induct = if coind orelse no_ind orelse length cs > 1 then raw_induct |
5094 | 711 |
else standard (raw_induct RSN (2, rev_mp)); |
712 |
||
8433 | 713 |
val (thy'', [intrs']) = |
714 |
thy' |
|
9598 | 715 |
|> PureThy.add_thmss [(("intros", intrs), atts)] |
8433 | 716 |
|>> (#1 o PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts)) |
717 |
|>> (if no_elim then I else #1 o PureThy.add_thmss [(("elims", elims), [])]) |
|
718 |
|>> (if no_ind then I else #1 o PureThy.add_thms |
|
8401 | 719 |
[((coind_prefix coind ^ "induct", induct), [RuleCases.case_names induct_cases])]) |
8433 | 720 |
|>> Theory.parent_path; |
8312
b470bc28b59d
add_cases_induct: accomodate no_elim and no_ind flags;
wenzelm
parents:
8307
diff
changeset
|
721 |
val elims' = if no_elim then elims else PureThy.get_thms thy'' "elims"; (* FIXME improve *) |
b470bc28b59d
add_cases_induct: accomodate no_elim and no_ind flags;
wenzelm
parents:
8307
diff
changeset
|
722 |
val induct' = if no_ind then induct else PureThy.get_thm thy'' (coind_prefix coind ^ "induct"); (* FIXME improve *) |
5094 | 723 |
in (thy'', |
724 |
{defs = fp_def::rec_sets_defs, |
|
725 |
mono = mono, |
|
726 |
unfold = unfold, |
|
7798
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7710
diff
changeset
|
727 |
intrs = intrs', |
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7710
diff
changeset
|
728 |
elims = elims', |
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7710
diff
changeset
|
729 |
mk_cases = mk_cases elims', |
5094 | 730 |
raw_induct = raw_induct, |
7798
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7710
diff
changeset
|
731 |
induct = induct'}) |
5094 | 732 |
end; |
733 |
||
6424 | 734 |
|
735 |
||
736 |
(** axiomatic introduction of (co)inductive sets **) |
|
5094 | 737 |
|
738 |
fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs |
|
8401 | 739 |
atts intros monos con_defs thy params paramTs cTs cnames induct_cases = |
5094 | 740 |
let |
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset
|
741 |
val _ = message (coind_prefix coind ^ "inductive set(s) " ^ commas_quote cnames); |
5094 | 742 |
|
6424 | 743 |
val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros); |
9235 | 744 |
val (thy', _, fp_def, rec_sets_defs, _, _) = |
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset
|
745 |
mk_ind_def declare_consts alt_name coind cs intr_ts monos con_defs thy |
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset
|
746 |
params paramTs cTs cnames; |
8375 | 747 |
val (elim_ts, elim_cases) = Library.split_list (mk_elims cs cTs params intr_ts intr_names); |
5094 | 748 |
val (_, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts; |
749 |
val ind_t = Logic.list_implies (ind_prems, mutual_ind_concl); |
|
9598 | 750 |
|
751 |
val (thy'', [intrs, raw_elims]) = |
|
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset
|
752 |
thy' |
9598 | 753 |
|> PureThy.add_axiomss_i [(("intros", intr_ts), atts), (("raw_elims", elim_ts), [])] |
754 |
|>> (if coind then I else |
|
8433 | 755 |
#1 o PureThy.add_axioms_i [(("raw_induct", ind_t), [apsnd (standard o split_rule)])]); |
5094 | 756 |
|
9598 | 757 |
val elims = map2 (fn (th, cases) => RuleCases.name cases th) (raw_elims, elim_cases); |
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset
|
758 |
val raw_induct = if coind then Drule.asm_rl else PureThy.get_thm thy'' "raw_induct"; |
5094 | 759 |
val induct = if coind orelse length cs > 1 then raw_induct |
760 |
else standard (raw_induct RSN (2, rev_mp)); |
|
761 |
||
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset
|
762 |
val (thy''', ([elims'], intrs')) = |
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset
|
763 |
thy'' |
8375 | 764 |
|> PureThy.add_thmss [(("elims", elims), [])] |
8433 | 765 |
|>> (if coind then I |
766 |
else #1 o PureThy.add_thms [(("induct", induct), [RuleCases.case_names induct_cases])]) |
|
767 |
|>>> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts) |
|
768 |
|>> Theory.parent_path; |
|
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset
|
769 |
val induct' = if coind then raw_induct else PureThy.get_thm thy''' "induct"; |
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset
|
770 |
in (thy''', |
9235 | 771 |
{defs = fp_def :: rec_sets_defs, |
8312
b470bc28b59d
add_cases_induct: accomodate no_elim and no_ind flags;
wenzelm
parents:
8307
diff
changeset
|
772 |
mono = Drule.asm_rl, |
b470bc28b59d
add_cases_induct: accomodate no_elim and no_ind flags;
wenzelm
parents:
8307
diff
changeset
|
773 |
unfold = Drule.asm_rl, |
8433 | 774 |
intrs = intrs', |
775 |
elims = elims', |
|
776 |
mk_cases = mk_cases elims', |
|
5094 | 777 |
raw_induct = raw_induct, |
7798
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7710
diff
changeset
|
778 |
induct = induct'}) |
5094 | 779 |
end; |
780 |
||
6424 | 781 |
|
782 |
||
783 |
(** introduction of (co)inductive sets **) |
|
5094 | 784 |
|
785 |
fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs |
|
6521 | 786 |
atts intros monos con_defs thy = |
5094 | 787 |
let |
6424 | 788 |
val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions"); |
6394 | 789 |
val sign = Theory.sign_of thy; |
5094 | 790 |
|
791 |
(*parameters should agree for all mutually recursive components*) |
|
792 |
val (_, params) = strip_comb (hd cs); |
|
793 |
val paramTs = map (try' (snd o dest_Free) "Parameter in recursive\ |
|
794 |
\ component is not a free variable: " sign) params; |
|
795 |
||
796 |
val cTs = map (try' (HOLogic.dest_setT o fastype_of) |
|
797 |
"Recursive component not of type set: " sign) cs; |
|
798 |
||
6437 | 799 |
val full_cnames = map (try' (fst o dest_Const o head_of) |
5094 | 800 |
"Recursive set not previously declared as constant: " sign) cs; |
6437 | 801 |
val cnames = map Sign.base_name full_cnames; |
5094 | 802 |
|
6424 | 803 |
val _ = seq (check_rule sign cs o snd o fst) intros; |
8401 | 804 |
val induct_cases = map (#1 o #1) intros; |
6437 | 805 |
|
9405 | 806 |
val (thy1, result as {elims, induct, ...}) = |
6437 | 807 |
(if ! quick_and_dirty then add_ind_axm else add_ind_def) |
6521 | 808 |
verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos |
8401 | 809 |
con_defs thy params paramTs cTs cnames induct_cases; |
8307 | 810 |
val thy2 = thy1 |
811 |
|> put_inductives full_cnames ({names = full_cnames, coind = coind}, result) |
|
9405 | 812 |
|> add_cases_induct no_elim (no_ind orelse coind) full_cnames elims induct induct_cases; |
6437 | 813 |
in (thy2, result) end; |
5094 | 814 |
|
6424 | 815 |
|
5094 | 816 |
|
6424 | 817 |
(** external interface **) |
818 |
||
6521 | 819 |
fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy = |
5094 | 820 |
let |
6394 | 821 |
val sign = Theory.sign_of thy; |
8100 | 822 |
val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termT) c_strings; |
6424 | 823 |
|
6521 | 824 |
val atts = map (Attrib.global_attribute thy) srcs; |
6424 | 825 |
val intr_names = map (fst o fst) intro_srcs; |
9405 | 826 |
fun read_rule s = Thm.read_cterm sign (s, propT) |
827 |
handle ERROR => error ("The error(s) above occurred for " ^ s); |
|
828 |
val intr_ts = map (Thm.term_of o read_rule o snd o fst) intro_srcs; |
|
6424 | 829 |
val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs; |
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
830 |
val (cs', intr_ts') = unify_consts sign cs intr_ts; |
5094 | 831 |
|
6424 | 832 |
val ((thy', con_defs), monos) = thy |
833 |
|> IsarThy.apply_theorems raw_monos |
|
834 |
|> apfst (IsarThy.apply_theorems raw_con_defs); |
|
835 |
in |
|
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
836 |
add_inductive_i verbose false "" coind false false cs' |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
837 |
atts ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy' |
5094 | 838 |
end; |
839 |
||
6424 | 840 |
|
841 |
||
6437 | 842 |
(** package setup **) |
843 |
||
844 |
(* setup theory *) |
|
845 |
||
8634 | 846 |
val setup = |
847 |
[InductiveData.init, |
|
9625 | 848 |
Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args, |
9598 | 849 |
"dynamic case analysis on sets")], |
8634 | 850 |
Attrib.add_attributes [("mono", mono_attr, "monotonicity rule")]]; |
6437 | 851 |
|
852 |
||
853 |
(* outer syntax *) |
|
6424 | 854 |
|
6723 | 855 |
local structure P = OuterParse and K = OuterSyntax.Keyword in |
6424 | 856 |
|
6521 | 857 |
fun mk_ind coind (((sets, (atts, intrs)), monos), con_defs) = |
6723 | 858 |
#1 o add_inductive true coind sets atts (map P.triple_swap intrs) monos con_defs; |
6424 | 859 |
|
860 |
fun ind_decl coind = |
|
6729 | 861 |
(Scan.repeat1 P.term --| P.marg_comment) -- |
9598 | 862 |
(P.$$$ "intros" |-- |
7152 | 863 |
P.!!! (P.opt_attribs -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) -- |
6729 | 864 |
Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] -- |
865 |
Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1 --| P.marg_comment) [] |
|
6424 | 866 |
>> (Toplevel.theory o mk_ind coind); |
867 |
||
6723 | 868 |
val inductiveP = |
869 |
OuterSyntax.command "inductive" "define inductive sets" K.thy_decl (ind_decl false); |
|
870 |
||
871 |
val coinductiveP = |
|
872 |
OuterSyntax.command "coinductive" "define coinductive sets" K.thy_decl (ind_decl true); |
|
6424 | 873 |
|
7107 | 874 |
|
875 |
val ind_cases = |
|
9625 | 876 |
P.opt_thm_name ":" -- Scan.repeat1 P.prop -- P.marg_comment |
7107 | 877 |
>> (Toplevel.theory o inductive_cases); |
878 |
||
879 |
val inductive_casesP = |
|
9598 | 880 |
OuterSyntax.improper_command "inductive_cases" |
881 |
"create simplified instances of elimination rules (improper)" K.thy_script ind_cases; |
|
7107 | 882 |
|
9643 | 883 |
val _ = OuterSyntax.add_keywords ["intros", "monos", "con_defs"]; |
7107 | 884 |
val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP]; |
6424 | 885 |
|
5094 | 886 |
end; |
6424 | 887 |
|
888 |
||
889 |
end; |