# HG changeset patch # User blanchet # Date 1391639402 -3600 # Node ID 3d2c97392e256eb2944ef10825b6a69cdb05eddf # Parent 580abab41c8cf44dc2ef4d3036ce5cf20d69c3dc adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas diff -r 580abab41c8c -r 3d2c97392e25 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Wed Feb 05 18:19:25 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Wed Feb 05 23:30:02 2014 +0100 @@ -143,7 +143,7 @@ |> (fn [cs] => cs | css => [s_disjs (map s_conjs css)]) end; -fun fold_rev_let_if_case ctxt f bound_Ts t = +fun fold_rev_let_if_case ctxt f bound_Ts = let val thy = Proof_Context.theory_of ctxt; @@ -158,17 +158,16 @@ (case fastype_of1 (bound_Ts, nth args n) of Type (s, Ts) => (case dest_case ctxt s Ts t of - SOME (ctr_sugar as {sel_splits = _ :: _, ...}, conds', branches) => - apfst (cons ctr_sugar) o fold_rev (uncurry fld) - (map (append conds o conjuncts_s) conds' ~~ branches) - | _ => apsnd (f conds t)) - | _ => apsnd (f conds t)) + SOME ({sel_splits = _ :: _, ...}, conds', branches) => + fold_rev (uncurry fld) (map (append conds o conjuncts_s) conds' ~~ branches) + | _ => f conds t) + | _ => f conds t) else - apsnd (f conds t) + f conds t end - | _ => apsnd (f conds t)) + | _ => f conds t) in - fld [] t o pair [] + fld [] end; fun case_of ctxt s = @@ -336,10 +335,23 @@ (fn bound_Ts => uncurry (massage_ctr bound_Ts) o Term.strip_comb); fun fold_rev_corec_code_rhs ctxt f = - snd ooo fold_rev_let_if_case ctxt (fn conds => uncurry (f conds) o Term.strip_comb); + fold_rev_let_if_case ctxt (fn conds => uncurry (f conds) o Term.strip_comb); fun case_thms_of_term ctxt bound_Ts t = - let val (ctr_sugars, _) = fold_rev_let_if_case ctxt (K (K I)) bound_Ts t () in + let + fun ctr_sugar_of_case c s = + (case ctr_sugar_of ctxt s of + SOME (ctr_sugar as {casex = Const (c', _), ...}) => if c' = c then SOME ctr_sugar else NONE + | _ => NONE); + fun add_ctr_sugar (s, Type (@{type_name fun}, [_, T])) = + binder_types T + |> map_filter (try (fst o dest_Type)) + |> distinct (op =) + |> map_filter (ctr_sugar_of_case s) + | add_ctr_sugar _ = []; + + val ctr_sugars = maps add_ctr_sugar (Term.add_consts t []); + in (maps #distincts ctr_sugars, maps #discIs ctr_sugars, maps #disc_exhausts ctr_sugars, maps #sel_splits ctr_sugars, maps #sel_split_asms ctr_sugars) end; @@ -884,10 +896,9 @@ let val sel_no = find_first (curry (op =) ctr o #ctr) basic_ctr_specs |> find_index (curry (op =) sel) o #sels o the; - fun find t = if has_call t then snd (fold_rev_let_if_case ctxt (K cons) [] t []) else []; in - find rhs_term - |> K |> nth_map sel_no |> AList.map_entry (op =) ctr + K (if has_call rhs_term then fold_rev_let_if_case ctxt (K cons) [] rhs_term [] else []) + |> nth_map sel_no |> AList.map_entry (op =) ctr end; fun applied_fun_of fun_name fun_T fun_args = diff -r 580abab41c8c -r 3d2c97392e25 src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Wed Feb 05 18:19:25 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Wed Feb 05 23:30:02 2014 +0100 @@ -130,7 +130,7 @@ m excludesss = prelude_tac ctxt defs (fun_sel RS trans) THEN cases_tac ctxt k m excludesss THEN - HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE' rtac ext ORELSE' + HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE' eresolve_tac falseEs ORELSE' resolve_tac split_connectI ORELSE' Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE' @@ -138,7 +138,9 @@ eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE' etac notE THEN' atac ORELSE' (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def comp_def split_def - sum.cases} @ mapsx @ map_comps @ map_idents))))); + sum.cases} @ mapsx @ map_comps @ map_idents))) ORELSE' + fo_rtac @{thm cong} ctxt ORELSE' + rtac ext)); fun mk_primcorec_ctr_tac ctxt m collapse disc_fun_opt sel_funs = HEADGOAL (rtac ((if null sel_funs then collapse else collapse RS sym) RS trans) THEN' diff -r 580abab41c8c -r 3d2c97392e25 src/HOL/Tools/BNF/bnf_tactics.ML --- a/src/HOL/Tools/BNF/bnf_tactics.ML Wed Feb 05 18:19:25 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_tactics.ML Wed Feb 05 23:30:02 2014 +0100 @@ -34,14 +34,15 @@ open Ctr_Sugar_General_Tactics open BNF_Util -(*stolen from Christian Urban's Cookbook*) +(*stolen from Christian Urban's Cookbook (and adapted slightly)*) fun fo_rtac thm = Subgoal.FOCUS (fn {concl, ...} => let val concl_pat = Drule.strip_imp_concl (cprop_of thm) val insts = Thm.first_order_match (concl_pat, concl) in rtac (Drule.instantiate_normalize insts thm) 1 - end); + end + handle Pattern.MATCH => no_tac); (*transforms f (g x) = h (k x) into f o g = h o k using first order matches for f, g, h, and k*) fun mk_pointfree ctxt thm = thm