399 split_beta}. *} |
399 split_beta}. *} |
400 |
400 |
401 ML_setup {* |
401 ML_setup {* |
402 |
402 |
403 local |
403 local |
404 val cond_split_eta = thm "cond_split_eta"; |
404 val cond_split_eta_ss = HOL_basic_ss addsimps [thm "cond_split_eta"] |
405 fun Pair_pat k 0 (Bound m) = (m = k) |
405 fun Pair_pat k 0 (Bound m) = (m = k) |
406 | Pair_pat k i (Const ("Pair", _) $ Bound m $ t) = i > 0 andalso |
406 | Pair_pat k i (Const ("Pair", _) $ Bound m $ t) = i > 0 andalso |
407 m = k+i andalso Pair_pat k (i-1) t |
407 m = k+i andalso Pair_pat k (i-1) t |
408 | Pair_pat _ _ _ = false; |
408 | Pair_pat _ _ _ = false; |
409 fun no_args k i (Abs (_, _, t)) = no_args (k+1) i t |
409 fun no_args k i (Abs (_, _, t)) = no_args (k+1) i t |
413 fun split_pat tp i (Abs (_,_,t)) = if tp 0 i t then SOME (i,t) else NONE |
413 fun split_pat tp i (Abs (_,_,t)) = if tp 0 i t then SOME (i,t) else NONE |
414 | split_pat tp i (Const ("split", _) $ Abs (_, _, t)) = split_pat tp (i+1) t |
414 | split_pat tp i (Const ("split", _) $ Abs (_, _, t)) = split_pat tp (i+1) t |
415 | split_pat tp i _ = NONE; |
415 | split_pat tp i _ = NONE; |
416 fun metaeq thy ss lhs rhs = mk_meta_eq (Goal.prove thy [] [] |
416 fun metaeq thy ss lhs rhs = mk_meta_eq (Goal.prove thy [] [] |
417 (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs))) |
417 (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs))) |
418 (K (simp_tac (Simplifier.inherit_context ss HOL_basic_ss addsimps [cond_split_eta]) 1))); |
418 (K (simp_tac (Simplifier.inherit_context ss cond_split_eta_ss) 1))); |
419 |
419 |
420 fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k+1) i t |
420 fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k+1) i t |
421 | beta_term_pat k i (t $ u) = Pair_pat k i (t $ u) orelse |
421 | beta_term_pat k i (t $ u) = Pair_pat k i (t $ u) orelse |
422 (beta_term_pat k i t andalso beta_term_pat k i u) |
422 (beta_term_pat k i t andalso beta_term_pat k i u) |
423 | beta_term_pat k i t = no_args k i t; |
423 | beta_term_pat k i t = no_args k i t; |