author  wenzelm 
Sun, 08 Nov 2009 18:43:42 +0100  
changeset 33522  737589bb9bb8 
parent 33519  e31a85f92ce9 
child 33666  e49bfeb0d822 
permissions  rwrr 
31738
7b9b9ba532ca
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31177
diff
changeset

1 
(* Title: HOLCF/Tools/fixrec.ML 
23152  2 
Author: Amber Telfer and Brian Huffman 
3 

4 
Recursive function definition package for HOLCF. 

5 
*) 

6 

31738
7b9b9ba532ca
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31177
diff
changeset

7 
signature FIXREC = 
23152  8 
sig 
30485  9 
val add_fixrec: bool > (binding * typ option * mixfix) list 
10 
> (Attrib.binding * term) list > local_theory > local_theory 

11 
val add_fixrec_cmd: bool > (binding * string option * mixfix) list 

30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

12 
> (Attrib.binding * string) list > local_theory > local_theory 
30485  13 
val add_fixpat: Thm.binding * term list > theory > theory 
14 
val add_fixpat_cmd: Attrib.binding * string list > theory > theory 

30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset

15 
val add_matchers: (string * string) list > theory > theory 
33442  16 
val fixrec_simp_add: attribute 
17 
val fixrec_simp_del: attribute 

33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

18 
val fixrec_simp_tac: Proof.context > int > tactic 
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset

19 
val setup: theory > theory 
23152  20 
end; 
21 

31738
7b9b9ba532ca
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31177
diff
changeset

22 
structure Fixrec :> FIXREC = 
23152  23 
struct 
24 

31095
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

25 
val def_cont_fix_eq = @{thm def_cont_fix_eq}; 
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

26 
val def_cont_fix_ind = @{thm def_cont_fix_ind}; 
23152  27 

28 

29 
fun fixrec_err s = error ("fixrec definition error:\n" ^ s); 

30 
fun fixrec_eq_err thy s eq = 

26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26343
diff
changeset

31 
fixrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq)); 
23152  32 

30132  33 
(*************************************************************************) 
34 
(***************************** building types ****************************) 

35 
(*************************************************************************) 

36 

23152  37 
(* >> is taken from holcf_logic.ML *) 
30132  38 
fun cfunT (T, U) = Type(@{type_name ">"}, [T, U]); 
39 

40 
infixr 6 >>; val (op >>) = cfunT; 

41 

42 
fun dest_cfunT (Type(@{type_name ">"}, [T, U])) = (T, U) 

43 
 dest_cfunT T = raise TYPE ("dest_cfunT", [T], []); 

44 

45 
fun maybeT T = Type(@{type_name "maybe"}, [T]); 

46 

47 
fun dest_maybeT (Type(@{type_name "maybe"}, [T])) = T 

48 
 dest_maybeT T = raise TYPE ("dest_maybeT", [T], []); 

49 

31095
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

50 
fun tupleT [] = HOLogic.unitT 
30132  51 
 tupleT [T] = T 
52 
 tupleT (T :: Ts) = HOLogic.mk_prodT (T, tupleT Ts); 

53 

33401
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset

54 
local 
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset

55 

fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset

56 
fun binder_cfun (Type(@{type_name ">"},[T, U])) = T :: binder_cfun U 
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset

57 
 binder_cfun (Type(@{type_name "fun"},[T, U])) = T :: binder_cfun U 
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset

58 
 binder_cfun _ = []; 
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset

59 

fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset

60 
fun body_cfun (Type(@{type_name ">"},[T, U])) = body_cfun U 
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset

61 
 body_cfun (Type(@{type_name "fun"},[T, U])) = body_cfun U 
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset

62 
 body_cfun T = T; 
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset

63 

fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset

64 
fun strip_cfun T : typ list * typ = 
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset

65 
(binder_cfun T, body_cfun T); 
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset

66 

fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset

67 
fun cfunsT (Ts, U) = List.foldr cfunT U Ts; 
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset

68 

fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset

69 
in 
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset

70 

30912
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30485
diff
changeset

71 
fun matchT (T, U) = 
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30485
diff
changeset

