author | haftmann |
Wed, 07 Oct 2009 14:01:26 +0200 | |
changeset 32887 | 85e7ab9020ba |
parent 31775 | 2b04504fcb69 |
child 33099 | b8cdd3d73022 |
permissions | -rw-r--r-- |
31775 | 1 |
(* Title: HOL/Tools/Function/inductive_wrap.ML |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
2 |
Author: Alexander Krauss, TU Muenchen |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
3 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
4 |
|
21237 | 5 |
A wrapper around the inductive package, restoring the quantifiers in |
6 |
the introduction and elimination rules. |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
7 |
*) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
8 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
9 |
signature FUNDEF_INDUCTIVE_WRAP = |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
10 |
sig |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
11 |
val inductive_def : term list |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
12 |
-> ((bstring * typ) * mixfix) * local_theory |
22166 | 13 |
-> thm list * (term * thm * thm * local_theory) |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
14 |
end |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
15 |
|
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
26535
diff
changeset
|
16 |
structure FundefInductiveWrap: FUNDEF_INDUCTIVE_WRAP = |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
17 |
struct |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
18 |
|
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
21025
diff
changeset
|
19 |
open FundefLib |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
20 |
|
22619 | 21 |
fun requantify ctxt lfix orig_def thm = |
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
21025
diff
changeset
|
22 |
let |
22619 | 23 |
val (qs, t) = dest_all_all orig_def |
21105 | 24 |
val thy = theory_of_thm thm |
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
21025
diff
changeset
|
25 |
val frees = frees_in_term ctxt t |
21237 | 26 |
|> remove (op =) lfix |
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
21025
diff
changeset
|
27 |
val vars = Term.add_vars (prop_of thm) [] |> rev |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
21025
diff
changeset
|
28 |
|
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
21025
diff
changeset
|
29 |
val varmap = frees ~~ vars |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
30 |
in |
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
21025
diff
changeset
|
31 |
fold_rev (fn Free (n, T) => |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
21025
diff
changeset
|
32 |
forall_intr_rename (n, cterm_of thy (Var (the_default (("",0), T) (AList.lookup (op =) varmap (n, T)))))) |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
21025
diff
changeset
|
33 |
qs |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
21025
diff
changeset
|
34 |
thm |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
21025
diff
changeset
|
35 |
end |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
21025
diff
changeset
|
36 |
|
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
21025
diff
changeset
|
37 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
38 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
39 |
fun inductive_def defs (((R, T), mixfix), lthy) = |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
40 |
let |
22166 | 41 |
val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) = |
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
29389
diff
changeset
|
42 |
Inductive.add_inductive_i |
26475
3cc1e48d0ce1
eliminated quiet_mode ref of some packages (avoid CRITICAL setmp!);
wenzelm
parents:
26129
diff
changeset
|
43 |
{quiet_mode = false, |
3cc1e48d0ce1
eliminated quiet_mode ref of some packages (avoid CRITICAL setmp!);
wenzelm
parents:
26129
diff
changeset
|
44 |
verbose = ! Toplevel.debug, |
24822 | 45 |
kind = Thm.internalK, |
28965 | 46 |
alt_name = Binding.empty, |
24816 | 47 |
coind = false, |
48 |
no_elim = false, |
|
26535
66bca8a4079c
Added skip_mono flag to inductive definition package.
berghofe
parents:
26475
diff
changeset
|
49 |
no_ind = false, |
29389 | 50 |
skip_mono = true, |
51 |
fork_mono = false} |
|
28965 | 52 |
[((Binding.name R, T), NoSyn)] (* the relation *) |
24816 | 53 |
[] (* no parameters *) |
28965 | 54 |
(map (fn t => (Attrib.empty_binding, t)) defs) (* the intros *) |
24816 | 55 |
[] (* no special monos *) |
56 |
lthy |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
57 |
|
22619 | 58 |
val intrs = map2 (requantify lthy (R, T)) defs intrs_gen |
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
21025
diff
changeset
|
59 |
|
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
21025
diff
changeset
|
60 |
val elim = elim_gen |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
21025
diff
changeset
|
61 |
|> forall_intr_vars (* FIXME... *) |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
62 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
63 |
in |
22612 | 64 |
(intrs, (Rdef, elim, induct, lthy)) |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
65 |
end |
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
21025
diff
changeset
|
66 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
67 |
end |