author | berghofe |
Wed, 13 Nov 2002 15:32:41 +0100 | |
changeset 13710 | 75bec2c1bfd5 |
child 13725 | 12404b452034 |
permissions | -rw-r--r-- |
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/inductive_realizer.ML |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
2 |
ID: $Id$ |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
3 |
Author: Stefan Berghofer, TU Muenchen |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
5 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
6 |
Porgram extraction from proofs involving inductive predicates: |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
7 |
Realizers for induction and elimination rules |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
8 |
*) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
9 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
10 |
signature INDUCTIVE_REALIZER = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
11 |
sig |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
12 |
val add_ind_realizers: string -> string list -> theory -> theory |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
13 |
val setup: (theory -> theory) list |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
14 |
end; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
15 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
16 |
structure InductiveRealizer : INDUCTIVE_REALIZER = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
17 |
struct |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
18 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
19 |
val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps"); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
20 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
21 |
fun prf_of thm = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
22 |
let val {sign, prop, der = (_, prf), ...} = rep_thm thm |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
23 |
in Reconstruct.reconstruct_proof sign prop prf end; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
24 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
25 |
fun forall_intr_prf (t, prf) = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
26 |
let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
27 |
in Abst (a, Some T, Proofterm.prf_abstract_over t prf) end; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
28 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
29 |
fun subsets [] = [[]] |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
30 |
| subsets (x::xs) = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
31 |
let val ys = subsets xs |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
32 |
in ys @ map (cons x) ys end; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
33 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
34 |
val set_of = fst o dest_Const o head_of o snd o HOLogic.dest_mem; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
35 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
36 |
fun strip_all t = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
37 |
let |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
38 |
fun strip used (Const ("all", _) $ Abs (s, T, t)) = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
39 |
let val s' = variant used s |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
40 |
in strip (s'::used) (subst_bound (Free (s', T), t)) end |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
41 |
| strip used ((t as Const ("==>", _) $ P) $ Q) = t $ strip used Q |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
42 |
| strip _ t = t; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
43 |
in strip (add_term_free_names (t, [])) t end; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
44 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
45 |
fun relevant_vars prop = foldr (fn |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
46 |
(Var ((a, i), T), vs) => (case strip_type T of |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
47 |
(_, Type (s, _)) => if s mem ["bool", "set"] then (a, T) :: vs else vs |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
48 |
| _ => vs) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
49 |
| (_, vs) => vs) (term_vars prop, []); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
50 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
51 |
fun params_of intr = map (fst o fst o dest_Var) (term_vars |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
52 |
(snd (HOLogic.dest_mem (HOLogic.dest_Trueprop |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
53 |
(Logic.strip_imp_concl intr))))); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
54 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
55 |
fun dt_of_intrs thy vs intrs = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
56 |
let |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
57 |
val iTs = term_tvars (prop_of (hd intrs)); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
58 |
val Tvs = map TVar iTs; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
59 |
val (_ $ (_ $ _ $ S)) = Logic.strip_imp_concl (prop_of (hd intrs)); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
60 |
val (Const (s, _), ts) = strip_comb S; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
61 |
val params = map dest_Var ts; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
62 |
val tname = space_implode "_" (Sign.base_name s ^ "T" :: vs); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
63 |
fun constr_of_intr intr = (Sign.base_name (Thm.name_of_thm intr), |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
64 |
map (Type.unvarifyT o snd) (rev (Term.add_vars ([], prop_of intr)) \\ params) @ |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
65 |
filter_out (equal Extraction.nullT) (map |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
66 |
(Type.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)), |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
67 |
NoSyn); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
68 |
in (map (fn a => "'" ^ a) vs @ map (fst o fst) iTs, tname, NoSyn, |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
69 |
map constr_of_intr intrs) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
70 |
end; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
71 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
72 |
fun gen_realizes (Const ("realizes", Type ("fun", [T, _])) $ t $ |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
73 |
(Const ("op :", Type ("fun", [U, _])) $ x $ Var (ixn, _))) = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
74 |
Var (ixn, [T, U] ---> HOLogic.boolT) $ t $ x |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
75 |
| gen_realizes (Const ("op :", Type ("fun", [U, _])) $ x $ Var (ixn, _)) = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
76 |
Var (ixn, U --> HOLogic.boolT) $ x |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
77 |
| gen_realizes (bla as Const ("realizes", Type ("fun", [T, _])) $ t $ P) = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
78 |
if T = Extraction.nullT then P |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
79 |
else (case strip_comb P of |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
80 |
(Var (ixn, U), ts) => list_comb (Var (ixn, T --> U), t :: ts) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
81 |
| _ => error "gen_realizes: variable expected") |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
82 |
| gen_realizes (t $ u) = gen_realizes t $ gen_realizes u |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
83 |
| gen_realizes (Abs (s, T, t)) = Abs (s, T, gen_realizes t) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
84 |
| gen_realizes t = t; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
85 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
86 |
fun mk_rlz T = Const ("realizes", [T, HOLogic.boolT] ---> HOLogic.boolT); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
87 |
fun mk_rlz' T = Const ("realizes", [T, propT] ---> propT); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
88 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
89 |
(** turn "P" into "%r x. realizes r (P x)" or "%r x. realizes r (x : P)" **) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
90 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
91 |
fun gen_rvar vs (t as Var ((a, 0), T)) = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
92 |
let val U = TVar (("'" ^ a, 0), HOLogic.typeS) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
93 |
in case try HOLogic.dest_setT T of |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
94 |
None => if body_type T <> HOLogic.boolT then t else |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
95 |
let |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
96 |
val Ts = binder_types T; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
97 |
val i = length Ts; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
98 |
val xs = map (pair "x") Ts; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
99 |
val u = list_comb (t, map Bound (i - 1 downto 0)) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
100 |
in |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
101 |
if a mem vs then |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
102 |
list_abs (("r", U) :: xs, mk_rlz U $ Bound i $ u) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
103 |
else list_abs (xs, mk_rlz Extraction.nullT $ Extraction.nullt $ u) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
104 |
end |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
105 |
| Some T' => if a mem vs then |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
106 |
Abs ("r", U, Abs ("x", T', mk_rlz U $ Bound 1 $ |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
107 |
(HOLogic.mk_mem (Bound 0, t)))) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
108 |
else Abs ("x", T', mk_rlz Extraction.nullT $ Extraction.nullt $ |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
109 |
(HOLogic.mk_mem (Bound 0, t))) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
110 |
end |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
111 |
| gen_rvar _ t = t; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
112 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
113 |
fun mk_realizes_eqn n vs intrs = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
114 |
let |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
115 |
val iTs = term_tvars (prop_of (hd intrs)); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
116 |
val Tvs = map TVar iTs; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
117 |
val _ $ (_ $ _ $ S) = concl_of (hd intrs); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
118 |
val (Const (s, T), ts') = strip_comb S; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
119 |
val setT = body_type T; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
120 |
val elT = HOLogic.dest_setT setT; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
121 |
val x = Var (("x", 0), elT); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
122 |
val rT = if n then Extraction.nullT |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
123 |
else Type (space_implode "_" (s ^ "T" :: vs), |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
124 |
map (fn a => TVar (("'" ^ a, 0), HOLogic.typeS)) vs @ Tvs); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
125 |
val r = if n then Extraction.nullt else Var ((Sign.base_name s, 0), rT); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
126 |
val rvs = relevant_vars S; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
127 |
val vs' = map fst rvs \\ vs; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
128 |
val rname = space_implode "_" (s ^ "R" :: vs); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
129 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
130 |
fun mk_Tprem n v = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
131 |
let val Some T = assoc (rvs, v) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
132 |
in (Const ("typeof", T --> Type ("Type", [])) $ Var ((v, 0), T), |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
133 |
Extraction.mk_typ (if n then Extraction.nullT |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
134 |
else TVar (("'" ^ v, 0), HOLogic.typeS))) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
135 |
end; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
136 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
137 |
val prems = map (mk_Tprem true) vs' @ map (mk_Tprem false) vs; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
138 |
val ts = map (gen_rvar vs) ts'; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
139 |
val argTs = map fastype_of ts; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
140 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
141 |
in ((prems, (Const ("typeof", setT --> Type ("Type", [])) $ S, |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
142 |
Extraction.mk_typ rT)), |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
143 |
(prems, (mk_rlz rT $ r $ HOLogic.mk_mem (x, S), |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
144 |
if n then |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
145 |
HOLogic.mk_mem (x, list_comb (Const (rname, argTs ---> setT), ts)) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
146 |
else HOLogic.mk_mem (HOLogic.mk_prod (r, x), list_comb (Const (rname, |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
147 |
argTs ---> HOLogic.mk_setT (HOLogic.mk_prodT (rT, elT))), ts))))) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
148 |
end; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
149 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
150 |
fun fun_of_prem thy rsets vs params rule intr = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
151 |
let |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
152 |
(* add_term_vars and Term.add_vars may return variables in different order *) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
153 |
val args = map (Free o apfst fst o dest_Var) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
154 |
(add_term_vars (prop_of intr, []) \\ map Var params); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
155 |
val args' = map (Free o apfst fst) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
156 |
(Term.add_vars ([], prop_of intr) \\ params); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
157 |
val rule' = strip_all rule; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
158 |
val conclT = Extraction.etype_of thy vs [] (Logic.strip_imp_concl rule'); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
159 |
val used = map (fst o dest_Free) args; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
160 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
161 |
fun is_rec t = not (null (term_consts t inter rsets)); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
162 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
163 |
fun is_meta (Const ("all", _) $ Abs (s, _, P)) = is_meta P |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
164 |
| is_meta (Const ("==>", _) $ _ $ Q) = is_meta Q |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
165 |
| is_meta (Const ("Trueprop", _) $ (Const ("op :", _) $ _ $ _)) = true |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
166 |
| is_meta _ = false; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
167 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
168 |
fun fun_of ts rts args used (prem :: prems) = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
169 |
let |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
170 |
val T = Extraction.etype_of thy vs [] prem; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
171 |
val [x, r] = variantlist (["x", "r"], used) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
172 |
in if T = Extraction.nullT |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
173 |
then fun_of ts rts args used prems |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
174 |
else if is_rec prem then |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
175 |
if is_meta prem then |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
176 |
let |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
177 |
val prem' :: prems' = prems; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
178 |
val U = Extraction.etype_of thy vs [] prem'; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
179 |
in if U = Extraction.nullT |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
180 |
then fun_of (Free (x, T) :: ts) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
181 |
(Free (r, binder_types T ---> HOLogic.unitT) :: rts) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
182 |
(Free (x, T) :: args) (x :: r :: used) prems' |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
183 |
else fun_of (Free (x, T) :: ts) (Free (r, U) :: rts) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
184 |
(Free (r, U) :: Free (x, T) :: args) (x :: r :: used) prems' |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
185 |
end |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
186 |
else (case strip_type T of |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
187 |
(Ts, Type ("*", [T1, T2])) => |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
188 |
let |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
189 |
val fx = Free (x, Ts ---> T1); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
190 |
val fr = Free (r, Ts ---> T2); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
191 |
val bs = map Bound (length Ts - 1 downto 0); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
192 |
val t = list_abs (map (pair "z") Ts, |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
193 |
HOLogic.mk_prod (list_comb (fx, bs), list_comb (fr, bs))) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
194 |
in fun_of (fx :: ts) (fr :: rts) (t::args) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
195 |
(x :: r :: used) prems |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
196 |
end |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
197 |
| (Ts, U) => fun_of (Free (x, T) :: ts) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
198 |
(Free (r, binder_types T ---> HOLogic.unitT) :: rts) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
199 |
(Free (x, T) :: args) (x :: r :: used) prems) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
200 |
else fun_of (Free (x, T) :: ts) rts (Free (x, T) :: args) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
201 |
(x :: used) prems |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
202 |
end |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
203 |
| fun_of ts rts args used [] = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
204 |
let val xs = rev (rts @ ts) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
205 |
in if conclT = Extraction.nullT |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
206 |
then list_abs_free (map dest_Free xs, HOLogic.unit) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
207 |
else list_abs_free (map dest_Free xs, list_comb |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
208 |
(Free ("r" ^ Sign.base_name (Thm.name_of_thm intr), |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
209 |
map fastype_of (rev args) ---> conclT), rev args)) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
210 |
end |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
211 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
212 |
in fun_of (rev args) [] args' used (Logic.strip_imp_prems rule') end; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
213 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
214 |
fun indrule_realizer thy induct raw_induct rsets params vs rec_names rss intrs dummies = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
215 |
let |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
216 |
val concls = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct)); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
217 |
val premss = mapfilter (fn (s, rs) => if s mem rsets then |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
218 |
Some (map (fn r => nth_elem (find_index_eq (prop_of r) (map prop_of intrs), |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
219 |
prems_of raw_induct)) rs) else None) rss; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
220 |
val concls' = mapfilter (fn (s, _) => if s mem rsets then |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
221 |
find_first (fn concl => s mem term_consts concl) concls |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
222 |
else None) rss; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
223 |
val fs = flat (snd (foldl_map (fn (intrs, (prems, dummy)) => |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
224 |
let |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
225 |
val (intrs1, intrs2) = splitAt (length prems, intrs); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
226 |
val fs = map (fn (rule, intr) => |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
227 |
fun_of_prem thy rsets vs params rule intr) (prems ~~ intrs1) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
228 |
in (intrs2, if dummy then Const ("arbitrary", |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
229 |
HOLogic.unitT --> body_type (fastype_of (hd fs))) :: fs |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
230 |
else fs) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
231 |
end) (intrs, (premss ~~ dummies)))); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
232 |
val frees = foldl Term.add_frees ([], fs); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
233 |
val Ts = map fastype_of fs; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
234 |
val rlzs = mapfilter (fn (a, concl) => |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
235 |
let val T = Extraction.etype_of thy vs [] concl |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
236 |
in if T = Extraction.nullT then None |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
237 |
else Some (list_comb (Const (a, Ts ---> T), fs)) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
238 |
end) (rec_names ~~ concls') |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
239 |
in if null rlzs then Extraction.nullt else |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
240 |
let |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
241 |
val r = foldr1 HOLogic.mk_prod rlzs; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
242 |
val x = Free ("x", Extraction.etype_of thy vs [] (hd (prems_of induct))); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
243 |
fun name_of_fn intr = "r" ^ Sign.base_name (Thm.name_of_thm intr); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
244 |
val r' = list_abs_free (mapfilter (fn intr => |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
245 |
apsome (pair (name_of_fn intr)) (assoc (frees, name_of_fn intr))) intrs, |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
246 |
if length concls = 1 then r $ x else r) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
247 |
in |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
248 |
if length concls = 1 then lambda x r' else r' |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
249 |
end |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
250 |
end; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
251 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
252 |
val nonempty_msg = explode "Nonemptiness check failed for datatype "; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
253 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
254 |
fun add_dummy name dname (x as (_, (vs, s, mfx, cs))) = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
255 |
if name = s then (true, (vs, s, mfx, (dname, [HOLogic.unitT], NoSyn) :: cs)) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
256 |
else x; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
257 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
258 |
fun add_dummies f dts used thy = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
259 |
apsnd (pair (map fst dts)) (transform_error (f (map snd dts)) thy) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
260 |
handle ERROR_MESSAGE msg => if nonempty_msg prefix explode msg then |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
261 |
let |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
262 |
val name = Sign.base_name |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
263 |
(implode (drop (length nonempty_msg, explode msg))); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
264 |
val dname = variant used "Dummy" |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
265 |
in add_dummies f (map (add_dummy name dname) dts) (dname :: used) thy |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
266 |
end |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
267 |
else error msg; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
268 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
269 |
fun mk_realizer thy vs params ((rule, rrule), rt) = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
270 |
let |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
271 |
val prems = prems_of rule; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
272 |
val xs = rev (Term.add_vars ([], prop_of rule)); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
273 |
val rs = gen_rems (op = o pairself fst) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
274 |
(rev (Term.add_vars ([], prop_of rrule)), xs); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
275 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
276 |
fun mk_prf _ [] prf = prf |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
277 |
| mk_prf rs (prem :: prems) prf = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
278 |
let val T = Extraction.etype_of thy vs [] prem |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
279 |
in if T = Extraction.nullT |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
280 |
then AbsP ("H", Some (mk_rlz' T $ Extraction.nullt $ prem), |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
281 |
mk_prf rs prems prf) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
282 |
else forall_intr_prf (Var (hd rs), AbsP ("H", Some (mk_rlz' T $ |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
283 |
Var (hd rs) $ prem), mk_prf (tl rs) prems prf)) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
284 |
end; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
285 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
286 |
val subst = map (fn v as (ixn, _) => (ixn, gen_rvar vs (Var v))) xs; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
287 |
val prf = Proofterm.map_proof_terms |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
288 |
(subst_vars ([], subst)) I (prf_of rrule); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
289 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
290 |
in (Thm.name_of_thm rule, (vs, |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
291 |
if rt = Extraction.nullt then rt else |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
292 |
foldr (uncurry lambda) (map Var xs, rt), |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
293 |
foldr forall_intr_prf (map Var xs, mk_prf rs prems (Proofterm.proof_combP |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
294 |
(prf, map PBound (length prems - 1 downto 0)))))) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
295 |
end; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
296 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
297 |
fun add_rule (rss, r) = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
298 |
let |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
299 |
val _ $ (_ $ _ $ S) = concl_of r; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
300 |
val (Const (s, _), _) = strip_comb S; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
301 |
val rs = if_none (assoc (rss, s)) []; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
302 |
in overwrite (rss, (s, rs @ [r])) end; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
303 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
304 |
fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
305 |
let |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
306 |
val iTs = term_tvars (prop_of (hd intrs)); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
307 |
val ar = length vs + length iTs; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
308 |
val (_ $ (_ $ _ $ S)) = Logic.strip_imp_concl (prop_of (hd intrs)); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
309 |
val (_, params) = strip_comb S; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
310 |
val params' = map dest_Var params; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
311 |
val rss = foldl add_rule ([], intrs); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
312 |
val (prfx, _) = split_last (NameSpace.unpack (fst (hd rss))); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
313 |
val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
314 |
val {path, ...} = Sign.rep_sg (sign_of thy); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
315 |
val thy1 = thy |> |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
316 |
Theory.root_path |> |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
317 |
Theory.add_path (NameSpace.pack prfx); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
318 |
val (ty_eqs, rlz_eqs) = split_list |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
319 |
(map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs rs) rss); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
320 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
321 |
val thy1' = thy1 |> |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
322 |
Theory.copy |> |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
323 |
Theory.add_types (map (fn s => (Sign.base_name s, ar, NoSyn)) tnames) |> |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
324 |
Theory.add_arities_i (map (fn s => |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
325 |
(s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames) |> |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
326 |
Extraction.add_typeof_eqns_i ty_eqs; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
327 |
val dts = mapfilter (fn (s, rs) => if s mem rsets then |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
328 |
Some (dt_of_intrs thy1' vs rs) else None) rss; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
329 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
330 |
(** datatype representing computational content of inductive set **) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
331 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
332 |
val (thy2, (dummies, dt_info)) = thy1 |> |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
333 |
(if null dts then rpair ([], None) else |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
334 |
apsnd (apsnd Some) o add_dummies (DatatypePackage.add_datatype_i false |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
335 |
(map #2 dts)) (map (pair false) dts) []) |>> |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
336 |
Extraction.add_typeof_eqns_i ty_eqs |>> |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
337 |
Extraction.add_realizes_eqns_i rlz_eqs; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
338 |
fun get f x = if_none (apsome f x) []; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
339 |
val rec_names = distinct (map (fst o dest_Const o head_of o fst o |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
340 |
HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) (get #rec_thms dt_info)); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
341 |
val (_, constrss) = foldl_map (fn ((recs, dummies), (s, rs)) => |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
342 |
if s mem rsets then |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
343 |
let |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
344 |
val (d :: dummies') = dummies; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
345 |
val (recs1, recs2) = splitAt (length rs, if d then tl recs else recs) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
346 |
in ((recs2, dummies'), map (head_of o hd o rev o snd o strip_comb o |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
347 |
fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) recs1) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
348 |
end |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
349 |
else ((recs, dummies), replicate (length rs) Extraction.nullt)) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
350 |
((get #rec_thms dt_info, dummies), rss); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
351 |
val rintrs = map (fn (intr, c) => Pattern.eta_contract (gen_realizes |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
352 |
(Extraction.realizes_of thy2 vs |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
353 |
c (prop_of (forall_intr_list (map (cterm_of (sign_of thy2) o Var) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
354 |
(rev (Term.add_vars ([], prop_of intr)) \\ params')) intr))))) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
355 |
(intrs ~~ flat constrss); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
356 |
val rlzsets = distinct (map (fn rintr => snd (HOLogic.dest_mem |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
357 |
(HOLogic.dest_Trueprop (Logic.strip_assums_concl rintr)))) rintrs); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
358 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
359 |
(** realizability predicate **) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
360 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
361 |
val (thy3', ind_info) = thy2 |> |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
362 |
InductivePackage.add_inductive_i false true "" false false false |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
363 |
(map Logic.unvarify rlzsets) (map (fn (rintr, intr) => |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
364 |
((Sign.base_name (Thm.name_of_thm intr), strip_all |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
365 |
(Logic.unvarify rintr)), [])) (rintrs ~~ intrs)) [] |>> |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
366 |
Theory.absolute_path; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
367 |
val thy3 = PureThy.hide_thms false |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
368 |
(map Thm.name_of_thm (#intrs ind_info)) thy3'; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
369 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
370 |
(** realizer for induction rule **) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
371 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
372 |
val Ps = mapfilter (fn _ $ M $ P => if set_of M mem rsets then |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
373 |
Some (fst (fst (dest_Var (head_of P)))) else None) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
374 |
(HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct))); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
375 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
376 |
fun add_ind_realizer (thy, Ps) = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
377 |
let |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
378 |
val r = indrule_realizer thy induct raw_induct rsets params' |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
379 |
(vs @ Ps) rec_names rss intrs dummies; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
380 |
val rlz = strip_all (Logic.unvarify (gen_realizes |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
381 |
(Extraction.realizes_of thy (vs @ Ps) r (prop_of induct)))); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
382 |
val rews = map mk_meta_eq |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
383 |
(fst_conv :: snd_conv :: get #rec_thms dt_info); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
384 |
val thm = simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems => |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
385 |
[if length rss = 1 then |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
386 |
cut_facts_tac [hd prems] 1 THEN etac (#induct ind_info) 1 |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
387 |
else EVERY [rewrite_goals_tac (rews @ all_simps), |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
388 |
REPEAT (rtac allI 1), rtac (#induct ind_info) 1], |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
389 |
rewrite_goals_tac rews, |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
390 |
REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY' |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
391 |
[K (rewrite_goals_tac rews), ObjectLogic.atomize_tac, |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
392 |
DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
393 |
val (thy', thm') = PureThy.store_thm ((space_implode "_" |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
394 |
(Thm.name_of_thm induct :: vs @ Ps @ ["correctness"]), thm), []) thy |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
395 |
in |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
396 |
Extraction.add_realizers_i |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
397 |
[mk_realizer thy' (vs @ Ps) params' ((induct, thm'), r)] thy' |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
398 |
end; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
399 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
400 |
(** realizer for elimination rules **) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
401 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
402 |
val case_names = map (fst o dest_Const o head_of o fst o HOLogic.dest_eq o |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
403 |
HOLogic.dest_Trueprop o prop_of o hd) (get #case_thms dt_info); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
404 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
405 |
fun add_elim_realizer Ps ((((elim, elimR), case_thms), case_name), dummy) thy = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
406 |
let |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
407 |
val (prem :: prems) = prems_of elim; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
408 |
val p = Logic.list_implies (prems @ [prem], concl_of elim); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
409 |
val T' = Extraction.etype_of thy (vs @ Ps) [] p; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
410 |
val T = if dummy then (HOLogic.unitT --> body_type T') --> T' else T'; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
411 |
val Ts = filter_out (equal Extraction.nullT) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
412 |
(map (Extraction.etype_of thy (vs @ Ps) []) (prems_of elim)); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
413 |
val r = if null Ps then Extraction.nullt |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
414 |
else list_abs (map (pair "x") Ts, list_comb (Const (case_name, T), |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
415 |
(if dummy then |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
416 |
[Abs ("x", HOLogic.unitT, Const ("arbitrary", body_type T))] |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
417 |
else []) @ |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
418 |
map Bound ((length prems - 1 downto 0) @ [length prems]))); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
419 |
val rlz = strip_all (Logic.unvarify (gen_realizes |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
420 |
(Extraction.realizes_of thy (vs @ Ps) r (prop_of elim)))); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
421 |
val rews = map mk_meta_eq case_thms; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
422 |
val thm = simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems => |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
423 |
[cut_facts_tac [hd prems] 1, |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
424 |
etac elimR 1, |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
425 |
ALLGOALS (EVERY' [etac Pair_inject, asm_simp_tac HOL_basic_ss]), |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
426 |
rewrite_goals_tac rews, |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
427 |
REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_tac THEN' |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
428 |
DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
429 |
val (thy', thm') = PureThy.store_thm ((space_implode "_" |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
430 |
(Thm.name_of_thm elim :: vs @ Ps @ ["correctness"]), thm), []) thy |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
431 |
in |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
432 |
Extraction.add_realizers_i |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
433 |
[mk_realizer thy' (vs @ Ps) params' ((elim, thm'), r)] thy' |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
434 |
end; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
435 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
436 |
(** add realizers to theory **) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
437 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
438 |
val rintr_thms = flat (map (fn (_, rs) => map (fn r => nth_elem |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
439 |
(find_index_eq r intrs, #intrs ind_info)) rs) rss); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
440 |
val thy4 = foldl add_ind_realizer (thy3, subsets Ps); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
441 |
val thy5 = Extraction.add_realizers_i |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
442 |
(map (mk_realizer thy4 vs params') |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
443 |
(map (fn ((rule, rrule), c) => ((rule, rrule), list_comb (c, |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
444 |
map Var (rev (Term.add_vars ([], prop_of rule)) \\ params')))) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
445 |
(flat (map snd rss) ~~ rintr_thms ~~ flat constrss))) thy4; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
446 |
val elimps = mapfilter (fn (s, _) => if s mem rsets then |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
447 |
find_first (fn (thm, _) => s mem term_consts (hd (prems_of thm))) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
448 |
(elims ~~ #elims ind_info) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
449 |
else None) rss; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
450 |
val thy6 = foldl (fn (thy, p as ((((elim, _), _), _), _)) => thy |> |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
451 |
add_elim_realizer [] p |> add_elim_realizer [fst (fst (dest_Var |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
452 |
(HOLogic.dest_Trueprop (concl_of elim))))] p) (thy5, |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
453 |
elimps ~~ get #case_thms dt_info ~~ case_names ~~ dummies) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
454 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
455 |
in Theory.add_path (NameSpace.pack (if_none path [])) thy6 end; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
456 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
457 |
fun add_ind_realizers name rsets thy = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
458 |
let |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
459 |
val (_, {intrs, induct, raw_induct, elims, ...}) = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
460 |
(case InductivePackage.get_inductive thy name of |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
461 |
None => error ("Unknown inductive set " ^ quote name) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
462 |
| Some info => info); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
463 |
val _ $ (_ $ _ $ S) = concl_of (hd intrs); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
464 |
val vss = sort (int_ord o pairself length) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
465 |
(subsets (map fst (relevant_vars S))) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
466 |
in |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
467 |
foldl (add_ind_realizer rsets intrs induct raw_induct elims) (thy, vss) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
468 |
end |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
469 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
470 |
fun rlz_attrib arg (thy, thm) = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
471 |
let |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
472 |
fun err () = error "ind_realizer: bad rule"; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
473 |
val sets = |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
474 |
(case HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of thm)) of |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
475 |
[_] => [set_of (HOLogic.dest_Trueprop (hd (prems_of thm)))] |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
476 |
| xs => map (set_of o fst o HOLogic.dest_imp) xs) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
477 |
handle TERM _ => err () | LIST _ => err (); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
478 |
in |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
479 |
(add_ind_realizers (hd sets) (case arg of |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
480 |
None => sets | Some None => [] |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
481 |
| Some (Some sets') => sets \\ map (Sign.intern_const (sign_of thy)) sets') |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
482 |
thy, thm) |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
483 |
end; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
484 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
485 |
val rlz_attrib_global = Attrib.syntax (Scan.lift |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
486 |
(Scan.option (Args.$$$ "irrelevant" |-- |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
487 |
Scan.option (Args.colon |-- Scan.repeat1 Args.name))) >> rlz_attrib); |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
488 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
489 |
val setup = [Attrib.add_attributes [("ind_realizer", |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
490 |
(rlz_attrib_global, K Attrib.undef_local_attribute), |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
491 |
"add realizers for inductive set")]]; |
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
492 |
|
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset
|
493 |
end; |