72 
body_cfun T >> cfunsT (binder_cfun T, U) >> U; 
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30485
diff
changeset

73 

33401
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset

74 
end 
30132  75 

76 
(*************************************************************************) 

77 
(***************************** building terms ****************************) 

78 
(*************************************************************************) 

23152  79 

80 
val mk_trp = HOLogic.mk_Trueprop; 

81 

82 
(* splits a cterm into the right and lefthand sides of equality *) 

83 
fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t); 

84 

85 
(* similar to Thm.head_of, but for continuous application *) 

26045  86 
fun chead_of (Const(@{const_name Rep_CFun},_)$f$t) = chead_of f 
23152  87 
 chead_of u = u; 
88 

30132  89 
fun capply_const (S, T) = 
90 
Const(@{const_name Rep_CFun}, (S >> T) > (S > T)); 

91 

92 
fun cabs_const (S, T) = 

93 
Const(@{const_name Abs_CFun}, (S > T) > (S >> T)); 

94 

31095
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

95 
fun mk_cabs t = 
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

96 
let val T = Term.fastype_of t 
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

97 
in cabs_const (Term.domain_type T, Term.range_type T) $ t end 
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

98 

30132  99 
fun mk_capply (t, u) = 
100 
let val (S, T) = 

101 
case Term.fastype_of t of 

102 
Type(@{type_name ">"}, [S, T]) => (S, T) 

103 
 _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]); 

104 
in capply_const (S, T) $ t $ u end; 

105 

106 
infix 0 ==; val (op ==) = Logic.mk_equals; 

107 
infix 1 ===; val (op ===) = HOLogic.mk_eq; 

108 
infix 9 ` ; val (op `) = mk_capply; 

109 

23152  110 
(* builds the expression (LAM v. rhs) *) 
30132  111 
fun big_lambda v rhs = 
112 
cabs_const (Term.fastype_of v, Term.fastype_of rhs) $ Term.lambda v rhs; 

23152  113 

114 
(* builds the expression (LAM v1 v2 .. vn. rhs) *) 

115 
fun big_lambdas [] rhs = rhs 

116 
 big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs); 

117 

30132  118 
fun mk_return t = 
119 
let val T = Term.fastype_of t 

120 
in Const(@{const_name Fixrec.return}, T >> maybeT T) ` t end; 

121 

122 
fun mk_bind (t, u) = 

123 
let val (T, mU) = dest_cfunT (Term.fastype_of u); 

124 
val bindT = maybeT T >> (T >> mU) >> mU; 

125 
in Const(@{const_name Fixrec.bind}, bindT) ` t ` u end; 

126 

127 
fun mk_mplus (t, u) = 

128 
let val mT = Term.fastype_of t 

129 
in Const(@{const_name Fixrec.mplus}, mT >> mT >> mT) ` t ` u end; 

130 

131 
fun mk_run t = 

132 
let val mT = Term.fastype_of t 

133 
val T = dest_maybeT mT 

134 
in Const(@{const_name Fixrec.run}, mT >> T) ` t end; 

135 

136 
fun mk_fix t = 

137 
let val (T, _) = dest_cfunT (Term.fastype_of t) 

