author  berghofe 
Wed, 07 Feb 2007 17:44:07 +0100  
changeset 22271  51a80e238b29 
parent 21858  05f57309170c 
child 22596  d0d2af4db18f 
permissions  rwrr 
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 

75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

5 
Porgram extraction from proofs involving inductive predicates: 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

6 
Realizers for induction and elimination rules 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

7 
*) 
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 
signature INDUCTIVE_REALIZER = 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

10 
sig 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

11 
val add_ind_realizers: string > string list > theory > theory 
18708  12 
val setup: theory > theory 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

13 
end; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

14 

75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

15 
structure InductiveRealizer : INDUCTIVE_REALIZER = 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

16 
struct 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

17 

22271  18 
(* FIXME: LocalTheory.note should return theorems with proper names! *) 
19 
fun name_of_thm thm = (case Proofterm.strip_combt (fst (Proofterm.strip_combP 

20 
(Proofterm.rewrite_proof (theory_of_thm thm) ([], []) (proof_of thm)))) of 

21 
(PThm (name, _, _, _), _) => name 

22 
 _ => error "name_of_thm: bad proof"); 

23 

24 
(* infer order of variables in intro rules from order of quantifiers in elim rule *) 

25 
fun infer_intro_vars elim arity intros = 

26 
let 

27 
val thy = theory_of_thm elim; 

28 
val _ :: cases = prems_of elim; 

29 
val used = map (fst o fst) (Term.add_vars (prop_of elim) []); 

30 
fun mtch (t, u) = 

31 
let 

32 
val params = Logic.strip_params t; 

33 
val vars = map (Var o apfst (rpair 0)) 

34 
(Name.variant_list used (map fst params) ~~ map snd params); 

35 
val ts = map (curry subst_bounds (rev vars)) 

36 
(List.drop (Logic.strip_assums_hyp t, arity)); 

37 
val us = Logic.strip_imp_prems u; 

38 
val tab = fold (Pattern.first_order_match thy) (ts ~~ us) 

39 
(Vartab.empty, Vartab.empty); 

40 
in 

41 
map (Envir.subst_vars tab) vars 

42 
end 

43 
in 

44 
map (mtch o apsnd prop_of) (cases ~~ intros) 

45 
end; 

46 

47 
(* read off arities of inductive predicates from raw induction rule *) 

48 
fun arities_of induct = 

49 
map (fn (_ $ t $ u) => 

50 
(fst (dest_Const (head_of t)), length (snd (strip_comb u)))) 

51 
(HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct))); 

52 

53 
(* read off parameters of inductive predicate from raw induction rule *) 

54 
fun params_of induct = 

55 
let 

56 
val (_ $ t $ u :: _) = 

57 
HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)); 

58 
val (_, ts) = strip_comb t; 

59 
val (_, us) = strip_comb u 

60 
in 

61 
List.take (ts, length ts  length us) 

62 
end; 

63 

13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

64 
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

65 

75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

66 
fun prf_of thm = 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

67 
let val {sign, prop, der = (_, prf), ...} = rep_thm thm 
22271  68 
in Reconstruct.expand_proof sign [("", NONE)] (Reconstruct.reconstruct_proof sign prop prf) end; (* FIXME *) 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

69 

75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

70 
fun forall_intr_prf (t, prf) = 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

71 
let val (a, T) = (case t of Var ((a, _), T) => (a, T)  Free p => p) 
15531  72 
in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end; 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

73 

22271  74 
fun forall_intr_term (t, u) = 
75 
let val (a, T) = (case t of Var ((a, _), T) => (a, T)  Free p => p) 

76 
in all T $ Abs (a, T, abstract_over (t, u)) end; 

77 

13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

78 
fun subsets [] = [[]] 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

79 
 subsets (x::xs) = 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

80 
let val ys = subsets xs 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

81 
in ys @ map (cons x) ys end; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

82 

22271  83 
val pred_of = fst o dest_Const o head_of; 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

84 

