author  wenzelm 
Sat, 15 Nov 2008 21:31:19 +0100  
changeset 28800  48f7bfebd31d 
parent 28328  9a647179c1e6 
child 28814  463c9e9111ae 
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 

28800  18 
(* FIXME: LocalTheory.note should return theorems with proper names! *) (* FIXME ?? *) 
22606
962f824c2df9
 Tried to make name_of_thm more robust against changes of the
berghofe
parents:
22596
diff
changeset

19 
fun name_of_thm thm = 
28800  20 
(case Proofterm.fold_proof_atoms false (fn PThm (_, ((name, _, _), _)) => cons name  _ => I) 
21 
[Proofterm.proof_of (Thm.proof_of thm)] [] of 

22 
[name] => name 

23 
 _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm thm)); 

22271  24 

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

25 
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

26 

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

27 
fun prf_of thm = 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26535
diff
changeset

28 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26535
diff
changeset

29 
val thy = Thm.theory_of_thm thm; 
28800  30 
val thm' = 
31 
Reconstruct.reconstruct_proof thy (Thm.prop_of thm) (Proofterm.proof_of (Thm.proof_of thm)); 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26535
diff
changeset

32 
in Reconstruct.expand_proof thy [("", NONE)] thm' end; (* FIXME *) 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

33 

27330  34 
fun forall_intr_prf t prf = 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

35 
let val (a, T) = (case t of Var ((a, _), T) => (a, T)  Free p => p) 
15531  36 
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

37 

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

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

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

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

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

42 

22271  43 
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

44 

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

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

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

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

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

51 
t $ strip_all' used names Q 

52 
 strip_all' _ _ t = t; 

53 

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

55 

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

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

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

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

59 

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

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

61 
(Var ((a, i), T), vs) => (case strip_type T of 
22271  62 
(_, 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

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

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

65 

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

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

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

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

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

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

73 
val tname = space_implode "_" (Sign.base_name s ^ "T" :: vs); 
22271  74 
fun constr_of_intr intr = (Sign.base_name (name_of_thm intr), 
19806  75 
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

76 
filter_out (equal Extraction.nullT) (map 
19806  77 
(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

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

79 
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

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

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

82 

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

83 
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

84 

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

86 

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

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

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

91 
val Ts = binder_types T; 

92 
val i = length Ts; 

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

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

95 
in 

96 
if a mem vs then 

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

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

99 
end 

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

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

101 

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

103 
let 
22271  104 
val concl = HOLogic.dest_Trueprop (concl_of (hd intrs)); 
105 
val iTs = term_tvars concl; 

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

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

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

110 
val predT = elTs > HOLogic.boolT; 

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

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

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

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

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

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

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

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

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

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

121 
val rname = space_implode "_" (s ^ "R" :: vs); 
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_Tprem n v = 
17485  124 
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

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

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

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

128 
end; 
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 
val prems = map (mk_Tprem true) vs' @ map (mk_Tprem false) vs; 
22271  131 
val ts = map (gen_rvar vs) params; 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

133 

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

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

138 
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

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

140 

22271  141 
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

142 
let 
22271  143 
val ctxt = ProofContext.init thy 
144 
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

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

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

148 
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

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

150 

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

151 
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

152 

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

153 
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

154 
 is_meta (Const ("==>", _) $ _ $ Q) = is_meta Q 
22271  155 
 is_meta (Const ("Trueprop", _) $ t) = (case head_of t of 
156 
Const (s, _) => can (InductivePackage.the_inductive ctxt) s 

157 
 _ => true) 

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

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

159 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

175 
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

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

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

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

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

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

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

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

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

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

185 
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

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

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

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

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

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

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

192 
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

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

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

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

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

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

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

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

201 
map fastype_of (rev args) > conclT), rev args)) 
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 

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

204 
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

205 

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

206 
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

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

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

213 
let 
22271  214 
val fs = map (fn (rule, (ivs, intr)) => 
215 
fun_of_prem thy rsets vs params rule ivs intr) (prems ~~ intrs) 

27982  216 
in if dummy then Const ("HOL.default_class.default", 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

217 
HOLogic.unitT > body_type (fastype_of (hd fs))) :: fs 
22271  218 
else fs 
219 
end) (premss ~~ dummies); 

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

221 
val Ts = map fastype_of fs; 
22271  222 
fun name_of_fn intr = "r" ^ Sign.base_name (name_of_thm intr) 
223 
in 

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

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

225 
let val T = Extraction.etype_of thy vs [] concl 
22271  226 
in if T = Extraction.nullT then (Extraction.nullt, names) else 
227 
let 

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

229 
val a :: names' = names 

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

231 
Option.map (pair (name_of_fn intr)) 

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

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

234 
end 

235 
end) concls rec_names) 

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

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

