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