22271  85 
fun strip_all' used names (Const ("all", _) $ Abs (s, T, t)) = 
86 
let val (s', names') = (case names of 

87 
[] => (Name.variant used s, []) 

88 
 name :: names' => (name, names')) 

89 
in strip_all' (s'::used) names' (subst_bound (Free (s', T), t)) end 

90 
 strip_all' used names ((t as Const ("==>", _) $ P) $ Q) = 

91 
t $ strip_all' used names Q 

92 
 strip_all' _ _ t = t; 

93 

94 
fun strip_all t = strip_all' (add_term_free_names (t, [])) [] t; 

95 

96 
fun strip_one name (Const ("all", _) $ Abs (s, T, Const ("==>", _) $ P $ Q)) = 

97 
(subst_bound (Free (name, T), P), subst_bound (Free (name, T), Q)) 

98 
 strip_one _ (Const ("==>", _) $ P $ Q) = (P, Q); 

13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

99 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

100 
fun relevant_vars prop = foldr (fn 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

101 
(Var ((a, i), T), vs) => (case strip_type T of 
22271  102 
(_, Type (s, _)) => if s mem ["bool"] then (a, T) :: vs else vs 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

103 
 _ => vs) 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

104 
 (_, vs) => vs) [] (term_vars prop); 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

105 

22271  106 
fun dt_of_intrs thy vs nparms intrs = 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

107 
let 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

108 
val iTs = term_tvars (prop_of (hd intrs)); 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

109 
val Tvs = map TVar iTs; 
22271  110 
val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop 
111 
(Logic.strip_imp_concl (prop_of (hd intrs)))); 

112 
val params = map dest_Var (Library.take (nparms, ts)); 

13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

113 
val tname = space_implode "_" (Sign.base_name s ^ "T" :: vs); 
22271  114 
fun constr_of_intr intr = (Sign.base_name (name_of_thm intr), 
19806  115 
map (Logic.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @ 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

116 
filter_out (equal Extraction.nullT) (map 
19806  117 
(Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)), 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

118 
NoSyn); 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

119 
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

120 
map constr_of_intr intrs) 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

121 
end; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

122 

75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

123 
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

124 

22271  125 
(** turn "P" into "%r x. realizes r (P x)" **) 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

126 

75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

127 
fun gen_rvar vs (t as Var ((a, 0), T)) = 
22271  128 
if body_type T <> HOLogic.boolT then t else 
129 
let 

130 
val U = TVar (("'" ^ a, 0), HOLogic.typeS) 

131 
val Ts = binder_types T; 

132 
val i = length Ts; 

133 
val xs = map (pair "x") Ts; 

134 
val u = list_comb (t, map Bound (i  1 downto 0)) 

135 
in 

136 
if a mem vs then 

137 
list_abs (("r", U) :: xs, mk_rlz U $ Bound i $ u) 

138 
else list_abs (xs, mk_rlz Extraction.nullT $ Extraction.nullt $ u) 

139 
end 

13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

140 
 gen_rvar _ t = t; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

141 

22271  142 
fun mk_realizes_eqn n vs nparms intrs = 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

143 
let 
22271  144 
val concl = HOLogic.dest_Trueprop (concl_of (hd intrs)); 
145 
val iTs = term_tvars concl; 

13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

146 
val Tvs = map TVar iTs; 
22271  147 
val (h as Const (s, T), us) = strip_comb concl; 
148 
val params = List.take (us, nparms); 

149 
val elTs = List.drop (binder_types T, nparms); 

150 
val predT = elTs > HOLogic.boolT; 

151 
val used = map (fst o fst o dest_Var) params; 

152 
val xs = map (Var o apfst (rpair 0)) 

153 
(Name.variant_list used (replicate (length elTs) "x") ~~ elTs); 

13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

154 
val rT = if n then Extraction.nullT 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

155 
else Type (space_implode "_" (s ^ "T" :: vs), 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

156 
map (fn a => TVar (("'" ^ a, 0), HOLogic.typeS)) vs @ Tvs); 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

