author  wenzelm 
Sat, 14 Dec 2013 17:28:05 +0100  
changeset 54742  7a86358a3c0b 
parent 52788  da1fdbfebd39 
child 55235  4b4627f5912b 
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 
Author: Stefan Berghofer, TU Muenchen 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

3 

36043  4 
Program extraction from proofs involving inductive predicates: 
29265
5b4247055bd7
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents:
28965
diff
changeset

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

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

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

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

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

13 

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

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

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

16 

33671  17 
(* FIXME: Local_Theory.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

18 
fun name_of_thm thm = 
28800  19 
(case Proofterm.fold_proof_atoms false (fn PThm (_, ((name, _, _), _)) => cons name  _ => I) 
28814  20 
[Thm.proof_of thm] [] of 
28800  21 
[name] => name 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31986
diff
changeset

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

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

24 
fun prf_of thm = 
44060  25 
Reconstruct.proof_of thm 
26 
> Reconstruct.expand_proof (Thm.theory_of_thm thm) [("", NONE)]; (* FIXME *) 

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

27 

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

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

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

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

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

32 

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

34 

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

43324
2b47822868e4
discontinued Name.variant to emphasize that this is oldstyle / indirect;
wenzelm
parents:
42375
diff
changeset

37 
[] => (singleton (Name.variant_list used) s, []) 
22271  38 
 name :: names' => (name, names')) 
39 
in strip_all' (s'::used) names' (subst_bound (Free (s', T), t)) end 

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

41 
t $ strip_all' used names Q 

42 
 strip_all' _ _ t = t; 

43 

29281  44 
fun strip_all t = strip_all' (Term.add_free_names t []) [] t; 
22271  45 

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

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

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

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

49 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset

50 
fun relevant_vars prop = fold (fn ((a, i), T) => fn vs => 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset

51 
(case strip_type T of 
36692
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36610
diff
changeset

52 
(_, Type (s, _)) => if s = @{type_name bool} then (a, T) :: vs else vs 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset

53 
 _ => vs)) (Term.add_vars prop []) []; 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset

54 

b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset

55 
val attach_typeS = map_types (map_atyps 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset

56 
(fn TFree (s, []) => TFree (s, HOLogic.typeS) 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset

57 
 TVar (ixn, []) => TVar (ixn, HOLogic.typeS) 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset

58 
 T => T)); 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

59 

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

61 
let 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset

62 
val iTs = rev (Term.add_tvars (prop_of (hd intrs)) []); 
22271  63 
val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop 
64 
(Logic.strip_imp_concl (prop_of (hd intrs)))); 

33957  65 
val params = map dest_Var (take nparms ts); 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30345
diff
changeset

66 
val tname = Binding.name (space_implode "_" (Long_Name.base_name s ^ "T" :: vs)); 
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30345
diff
changeset

67 
fun constr_of_intr intr = (Binding.name (Long_Name.base_name (name_of_thm intr)), 
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35625
diff
changeset

68 
map (Logic.unvarifyT_global o snd) (subtract (op =) params (rev (Term.add_vars (prop_of intr) []))) @ 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

69 
filter_out (equal Extraction.nullT) (map 
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35625
diff
changeset

70 
(Logic.unvarifyT_global o Extraction.etype_of thy vs []) (prems_of intr)), 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

71 
NoSyn); 
45839
43a5b86bc102
'datatype' specifications allow explicit sort constraints;
wenzelm
parents:
45701
diff
changeset

72 
in 
43a5b86bc102
'datatype' specifications allow explicit sort constraints;
wenzelm
parents:
45701
diff
changeset

73 
((tname, map (rpair dummyS) (map (fn a => "'" ^ a) vs @ map (fst o fst) iTs), NoSyn), 
43a5b86bc102
'datatype' specifications allow explicit sort constraints;
wenzelm
parents:
45701
diff
changeset

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

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

76 

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

77 
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

78 

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

80 

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

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

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset

84 
val U = TVar (("'" ^ a, 0), []) 
22271  85 
val Ts = binder_types T; 
86 
val i = length Ts; 

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

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

89 
in 

36692
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36610
diff
changeset

90 
if member (op =) vs a then 
46219
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset

91 
fold_rev Term.abs (("r", U) :: xs) (mk_rlz U $ Bound i $ u) 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset

92 
else 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset

93 
fold_rev Term.abs xs (mk_rlz Extraction.nullT $ Extraction.nullt $ u) 
22271  94 
end 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

96 

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

98 
let 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset

99 
val intr = map_types Type.strip_sorts (prop_of (hd intrs)); 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset

100 
val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl intr); 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset

