author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46961  5c6955f487e5 
child 54742  7a86358a3c0b 
permissions  rwrr 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

1 
(* Title: HOL/Nominal/nominal_primrec.ML 
29265
5b4247055bd7
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents:
29097
diff
changeset

2 
Author: Norbert Voelker, FernUni Hagen 
5b4247055bd7
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents:
29097
diff
changeset

3 
Author: Stefan Berghofer, TU Muenchen 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

4 

ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

5 
Package for defining functions on nominal datatypes by primitive recursion. 
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31177
diff
changeset

6 
Taken from HOL/Tools/primrec.ML 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

7 
*) 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

8 

ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

9 
signature NOMINAL_PRIMREC = 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

10 
sig 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

11 
val add_primrec: term list option > term option > 
29581  12 
(binding * typ option * mixfix) list > 
13 
(binding * typ option * mixfix) list > 

29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

14 
(Attrib.binding * term) list > local_theory > Proof.state 
30487
a14ff49d3083
simplified preparation and outer parsing of specification;
wenzelm
parents:
30364
diff
changeset

15 
val add_primrec_cmd: string list option > string option > 
a14ff49d3083
simplified preparation and outer parsing of specification;
wenzelm
parents:
30364
diff
changeset

16 
(binding * string option * mixfix) list > 
a14ff49d3083
simplified preparation and outer parsing of specification;
wenzelm
parents:
30364
diff
changeset

17 
(binding * string option * mixfix) list > 
a14ff49d3083
simplified preparation and outer parsing of specification;
wenzelm
parents:
30364
diff
changeset

18 
(Attrib.binding * string) list > local_theory > Proof.state 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

19 
end; 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

20 

ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

21 
structure NominalPrimrec : NOMINAL_PRIMREC = 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

22 
struct 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

23 

ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

24 
exception RecError of string; 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

25 

ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

26 
fun primrec_err s = error ("Nominal primrec definition error:\n" ^ s); 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

27 
fun primrec_eq_err lthy s eq = 
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

28 
primrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term lthy eq)); 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

29 

ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

30 

ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

31 
(* preprocessing of equations *) 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

32 

29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

33 
fun unquantify t = 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

34 
let 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

35 
val (vs, Ts) = split_list (strip_qnt_vars "all" t); 
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

36 
val body = strip_qnt_body "all" t; 
43326
47cf4bc789aa
simplified Name.variant  discontinued builtin fold_map;
wenzelm
parents:
43324
diff
changeset

37 
val (vs', _) = fold_map Name.variant vs (Name.make_context (fold_aterms 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

38 
(fn Free (v, _) => insert (op =) v  _ => I) body [])) 
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