157 
val r = if n then Extraction.nullt else Var ((Sign.base_name s, 0), rT); 
22271  158 
val S = list_comb (h, params @ xs); 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

159 
val rvs = relevant_vars S; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

160 
val vs' = map fst rvs \\ vs; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

161 
val rname = space_implode "_" (s ^ "R" :: vs); 
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 mk_Tprem n v = 
17485  164 
let val T = (the o AList.lookup (op =) rvs) v 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

165 
in (Const ("typeof", T > Type ("Type", [])) $ Var ((v, 0), T), 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

166 
Extraction.mk_typ (if n then Extraction.nullT 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

167 
else TVar (("'" ^ v, 0), HOLogic.typeS))) 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

168 
end; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

169 

75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

170 
val prems = map (mk_Tprem true) vs' @ map (mk_Tprem false) vs; 
22271  171 
val ts = map (gen_rvar vs) params; 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

172 
val argTs = map fastype_of ts; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

173 

22271  174 
in ((prems, (Const ("typeof", HOLogic.boolT > Type ("Type", [])) $ S, 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

175 
Extraction.mk_typ rT)), 
22271  176 
(prems, (mk_rlz rT $ r $ S, 
177 
if n then list_comb (Const (rname, argTs > predT), ts @ xs) 

178 
else list_comb (Const (rname, argTs @ [rT] > predT), ts @ [r] @ xs)))) 

13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

179 
end; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

180 

22271  181 
fun fun_of_prem thy rsets vs params rule ivs intr = 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

182 
let 
22271  183 
val ctxt = ProofContext.init thy 
184 
val args = map (Free o apfst fst o dest_Var) ivs; 

13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

185 
val args' = map (Free o apfst fst) 
16861  186 
(Term.add_vars (prop_of intr) [] \\ params); 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

187 
val rule' = strip_all rule; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

188 
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

189 
val used = map (fst o dest_Free) args; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

190 

75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

191 
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

192 

75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

193 
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

194 
 is_meta (Const ("==>", _) $ _ $ Q) = is_meta Q 
22271  195 
 is_meta (Const ("Trueprop", _) $ t) = (case head_of t of 
196 
Const (s, _) => can (InductivePackage.the_inductive ctxt) s 

197 
 _ => true) 

13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

198 
 is_meta _ = false; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

199 

75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

200 
fun fun_of ts rts args used (prem :: prems) = 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

201 
let 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

202 
val T = Extraction.etype_of thy vs [] prem; 
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19806
diff
changeset

203 
val [x, r] = Name.variant_list used ["x", "r"] 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

204 
in if T = Extraction.nullT 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

205 
then fun_of ts rts args used prems 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

206 
else if is_rec prem then 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

207 
if is_meta prem then 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

208 
let 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

209 
val prem' :: prems' = prems; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

210 
val U = Extraction.etype_of thy vs [] prem'; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

211 
in if U = Extraction.nullT 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

212 
then fun_of (Free (x, T) :: ts) 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

213 
(Free (r, binder_types T > HOLogic.unitT) :: rts) 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

214 
(Free (x, T) :: args) (x :: r :: used) prems' 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

215 
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