237 

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

238 
fun add_dummy name dname (x as (_, (vs, s, mfx, cs))) = 
23577  239 
if (name: string) = s then (true, (vs, s, mfx, (dname, [HOLogic.unitT], NoSyn) :: cs)) 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

241 

18314  242 
fun add_dummies f [] _ thy = 
243 
(([], NONE), thy) 

244 
 add_dummies f dts used thy = 

245 
thy 

246 
> f (map snd dts) 

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

248 
handle DatatypeAux.Datatype_Empty name' => 

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

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

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

251 
val dname = Name.variant used "Dummy" 
18314  252 
in 
253 
thy 

254 
> 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

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

256 

22271  257 
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

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

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

261 
val vs1 = map Var (filter_out (fn ((a, _), _) => a mem rvs) xs); 
16861  262 
val rlzvs = rev (Term.add_vars (prop_of rrule) []); 
17485  263 
val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs; 
22271  264 
val rs = map Var (subtract (op = o pairself fst) xs rlzvs); 
27330  265 
val rlz' = fold_rev Logic.all (vs2 @ rs) (prop_of rrule); 
266 
val rlz'' = fold_rev Logic.all vs2 rlz 

22271  267 
in (name, (vs, 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

269 
foldr (uncurry lambda) rt vs1, 
22271  270 
ProofRewriteRules.un_hhf_proof rlz' rlz'' 
27330  271 
(fold_rev forall_intr_prf (vs2 @ rs) (prf_of rrule)))) 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

273 

24157
409cd6eaa7ea
Added renaming function to prevent correctness proof for realizer
berghofe
parents:
23590
diff
changeset

274 
fun rename tab = map (fn x => the_default x (AList.lookup op = tab x)); 
409cd6eaa7ea
Added renaming function to prevent correctness proof for realizer
berghofe
parents:
23590
diff
changeset

275 

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

276 
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

277 
let 
22271  278 
val qualifier = NameSpace.qualifier (name_of_thm induct); 
26343
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset

279 
val inducts = PureThy.get_thms thy (NameSpace.qualified qualifier "inducts"); 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

281 
val ar = length vs + length iTs; 
22790
e1cff9268177
Moved functions infer_intro_vars, arities_of, params_of, and
berghofe
parents:
22606
diff
changeset

282 
val params = InductivePackage.params_of raw_induct; 
e1cff9268177
Moved functions infer_intro_vars, arities_of, params_of, and
berghofe
parents:
22606
diff
changeset

283 
val arities = InductivePackage.arities_of raw_induct; 
22271  284 
val nparms = length params; 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

285 
val params' = map dest_Var params; 
22790
e1cff9268177
Moved functions infer_intro_vars, arities_of, params_of, and
berghofe
parents:
22606
diff
changeset

286 
val rss = InductivePackage.partition_rules raw_induct intrs; 
22271  287 
val rss' = map (fn (((s, rs), (_, arity)), elim) => 
22790
e1cff9268177
Moved functions infer_intro_vars, arities_of, params_of, and
berghofe
parents:
22606
diff
changeset

288 
(s, (InductivePackage.infer_intro_vars elim arity rs ~~ rs))) 
e1cff9268177
Moved functions infer_intro_vars, arities_of, params_of, and
berghofe
parents:
22606
diff
changeset

289 
(rss ~~ arities ~~ elims); 
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
21646
diff
changeset

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

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

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

293 
val thy1 = thy > 
24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24157
diff
changeset

294 
Sign.root_path > 
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24157
diff
changeset

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

