author  wenzelm 
Wed, 26 Apr 2006 22:38:05 +0200  
changeset 19473  d87a8838afa4 
parent 19046  bc5c6c9b114e 
child 19510  29fc4e5a638c 
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 

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

18 
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

19 

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

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

21 
let val {sign, prop, der = (_, prf), ...} = rep_thm thm 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

22 
in Reconstruct.reconstruct_proof sign prop prf end; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

23 

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

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

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

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 

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

33 
val set_of = fst o dest_Const o head_of o snd o HOLogic.dest_mem; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

34 

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

35 
fun strip_all t = 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

37 
fun strip used (Const ("all", _) $ Abs (s, T, t)) = 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

38 
let val s' = variant used s 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

39 
in strip (s'::used) (subst_bound (Free (s', T), t)) end 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

40 
 strip used ((t as Const ("==>", _) $ P) $ Q) = t $ strip used Q 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

42 
in strip (add_term_free_names (t, [])) t end; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

43 

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

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

45 
(Var ((a, i), T), vs) => (case strip_type T of 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

46 
(_, Type (s, _)) => if s mem ["bool", "set"] then (a, T) :: vs else vs 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

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

49 

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

50 
fun params_of intr = map (fst o fst o dest_Var) (term_vars 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

51 
(snd (HOLogic.dest_mem (HOLogic.dest_Trueprop 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

52 
(Logic.strip_imp_concl intr))))); 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

53 

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

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

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

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

57 
val Tvs = map TVar iTs; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

58 
val (_ $ (_ $ _ $ S)) = Logic.strip_imp_concl (prop_of (hd intrs)); 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

59 
val (Const (s, _), ts) = strip_comb S; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

60 
val params = map dest_Var ts; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

61 
val tname = space_implode "_" (Sign.base_name s ^ "T" :: vs); 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

62 
fun constr_of_intr intr = (Sign.base_name (Thm.name_of_thm intr), 
16861  63 
map (Type.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

64 
filter_out (equal Extraction.nullT) (map 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

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

67 
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

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

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

70 

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

71 
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

72 

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

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

74 

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

75 
fun gen_rvar vs (t as Var ((a, 0), T)) = 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

76 
let val U = TVar (("'" ^ a, 0), HOLogic.typeS) 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

77 
in case try HOLogic.dest_setT T of 
15531  78 
NONE => if body_type T <> HOLogic.boolT then t else 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

80 
val Ts = binder_types T; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

81 
val i = length Ts; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

82 
val xs = map (pair "x") Ts; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

83 
val u = list_comb (t, map Bound (i  1 downto 0)) 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

85 
if a mem vs then 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

86 
list_abs (("r", U) :: xs, mk_rlz U $ Bound i $ u) 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

87 
else list_abs (xs, mk_rlz Extraction.nullT $ Extraction.nullt $ u) 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

88 
end 
15531  89 
 SOME T' => if a mem vs then 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

90 
Abs ("r", U, Abs ("x", T', mk_rlz U $ Bound 1 $ 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

91 
(HOLogic.mk_mem (Bound 0, t)))) 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

92 
else Abs ("x", T', mk_rlz Extraction.nullT $ Extraction.nullt $ 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

93 
(HOLogic.mk_mem (Bound 0, t))) 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

94 
end 
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 

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

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

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

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

100 
val Tvs = map TVar iTs; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

101 
val _ $ (_ $ _ $ S) = concl_of (hd intrs); 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

102 
val (Const (s, T), ts') = strip_comb S; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

103 
val setT = body_type T; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

104 
val elT = HOLogic.dest_setT setT; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

105 
val x = Var (("x", 0), elT); 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

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

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

109 
val r = if n then Extraction.nullt else Var ((Sign.base_name s, 0), rT); 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

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

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

113 

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

114 
fun mk_Tprem n v = 
17485  115 
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

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

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

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

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

120 

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

121 
val prems = map (mk_Tprem true) vs' @ map (mk_Tprem false) vs; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

122 
val ts = map (gen_rvar vs) ts'; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

124 

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

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

126 
Extraction.mk_typ rT)), 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

127 
(prems, (mk_rlz rT $ r $ HOLogic.mk_mem (x, S), 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

128 
if n then 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

129 
HOLogic.mk_mem (x, list_comb (Const (rname, argTs > setT), ts)) 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

130 
else HOLogic.mk_mem (HOLogic.mk_prod (r, x), list_comb (Const (rname, 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

131 
argTs > HOLogic.mk_setT (HOLogic.mk_prodT (rT, elT))), ts))))) 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

133 

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

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

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

136 
(* add_term_vars and Term.add_vars may return variables in different order *) 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

137 
val args = map (Free o apfst fst o dest_Var) 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

138 
(add_term_vars (prop_of intr, []) \\ map Var params); 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

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

142 
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

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

144 

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

145 
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

146 

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

147 
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

148 
 is_meta (Const ("==>", _) $ _ $ Q) = is_meta Q 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

149 
 is_meta (Const ("Trueprop", _) $ (Const ("op :", _) $ _ $ _)) = true 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

151 

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

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

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

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

155 
val [x, r] = variantlist (["x", "r"], used) 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

167 
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

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

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

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

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

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

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

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

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

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

177 
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

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

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

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

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

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

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

184 
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

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

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

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

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

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

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

191 
else list_abs_free (map dest_Free xs, list_comb 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

192 
(Free ("r" ^ Sign.base_name (Thm.name_of_thm intr), 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

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

196 
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

197 

18008  198 
fun find_first f = Library.find_first f; 
199 

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

200 
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

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

202 
val concls = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct)); 
15570  203 
val premss = List.mapPartial (fn (s, rs) => if s mem rsets then 
204 
SOME (map (fn r => List.nth (prems_of raw_induct, 

205 
find_index_eq (prop_of r) (map prop_of intrs))) rs) else NONE) rss; 

206 
val concls' = List.mapPartial (fn (s, _) => if s mem rsets then 

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

207 
find_first (fn concl => s mem term_consts concl) concls 
15531  208 
else NONE) rss; 
15570  209 
val fs = List.concat (snd (foldl_map (fn (intrs, (prems, dummy)) => 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

210 
let 
19473  211 
val (intrs1, intrs2) = chop (length prems) intrs; 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

212 
val fs = map (fn (rule, intr) => 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

213 
fun_of_prem thy rsets vs params rule intr) (prems ~~ intrs1) 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

214 
in (intrs2, if dummy then Const ("arbitrary", 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

215 
HOLogic.unitT > body_type (fastype_of (hd fs))) :: fs 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

216 
else fs) 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

217 
end) (intrs, (premss ~~ dummies)))); 
16861  218 
val frees = fold Term.add_frees fs []; 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

219 
val Ts = map fastype_of fs; 
15570  220 
val rlzs = List.mapPartial (fn (a, concl) => 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

221 
let val T = Extraction.etype_of thy vs [] concl 
15531  222 
in if T = Extraction.nullT then NONE 
223 
else SOME (list_comb (Const (a, Ts > T), fs)) 

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

224 
end) (rec_names ~~ concls') 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

225 
in if null rlzs then Extraction.nullt else 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

227 
val r = foldr1 HOLogic.mk_prod rlzs; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

228 
val x = Free ("x", Extraction.etype_of thy vs [] (hd (prems_of induct))); 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

229 
fun name_of_fn intr = "r" ^ Sign.base_name (Thm.name_of_thm intr); 
15570  230 
val r' = list_abs_free (List.mapPartial (fn intr => 
17485  231 
Option.map (pair (name_of_fn intr)) (AList.lookup (op =) frees (name_of_fn intr))) intrs, 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

232 
if length concls = 1 then r $ x else r) 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

234 
if length concls = 1 then lambda x r' else r' 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

239 
if name = s then (true, (vs, s, mfx, (dname, [HOLogic.unitT], NoSyn) :: cs)) 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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'; 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

251 
val dname = 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 

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

257 
fun mk_realizer thy vs params ((rule, rrule), rt) = 
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 prems = prems_of rule ~~ prems_of rrule; 
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13710
diff
changeset

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

262 
val vs1 = map Var (filter_out (fn ((a, _), _) => a mem rvs) xs); 
16861  263 
val rlzvs = rev (Term.add_vars (prop_of rrule) []); 
17485  264 
val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs; 
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13710
diff
changeset

265 
val rs = gen_rems (op = o pairself fst) (rlzvs, xs); 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

266 

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

267 
fun mk_prf _ [] prf = prf 
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13710
diff
changeset

268 
 mk_prf rs ((prem, rprem) :: prems) prf = 
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13710
diff
changeset

269 
if Extraction.etype_of thy vs [] prem = Extraction.nullT 
15531  270 
then AbsP ("H", SOME rprem, mk_prf rs prems prf) 
271 
else forall_intr_prf (Var (hd rs), AbsP ("H", SOME rprem, 

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

272 
mk_prf (tl rs) prems prf)); 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

273 

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

274 
in (Thm.name_of_thm rule, (vs, 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

276 
foldr (uncurry lambda) rt vs1, 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

277 
foldr forall_intr_prf (mk_prf rs prems (Proofterm.proof_combP 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

278 
(prf_of rrule, map PBound (length prems  1 downto 0)))) vs2)) 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

280 

17485  281 
fun add_rule r rss = 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

283 
val _ $ (_ $ _ $ S) = concl_of r; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

284 
val (Const (s, _), _) = strip_comb S; 
17485  285 
in 
286 
rss 

287 
> AList.default (op =) (s, []) 

288 
> AList.map_entry (op =) s (fn rs => rs @ [r]) 

289 
end; 

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

290 

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

291 
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

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

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

294 
val ar = length vs + length iTs; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

295 
val (_ $ (_ $ _ $ S)) = Logic.strip_imp_concl (prop_of (hd intrs)); 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

296 
val (_, params) = strip_comb S; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

297 
val params' = map dest_Var params; 
17485  298 
val rss = [] > Library.fold add_rule intrs; 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

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

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

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

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

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

305 
val (ty_eqs, rlz_eqs) = split_list 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

307 

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

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

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

310 
Theory.add_types (map (fn s => (Sign.base_name s, ar, NoSyn)) tnames) > 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

311 
Theory.add_arities_i (map (fn s => 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

312 
(s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames) > 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

316 

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

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

318 

18314  319 
val ((dummies, dt_info), thy2) = 
18008  320 
thy1 
18314  321 
> add_dummies 
322 
(DatatypePackage.add_datatype_i false false (map #2 dts)) 

323 
(map (pair false) dts) [] 

324 
> Extraction.add_typeof_eqns_i ty_eqs 

325 
> Extraction.add_realizes_eqns_i rlz_eqs; 

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

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

327 
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

328 
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

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

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

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

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

334 
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

335 
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

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

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

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

340 
(Extraction.realizes_of thy2 vs 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

341 
c (prop_of (forall_intr_list (map (cterm_of (sign_of thy2) o Var) 
16861  342 
(rev (Term.add_vars (prop_of intr) []) \\ params')) intr)))) 
15570  343 
(intrs ~~ List.concat constrss); 
19046
bc5c6c9b114e
removed distinct, renamed gen_distinct to distinct;
wenzelm
parents:
18929
diff
changeset

344 
val rlzsets = distinct (op =) (map (fn rintr => snd (HOLogic.dest_mem 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

345 
(HOLogic.dest_Trueprop (Logic.strip_assums_concl rintr)))) rintrs); 
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 

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

349 
val (thy3', ind_info) = thy2 > 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

350 
InductivePackage.add_inductive_i false true "" false false false 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

351 
(map Logic.unvarify rlzsets) (map (fn (rintr, intr) => 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

352 
((Sign.base_name (Thm.name_of_thm intr), strip_all 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

353 
(Logic.unvarify rintr)), [])) (rintrs ~~ intrs)) [] >> 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

355 
val thy3 = PureThy.hide_thms false 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

356 
(map Thm.name_of_thm (#intrs ind_info)) thy3'; 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

357 

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

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

359 

15570  360 
val Ps = List.mapPartial (fn _ $ M $ P => if set_of M mem rsets then 
15531  361 
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

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

363 

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

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

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

366 
val r = indrule_realizer thy induct raw_induct rsets params' 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

367 
(vs @ Ps) rec_names rss intrs dummies; 
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13710
diff
changeset

368 
val rlz = strip_all (Logic.unvarify 
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13710
diff
changeset

369 
(Extraction.realizes_of thy (vs @ Ps) r (prop_of induct))); 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

371 
(fst_conv :: snd_conv :: get #rec_thms dt_info); 
17959  372 
val thm = OldGoals.simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems => 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

373 
[if length rss = 1 then 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

374 
cut_facts_tac [hd prems] 1 THEN etac (#induct ind_info) 1 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

375 
else EVERY [rewrite_goals_tac (rews @ all_simps), 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

376 
REPEAT (rtac allI 1), rtac (#induct ind_info) 1], 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

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

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

380 
DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]); 
18358  381 
val (thm', thy') = PureThy.store_thm ((space_implode "_" 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

382 
(Thm.name_of_thm induct :: vs @ Ps @ ["correctness"]), thm), []) thy 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

384 
Extraction.add_realizers_i 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

385 
[mk_realizer thy' (vs @ Ps) params' ((induct, thm'), r)] thy' 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

387 

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

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

389 

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

390 
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

391 
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

392 

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

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

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

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

396 
val (prem :: prems) = prems_of elim; 
13921
69c627b6b28d
Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents:
13725
diff
changeset

397 
fun reorder1 (p, intr) = 
15570  398 
Library.foldl (fn (t, ((s, _), T)) => all T $ lambda (Free (s, T)) t) 
16861  399 
(strip_all p, Term.add_vars (prop_of intr) [] \\ params'); 
13921
69c627b6b28d
Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents:
13725
diff
changeset

400 
fun reorder2 (intr, i) = 
69c627b6b28d
Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents:
13725
diff
changeset

401 
let 
13928
d572aeea3ff3
Fixed problem in add_elim_realizer (concerning inductive predicates with
berghofe
parents:
13921
diff
changeset

402 
val fs1 = term_vars (prop_of intr) \\ params; 
16861  403 
val fs2 = Term.add_vars (prop_of intr) [] \\ params' 
15570  404 
in Library.foldl (fn (t, x) => lambda (Var x) t) 
13921
69c627b6b28d
Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents:
13725
diff
changeset

405 
(list_comb (Bound (i + length fs1), fs1), fs2) 
69c627b6b28d
Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents:
13725
diff
changeset

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

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

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

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

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

411 
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

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

413 
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

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

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

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

417 
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

418 
[Bound (length prems)])); 
13725
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13710
diff
changeset

419 
val rlz = strip_all (Logic.unvarify 
12404b452034
Changed format of realizers / correctness proofs.
berghofe
parents:
13710
diff
changeset

420 
(Extraction.realizes_of thy (vs @ Ps) r (prop_of elim))); 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

421 
val rews = map mk_meta_eq case_thms; 
17959  422 
val thm = OldGoals.simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems => 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

424 
etac elimR 1, 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

425 
ALLGOALS (EVERY' [etac Pair_inject, asm_simp_tac HOL_basic_ss]), 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

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

428 
DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]); 
18358  429 
val (thm', thy') = PureThy.store_thm ((space_implode "_" 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

430 
(Thm.name_of_thm elim :: vs @ Ps @ ["correctness"]), thm), []) thy 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

432 
Extraction.add_realizers_i 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

433 
[mk_realizer thy' (vs @ Ps) params' ((elim, thm'), r)] thy' 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

435 

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

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

437 

15570  438 
val rintr_thms = List.concat (map (fn (_, rs) => map (fn r => List.nth 
439 
(#intrs ind_info, find_index_eq r intrs)) rs) rss); 

440 
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

441 
val thy5 = Extraction.add_realizers_i 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

442 
(map (mk_realizer thy4 vs params') 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

443 
(map (fn ((rule, rrule), c) => ((rule, rrule), list_comb (c, 
16861  444 
map Var (rev (Term.add_vars (prop_of rule) []) \\ params')))) 
15570  445 
(List.concat (map snd rss) ~~ rintr_thms ~~ List.concat constrss))) thy4; 
446 
val elimps = List.mapPartial (fn (s, intrs) => if s mem rsets then 

447 
Option.map (rpair intrs) (find_first (fn (thm, _) => 

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

448 
s mem term_consts (hd (prems_of thm))) (elims ~~ #elims ind_info)) 
15531  449 
else NONE) rss; 
15570  450 
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

451 
add_elim_realizer [] p > add_elim_realizer [fst (fst (dest_Var 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

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

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

454 

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

456 

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

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

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

459 
val (_, {intrs, induct, raw_induct, elims, ...}) = 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

460 
(case InductivePackage.get_inductive thy name of 
15531  461 
NONE => error ("Unknown inductive set " ^ quote name) 
462 
 SOME info => info); 

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

463 
val _ $ (_ $ _ $ S) = concl_of (hd intrs); 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

464 
val vss = sort (int_ord o pairself length) 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

465 
(subsets (map fst (relevant_vars S))) 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

466 
in 
15570  467 
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

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

469 

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

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

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

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

474 
(case HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of thm)) of 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

475 
[_] => [set_of (HOLogic.dest_Trueprop (hd (prems_of thm)))] 
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

476 
 xs => map (set_of o fst o HOLogic.dest_imp) xs) 
15570  477 
handle TERM _ => err ()  Empty => err (); 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

478 
in 
18728  479 
add_ind_realizers (hd sets) 
480 
(case arg of 

15531  481 
NONE => sets  SOME NONE => [] 
15703  482 
 SOME (SOME sets') => sets \\ sets') 
18728  483 
end); 
13710
75bec2c1bfd5
New package for constructing realizers for introduction and elimination
berghofe
parents:
diff
changeset

484 

18728  485 
val ind_realizer = Attrib.syntax 
15703  486 
((Scan.option (Scan.lift (Args.$$$ "irrelevant")  
487 
Scan.option (Scan.lift (Args.colon)  

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

489 

18708  490 
val setup = 
18728  491 
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

492 

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

493 
end; 
15706  494 