216 
(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

217 
end 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

218 
else (case strip_type T of 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

219 
(Ts, Type ("*", [T1, T2])) => 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

220 
let 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

221 
val fx = Free (x, Ts > T1); 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

222 
val fr = Free (r, Ts > T2); 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

223 
val bs = map Bound (length Ts  1 downto 0); 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

224 
val t = list_abs (map (pair "z") Ts, 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

225 
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

226 
in fun_of (fx :: ts) (fr :: rts) (t::args) 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

227 
(x :: r :: used) prems 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

228 
end 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

229 
 (Ts, U) => fun_of (Free (x, T) :: ts) 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

230 
(Free (r, binder_types T > HOLogic.unitT) :: rts) 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

231 
(Free (x, T) :: args) (x :: r :: used) prems) 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

232 
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

233 
(x :: used) prems 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

234 
end 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

235 
 fun_of ts rts args used [] = 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

236 
let val xs = rev (rts @ ts) 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

237 
in if conclT = Extraction.nullT 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

238 
then list_abs_free (map dest_Free xs, HOLogic.unit) 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

239 
else list_abs_free (map dest_Free xs, list_comb 
22271  240 
(Free ("r" ^ Sign.base_name (name_of_thm intr), 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

241 
map fastype_of (rev args) > conclT), rev args)) 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

242 
end 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

243 

13921
69c627b6b28d
Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents:
13725
diff
changeset

244 
in fun_of args' [] (rev args) used (Logic.strip_imp_prems rule') end; 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

245 

75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

246 
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

247 
let 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

248 
val concls = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct)); 
15570  249 
val premss = List.mapPartial (fn (s, rs) => if s mem rsets then 
22271  250 
SOME (rs, map (fn (_, r) => List.nth (prems_of raw_induct, 
15570  251 
find_index_eq (prop_of r) (map prop_of intrs))) rs) else NONE) rss; 
22271  252 
val fs = maps (fn ((intrs, prems), dummy) => 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

253 
let 
22271  254 
val fs = map (fn (rule, (ivs, intr)) => 
255 
fun_of_prem thy rsets vs params rule ivs intr) (prems ~~ intrs) 

256 
in if dummy then Const ("arbitrary", 

13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

257 
HOLogic.unitT > body_type (fastype_of (hd fs))) :: fs 
22271  258 
else fs 
259 
end) (premss ~~ dummies); 

16861  260 
val frees = fold Term.add_frees fs []; 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

261 
val Ts = map fastype_of fs; 
22271  262 
fun name_of_fn intr = "r" ^ Sign.base_name (name_of_thm intr) 
263 
in 

264 
fst (fold_map (fn concl => fn names => 

13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

265 
let val T = Extraction.etype_of thy vs [] concl 
22271  266 
in if T = Extraction.nullT then (Extraction.nullt, names) else 
267 
let 

268 
val Type ("fun", [U, _]) = T; 

269 
val a :: names' = names 

270 
in (list_abs_free (("x", U) :: List.mapPartial (fn intr => 

271 
Option.map (pair (name_of_fn intr)) 

272 
(AList.lookup (op =) frees (name_of_fn intr))) intrs, 

273 
list_comb (Const (a, Ts > T), fs) $ Free ("x", U)), names') 

274 
end 

275 
end) concls rec_names) 

13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

276 
end; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

277 

75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

278 
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

279 
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

280 
else x; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

281 

18314  282 
fun add_dummies f [] _ thy = 
283 
(([], NONE), thy) 

284 
 add_dummies f dts used thy = 

285 
thy 

286 
> f (map snd dts) 

287 
> (fn dtinfo => pair ((map fst dts), SOME dtinfo)) 

288 
handle DatatypeAux.Datatype_Empty name' => 

13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

289 
let 
14888
99ac3eb0f84e
add_dummies no longer uses transform_error but handles specific
berghofe
parents:
13928
diff
changeset

290 
val name = Sign.base_name name'; 
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19806
diff
changeset

291 
val dname = Name.variant used "Dummy" 
18314  292 
in 
293 
thy 

294 
> add_dummies f (map (add_dummy name dname) dts) (dname :: used) 

14888
99ac3eb0f84e
add_dummies no longer uses transform_error but handles specific
berghofe
parents:
13928
diff
changeset

295 
end; 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

296 

22271  297 
fun mk_realizer thy vs (name, rule, rrule, rlz, rt) = 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

298 
let 
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13710
diff
changeset

299 
val rvs = map fst (relevant_vars (prop_of rule)); 
16861  300 
val xs = rev (Term.add_vars (prop_of rule) []); 
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13710
diff
changeset

301 
val vs1 = map Var (filter_out (fn ((a, _), _) => a mem rvs) xs); 
16861  302 
val rlzvs = rev (Term.add_vars (prop_of rrule) []); 
17485  303 
val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs; 
22271  304 
val rs = map Var (subtract (op = o pairself fst) xs rlzvs); 
305 
val rlz' = foldr forall_intr_term (prop_of rrule) (vs2 @ rs); 

306 
val rlz'' = foldr forall_intr_term rlz vs2 

307 
in (name, (vs, 

13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

308 
if rt = Extraction.nullt then rt else 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

309 
foldr (uncurry lambda) rt vs1, 
22271  310 
ProofRewriteRules.un_hhf_proof rlz' rlz'' 
311 
(foldr forall_intr_prf (prf_of rrule) (vs2 @ rs)))) 

13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

312 
end; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

313 

22271  314 
fun partition_rules induct intrs = 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

315 
let 
22271  316 
fun name_of t = fst (dest_Const (head_of t)); 
317 
val ts = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)); 

