author  huffman 
Tue, 02 Mar 2010 17:21:10 0800  
changeset 35525  fa231b86cb1e 
parent 33766  c679f05600cd 
child 35527  f4282471461d 
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 *) 
35525  38 
fun cfunT (T, U) = Type(@{type_name cfun}, [T, U]); 
30132  39 

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

41 

35525  42 
fun dest_cfunT (Type(@{type_name cfun}, [T, U])) = (T, U) 
30132  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 

35525  56 
fun binder_cfun (Type(@{type_name cfun},[T, U])) = T :: binder_cfun U 
33401
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 

35525  60 
fun body_cfun (Type(@{type_name cfun},[T, U])) = body_cfun U 
33401
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 

35525  102 
Type(@{type_name cfun}, [S, T]) => (S, T) 
30132  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 (fixdef_thms : (term * (string * thm)) list, lthy') = lthy 
33766
c679f05600cd
adapted Local_Theory.define  eliminated odd thm kind;
wenzelm
parents:
33726
diff
changeset

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

214 
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

215 
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

216 
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

217 
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

218 
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

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

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

221 
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

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

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

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

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

228 
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

229 
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

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

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

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

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

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

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

236 
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

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

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

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

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

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

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

243 
val (thmss, lthy'') = lthy' 
33671  244 
> fold_map Local_Theory.note (induct_note :: map unfold_note unfold_thms); 
23152  245 
in 
30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

246 
(lthy'', names, fixdef_thms, map snd unfold_thms) 
23152  247 
end; 
248 

249 
(*************************************************************************) 

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

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

252 

33522  253 
structure FixrecMatchData = Theory_Data 
254 
( 

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

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

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

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

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

260 

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

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

262 
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

263 

30157  264 
fun taken_names (t : term) : bstring list = 
265 
let 

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

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

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

270 
 taken (_ , bs) = bs; 

271 
in 

272 
taken (t, []) 

273 
end; 

23152  274 

275 
(* 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

276 
fun pre_build match_name pat rhs vs taken = 
23152  277 
case pat of 
26045  278 
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

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

281 
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

282 
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

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

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

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

286 
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

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

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

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

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

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

295 
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

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

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

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

302 

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

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

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

305 
fun building match_name pat rhs vs taken = 
23152  306 
case pat of 
26045  307 
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

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

310 
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

311 
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

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

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

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

315 
^ ML_Syntax.print_term pat); 
23152  316 

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

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

318 
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

319 

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

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

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

322 
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

323 
in 
30157  324 
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

325 
end; 
23152  326 

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

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

329 
fun fatbar arity ms = 

330 
let 

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

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

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

23152  335 
fun unLAM 0 t = t 
336 
 unLAM n (_$Abs(_,_,t)) = unLAM (n1) t 

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

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

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

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

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

346 
(* this is the patternmatching compiler function *) 

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

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

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

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

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

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

355 
val rhs = fatbar arity mats; 

356 
in 

30132  357 
mk_trp (cname === rhs) 
23152  358 
end; 
359 

360 
(*************************************************************************) 

361 
(********************** Proving associated theorems **********************) 

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

363 

33519  364 
structure FixrecSimpData = Generic_Data 
365 
( 

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

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

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

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

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

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

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

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

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

375 

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

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

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

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

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

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

381 
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

382 
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

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

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

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

388 
in 

389 
CHANGED (rtac rule i THEN asm_simp_tac ss i) 

390 
end 

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

391 
in 
33505  392 
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

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

394 

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

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

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

398 

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

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

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

402 

23152  403 
(* 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

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

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

407 
[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

408 
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

409 
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

410 
fun prove_eqn (bind, eqn_t) = (bind, prove_term eqn_t); 
23152  411 
in 
412 
map prove_eqn eqns 

413 
end; 

414 

415 
(*************************************************************************) 

416 
(************************* Main fixrec function **************************) 

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

418 

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

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

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

421 

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

422 
fun gen_fixrec 
30485  423 
prep_spec 
30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

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

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

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

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

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

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

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

433 
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

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

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

436 
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

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

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

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

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

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

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

443 

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

444 
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

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

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

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

448 

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

449 
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

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

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

452 
add_fixdefs fixes spec' lthy; 
23152  453 
in 
454 
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

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

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

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

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

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

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

461 
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

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

464 
val (_, lthy'') = lthy' 
33671  465 
> fold_map Local_Theory.note (simps1 @ simps2); 
23152  466 
in 
30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

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

469 
else lthy' 
23152  470 
end; 
471 

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

472 
in 
23152  473 

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

474 
val add_fixrec = gen_fixrec Specification.check_spec; 
0878aecbf119
eliminated slightly odd name space grouping  now managed by Isar toplevel;
wenzelm
parents:
33671
diff
changeset

475 
val add_fixrec_cmd = gen_fixrec Specification.read_spec; 
30158
83c50c62cf23
fixrec package uses newstyle syntax and localtheory interface
huffman
parents:
30157
diff
changeset

476 

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

477 
end; (* local *) 
23152  478 

479 
(*************************************************************************) 

480 
(******************************** Fixpat *********************************) 

481 
(*************************************************************************) 

482 

483 
fun fix_pat thy t = 

484 
let 

485 
val T = fastype_of t; 

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

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

488 
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

489 
val unfold_thm = PureThy.get_thm thy (cname^"_unfold"); 
23152  490 
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

491 
(fn _ => EVERY [stac unfold_thm 1, simp_tac (global_simpset_of thy) 1]); 
23152  492 
in simp end; 
493 

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

495 
let 

496 
val atts = map (prep_attrib thy) srcs; 

497 
val ts = map (prep_term thy) strings; 

498 
val simps = map (fix_pat thy) ts; 

499 
in 

29585  500 
(snd o PureThy.add_thmss [((name, simps), atts)]) thy 
23152  501 
end; 
502 

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

23152  505 

506 

507 
(*************************************************************************) 

508 
(******************************** Parsers ********************************) 

509 
(*************************************************************************) 

510 

511 
local structure P = OuterParse and K = OuterKeyword in 

512 

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

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

23152  516 

30485  517 
val _ = OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl 
518 
(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

519 

30485  520 
end; 
23152  521 

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

522 
val setup = 
33522  523 
Attrib.setup @{binding fixrec_simp} 
33427  524 
(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

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

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

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

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

529 

24867  530 
end; 