39 
in (curry subst_bounds (map2 (curry Free) vs' Ts > rev) body) end; 
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

40 

30487
a14ff49d3083
simplified preparation and outer parsing of specification;
wenzelm
parents:
30364
diff
changeset

41 
fun process_eqn lthy is_fixed spec rec_fns = 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

42 
let 
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

43 
val eq = unquantify spec; 
30487
a14ff49d3083
simplified preparation and outer parsing of specification;
wenzelm
parents:
30364
diff
changeset

44 
val (lhs, rhs) = 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

45 
HOLogic.dest_eq (HOLogic.dest_Trueprop (Logic.strip_imp_concl eq)) 
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

46 
handle TERM _ => raise RecError "not a proper equation"; 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

47 

ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

48 
val (recfun, args) = strip_comb lhs; 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

49 
val fname = case recfun of Free (v, _) => if is_fixed v then v 
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

50 
else raise RecError "illegal head of function equation" 
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

51 
 _ => raise RecError "illegal head of function equation"; 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

52 

ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

53 
val (ls', rest) = take_prefix is_Free args; 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

54 
val (middle, rs') = take_suffix is_Free rest; 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

55 
val rpos = length ls'; 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

56 

ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

57 
val (constr, cargs') = if null middle then raise RecError "constructor missing" 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

58 
else strip_comb (hd middle); 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

59 
val (cname, T) = dest_Const constr 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

60 
handle TERM _ => raise RecError "illformed constructor"; 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

61 
val (tname, _) = dest_Type (body_type T) handle TYPE _ => 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

62 
raise RecError "cannot determine datatype associated with function" 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

63 

ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

64 
val (ls, cargs, rs) = 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

65 
(map dest_Free ls', map dest_Free cargs', map dest_Free rs') 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

66 
handle TERM _ => raise RecError "illegal argument in pattern"; 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

67 
val lfrees = ls @ rs @ cargs; 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

68 

ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

69 
fun check_vars _ [] = () 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

70 
 check_vars s vars = raise RecError (s ^ commas_quote (map fst vars)) 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

71 
in 
30487
a14ff49d3083
simplified preparation and outer parsing of specification;
wenzelm
parents:
30364
diff
changeset

72 
if length middle > 1 then 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

73 
raise RecError "more than one nonvariable in pattern" 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

74 
else 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

75 
(check_vars "repeated variable names in pattern: " (duplicates (op =) lfrees); 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

76 
check_vars "extra variables on rhs: " 
44121  77 
(map dest_Free (Misc_Legacy.term_frees rhs) > subtract (op =) lfrees 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

78 
> filter_out (is_fixed o fst)); 
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

79 
case AList.lookup (op =) rec_fns fname of 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

80 
NONE => 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

81 
(fname, (tname, rpos, [(cname, (ls, cargs, rs, rhs, eq))]))::rec_fns 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

82 
 SOME (_, rpos', eqns) => 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

83 
if AList.defined (op =) eqns cname then 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

84 
raise RecError "constructor already occurred as pattern" 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

85 
else if rpos <> rpos' then 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

86 
raise RecError "position of recursive argument inconsistent" 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

87 
else 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

88 
AList.update (op =) 
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

89 
(fname, (tname, rpos, (cname, (ls, cargs, rs, rhs, eq))::eqns)) 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

90 
rec_fns) 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

91 
end 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

92 
handle RecError s => primrec_eq_err lthy s spec; 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

93 

ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

94 
val param_err = "Parameters must be the same for all recursive functions"; 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

95 

29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

96 
fun process_fun lthy descr eqns (i, fname) (fnames, fnss) = 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

97 
let 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

98 
val (_, (tname, _, constrs)) = nth descr i; 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

99 

ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

100 
(* substitute "fname ls x rs" by "y" for (x, (_, y)) in subs *) 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

101 

ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

102 
fun subst [] t fs = (t, fs) 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

103 
 subst subs (Abs (a, T, t)) fs = 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

104 
fs 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

105 
> subst subs t 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

106 
> (fn t' => pair (Abs (a, T, t'))) 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

107 
 subst subs (t as (_ $ _)) fs = 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

108 
let 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

109 
val (f, ts) = strip_comb t; 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

110 
in 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

111 
if is_Free f 
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

112 
andalso member (fn ((v, _), (w, _)) => v = w) eqns (dest_Free f) then 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

113 
let 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

114 
val (fname', _) = dest_Free f; 
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

115 
val (_, rpos, eqns') = the (AList.lookup (op =) eqns fname'); 
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

116 
val (ls, rs'') = chop rpos ts 
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

117 
val (x', rs) = case rs'' of 
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

118 
x' :: rs => (x', rs) 
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

119 
 [] => raise RecError ("not enough arguments in recursive application\n" 
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

120 
^ "of function " ^ quote fname' ^ " on rhs"); 
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

121 
val rs' = (case eqns' of 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

122 
(_, (ls', _, rs', _, _)) :: _ => 
23006
c46abff9a7a0
Fixed bug in subst causing primrec functions returning functions
berghofe
parents:
22728
diff
changeset

123 
let val (rs1, rs2) = chop (length rs') rs 
c46abff9a7a0
Fixed bug in subst causing primrec functions returning functions
berghofe
parents:
22728
diff
changeset

124 
in 
c46abff9a7a0
Fixed bug in subst causing primrec functions returning functions
berghofe
parents:
22728
diff
changeset

125 
if ls = map Free ls' andalso rs1 = map Free rs' then rs2 
c46abff9a7a0
Fixed bug in subst causing primrec functions returning functions
berghofe
parents:
22728
diff
changeset

126 
else raise RecError param_err 
c46abff9a7a0
Fixed bug in subst causing primrec functions returning functions
berghofe
parents:
22728
diff
changeset

127 
end 
c46abff9a7a0
Fixed bug in subst causing primrec functions returning functions
berghofe
parents:
22728
diff
changeset

128 
 _ => raise RecError ("no equations for " ^ quote fname')); 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

129 
val (x, xs) = strip_comb x' 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

130 
in case AList.lookup (op =) subs x 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

131 
of NONE => 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

132 
fs 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

133 
> fold_map (subst subs) ts 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

134 
> (fn ts' => pair (list_comb (f, ts'))) 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

135 
 SOME (i', y) => 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

136 
fs 
23006
c46abff9a7a0
Fixed bug in subst causing primrec functions returning functions
berghofe
parents:
22728
diff
changeset

137 
> fold_map (subst subs) (xs @ rs') 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

138 
> process_fun lthy descr eqns (i', fname') 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

139 
> (fn ts' => pair (list_comb (y, ts'))) 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

140 
end 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

141 
else 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

142 
fs 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

143 
> fold_map (subst subs) (f :: ts) 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

144 
> (fn (f'::ts') => pair (list_comb (f', ts'))) 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

145 
end 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

146 
 subst _ t fs = (t, fs); 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

147 

ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

148 
(* translate rec equations into function arguments suitable for rec comb *) 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

149 

29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

150 
fun trans eqns (cname, cargs) (fnames', fnss', fns) = 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

151 
(case AList.lookup (op =) eqns cname of 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

152 
NONE => (warning ("No equation for constructor " ^ quote cname ^ 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

153 
"\nin definition of function " ^ quote fname); 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

154 
(fnames', fnss', (Const (@{const_name undefined}, dummyT))::fns)) 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

155 
 SOME (ls, cargs', rs, rhs, eq) => 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

156 
let 
45736  157 
val recs = filter (Datatype_Aux.is_rec_type o snd) (cargs' ~~ cargs); 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

158 
val rargs = map fst recs; 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

159 
val subs = map (rpair dummyT o fst) 
29276  160 
(rev (Term.rename_wrt_term rhs rargs)); 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

161 
val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z => 
45736  162 
(Free x, (Datatype_Aux.body_index y, Free z))) recs subs) rhs (fnames', fnss') 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

163 
handle RecError s => primrec_eq_err lthy s eq 
44241  164 
in (fnames'', fnss'', fold_rev absfree (cargs' @ subs) rhs' :: fns) 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

165 
end) 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

166 

29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

167 
in (case AList.lookup (op =) fnames i of 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

168 
NONE => 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

169 
if exists (fn (_, v) => fname = v) fnames then 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

170 
raise RecError ("inconsistent functions for datatype " ^ quote tname) 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

171 
else 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

172 
let 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

173 
val SOME (_, _, eqns' as (_, (ls, _, rs, _, _)) :: _) = 
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

174 
AList.lookup (op =) eqns fname; 
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

175 
val (fnames', fnss', fns) = fold_rev (trans eqns') constrs 
30487
a14ff49d3083
simplified preparation and outer parsing of specification;
wenzelm
parents:
30364
diff
changeset

176 
((i, fname)::fnames, fnss, []) 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

177 
in 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

178 
(fnames', (i, (fname, ls, rs, fns))::fnss') 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

179 
end 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

180 
 SOME fname' => 
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

181 
if fname = fname' then (fnames, fnss) 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

182 
else raise RecError ("inconsistent functions for datatype " ^ quote tname)) 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

183 
end; 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

184 

ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

185 

ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

186 
(* prepare functions needed for definitions *) 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

187 

ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

188 
fun get_fns fns ((i : int, (tname, _, constrs)), rec_name) (fs, defs) = 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

189 
case AList.lookup (op =) fns i of 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

190 
NONE => 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

191 
let 
28524  192 
val dummy_fns = map (fn (_, cargs) => Const (@{const_name undefined}, 
45736  193 
replicate (length cargs + length (filter Datatype_Aux.is_rec_type cargs)) 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

194 
dummyT > HOLogic.unitT)) constrs; 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

195 
val _ = warning ("No function definition for datatype " ^ quote tname) 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

196 
in 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

197 
(dummy_fns @ fs, defs) 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

198 
end 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

199 
 SOME (fname, ls, rs, fs') => (fs' @ fs, (fname, ls, rs, rec_name, tname) :: defs); 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

200 

ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

201 

ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

202 
(* make definition *) 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

203 

29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

204 
fun make_def ctxt fixes fs (fname, ls, rs, rec_name, tname) = 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

205 
let 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

206 
val used = map fst (fold Term.add_frees fs []); 
43324
2b47822868e4
discontinued Name.variant to emphasize that this is oldstyle / indirect;
wenzelm
parents:
42361
diff
changeset

207 
val x = (singleton (Name.variant_list used) "x", dummyT); 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

208 
val frees = ls @ x :: rs; 
44241  209 
val raw_rhs = fold_rev absfree frees 
210 
(list_comb (Const (rec_name, dummyT), fs @ [Free x])) 

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

211 
val def_name = Thm.def_name (Long_Name.base_name fname); 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

212 
val rhs = singleton (Syntax.check_terms ctxt) raw_rhs; 
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

213 
val SOME var = get_first (fn ((b, _), mx) => 
30223
24d975352879
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents:
29581
diff
changeset

214 
if Binding.name_of b = fname then SOME (b, mx) else NONE) fixes; 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

215 
in 
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

216 
((var, ((Binding.name def_name, []), rhs)), 
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

217 
subst_bounds (rev (map Free frees), strip_abs_body rhs)) 
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

218 
end; 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

219 

ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

220 

ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

221 
(* find datatypes which contain all datatypes in tnames' *) 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

222 

31938  223 
fun find_dts (dt_info : NominalDatatype.nominal_datatype_info Symtab.table) _ [] = [] 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

224 
 find_dts dt_info tnames' (tname::tnames) = 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

225 
(case Symtab.lookup dt_info tname of 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

226 
NONE => primrec_err (quote tname ^ " is not a nominal datatype") 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

227 
 SOME dt => 
33038  228 
if subset (op =) (tnames', map (#1 o snd) (#descr dt)) then 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

229 
(tname, dt)::(find_dts dt_info tnames' tnames) 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

230 
else find_dts dt_info tnames' tnames); 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

231 

ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

232 
fun common_prefix eq ([], _) = [] 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

233 
 common_prefix eq (_, []) = [] 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

234 
 common_prefix eq (x :: xs, y :: ys) = 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

235 
if eq (x, y) then x :: common_prefix eq (xs, ys) else []; 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

236 

ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

237 
local 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

238 

33726
0878aecbf119
eliminated slightly odd name space grouping  now managed by Isar toplevel;
wenzelm
parents:
33671
diff
changeset

239 
fun gen_primrec prep_spec prep_term invs fctxt raw_fixes raw_params raw_spec lthy = 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

240 
let 
30487
a14ff49d3083
simplified preparation and outer parsing of specification;
wenzelm
parents:
30364
diff
changeset

241 
val (fixes', spec) = fst (prep_spec (raw_fixes @ raw_params) raw_spec lthy); 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

242 
val fixes = List.take (fixes', length raw_fixes); 
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

243 
val (names_atts, spec') = split_list spec; 
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

244 
val eqns' = map unquantify spec' 
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

245 
val eqns = fold_rev (process_eqn lthy (fn v => Variable.is_fixed lthy v 
30223
24d975352879
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents:
29581
diff
changeset

246 
orelse exists (fn ((w, _), _) => v = Binding.name_of w) fixes)) spec' []; 
42361  247 
val dt_info = NominalDatatype.get_nominal_datatypes (Proof_Context.theory_of lthy); 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

248 
val lsrs :: lsrss = maps (fn (_, (_, _, eqns)) => 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

249 
map (fn (_, (ls, _, rs, _, _)) => ls @ rs) eqns) eqns 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

250 
val _ = 
33038  251 
(if forall (curry (eq_set (op =)) lsrs) lsrss andalso forall 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

252 
(fn (_, (_, _, (_, (ls, _, rs, _, _)) :: eqns)) => 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

253 
forall (fn (_, (ls', _, rs', _, _)) => 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

254 
ls = ls' andalso rs = rs') eqns 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

255 
 _ => true) eqns 
22330
00ca68f5ce29
Replaced "raise RecError" by "primrec_err" in function
berghofe
parents:
22101
diff
changeset

256 
then () else primrec_err param_err); 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

257 
val tnames = distinct (op =) (map (#1 o snd) eqns); 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

258 
val dts = find_dts dt_info tnames tnames; 
30487
a14ff49d3083
simplified preparation and outer parsing of specification;
wenzelm
parents:
30364
diff
changeset

259 
val main_fns = 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

260 
map (fn (tname, {index, ...}) => 
30487
a14ff49d3083
simplified preparation and outer parsing of specification;
wenzelm
parents:
30364
diff
changeset

261 
(index, 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

262 
(fst o the o find_first (fn (_, x) => #1 x = tname)) eqns)) 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

263 
dts; 
30487
a14ff49d3083
simplified preparation and outer parsing of specification;
wenzelm
parents:
30364
diff
changeset

264 
val {descr, rec_names, rec_rewrites, ...} = 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

265 
if null dts then 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

266 
primrec_err ("datatypes " ^ commas_quote tnames ^ "\nare not mutually recursive") 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

267 
else snd (hd dts); 
22434
081a62852313
 Replaced fold by fold_rev to make sure that list of predicate
berghofe
parents:
22330
diff
changeset

268 
val descr = map (fn (i, (tname, args, constrs)) => (i, (tname, args, 
081a62852313
 Replaced fold by fold_rev to make sure that list of predicate
berghofe
parents:
22330
diff
changeset

269 
map (fn (cname, cargs) => (cname, fold (fn (dTs, dT) => fn dTs' => 
081a62852313
 Replaced fold by fold_rev to make sure that list of predicate
berghofe
parents:
22330
diff
changeset

270 
dTs' @ dTs @ [dT]) cargs [])) constrs))) descr; 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

271 
val (fnames, fnss) = fold_rev (process_fun lthy descr eqns) main_fns ([], []); 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

272 
val (fs, defs) = fold_rev (get_fns fnss) (descr ~~ rec_names) ([], []); 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

273 
val defs' = map (make_def lthy fixes fs) defs; 
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

274 
val names1 = map snd fnames; 
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

275 
val names2 = map fst eqns; 
33038  276 
val _ = if eq_set (op =) (names1, names2) then () 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

277 
else primrec_err ("functions " ^ commas_quote names2 ^ 
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

278 
"\nare not mutually recursive"); 
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

279 
val (defs_thms, lthy') = lthy > 
33766
c679f05600cd
adapted Local_Theory.define  eliminated odd thm kind;
wenzelm
parents:
33726
diff
changeset

280 
fold_map (apfst (snd o snd) oo Local_Theory.define o fst) defs'; 
30223
24d975352879
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents:
29581
diff
changeset

281 
val qualify = Binding.qualify false 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset

282 
(space_implode "_" (map (Long_Name.base_name o #1) defs)); 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

283 
val names_atts' = map (apfst qualify) names_atts; 
42361  284 
val cert = cterm_of (Proof_Context.theory_of lthy'); 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

285 

ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

286 
fun mk_idx eq = 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

287 
let 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

288 
val Free (name, _) = head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

289 
(Logic.strip_imp_concl eq)))); 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

290 
val SOME i = AList.lookup op = (map swap fnames) name; 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

291 
val SOME (_, _, constrs) = AList.lookup op = descr i; 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

292 
val SOME (_, _, eqns'') = AList.lookup op = eqns name; 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

293 
val SOME (cname, (_, cargs, _, _, _)) = find_first 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

294 
(fn (_, (_, _, _, _, eq')) => eq = eq') eqns'' 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

295 
in (i, find_index (fn (cname', _) => cname = cname') constrs, cargs) end; 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

296 

ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

297 
val rec_rewritess = 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

298 
unflat (map (fn (_, (_, _, constrs)) => constrs) descr) rec_rewrites; 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

299 
val fvars = rec_rewrites > hd > concl_of > HOLogic.dest_Trueprop > 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

300 
HOLogic.dest_eq > fst > strip_comb > snd > take_prefix is_Var > fst; 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

301 
val (pvars, ctxtvars) = List.partition 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

302 
(equal HOLogic.boolT o body_type o snd) 
35098
45dec8e27c4b
Fixed bug in code for guessing the name of the variable representing the freshness context.
berghofe
parents:
33968
diff
changeset

303 
(subtract (op =) 
45dec8e27c4b
Fixed bug in code for guessing the name of the variable representing the freshness context.
berghofe
parents:
33968
diff
changeset

304 
(Term.add_vars (concl_of (hd rec_rewrites)) []) 
45dec8e27c4b
Fixed bug in code for guessing the name of the variable representing the freshness context.
berghofe
parents:
33968
diff
changeset

305 
(fold_rev (Term.add_vars o Logic.strip_assums_concl) 
45dec8e27c4b
Fixed bug in code for guessing the name of the variable representing the freshness context.
berghofe
parents:
33968
diff
changeset

306 
(prems_of (hd rec_rewrites)) [])); 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

307 
val cfs = defs' > hd > snd > strip_comb > snd > 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

308 
curry (List.take o swap) (length fvars) > map cert; 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

309 
val invs' = (case invs of 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

310 
NONE => map (fn (i, _) => 
45740  311 
Abs ("x", fastype_of (snd (nth defs' i)), @{term True})) descr 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

312 
 SOME invs' => map (prep_term lthy') invs'); 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

313 
val inst = (map cert fvars ~~ cfs) @ 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

314 
(map (cert o Var) pvars ~~ map cert invs') @ 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

315 
(case ctxtvars of 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

316 
[ctxtvar] => [(cert (Var ctxtvar), 
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

317 
cert (the_default HOLogic.unit (Option.map (prep_term lthy') fctxt)))] 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

318 
 _ => []); 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

319 
val rec_rewrites' = map (fn eq => 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

320 
let 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

321 
val (i, j, cargs) = mk_idx eq 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

322 
val th = nth (nth rec_rewritess i) j; 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

323 
val cargs' = th > concl_of > HOLogic.dest_Trueprop > 
41489
8e2b8649507d
standardized split_last/last_elem towards List.last;
wenzelm
parents:
36960
diff
changeset

324 
HOLogic.dest_eq > fst > strip_comb > snd > List.last > 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

325 
strip_comb > snd 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

326 
in (cargs, Logic.strip_imp_prems eq, 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

327 
Drule.cterm_instantiate (inst @ 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

328 
(map cert cargs' ~~ map (cert o Free) cargs)) th) 
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

329 
end) eqns'; 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

330 

ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

331 
val prems = foldr1 (common_prefix op aconv) (map (prems_of o #3) rec_rewrites'); 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

332 
val cprems = map cert prems; 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

333 
val asms = map Thm.assume cprems; 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

334 
val premss = map (fn (cargs, eprems, eqn) => 
46215
0da9433f959e
discontinued oldstyle Term.list_all_free in favour of plain Logic.all;
wenzelm
parents:
45740
diff
changeset

335 
map (fn t => fold_rev (Logic.all o Free) cargs (Logic.list_implies (eprems, t))) 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

336 
(List.drop (prems_of eqn, length prems))) rec_rewrites'; 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

337 
val cpremss = map (map cert) premss; 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

338 
val asmss = map (map Thm.assume) cpremss; 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

339 

ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

340 
fun mk_eqn ((cargs, eprems, eqn), asms') = 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

341 
let 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

342 
val ceprems = map cert eprems; 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

343 
val asms'' = map Thm.assume ceprems; 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

344 
val ccargs = map (cert o Free) cargs; 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

345 
val asms''' = map (fn th => implies_elim_list 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

346 
(forall_elim_list ccargs th) asms'') asms' 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

347 
in 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

348 
implies_elim_list eqn (asms @ asms''') > 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

349 
implies_intr_list ceprems > 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

350 
forall_intr_list ccargs 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

351 
end; 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

352 

ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

353 
val rule_prems = cprems @ flat cpremss; 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

354 
val rule = implies_intr_list rule_prems 
23418  355 
(Conjunction.intr_balanced (map mk_eqn (rec_rewrites' ~~ asmss))); 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

356 

29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

357 
val goals = map (fn ((cargs, _, _), eqn) => 
46215
0da9433f959e
discontinued oldstyle Term.list_all_free in favour of plain Logic.all;
wenzelm
parents:
45740
diff
changeset

358 
(fold_rev (Logic.all o Free) cargs eqn, [])) (rec_rewrites' ~~ eqns'); 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

359 

ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

360 
in 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

361 
lthy' > 
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

362 
Variable.add_fixes (map fst lsrs) > snd > 
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
35098
diff
changeset

363 
Proof.theorem NONE 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

364 
(fn thss => fn goal_ctxt => 
45592  365 
let 
366 
val simps = Proof_Context.export goal_ctxt lthy' (flat thss); 

367 
val (simps', lthy'') = 

33671  368 
fold_map Local_Theory.note (names_atts' ~~ map single simps) lthy'; 
45592  369 
in 
370 
lthy'' 

371 
> Local_Theory.note 

372 
((qualify (Binding.name "simps"), @{attributes [simp, nitpick_simp]}), maps snd simps') 

373 
> snd 

374 
end) 

21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

375 
[goals] > 
30510
4120fc59dd85
unified type Proof.method and pervasive METHOD combinators;
wenzelm
parents:
30487
diff
changeset

376 
Proof.apply (Method.Basic (fn _ => RAW_METHOD (fn _ => 
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

377 
rewrite_goals_tac defs_thms THEN 
32196  378 
compose_tac (false, rule, length rule_prems) 1))) > 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

379 
Seq.hd 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

380 
end; 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

381 

ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

382 
in 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

383 

33726
0878aecbf119
eliminated slightly odd name space grouping  now managed by Isar toplevel;
wenzelm
parents:
33671
diff
changeset

384 
val add_primrec = gen_primrec Specification.check_spec (K I); 
0878aecbf119
eliminated slightly odd name space grouping  now managed by Isar toplevel;
wenzelm
parents:
33671
diff
changeset

385 
val add_primrec_cmd = gen_primrec Specification.read_spec Syntax.read_term; 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

386 

29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
29006
diff
changeset

387 
end; 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

388 

ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

389 

ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

390 
(* outer syntax *) 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

391 

36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset

392 
val freshness_context = Parse.reserved "freshness_context"; 
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset

393 
val invariant = Parse.reserved "invariant"; 
24867  394 

46949  395 
fun unless_flag scan = Scan.unless ((freshness_context  invariant)  @{keyword ":"}) scan; 
24906
557a9cd9370c
turned keywords invariant/freshness_context into reserved indentifiers;
wenzelm
parents:
24867
diff
changeset

396 

46949  397 
val parser1 = (freshness_context  @{keyword ":"})  unless_flag Parse.term >> SOME; 
398 
val parser2 = (invariant  @{keyword ":"})  

36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset

399 
(Scan.repeat1 (unless_flag Parse.term) >> SOME)  Scan.optional parser1 NONE  
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

400 
(parser1 >> pair NONE); 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

401 
val options = 
46949  402 
Scan.optional (@{keyword "("}  Parse.!!! (parser2  @{keyword ")"})) (NONE, NONE); 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

403 

24867  404 
val _ = 
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset

405 
Outer_Syntax.local_theory_to_proof @{command_spec "nominal_primrec"} 
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset

406 
"define primitive recursive functions on nominal datatypes" 
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset

407 
(options  Parse.fixes  Parse.for_fixes  Parse_Spec.where_alt_specs 
30487
a14ff49d3083
simplified preparation and outer parsing of specification;
wenzelm
parents:
30364
diff
changeset

408 
>> (fn ((((invs, fctxt), fixes), params), specs) => 
a14ff49d3083
simplified preparation and outer parsing of specification;
wenzelm
parents:
30364
diff
changeset

409 
add_primrec_cmd invs fctxt fixes params specs)); 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

410 

ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

411 
end; 
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
diff
changeset

412 