318 
val sets = map (name_of o fst o HOLogic.dest_imp) ts; 

17485  319 
in 
22271  320 
map (fn s => (s, filter 
321 
(equal s o name_of o HOLogic.dest_Trueprop o concl_of) intrs)) sets 

17485  322 
end; 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

323 

75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

324 
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

325 
let 
22271  326 
val qualifier = NameSpace.qualifier (name_of_thm induct); 
327 
val inducts = PureThy.get_thms thy (Name 

328 
(NameSpace.qualified qualifier "inducts")); 

13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

329 
val iTs = term_tvars (prop_of (hd intrs)); 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

330 
val ar = length vs + length iTs; 
22271  331 
val params = params_of raw_induct; 
332 
val arities = arities_of raw_induct; 

333 
val nparms = length params; 

13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

334 
val params' = map dest_Var params; 
22271  335 
val rss = partition_rules raw_induct intrs; 
336 
val rss' = map (fn (((s, rs), (_, arity)), elim) => 

337 
(s, (infer_intro_vars elim arity rs ~~ rs))) (rss ~~ arities ~~ elims); 

21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
21646
diff
changeset

338 
val (prfx, _) = split_last (NameSpace.explode (fst (hd rss))); 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

339 
val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets; 
16123  340 

13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

341 
val thy1 = thy > 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

342 
Theory.root_path > 
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
21646
diff
changeset

343 
Theory.add_path (NameSpace.implode prfx); 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

344 
val (ty_eqs, rlz_eqs) = split_list 
22271  345 
(map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs nparms rs) rss); 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

346 

75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

347 
val thy1' = thy1 > 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

348 
Theory.copy > 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