101 
val iTs = rev (Term.add_tvars intr []); 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

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

106 
val predT = elTs > HOLogic.boolT; 

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

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

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

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

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

111 
else Type (space_implode "_" (s ^ "T" :: vs), 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset

112 
map (fn a => TVar (("'" ^ a, 0), [])) vs @ Tvs); 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30345
diff
changeset

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

115 
val rvs = relevant_vars S; 
33040  116 
val vs' = subtract (op =) vs (map fst rvs); 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

117 
val rname = space_implode "_" (s ^ "R" :: vs); 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

118 

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

119 
fun mk_Tprem n v = 
17485  120 
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

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

122 
Extraction.mk_typ (if n then Extraction.nullT 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset

123 
else TVar (("'" ^ v, 0), []))) 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

125 

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

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

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

129 

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

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

134 
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

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

136 

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

138 
let 
42361  139 
val ctxt = Proof_Context.init_global thy 
22271  140 
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

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

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

144 
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

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

146 

29271
1d685baea08e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29265
diff
changeset

147 
val is_rec = exists_Const (fn (c, _) => member (op =) rsets c); 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

148 

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

149 
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

150 
 is_meta (Const ("==>", _) $ _ $ Q) = is_meta Q 
35364  151 
 is_meta (Const (@{const_name Trueprop}, _) $ t) = 
152 
(case head_of t of 

153 
Const (s, _) => can (Inductive.the_inductive ctxt) s 

154 
 _ => true) 

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

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

156 

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

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

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

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

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

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

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

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

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

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

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

167 
val U = Extraction.etype_of thy vs [] prem'; 
46219
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset

168 
in 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset

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

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

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

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

173 
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

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

175 
end 
46219
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset

176 
else 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset

177 
(case strip_type T of 
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37236
diff
changeset

178 
(Ts, Type (@{type_name Product_Type.prod}, [T1, T2])) => 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

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

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

182 
val bs = map Bound (length Ts  1 downto 0); 
46219
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset

183 
val t = 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset

184 
fold_rev (Term.abs o pair "z") Ts 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset

185 
(HOLogic.mk_prod (list_comb (fx, bs), list_comb (fr, bs))); 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset

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

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

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

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

190 
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

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

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

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

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

195 
in if conclT = Extraction.nullT 
44241  196 
then fold_rev (absfree o dest_Free) xs HOLogic.unit 
197 
else fold_rev (absfree o dest_Free) xs 

198 
(list_comb 

199 
(Free ("r" ^ Long_Name.base_name (name_of_thm intr), 

200 
map fastype_of (rev args) > conclT), rev args)) 

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

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

202 

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

203 
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

204 

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

205 
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

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

207 
val concls = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct)); 
31986  208 
val premss = map_filter (fn (s, rs) => if member (op =) rsets s then 
209 
SOME (rs, map (fn (_, r) => nth (prems_of raw_induct) 

210 
(find_index (fn prp => prp = prop_of r) (map prop_of intrs))) rs) else NONE) rss; 

