equal
deleted
inserted
replaced
251 | Const(_,_) => (pat, (vs, rhs)) |
251 | Const(_,_) => (pat, (vs, rhs)) |
252 | _ => fixrec_err ("invalid function pattern: " |
252 | _ => fixrec_err ("invalid function pattern: " |
253 ^ ML_Syntax.print_term pat) |
253 ^ ML_Syntax.print_term pat) |
254 |
254 |
255 fun strip_alls t = |
255 fun strip_alls t = |
256 if Logic.is_all t then strip_alls (snd (Logic.dest_all t)) else t |
256 (case try Logic.dest_all t of |
|
257 SOME (_, u) => strip_alls u |
|
258 | NONE => t) |
257 |
259 |
258 fun compile_eq match_name eq = |
260 fun compile_eq match_name eq = |
259 let |
261 let |
260 val (lhs,rhs) = dest_eqs (Logic.strip_imp_concl (strip_alls eq)) |
262 val (lhs,rhs) = dest_eqs (Logic.strip_imp_concl (strip_alls eq)) |
261 in |
263 in |
291 |
293 |
292 fun fixrec_simp_tac ctxt = |
294 fun fixrec_simp_tac ctxt = |
293 let |
295 let |
294 val tab = FixrecUnfoldData.get (Context.Proof ctxt) |
296 val tab = FixrecUnfoldData.get (Context.Proof ctxt) |
295 val ss = Simplifier.simpset_of ctxt |
297 val ss = Simplifier.simpset_of ctxt |
296 fun concl t = |
298 val concl = HOLogic.dest_Trueprop o Logic.strip_imp_concl o strip_alls |
297 if Logic.is_all t then concl (snd (Logic.dest_all t)) |
|
298 else HOLogic.dest_Trueprop (Logic.strip_imp_concl t) |
|
299 fun tac (t, i) = |
299 fun tac (t, i) = |
300 let |
300 let |
301 val (c, _) = |
301 val (c, _) = |
302 (dest_Const o head_of o chead_of o fst o HOLogic.dest_eq o concl) t |
302 (dest_Const o head_of o chead_of o fst o HOLogic.dest_eq o concl) t |
303 val unfold_thm = the (Symtab.lookup tab c) |
303 val unfold_thm = the (Symtab.lookup tab c) |