349 
Theory.add_types (map (fn s => (Sign.base_name s, ar, NoSyn)) tnames) > 
19510  350 
fold (fn s => AxClass.axiomatize_arity_i 
351 
(s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames > 

13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

352 
Extraction.add_typeof_eqns_i ty_eqs; 
15570  353 
val dts = List.mapPartial (fn (s, rs) => if s mem rsets then 
22271  354 
SOME (dt_of_intrs thy1' vs nparms rs) else NONE) rss; 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

355 

75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

356 
(** datatype representing computational content of inductive set **) 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

357 

18314  358 
val ((dummies, dt_info), thy2) = 
18008  359 
thy1 
18314  360 
> add_dummies 
361 
(DatatypePackage.add_datatype_i false false (map #2 dts)) 

362 
(map (pair false) dts) [] 

363 
> Extraction.add_typeof_eqns_i ty_eqs 

364 
> Extraction.add_realizes_eqns_i rlz_eqs; 

365 
fun get f = (these oo Option.map) f; 

19046
bc5c6c9b114e
removed distinct, renamed gen_distinct to distinct;
wenzelm
parents:
18929
diff
changeset

366 
val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

367 
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

368 
val (_, constrss) = foldl_map (fn ((recs, dummies), (s, rs)) => 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

369 
if s mem rsets then 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

370 
let 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

371 
val (d :: dummies') = dummies; 
19473  372 
val (recs1, recs2) = chop (length rs) (if d then tl recs else recs) 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

373 
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

374 
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

375 
end 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

376 
else ((recs, dummies), replicate (length rs) Extraction.nullt)) 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

377 
((get #rec_thms dt_info, dummies), rss); 
18929  378 
val rintrs = map (fn (intr, c) => Envir.eta_contract 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

379 
(Extraction.realizes_of thy2 vs 
22271  380 
(if c = Extraction.nullt then c else list_comb (c, map Var (rev 
381 
(Term.add_vars (prop_of intr) []) \\ params'))) (prop_of intr))) 

382 
(maps snd rss ~~ List.concat constrss); 

383 
val (rlzpreds, rlzpreds') = split_list 

384 
(distinct (op = o pairself (#1 o #1)) (map (fn rintr => 

385 
let 

386 
val Const (s, T) = head_of (HOLogic.dest_Trueprop 

387 
(Logic.strip_assums_concl rintr)); 

388 
val s' = Sign.base_name s; 

389 
val T' = Logic.unvarifyT T 

390 
in ((s', SOME T', NoSyn), 

391 
(Const (s, T'), Free (s', T'))) 

392 
end) rintrs)); 

393 
val rlzparams = map (fn Var ((s, _), T) => (s, SOME (Logic.unvarifyT T))) 

394 
(List.take (snd (strip_comb 

395 
(HOLogic.dest_Trueprop (Logic.strip_assums_concl (hd rintrs)))), nparms)); 

13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

396 

75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

397 
(** realizability predicate **) 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

398 

22271  399 
val (ind_info, thy3') = thy2 > 
400 
TheoryTarget.init NONE > 

401 
InductivePackage.add_inductive_i false "" false false false 

402 
rlzpreds rlzparams (map (fn (rintr, intr) => 

403 
((Sign.base_name (name_of_thm intr), []), 

404 
subst_atomic rlzpreds' (Logic.unvarify rintr))) 

405 
(rintrs ~~ maps snd rss)) [] > 

406 
ProofContext.theory_of o LocalTheory.exit > 

13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

407 
Theory.absolute_path; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

408 
val thy3 = PureThy.hide_thms false 
22271  409 
(map name_of_thm (#intrs ind_info)) thy3'; 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

410 

75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

411 
(** realizer for induction rule **) 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

412 

22271  413 
val Ps = List.mapPartial (fn _ $ M $ P => if pred_of M mem rsets then 
15531  414 
SOME (fst (fst (dest_Var (head_of P)))) else NONE) 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

415 
(HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct))); 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

416 

75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

417 
fun add_ind_realizer (thy, Ps) = 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

418 
let 
22271  419 
val rs = indrule_realizer thy induct raw_induct rsets params' 
420 
(vs @ Ps) rec_names rss' intrs dummies; 

421 
val rlzs = map (fn (r, ind) => Extraction.realizes_of thy (vs @ Ps) r 

422 
(prop_of ind)) (rs ~~ inducts); 

423 
val used = foldr add_term_free_names [] rlzs; 

424 
val rnames = Name.variant_list used (replicate (length inducts) "r"); 

425 
val rnames' = Name.variant_list 

426 
(used @ rnames) (replicate (length intrs) "s"); 

427 
val rlzs' as (prems, _, _) :: _ = map (fn (rlz, name) => 

428 
let 

429 
val (P, Q) = strip_one name (Logic.unvarify rlz); 

430 
val Q' = strip_all' [] rnames' Q 

431 
in 

432 
(Logic.strip_imp_prems Q', P, Logic.strip_imp_concl Q') 

433 
end) (rlzs ~~ rnames); 

434 
val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map 

435 
(fn (_, _ $ P, _ $ Q) => HOLogic.mk_imp (P, Q)) rlzs')); 

13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

436 
val rews = map mk_meta_eq 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

437 
(fst_conv :: snd_conv :: get #rec_thms dt_info); 
22271  438 
val thm = Goal.prove_global thy [] prems concl (fn prems => EVERY 
439 
[rtac (#raw_induct ind_info) 1, 

13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

440 
rewrite_goals_tac rews, 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

441 
REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY' 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

442 
[K (rewrite_goals_tac rews), ObjectLogic.atomize_tac, 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

443 
DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]); 
18358  444 
val (thm', thy') = PureThy.store_thm ((space_implode "_" 
22271  445 
(NameSpace.qualified qualifier "induct" :: vs @ Ps @ 
446 
["correctness"]), thm), []) thy; 

447 
val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp))) 

448 
(DatatypeAux.split_conj_thm thm'); 

449 
val ([thms'], thy'') = PureThy.add_thmss 

450 
[((space_implode "_" 

451 
(NameSpace.qualified qualifier "inducts" :: vs @ Ps @ 

452 
["correctness"]), thms), [])] thy'; 

453 
val realizers = inducts ~~ thms' ~~ rlzs ~~ rs; 

13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

454 
in 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

455 
Extraction.add_realizers_i 
22271  456 
(map (fn (((ind, corr), rlz), r) => 
457 
mk_realizer thy' (vs @ Ps) (Thm.get_name ind, ind, corr, rlz, r)) 

458 
realizers @ (case realizers of 

459 
[(((ind, corr), rlz), r)] => 

460 
[mk_realizer thy' (vs @ Ps) (NameSpace.qualified qualifier "induct", 

461 
ind, corr, rlz, r)] 

462 
 _ => [])) thy'' 

13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

463 
end; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

464 

75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

465 
(** realizer for elimination rules **) 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

466 

75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

467 
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

468 
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

469 

13921
69c627b6b28d
Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents:
13725
diff
changeset

470 
fun add_elim_realizer Ps 
69c627b6b28d
Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents:
13725
diff
changeset

471 
(((((elim, elimR), intrs), case_thms), case_name), dummy) thy = 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

472 
let 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

473 
val (prem :: prems) = prems_of elim; 
22271  474 
fun reorder1 (p, (_, intr)) = 
15570  475 
Library.foldl (fn (t, ((s, _), T)) => all T $ lambda (Free (s, T)) t) 
16861  476 
(strip_all p, Term.add_vars (prop_of intr) [] \\ params'); 
22271  477 
fun reorder2 ((ivs, intr), i) = 
478 
let val fs = Term.add_vars (prop_of intr) [] \\ params' 

15570  479 
in Library.foldl (fn (t, x) => lambda (Var x) t) 
22271  480 
(list_comb (Bound (i + length ivs), ivs), fs) 
13921
69c627b6b28d
Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents:
13725
diff
changeset

481 
end; 
69c627b6b28d
Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents:
13725
diff
changeset

482 
val p = Logic.list_implies 
69c627b6b28d
Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents:
13725
diff
changeset

483 
(map reorder1 (prems ~~ intrs) @ [prem], concl_of elim); 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

484 
val T' = Extraction.etype_of thy (vs @ Ps) [] p; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

485 
val T = if dummy then (HOLogic.unitT > body_type T') > T' else T'; 
13921
69c627b6b28d
Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents:
13725
diff
changeset

486 
val Ts = map (Extraction.etype_of thy (vs @ Ps) []) (prems_of elim); 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

487 
val r = if null Ps then Extraction.nullt 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

488 
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

489 
(if dummy then 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

490 
[Abs ("x", HOLogic.unitT, Const ("arbitrary", body_type T))] 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

491 
else []) @ 
13921
69c627b6b28d
Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents:
13725
diff
changeset

492 
map reorder2 (intrs ~~ (length prems  1 downto 0)) @ 
69c627b6b28d
Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents:
13725
diff
changeset

493 
[Bound (length prems)])); 
22271  494 
val rlz = Extraction.realizes_of thy (vs @ Ps) r (prop_of elim); 
495 
val rlz' = strip_all (Logic.unvarify rlz); 

13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

496 
val rews = map mk_meta_eq case_thms; 
22271  497 
val thm = Goal.prove_global thy [] 
498 
(Logic.strip_imp_prems rlz') (Logic.strip_imp_concl rlz') (fn prems => EVERY 

13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

499 
[cut_facts_tac [hd prems] 1, 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

500 
etac elimR 1, 
22271  501 
ALLGOALS (asm_simp_tac HOL_basic_ss), 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

502 
rewrite_goals_tac rews, 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

503 
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

504 
DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]); 
18358  505 
val (thm', thy') = PureThy.store_thm ((space_implode "_" 
22271  506 
(name_of_thm elim :: vs @ Ps @ ["correctness"]), thm), []) thy 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

507 
in 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

508 
Extraction.add_realizers_i 
22271  509 
[mk_realizer thy' (vs @ Ps) (name_of_thm elim, elim, thm', rlz, r)] thy' 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

510 
end; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

511 

75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

512 
(** add realizers to theory **) 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

513 

15570  514 
val thy4 = Library.foldl add_ind_realizer (thy3, subsets Ps); 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

515 
val thy5 = Extraction.add_realizers_i 
22271  516 
(map (mk_realizer thy4 vs) (map (fn (((rule, rrule), rlz), c) => 
517 
(name_of_thm rule, rule, rrule, rlz, 

518 
list_comb (c, map Var (rev (Term.add_vars (prop_of rule) []) \\ params')))) 

519 
(List.concat (map snd rss) ~~ #intrs ind_info ~~ rintrs ~~ 

520 
List.concat constrss))) thy4; 

521 
val elimps = List.mapPartial (fn ((s, intrs), p) => 

522 
if s mem rsets then SOME (p, intrs) else NONE) 

523 
(rss' ~~ (elims ~~ #elims ind_info)); 

15570  524 
val thy6 = Library.foldl (fn (thy, p as (((((elim, _), _), _), _), _)) => thy > 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

525 
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

526 
(HOLogic.dest_Trueprop (concl_of elim))))] p) (thy5, 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

527 
elimps ~~ get #case_thms dt_info ~~ case_names ~~ dummies) 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

528 

16123  529 
in Theory.restore_naming thy thy6 end; 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

530 

75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

531 
fun add_ind_realizers name rsets thy = 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

532 
let 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

533 
val (_, {intrs, induct, raw_induct, elims, ...}) = 
22271  534 
InductivePackage.the_inductive (ProofContext.init thy) name; 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

535 
val vss = sort (int_ord o pairself length) 
22271  536 
(subsets (map fst (relevant_vars (concl_of (hd intrs))))) 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

537 
in 
15570  538 
Library.foldl (add_ind_realizer rsets intrs induct raw_induct elims) (thy, vss) 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

539 
end 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

540 

20897  541 
fun rlz_attrib arg = Thm.declaration_attribute (fn thm => Context.mapping 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

542 
let 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

543 
fun err () = error "ind_realizer: bad rule"; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

544 
val sets = 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

545 
(case HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of thm)) of 
22271  546 
[_] => [pred_of (HOLogic.dest_Trueprop (hd (prems_of thm)))] 
547 
 xs => map (pred_of o fst o HOLogic.dest_imp) xs) 

15570  548 
handle TERM _ => err ()  Empty => err (); 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

549 
in 
18728  550 
add_ind_realizers (hd sets) 
551 
(case arg of 

15531  552 
NONE => sets  SOME NONE => [] 
15703  553 
 SOME (SOME sets') => sets \\ sets') 
20897  554 
end I); 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

555 

18728  556 
val ind_realizer = Attrib.syntax 
15703  557 
((Scan.option (Scan.lift (Args.$$$ "irrelevant")  
558 
Scan.option (Scan.lift (Args.colon)  

18728  559 
Scan.repeat1 Args.const))) >> rlz_attrib); 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

560 

18708  561 
val setup = 
18728  562 
Attrib.add_attributes [("ind_realizer", ind_realizer, "add realizers for inductive set")]; 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

563 

75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

564 
end; 
15706  565 