22271  211 
val fs = maps (fn ((intrs, prems), dummy) => 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

35364  215 
in 
216 
if dummy then Const (@{const_name default}, 

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; 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30345
diff
changeset

222 
fun name_of_fn intr = "r" ^ Long_Name.base_name (name_of_thm intr) 
22271  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 

44241  230 
in 
231 
(fold_rev absfree (("x", U) :: map_filter (fn intr => 

232 
Option.map (pair (name_of_fn intr)) 

233 
(AList.lookup (op =) frees (name_of_fn intr))) intrs) 

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

22271  235 
end 
236 
end) concls rec_names) 

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

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

238 

45839
43a5b86bc102
'datatype' specifications allow explicit sort constraints;
wenzelm
parents:
45701
diff
changeset

239 
fun add_dummy name dname (x as (_, ((s, vs, mx), cs))) = 
43a5b86bc102
'datatype' specifications allow explicit sort constraints;
wenzelm
parents:
45701
diff
changeset

240 
if Binding.eq_name (name, s) 
43a5b86bc102
'datatype' specifications allow explicit sort constraints;
wenzelm
parents:
45701
diff
changeset

241 
then (true, ((s, vs, mx), (dname, [HOLogic.unitT], NoSyn) :: cs)) 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

243 

18314  244 
fun add_dummies f [] _ thy = 
245 
(([], NONE), thy) 

246 
 add_dummies f dts used thy = 

247 
thy 

248 
> f (map snd dts) 

30345  249 
> (fn dtinfo => pair (map fst dts, SOME dtinfo)) 
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33957
diff
changeset

250 
handle Datatype_Aux.Datatype_Empty name' => 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

251 
let 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30345
diff
changeset

252 
val name = Long_Name.base_name name'; 
43324
2b47822868e4
discontinued Name.variant to emphasize that this is oldstyle / indirect;
wenzelm
parents:
42375
diff
changeset

253 
val dname = singleton (Name.variant_list used) "Dummy"; 
18314  254 
in 
255 
thy 

30345  256 
> add_dummies f (map (add_dummy (Binding.name name) (Binding.name dname)) dts) (dname :: used) 
14888
99ac3eb0f84e
add_dummies no longer uses transform_error but handles specific
berghofe
parents:
13928
diff
changeset

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

258 

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

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

261 
val rvs = map fst (relevant_vars (prop_of rule)); 
16861  262 
val xs = rev (Term.add_vars (prop_of rule) []); 
36692
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36610
diff
changeset

263 
val vs1 = map Var (filter_out (fn ((a, _), _) => member (op =) rvs a) xs); 
16861  264 
val rlzvs = rev (Term.add_vars (prop_of rrule) []); 
17485  265 
val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs; 
22271  266 
val rs = map Var (subtract (op = o pairself fst) xs rlzvs); 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset

267 
val rlz' = fold_rev Logic.all rs (prop_of rrule) 
22271  268 
in (name, (vs, 
33338  269 
if rt = Extraction.nullt then rt else fold_rev lambda vs1 rt, 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset

270 
Extraction.abs_corr_shyps thy rule vs vs2 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset

271 
(ProofRewriteRules.un_hhf_proof rlz' (attach_typeS rlz) 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset

272 
(fold_rev Proofterm.forall_intr_proof' rs (prf_of rrule))))) 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

274 

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

275 
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

276 

33244  277 
fun add_ind_realizer rsets intrs induct raw_induct elims vs thy = 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

278 
let 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30345
diff
changeset

279 
val qualifier = Long_Name.qualifier (name_of_thm induct); 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37678
diff
changeset

280 
val inducts = Global_Theory.get_thms thy (Long_Name.qualify qualifier "inducts"); 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset

281 
val iTs = rev (Term.add_tvars (prop_of (hd intrs)) []); 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

282 
val ar = length vs + length iTs; 
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31668
diff
changeset

283 
val params = Inductive.params_of raw_induct; 
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31668
diff
changeset

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

286 
val params' = map dest_Var params; 
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31668
diff
changeset

287 
val rss = Inductive.partition_rules raw_induct intrs; 
22271  288 
val rss' = map (fn (((s, rs), (_, arity)), elim) => 
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31668
diff
changeset

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

290 
(rss ~~ arities ~~ elims); 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30345
diff
changeset

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

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

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

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

295 
Sign.root_path > 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30345
diff
changeset

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

297 
val (ty_eqs, rlz_eqs) = split_list 
36692
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36610
diff
changeset

298 
(map (fn (s, rs) => mk_realizes_eqn (not (member (op =) rsets s)) vs nparms rs) rss); 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

299 

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

300 
val thy1' = thy1 > 
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42361
diff
changeset

301 
Sign.add_types_global 
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42361
diff
changeset

302 
(map (fn s => (Binding.name (Long_Name.base_name s), ar, NoSyn)) tnames) > 
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42361
diff
changeset

303 
Extraction.add_typeof_eqns_i ty_eqs; 
36692
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36610
diff
changeset

304 
val dts = map_filter (fn (s, rs) => if member (op =) rsets s then 
22271  305 
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

306 

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

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

308 

31783
cfbe9609ceb1
add_datatypes does not yield particular rules any longer
haftmann
parents:
31781
diff
changeset

309 
val ((dummies, some_dt_names), thy2) = 
18008  310 
thy1 
45701  311 
> add_dummies (Datatype.add_datatype {strict = false, quiet = false}) 
312 
(map (pair false) dts) [] 

18314  313 
> Extraction.add_typeof_eqns_i ty_eqs 
314 
> Extraction.add_realizes_eqns_i rlz_eqs; 

31783
cfbe9609ceb1
add_datatypes does not yield particular rules any longer
haftmann
parents:
31781
diff
changeset

315 
val dt_names = these some_dt_names; 
31784  316 
val case_thms = map (#case_rewrites o Datatype.the_info thy2) dt_names; 
45701  317 
val rec_thms = 
318 
if null dt_names then [] 

319 
else #rec_rewrites (Datatype.the_info thy2 (hd dt_names)); 

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

320 
val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o 
31781
861e675f01e6
add_datatype interface yields type names and less rules
haftmann
parents:
31723
diff
changeset

321 
HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) rec_thms); 
31458  322 
val (constrss, _) = fold_map (fn (s, rs) => fn (recs, dummies) => 
323 
if member (op =) rsets s then 

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

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

325 
val (d :: dummies') = dummies; 
19473  326 
val (recs1, recs2) = chop (length rs) (if d then tl recs else recs) 
31458  327 
in (map (head_of o hd o rev o snd o strip_comb o fst o 
328 
HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) recs1, (recs2, dummies')) 

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

329 
end 
31458  330 
else (replicate (length rs) Extraction.nullt, (recs, dummies))) 
31781
861e675f01e6
add_datatype interface yields type names and less rules
haftmann
parents:
31723
diff
changeset

331 
rss (rec_thms, dummies); 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset

332 
val rintrs = map (fn (intr, c) => attach_typeS (Envir.eta_contract 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

333 
(Extraction.realizes_of thy2 vs 
22271  334 
(if c = Extraction.nullt then c else list_comb (c, map Var (rev 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset

335 
(subtract (op =) params' (Term.add_vars (prop_of intr) []))))) (prop_of intr)))) 
32952  336 
(maps snd rss ~~ flat constrss); 
30345  337 
val (rlzpreds, rlzpreds') = 
338 
rintrs > map (fn rintr => 

22271  339 
let 
30345  340 
val Const (s, T) = head_of (HOLogic.dest_Trueprop (Logic.strip_assums_concl rintr)); 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30345
diff
changeset

341 
val s' = Long_Name.base_name s; 
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35625
diff
changeset

342 
val T' = Logic.unvarifyT_global T; 
30345  343 
in (((s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end) 
344 
> distinct (op = o pairself (#1 o #1)) 

345 
> map (apfst (apfst (apfst Binding.name))) 

346 
> split_list; 

347 

35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35625
diff
changeset

348 
val rlzparams = map (fn Var ((s, _), T) => (s, Logic.unvarifyT_global T)) 
22271  349 
(List.take (snd (strip_comb 
350 
(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

351 

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

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

353 

22271  354 
val (ind_info, thy3') = thy2 > 
33726
0878aecbf119
eliminated slightly odd name space grouping  now managed by Isar toplevel;
wenzelm
parents:
33671
diff
changeset

355 
Inductive.add_inductive_global 
33669  356 
{quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false, 
49170
03bee3a6a1b7
discontinued obsolete fork_mono to loosen some brakes  NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
wenzelm
parents:
47060
diff
changeset

357 
no_elim = false, no_ind = false, skip_mono = false} 
22271  358 
rlzpreds rlzparams (map (fn (rintr, intr) => 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30345
diff
changeset

359 
((Binding.name (Long_Name.base_name (name_of_thm intr)), []), 
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35625
diff
changeset

360 
subst_atomic rlzpreds' (Logic.unvarify_global rintr))) 
22271  361 
(rintrs ~~ maps snd rss)) [] > 
30435
e62d6ecab6ad
explicit Binding.qualified_name  prevents implicitly qualified bstring;
wenzelm
parents:
30364
diff
changeset

362 
Sign.root_path; 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37678
diff
changeset

363 
val thy3 = fold (Global_Theory.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

364 

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

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

366 

36692
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36610
diff
changeset

367 
val Ps = map_filter (fn _ $ M $ P => if member (op =) rsets (pred_of M) then 
15531  368 
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

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

370 

33244  371 
fun add_ind_realizer Ps thy = 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

373 
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

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

375 
(hd (prems_of (hd inducts))))), nparms))) vs; 
22271  376 
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

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

378 
val rlzs = map (fn (r, ind) => Extraction.realizes_of thy (vs' @ Ps) r 
22271  379 
(prop_of ind)) (rs ~~ inducts); 
29281  380 
val used = fold Term.add_free_names rlzs []; 
22271  381 
val rnames = Name.variant_list used (replicate (length inducts) "r"); 
382 
val rnames' = Name.variant_list 

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

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

385 
let 

35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35625
diff
changeset

386 
val (P, Q) = strip_one name (Logic.unvarify_global rlz); 
22271  387 
val Q' = strip_all' [] rnames' Q 
388 
in 

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

390 
end) (rlzs ~~ rnames); 

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

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

37136  393 
val rews = map mk_meta_eq (@{thm fst_conv} :: @{thm snd_conv} :: rec_thms); 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset

394 
val thm = Goal.prove_global thy [] 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset

395 
(map attach_typeS prems) (attach_typeS concl) 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52788
diff
changeset

396 
(fn {context = ctxt, prems} => EVERY 
22271  397 
[rtac (#raw_induct ind_info) 1, 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52788
diff
changeset

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

399 
REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY' 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52788
diff
changeset

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

401 
DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]); 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37678
diff
changeset

402 
val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_" 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30345
diff
changeset

403 
(Long_Name.qualify qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy; 
22271  404 
val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp))) 
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33957
diff
changeset

405 
(Datatype_Aux.split_conj_thm thm'); 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37678
diff
changeset

406 
val ([thms'], thy'') = Global_Theory.add_thmss 
30435
e62d6ecab6ad
explicit Binding.qualified_name  prevents implicitly qualified bstring;
wenzelm
parents:
30364
diff
changeset

407 
[((Binding.qualified_name (space_implode "_" 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30345
diff
changeset

408 
(Long_Name.qualify qualifier "inducts" :: vs' @ Ps @ 
29579  409 
["correctness"])), thms), [])] thy'; 
22271  410 
val realizers = inducts ~~ thms' ~~ rlzs ~~ rs; 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

412 
Extraction.add_realizers_i 
22271  413 
(map (fn (((ind, corr), rlz), r) => 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset

414 
mk_realizer thy'' (vs' @ Ps) (Thm.derivation_name ind, ind, corr, rlz, r)) 
22271  415 
realizers @ (case realizers of 
416 
[(((ind, corr), rlz), r)] => 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset

417 
[mk_realizer thy'' (vs' @ Ps) (Long_Name.qualify qualifier "induct", 
22271  418 
ind, corr, rlz, r)] 
419 
 _ => [])) thy'' 

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

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

421 

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

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

423 

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

424 
val case_names = map (fst o dest_Const o head_of o fst o HOLogic.dest_eq o 
31781
861e675f01e6
add_datatype interface yields type names and less rules
haftmann
parents:
31723
diff
changeset

425 
HOLogic.dest_Trueprop o prop_of o hd) case_thms; 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

426 

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

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

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

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

430 
val (prem :: prems) = prems_of elim; 
22271  431 
fun reorder1 (p, (_, intr)) = 
33244  432 
fold (fn ((s, _), T) => Logic.all (Free (s, T))) 
433 
(subtract (op =) params' (Term.add_vars (prop_of intr) [])) 

434 
(strip_all p); 

22271  435 
fun reorder2 ((ivs, intr), i) = 
33040  436 
let val fs = subtract (op =) params' (Term.add_vars (prop_of intr) []) 
33244  437 
in fold (lambda o Var) fs (list_comb (Bound (i + length ivs), ivs)) end; 
13921
69c627b6b28d
Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents:
13725
diff
changeset

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

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

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

441 
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

442 
val Ts = map (Extraction.etype_of thy (vs @ Ps) []) (prems_of elim); 
46219
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset

443 
val r = 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset

444 
if null Ps then Extraction.nullt 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset

445 
else 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset

446 
fold_rev (Term.abs o pair "x") Ts 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset

447 
(list_comb (Const (case_name, T), 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset

448 
(if dummy then 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset

449 
[Abs ("x", HOLogic.unitT, Const (@{const_name default}, body_type T))] 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset

450 
else []) @ 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset

451 
map reorder2 (intrs ~~ (length prems  1 downto 0)) @ 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45839
diff
changeset

452 
[Bound (length prems)])); 
22271  453 
val rlz = Extraction.realizes_of thy (vs @ Ps) r (prop_of elim); 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset

454 
val rlz' = attach_typeS (strip_all (Logic.unvarify_global rlz)); 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

455 
val rews = map mk_meta_eq case_thms; 
22271  456 
val thm = Goal.prove_global thy [] 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49170
diff
changeset

457 
(Logic.strip_imp_prems rlz') (Logic.strip_imp_concl rlz') 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49170
diff
changeset

458 
(fn {context = ctxt, prems, ...} => EVERY 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49170
diff
changeset

459 
[cut_tac (hd prems) 1, 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49170
diff
changeset

460 
etac elimR 1, 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49170
diff
changeset

461 
ALLGOALS (asm_simp_tac (put_simpset HOL_basic_ss ctxt)), 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52788
diff
changeset

462 
rewrite_goals_tac ctxt rews, 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52788
diff
changeset

463 
REPEAT ((resolve_tac prems THEN_ALL_NEW (Object_Logic.atomize_prems_tac ctxt THEN' 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
49170
diff
changeset

464 
DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]); 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
37678
diff
changeset

465 
val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_" 
29579  466 
(name_of_thm elim :: vs @ Ps @ ["correctness"])), thm) thy 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

468 
Extraction.add_realizers_i 
22271  469 
[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

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

471 

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

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

473 

33244  474 
val thy4 = fold add_ind_realizer (subsets Ps) thy3; 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

475 
val thy5 = Extraction.add_realizers_i 
22271  476 
(map (mk_realizer thy4 vs) (map (fn (((rule, rrule), rlz), c) => 
477 
(name_of_thm rule, rule, rrule, rlz, 

33040  478 
list_comb (c, map Var (subtract (op =) params' (rev (Term.add_vars (prop_of rule) [])))))) 
32952  479 
(maps snd rss ~~ #intrs ind_info ~~ rintrs ~~ flat constrss))) thy4; 
480 
val elimps = map_filter (fn ((s, intrs), p) => 

36692
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36610
diff
changeset

481 
if member (op =) rsets s then SOME (p, intrs) else NONE) 
22271  482 
(rss' ~~ (elims ~~ #elims ind_info)); 
33244  483 
val thy6 = 
484 
fold (fn p as (((((elim, _), _), _), _), _) => 

485 
add_elim_realizer [] p #> 

486 
add_elim_realizer [fst (fst (dest_Var (HOLogic.dest_Trueprop (concl_of elim))))] p) 

487 
(elimps ~~ case_thms ~~ case_names ~~ dummies) thy5; 

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

488 

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

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

490 

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

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

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

493 
val (_, {intrs, induct, raw_induct, elims, ...}) = 
42361  494 
Inductive.the_inductive (Proof_Context.init_global thy) name; 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

497 
in 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36945
diff
changeset

498 
fold_rev (add_ind_realizer rsets intrs induct raw_induct elims) vss thy 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

500 

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

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

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

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

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

47060
e2741ec9ae36
prefer explicitly qualified exception List.Empty;
wenzelm
parents:
46708
diff
changeset

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

509 
in 
18728  510 
add_ind_realizers (hd sets) 
511 
(case arg of 

15531  512 
NONE => sets  SOME NONE => [] 
33040  513 
 SOME (SOME sets') => subtract (op =) sets' sets) 
20897  514 
end I); 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

515 

18708  516 
val setup = 
30722
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30528
diff
changeset

517 
Attrib.setup @{binding ind_realizer} 
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30528
diff
changeset

518 
((Scan.option (Scan.lift (Args.$$$ "irrelevant")  
35402  519 
Scan.option (Scan.lift (Args.colon)  Scan.repeat1 (Args.const true)))) >> rlz_attrib) 
30722
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30528
diff
changeset

520 
"add realizers for inductive set"; 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

521 

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

522 
end; 
15706  523 