1.1 --- a/src/HOL/BNF/BNF_FP_Base.thy	Thu Sep 19 01:15:26 2013 +0200
     1.2 +++ b/src/HOL/BNF/BNF_FP_Base.thy	Thu Sep 19 02:30:45 2013 +0200
     1.3 @@ -172,6 +172,15 @@
     1.4     (if b then f y else if b' then x' else f y')"
     1.5    by simp
     1.6  
     1.7 +lemma if_then_else_True_False:
     1.8 +  "(if p then False else r) \<longleftrightarrow> \<not> p \<and> r"
     1.9 +  "(if p then True else r) \<longleftrightarrow> p \<or> r"
    1.10 +  "(if p then q else False) \<longleftrightarrow> p \<and> q"
    1.11 +  "(if p then q else True) \<longleftrightarrow> \<not> p \<or> q"
    1.12 +by simp_all
    1.13 +
    1.14 +lemmas bool_if_simps = bool_simps(7,8,15-17,19,21-24,29-32) if_then_else_True_False
    1.15 +
    1.16  ML_file "Tools/bnf_fp_util.ML"
    1.17  ML_file "Tools/bnf_fp_def_sugar_tactics.ML"
    1.18  ML_file "Tools/bnf_fp_def_sugar.ML"

     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 19 01:15:26 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 19 02:30:45 2013 +0200
     2.3 @@ -59,6 +59,7 @@
     2.4      (typ -> typ -> term -> term) -> typ list -> typ -> term -> term
     2.5    val expand_corec_code_rhs: Proof.context -> (term -> bool) -> typ list -> term -> term
     2.6    val massage_corec_code_rhs: Proof.context -> (term -> term list -> term) -> typ -> term -> term
     2.7 +  val simplify_bool_ifs: theory -> term -> term list
     2.8    val rec_specs_of: binding list -> typ list -> typ list -> (term -> int list) ->
     2.9      ((term * term list list) list) list -> local_theory ->
    2.10      (bool * rec_spec list * typ list * thm * thm list) * local_theory
    2.11 @@ -297,6 +298,15 @@
    2.12  fun massage_corec_code_rhs ctxt massage_ctr =
    2.13    massage_let_and_if ctxt (K false) (uncurry massage_ctr o Term.strip_comb);
    2.14  
    2.15 +fun add_conjuncts (Const (@{const_name conj}, _) $ t $ t') = add_conjuncts t o add_conjuncts t'
    2.16 +  | add_conjuncts t = cons t;
    2.17 +
    2.18 +fun conjuncts t = add_conjuncts t [];
    2.19 +
    2.20 +fun simplify_bool_ifs thy =
    2.21 +  Raw_Simplifier.rewrite_term thy @{thms bool_if_simps[THEN eq_reflection]} []
    2.22 +  #> conjuncts #> (fn [@{term True}] => [] | ts => ts);
    2.23 +
    2.24  fun indexed xs h = let val h' = h + length xs in (h upto h' - 1, h') end;
    2.25  fun indexedd xss = fold_map indexed xss;
    2.26  fun indexeddd xsss = fold_map indexedd xsss;