138 
in Const(@{const_name fix}, (T >> T) >> T) ` t end; 

23152  139 

31095
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

140 
fun mk_cont t = 
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

141 
let val T = Term.fastype_of t 
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

142 
in Const(@{const_name cont}, T > HOLogic.boolT) $ t end; 
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

143 

b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

144 
val mk_fst = HOLogic.mk_fst 
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

145 
val mk_snd = HOLogic.mk_snd 
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

146 

b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

147 
(* builds the expression (v1,v2,..,vn) *) 
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

148 
fun mk_tuple [] = HOLogic.unit 
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

149 
 mk_tuple (t::[]) = t 
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

150 
 mk_tuple (t::ts) = HOLogic.mk_prod (t, mk_tuple ts); 
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

151 

b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

152 
(* builds the expression (%(v1,v2,..,vn). rhs) *) 
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

153 
fun lambda_tuple [] rhs = Term.lambda (Free("unit", HOLogic.unitT)) rhs 
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

154 
 lambda_tuple (v::[]) rhs = Term.lambda v rhs 
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

155 
 lambda_tuple (v::vs) rhs = 
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

156 
HOLogic.mk_split (Term.lambda v (lambda_tuple vs rhs)); 
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

157 

b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

158 

23152  159 
(*************************************************************************) 
160 
(************* fixedpoint definitions and unfolding theorems ************) 

161 
(*************************************************************************) 

162 

33519  163 
structure FixrecUnfoldData = Generic_Data 
164 
( 

33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

165 
type T = thm Symtab.table; 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

166 
val empty = Symtab.empty; 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

167 
val extend = I; 
33519  168 
fun merge data : T = Symtab.merge (K true) data; 
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

169 
); 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

170 

7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

171 
local 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

172 

7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

173 
fun name_of (Const (n, T)) = n 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

174 
 name_of (Free (n, T)) = n 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

175 
 name_of _ = fixrec_err "name_of" 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

176 

7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

177 
val lhs_name = 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

178 
name_of o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of; 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

179 

7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

180 
in 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

181 

33442  182 
val add_unfold : attribute = 
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

183 
Thm.declaration_attribute 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

184 
(fn th => FixrecUnfoldData.map (Symtab.insert (K true) (lhs_name th, th))); 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

185 

7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

186 
end 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

187 

30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

188 
fun add_fixdefs 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

189 
(fixes : ((binding * typ) * mixfix) list) 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

190 
(spec : (Attrib.binding * term) list) 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

191 
(lthy : local_theory) = 
23152  192 
let 
31095
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

193 
val thy = ProofContext.theory_of lthy; 
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:
30211
diff
changeset

194 
val names = map (Binding.name_of o fst o fst) fixes; 
30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

195 
val all_names = space_implode "_" names; 
32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
31740
diff
changeset

196 
val (lhss, rhss) = ListPair.unzip (map (dest_eqs o snd) spec); 
31095
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

197 
val functional = lambda_tuple lhss (mk_tuple rhss); 
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

198 
val fixpoint = mk_fix (mk_cabs functional); 
23152  199 

31095
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

200 
val cont_thm = 
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

201 
Goal.prove lthy [] [] (mk_trp (mk_cont functional)) 
32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
31740
diff
changeset

202 
(K (simp_tac (simpset_of lthy) 1)); 
31095
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

203 

30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

204 
fun one_def (l as Free(n,_)) r = 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset

205 
let val b = Long_Name.base_name n 
30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

206 
in ((Binding.name (b^"_def"), []), r) end 
23152  207 
 one_def _ _ = fixrec_err "fixdefs: lhs not of correct form"; 
208 
fun defs [] _ = [] 

209 
 defs (l::[]) r = [one_def l r] 

31095
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

210 
 defs (l::ls) r = one_def l (mk_fst r) :: defs ls (mk_snd r); 
30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

211 
val fixdefs = defs lhss fixpoint; 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

212 
val define_all = fold_map (LocalTheory.define Thm.definitionK); 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

213 
val (fixdef_thms : (term * (string * thm)) list, lthy') = lthy 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

214 
> define_all (map (apfst fst) fixes ~~ fixdefs); 
31095
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

215 
fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2]; 
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

216 
val tuple_fixdef_thm = foldr1 pair_equalI (map (snd o snd) fixdef_thms); 
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

217 
val P = Var (("P", 0), map Term.fastype_of lhss > HOLogic.boolT); 
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

218 
val predicate = lambda_tuple lhss (list_comb (P, lhss)); 
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

219 
val tuple_induct_thm = (def_cont_fix_ind OF [tuple_fixdef_thm, cont_thm]) 
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

220 
> Drule.instantiate' [] [SOME (Thm.cterm_of thy predicate)] 
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

221 
> LocalDefs.unfold lthy @{thms split_paired_all split_conv split_strict}; 
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

222 
val tuple_unfold_thm = (def_cont_fix_eq OF [tuple_fixdef_thm, cont_thm]) 
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

223 
> LocalDefs.unfold lthy' @{thms split_conv}; 
23152  224 
fun unfolds [] thm = [] 
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

225 
 unfolds (n::[]) thm = [(n, thm)] 
23152  226 
 unfolds (n::ns) thm = let 
31095
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

227 
val thmL = thm RS @{thm Pair_eqD1}; 
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

228 
val thmR = thm RS @{thm Pair_eqD2}; 
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

229 
in (n, thmL) :: unfolds ns thmR end; 
31095
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset

230 
val unfold_thms = unfolds names tuple_unfold_thm; 
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

231 
val induct_note : Attrib.binding * Thm.thm list = 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

232 
let 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

233 
val thm_name = Binding.name (all_names ^ "_induct"); 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

234 
in 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

235 
((thm_name, []), [tuple_induct_thm]) 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

236 
end; 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

237 
fun unfold_note (name, thm) : Attrib.binding * Thm.thm list = 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

238 
let 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

239 
val thm_name = Binding.name (name ^ "_unfold"); 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

240 
val src = Attrib.internal (K add_unfold); 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

241 
in 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

242 
((thm_name, [src]), [thm]) 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

243 
end; 
30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

244 
val (thmss, lthy'') = lthy' 
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

245 
> fold_map (LocalTheory.note Thm.generatedK) 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

246 
(induct_note :: map unfold_note unfold_thms); 
23152  247 
in 
30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

248 
(lthy'', names, fixdef_thms, map snd unfold_thms) 
23152  249 
end; 
250 

251 
(*************************************************************************) 

252 
(*********** monadic notation and pattern matching compilation ***********) 

253 
(*************************************************************************) 

254 

33522  255 
structure FixrecMatchData = Theory_Data 
256 
( 

30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset

257 
type T = string Symtab.table; 
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset

258 
val empty = Symtab.empty; 
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset

259 
val extend = I; 
33522  260 
fun merge data = Symtab.merge (K true) data; 
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset

261 
); 
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset

262 

6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset

263 
(* associate match functions with pattern constants *) 
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset

264 
fun add_matchers ms = FixrecMatchData.map (fold Symtab.update ms); 
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset

265 

30157  266 
fun taken_names (t : term) : bstring list = 
267 
let 

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

268 
fun taken (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs 
30157  269 
 taken (Free(a,_) , bs) = insert (op =) a bs 
270 
 taken (f $ u , bs) = taken (f, taken (u, bs)) 

271 
 taken (Abs(a,_,t), bs) = taken (t, insert (op =) a bs) 

272 
 taken (_ , bs) = bs; 

273 
in 

274 
taken (t, []) 

275 
end; 

23152  276 

277 
(* builds a monadic term for matching a constructor pattern *) 

30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset

278 
fun pre_build match_name pat rhs vs taken = 
23152  279 
case pat of 
26045  280 
Const(@{const_name Rep_CFun},_)$f$(v as Free(n,T)) => 
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset

281 
pre_build match_name f rhs (v::vs) taken 
26045  282 
 Const(@{const_name Rep_CFun},_)$f$x => 
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset

283 
let val (rhs', v, taken') = pre_build match_name x rhs [] taken; 
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset

284 
in pre_build match_name f rhs' (v::vs) taken' end 
33401
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset

285 
 f$(v as Free(n,T)) => 
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset

286 
pre_build match_name f rhs (v::vs) taken 
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset

287 
 f$x => 
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset

288 
let val (rhs', v, taken') = pre_build match_name x rhs [] taken; 
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset

289 
in pre_build match_name f rhs' (v::vs) taken' end 
23152  290 
 Const(c,T) => 
291 
let 

292 
val n = Name.variant taken "v"; 

26045  293 
fun result_type (Type(@{type_name ">"},[_,T])) (x::xs) = result_type T xs 
33401
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset

294 
 result_type (Type (@{type_name "fun"},[_,T])) (x::xs) = result_type T xs 
23152  295 
 result_type T _ = T; 
296 
val v = Free(n, result_type T vs); 

30912
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30485
diff
changeset

297 
val m = Const(match_name c, matchT (T, fastype_of rhs)); 
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30485
diff
changeset

298 
val k = big_lambdas vs rhs; 
23152  299 
in 
30912
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30485
diff
changeset

300 
(m`v`k, v, n::taken) 
23152  301 
end 
302 
 Free(n,_) => fixrec_err ("expected constructor, found free variable " ^ quote n) 

303 
 _ => fixrec_err "pre_build: invalid pattern"; 

304 

305 
(* builds a monadic term for matching a function definition pattern *) 

306 
(* returns (name, arity, matcher) *) 

30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset

307 
fun building match_name pat rhs vs taken = 
23152  308 
case pat of 
26045  309 
Const(@{const_name Rep_CFun}, _)$f$(v as Free(n,T)) => 
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset

310 
building match_name f rhs (v::vs) taken 
26045  311 
 Const(@{const_name Rep_CFun}, _)$f$x => 
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset

312 
let val (rhs', v, taken') = pre_build match_name x rhs [] taken; 
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset

313 
in building match_name f rhs' (v::vs) taken' end 
30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

314 
 Free(_,_) => ((pat, length vs), big_lambdas vs rhs) 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

315 
 Const(_,_) => ((pat, length vs), big_lambdas vs rhs) 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

316 
 _ => fixrec_err ("function is not declared as constant in theory: " 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

317 
^ ML_Syntax.print_term pat); 
23152  318 

30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

319 
fun strip_alls t = 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

320 
if Logic.is_all t then strip_alls (snd (Logic.dest_all t)) else t; 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

321 

83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

322 
fun match_eq match_name eq = 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

323 
let 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

324 
val (lhs,rhs) = dest_eqs (Logic.strip_imp_concl (strip_alls eq)); 
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset

325 
in 
30157  326 
building match_name lhs (mk_return rhs) [] (taken_names eq) 
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset

327 
end; 
23152  328 

329 
(* returns the sum (using +++) of the terms in ms *) 

330 
(* also applies "run" to the result! *) 

331 
fun fatbar arity ms = 

332 
let 

30132  333 
fun LAM_Ts 0 t = ([], Term.fastype_of t) 
334 
 LAM_Ts n (_ $ Abs(_,T,t)) = 

335 
let val (Ts, U) = LAM_Ts (n1) t in (T::Ts, U) end 

336 
 LAM_Ts _ _ = fixrec_err "fatbar: internal error, not enough LAMs"; 

23152  337 
fun unLAM 0 t = t 
338 
 unLAM n (_$Abs(_,_,t)) = unLAM (n1) t 

339 
 unLAM _ _ = fixrec_err "fatbar: internal error, not enough LAMs"; 

30132  340 
fun reLAM ([], U) t = t 
341 
 reLAM (T::Ts, U) t = reLAM (Ts, T >> U) (cabs_const(T,U)$Abs("",T,t)); 

342 
val msum = foldr1 mk_mplus (map (unLAM arity) ms); 

343 
val (Ts, U) = LAM_Ts arity (hd ms) 

23152  344 
in 
30132  345 
reLAM (rev Ts, dest_maybeT U) (mk_run msum) 
23152  346 
end; 
347 

348 
(* this is the patternmatching compiler function *) 

30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

349 
fun compile_pats match_name eqs = 
23152  350 
let 
30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

351 
val (((n::names),(a::arities)),mats) = 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

352 
apfst ListPair.unzip (ListPair.unzip (map (match_eq match_name) eqs)); 
23152  353 
val cname = if forall (fn x => n=x) names then n 
354 
else fixrec_err "all equations in block must define the same function"; 

355 
val arity = if forall (fn x => a=x) arities then a 

356 
else fixrec_err "all equations in block must have the same arity"; 

357 
val rhs = fatbar arity mats; 

358 
in 

30132  359 
mk_trp (cname === rhs) 
23152  360 
end; 
361 

362 
(*************************************************************************) 

363 
(********************** Proving associated theorems **********************) 

364 
(*************************************************************************) 

365 

33519  366 
structure FixrecSimpData = Generic_Data 
367 
( 

33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

368 
type T = simpset; 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

369 
val empty = 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

370 
HOL_basic_ss 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

371 
addsimps simp_thms 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

372 
addsimps [@{thm beta_cfun}] 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

373 
addsimprocs [@{simproc cont_proc}]; 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

374 
val extend = I; 
33519  375 
val merge = merge_ss; 
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

376 
); 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

377 

7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

378 
fun fixrec_simp_tac ctxt = 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

379 
let 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

380 
val tab = FixrecUnfoldData.get (Context.Proof ctxt); 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

381 
val ss = FixrecSimpData.get (Context.Proof ctxt); 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

382 
fun concl t = 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

383 
if Logic.is_all t then concl (snd (Logic.dest_all t)) 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

384 
else HOLogic.dest_Trueprop (Logic.strip_imp_concl t); 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

385 
fun tac (t, i) = 
33430  386 
let 
387 
val Const (c, T) = chead_of (fst (HOLogic.dest_eq (concl t))); 

388 
val unfold_thm = the (Symtab.lookup tab c); 

389 
val rule = unfold_thm RS @{thm ssubst_lhs}; 

390 
in 

391 
CHANGED (rtac rule i THEN asm_simp_tac ss i) 

392 
end 

33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

393 
in 
33505  394 
SUBGOAL (fn ti => the_default no_tac (try tac ti)) 
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

395 
end; 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

396 

33442  397 
val fixrec_simp_add : attribute = 
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

398 
Thm.declaration_attribute 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

399 
(fn th => FixrecSimpData.map (fn ss => ss addsimps [th])); 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

400 

33442  401 
val fixrec_simp_del : attribute = 
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

402 
Thm.declaration_attribute 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

403 
(fn th => FixrecSimpData.map (fn ss => ss delsimps [th])); 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

404 

23152  405 
(* proves a block of pattern matching equations as theorems, using unfold *) 
32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
31740
diff
changeset

406 
fun make_simps ctxt (unfold_thm, eqns : (Attrib.binding * term) list) = 
23152  407 
let 
30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

408 
val tacs = 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

409 
[rtac (unfold_thm RS @{thm ssubst_lhs}) 1, 
32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
31740
diff
changeset

410 
asm_simp_tac (simpset_of ctxt) 1]; 
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
31740
diff
changeset

411 
fun prove_term t = Goal.prove ctxt [] [] t (K (EVERY tacs)); 
30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

412 
fun prove_eqn (bind, eqn_t) = (bind, prove_term eqn_t); 
23152  413 
in 
414 
map prove_eqn eqns 

415 
end; 

416 

417 
(*************************************************************************) 

418 
(************************* Main fixrec function **************************) 

419 
(*************************************************************************) 

420 

30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

421 
local 
31738
7b9b9ba532ca
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31177
diff
changeset

422 
(* code adapted from HOL/Tools/primrec.ML *) 
30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

423 

83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

424 
fun gen_fixrec 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

425 
(set_group : bool) 
30485  426 
prep_spec 
30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

427 
(strict : bool) 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

428 
raw_fixes 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

429 
raw_spec 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

430 
(lthy : local_theory) = 
23152  431 
let 
30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

432 
val (fixes : ((binding * typ) * mixfix) list, 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

433 
spec : (Attrib.binding * term) list) = 
30485  434 
fst (prep_spec raw_fixes raw_spec lthy); 
30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

435 
val chead_of_spec = 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

436 
chead_of o fst o dest_eqs o Logic.strip_imp_concl o strip_alls o snd; 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

437 
fun name_of (Free (n, _)) = n 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

438 
 name_of t = fixrec_err ("unknown term"); 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

439 
val all_names = map (name_of o chead_of_spec) spec; 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

440 
val names = distinct (op =) all_names; 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

441 
fun block_of_name n = 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

442 
map_filter 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

443 
(fn (m,eq) => if m = n then SOME eq else NONE) 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

444 
(all_names ~~ spec); 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

445 
val blocks = map block_of_name names; 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

446 

83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

447 
val matcher_tab = FixrecMatchData.get (ProofContext.theory_of lthy); 
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset

448 
fun match_name c = 
30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

449 
case Symtab.lookup matcher_tab c of SOME m => m 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

450 
 NONE => fixrec_err ("unknown pattern constructor: " ^ c); 
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset

451 

30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

452 
val matches = map (compile_pats match_name) (map (map snd) blocks); 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

453 
val spec' = map (pair Attrib.empty_binding) matches; 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

454 
val (lthy', cnames, fixdef_thms, unfold_thms) = 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

455 
add_fixdefs fixes spec' lthy; 
23152  456 
in 
457 
if strict then let (* only prove simp rules if strict = true *) 

30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

458 
val simps : (Attrib.binding * thm) list list = 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

459 
map (make_simps lthy') (unfold_thms ~~ blocks); 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

460 
fun mk_bind n : Attrib.binding = 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

461 
(Binding.name (n ^ "_simps"), 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

462 
[Attrib.internal (K Simplifier.simp_add)]); 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

463 
val simps1 : (Attrib.binding * thm list) list = 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

464 
map (fn (n,xs) => (mk_bind n, map snd xs)) (names ~~ simps); 
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

465 
val simps2 : (Attrib.binding * thm list) list = 
32952  466 
map (apsnd (fn thm => [thm])) (flat simps); 
30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

467 
val (_, lthy'') = lthy' 
31177  468 
> fold_map (LocalTheory.note Thm.generatedK) (simps1 @ simps2); 
23152  469 
in 
30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

470 
lthy'' 
23152  471 
end 
30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

472 
else lthy' 
23152  473 
end; 
474 

30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

475 
in 
23152  476 

30485  477 
val add_fixrec = gen_fixrec false Specification.check_spec; 
478 
val add_fixrec_cmd = gen_fixrec true Specification.read_spec; 

30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

479 

83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

480 
end; (* local *) 
23152  481 

482 
(*************************************************************************) 

483 
(******************************** Fixpat *********************************) 

484 
(*************************************************************************) 

485 

486 
fun fix_pat thy t = 

487 
let 

488 
val T = fastype_of t; 

489 
val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T)); 

490 
val cname = case chead_of t of Const(c,_) => c  _ => 

491 
fixrec_err "function is not declared as constant in theory"; 

26343
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset

492 
val unfold_thm = PureThy.get_thm thy (cname^"_unfold"); 
23152  493 
val simp = Goal.prove_global thy [] [] eq 
32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
31740
diff
changeset

494 
(fn _ => EVERY [stac unfold_thm 1, simp_tac (global_simpset_of thy) 1]); 
23152  495 
in simp end; 
496 

497 
fun gen_add_fixpat prep_term prep_attrib ((name, srcs), strings) thy = 

498 
let 

499 
val atts = map (prep_attrib thy) srcs; 

500 
val ts = map (prep_term thy) strings; 

501 
val simps = map (fix_pat thy) ts; 

502 
in 

29585  503 
(snd o PureThy.add_thmss [((name, simps), atts)]) thy 
23152  504 
end; 
505 

30485  506 
val add_fixpat = gen_add_fixpat Sign.cert_term (K I); 
507 
val add_fixpat_cmd = gen_add_fixpat Syntax.read_term_global Attrib.attribute; 

23152  508 

509 

510 
(*************************************************************************) 

511 
(******************************** Parsers ********************************) 

512 
(*************************************************************************) 

513 

514 
local structure P = OuterParse and K = OuterKeyword in 

515 

30485  516 
val _ = OuterSyntax.local_theory "fixrec" "define recursive functions (HOLCF)" K.thy_decl 
517 
((P.opt_keyword "permissive" >> not)  P.fixes  SpecParse.where_alt_specs 

518 
>> (fn ((strict, fixes), specs) => add_fixrec_cmd strict fixes specs)); 

23152  519 

30485  520 
val _ = OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl 
521 
(SpecParse.specs >> (Toplevel.theory o add_fixpat_cmd)); 

33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

522 

30485  523 
end; 
23152  524 

33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

525 
val setup = 
33522  526 
Attrib.setup @{binding fixrec_simp} 
33427  527 
(Attrib.add_del fixrec_simp_add fixrec_simp_del) 
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

528 
"declaration of fixrec simp rule" 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

529 
#> Method.setup @{binding fixrec_simp} 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

530 
(Scan.succeed (SIMPLE_METHOD' o fixrec_simp_tac)) 
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset

531 
"pattern prover for fixrec constants"; 
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset

532 

24867  533 
end; 