author | wenzelm |
Tue, 02 Oct 2007 22:23:28 +0200 | |
changeset 24816 | 2d0fa8f31804 |
parent 24746 | 6d42be359d57 |
child 24822 | b854842e0b8d |
permissions | -rw-r--r-- |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/function_package/inductive_wrap.ML |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
2 |
ID: $Id$ |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
3 |
Author: Alexander Krauss, TU Muenchen |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
4 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
5 |
|
21237 | 6 |
A wrapper around the inductive package, restoring the quantifiers in |
7 |
the introduction and elimination rules. |
|
20523
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 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
10 |
signature FUNDEF_INDUCTIVE_WRAP = |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
11 |
sig |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
12 |
val inductive_def : term list |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
13 |
-> ((bstring * typ) * mixfix) * local_theory |
22166 | 14 |
-> 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
|
15 |
end |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
16 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
17 |
structure FundefInductiveWrap = |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
18 |
struct |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
19 |
|
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
21025
diff
changeset
|
20 |
open FundefLib |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
21 |
|
22619 | 22 |
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
|
23 |
let |
22619 | 24 |
val (qs, t) = dest_all_all orig_def |
21105 | 25 |
val thy = theory_of_thm thm |
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
21025
diff
changeset
|
26 |
val frees = frees_in_term ctxt t |
21237 | 27 |
|> remove (op =) lfix |
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
21025
diff
changeset
|
28 |
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
|
29 |
|
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
21025
diff
changeset
|
30 |
val varmap = frees ~~ vars |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
31 |
in |
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
21025
diff
changeset
|
32 |
fold_rev (fn Free (n, T) => |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
21025
diff
changeset
|
33 |
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
|
34 |
qs |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
21025
diff
changeset
|
35 |
thm |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
21025
diff
changeset
|
36 |
end |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
21025
diff
changeset
|
37 |
|
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
21025
diff
changeset
|
38 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
39 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
40 |
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
|
41 |
let |
22166 | 42 |
val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) = |
24816 | 43 |
InductivePackage.add_inductive_i |
44 |
{verbose = ! Toplevel.debug, |
|
45 |
kind = Thm.theoremK, |
|
46 |
alt_name = "", |
|
47 |
coind = false, |
|
48 |
no_elim = false, |
|
49 |
no_ind = false} |
|
50 |
[((R, T), NoSyn)] (* the relation *) |
|
51 |
[] (* no parameters *) |
|
52 |
(map (fn t => (("", []), t)) defs) (* the intros *) |
|
53 |
[] (* no special monos *) |
|
54 |
lthy |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
55 |
|
22619 | 56 |
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
|
57 |
|
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
21025
diff
changeset
|
58 |
val elim = elim_gen |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
21025
diff
changeset
|
59 |
|> forall_intr_vars (* FIXME... *) |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
60 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
61 |
in |
22612 | 62 |
(intrs, (Rdef, elim, induct, lthy)) |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
63 |
end |
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
21025
diff
changeset
|
64 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
diff
changeset
|
65 |
end |