296 
val (ty_eqs, rlz_eqs) = split_list 
22271  297 
(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

298 

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

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

300 
Theory.copy > 
24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24157
diff
changeset

301 
Sign.add_types (map (fn s => (Sign.base_name s, ar, NoSyn)) tnames) > 
24926
bcb6b098df11
AxClass.axiomatize: renamed XXX_i to XXX, and XXX to XXX_cmd;
wenzelm
parents:
24816
diff
changeset

302 
fold (fn s => AxClass.axiomatize_arity 
19510  303 
(s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames > 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

304 
Extraction.add_typeof_eqns_i ty_eqs; 
15570  305 
val dts = List.mapPartial (fn (s, rs) => if s mem rsets then 
22271  306 
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

307 

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

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

309 

18314  310 
val ((dummies, dt_info), thy2) = 
18008  311 
thy1 
18314  312 
> add_dummies 
27112  313 
(DatatypePackage.add_datatype false false (map #2 dts)) 
18314  314 
(map (pair false) dts) [] 
315 
> Extraction.add_typeof_eqns_i ty_eqs 

316 
> Extraction.add_realizes_eqns_i rlz_eqs; 

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

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

318 
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

319 
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

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

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

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

323 
val (d :: dummies') = dummies; 
19473  324 
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

325 
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

326 
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

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

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

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

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

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

335 
val (rlzpreds, rlzpreds') = split_list 

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

337 
let 

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

339 
(Logic.strip_assums_concl rintr)); 

340 
val s' = Sign.base_name s; 

341 
val T' = Logic.unvarifyT T 

28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27982
diff
changeset

342 
in (((Name.binding s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end) rintrs)); 
24746
6d42be359d57
Adapted to changes in interface of add_inductive_i.
berghofe
parents:
24712
diff
changeset

343 
val rlzparams = map (fn Var ((s, _), T) => (s, Logic.unvarifyT T)) 
22271  344 
(List.take (snd (strip_comb 
345 
(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

346 

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

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

348 

22271  349 
val (ind_info, thy3') = thy2 > 
26128  350 
InductivePackage.add_inductive_global (serial_string ()) 
28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27982
diff
changeset

351 
{quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = Name.no_binding, 
26535
66bca8a4079c
Added skip_mono flag to inductive definition package.
berghofe
parents:
26481
diff
changeset

352 
coind = false, no_elim = false, no_ind = false, skip_mono = false} 
22271  353 
rlzpreds rlzparams (map (fn (rintr, intr) => 
28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27982
diff
changeset

354 
((Name.binding (Sign.base_name (name_of_thm intr)), []), 
22271  355 
subst_atomic rlzpreds' (Logic.unvarify rintr))) 
356 
(rintrs ~~ maps snd rss)) [] > 

24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24157
diff
changeset

357 
Sign.absolute_path; 
26663  358 
val thy3 = fold (PureThy.hide_fact false o name_of_thm) (#intrs ind_info) thy3'; 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

359 

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

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

361 

22271  362 
val Ps = List.mapPartial (fn _ $ M $ P => if pred_of M mem rsets then 
15531  363 
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

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

365 

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

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

367 
let 
24157
409cd6eaa7ea
Added renaming function to prevent correctness proof for realizer
berghofe
parents:
23590
diff
changeset

368 
val vs' = rename (map (pairself (fst o fst o dest_Var)) 
409cd6eaa7ea
Added renaming function to prevent correctness proof for realizer
berghofe
parents:
23590
diff
changeset

369 
(params ~~ List.take (snd (strip_comb (HOLogic.dest_Trueprop 
409cd6eaa7ea
Added renaming function to prevent correctness proof for realizer
berghofe
parents:
23590
diff
changeset

370 
(hd (prems_of (hd inducts))))), nparms))) vs; 
22271  371 
val rs = indrule_realizer thy induct raw_induct rsets params' 
24157
409cd6eaa7ea
Added renaming function to prevent correctness proof for realizer
berghofe
parents:
23590
diff
changeset

372 
(vs' @ Ps) rec_names rss' intrs dummies; 
409cd6eaa7ea
Added renaming function to prevent correctness proof for realizer
berghofe
parents:
23590
diff
changeset

373 
val rlzs = map (fn (r, ind) => Extraction.realizes_of thy (vs' @ Ps) r 
22271  374 
(prop_of ind)) (rs ~~ inducts); 
375 
val used = foldr add_term_free_names [] rlzs; 

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

377 
val rnames' = Name.variant_list 

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

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

380 
let 

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

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

383 
in 

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

385 
end) (rlzs ~~ rnames); 

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

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

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

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

389 
(fst_conv :: snd_conv :: get #rec_thms dt_info); 
26711  390 
val thm = Goal.prove_global thy [] prems concl (fn {prems, ...} => EVERY 
22271  391 
[rtac (#raw_induct ind_info) 1, 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

393 
REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY' 
23590
ad95084a5c63
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23577
diff
changeset

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

395 
DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]); 
26481  396 
val (thm', thy') = PureThy.store_thm (space_implode "_" 
397 
(NameSpace.qualified qualifier "induct" :: vs' @ Ps @ ["correctness"]), thm) thy; 

22271  398 
val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp))) 
399 
(DatatypeAux.split_conj_thm thm'); 

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

401 
[((space_implode "_" 

24157
409cd6eaa7ea
Added renaming function to prevent correctness proof for realizer
berghofe
parents:
23590
diff
changeset

402 
(NameSpace.qualified qualifier "inducts" :: vs' @ Ps @ 
22271  403 
["correctness"]), thms), [])] thy'; 
404 
val realizers = inducts ~~ thms' ~~ rlzs ~~ rs; 

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

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

406 
Extraction.add_realizers_i 
22271  407 
(map (fn (((ind, corr), rlz), r) => 
24157
409cd6eaa7ea
Added renaming function to prevent correctness proof for realizer
berghofe
parents:
23590
diff
changeset

408 
mk_realizer thy' (vs' @ Ps) (Thm.get_name ind, ind, corr, rlz, r)) 
22271  409 
realizers @ (case realizers of 
410 
[(((ind, corr), rlz), r)] => 

24157
409cd6eaa7ea
Added renaming function to prevent correctness proof for realizer
berghofe
parents:
23590
diff
changeset

411 
[mk_realizer thy' (vs' @ Ps) (NameSpace.qualified qualifier "induct", 
22271  412 
ind, corr, rlz, r)] 
413 
 _ => [])) thy'' 

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

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

415 

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

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

417 

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

418 
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

419 
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

420 

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

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

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

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

424 
val (prem :: prems) = prems_of elim; 
22271  425 
fun reorder1 (p, (_, intr)) = 
27330  426 
Library.foldl (fn (t, ((s, _), T)) => Logic.all (Free (s, T)) t) 
16861  427 
(strip_all p, Term.add_vars (prop_of intr) [] \\ params'); 
22271  428 
fun reorder2 ((ivs, intr), i) = 
429 
let val fs = Term.add_vars (prop_of intr) [] \\ params' 

15570  430 
in Library.foldl (fn (t, x) => lambda (Var x) t) 
22271  431 
(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

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

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

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

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

436 
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

437 
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

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

439 
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

440 
(if dummy then 
27982  441 
[Abs ("x", HOLogic.unitT, Const ("HOL.default_class.default", body_type T))] 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

443 
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

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

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

447 
val rews = map mk_meta_eq case_thms; 
22271  448 
val thm = Goal.prove_global thy [] 
26711  449 
(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

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

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

453 
rewrite_goals_tac rews, 
23590
ad95084a5c63
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23577
diff
changeset

454 
REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_prems_tac THEN' 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

455 
DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]); 
26481  456 
val (thm', thy') = PureThy.store_thm (space_implode "_" 
457 
(name_of_thm elim :: vs @ Ps @ ["correctness"]), thm) thy 

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

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

459 
Extraction.add_realizers_i 
22271  460 
[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

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

462 

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

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

464 

15570  465 
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

466 
val thy5 = Extraction.add_realizers_i 
22271  467 
(map (mk_realizer thy4 vs) (map (fn (((rule, rrule), rlz), c) => 
468 
(name_of_thm rule, rule, rrule, rlz, 

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

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

471 
List.concat constrss))) thy4; 

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

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

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

15570  475 
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

476 
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

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

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

479 

24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24157
diff
changeset

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

481 

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

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

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

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

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

488 
in 
15570  489 
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

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

491 

20897  492 
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

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

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

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

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

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

500 
in 
18728  501 
add_ind_realizers (hd sets) 
502 
(case arg of 

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

506 

18728  507 
val ind_realizer = Attrib.syntax 
15703  508 
((Scan.option (Scan.lift (Args.$$$ "irrelevant")  
509 
Scan.option (Scan.lift (Args.colon)  

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

511 

18708  512 
val setup = 
18728  513 
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

514 

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

515 
end; 
15706  516 