# HG changeset patch
# User blanchet
# Date 1380104946 -7200
# Node ID a1a52423601fc8ba17e112cb8666c8cdb62b2ad0
# Parent  5d45882b4f366012d7fd2513d148fe225f7e8c0c
more powerful fold

diff -r 5d45882b4f36 -r a1a52423601f src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Wed Sep 25 12:00:22 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Wed Sep 25 12:29:06 2013 +0200
@@ -51,11 +51,6 @@
 val abs_tuple = HOLogic.tupled_lambda o HOLogic.mk_tuple;
 fun drop_All t = subst_bounds (strip_qnt_vars @{const_name all} t |> map Free |> rev,
   strip_qnt_body @{const_name all} t)
-fun s_not @{const True} = @{const False}
-  | s_not @{const False} = @{const True}
-  | s_not (@{const Not} $ t) = t
-  | s_not (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
-  | s_not t = HOLogic.mk_not t
 val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default @{const True};
 val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default @{const False};
 fun invert_prems [t] = map s_not (HOLogic.disjuncts t)
diff -r 5d45882b4f36 -r a1a52423601f src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 25 12:00:22 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 25 12:29:06 2013 +0200
@@ -51,6 +51,7 @@
      nested_map_comps: thm list,
      ctr_specs: corec_ctr_spec list}
 
+  val s_not: term -> term
   val massage_indirect_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) ->
     typ list -> term -> term -> term -> term
   val massage_direct_corec_call: Proof.context -> (term -> bool) -> (term -> term) -> typ list ->
@@ -60,8 +61,8 @@
   val expand_corec_code_rhs: Proof.context -> (term -> bool) -> typ list -> term -> term
   val massage_corec_code_rhs: Proof.context -> (term -> term list -> term) -> typ list -> typ ->
     term -> term
-  val fold_rev_corec_code_rhs: Proof.context -> (term -> term list -> 'a -> 'a) -> typ list ->
-    term -> 'a -> 'a
+  val fold_rev_corec_code_rhs: Proof.context -> (term list -> term -> term list -> 'a -> 'a) ->
+    typ list -> term -> 'a -> 'a
   val rec_specs_of: binding list -> typ list -> typ list -> (term -> int list) ->
     ((term * term list list) list) list -> local_theory ->
     (bool * rec_spec list * typ list * thm * thm list) * local_theory
@@ -138,6 +139,12 @@
 fun unexpected_corec_call ctxt t =
   error ("Unexpected corecursive call: " ^ quote (Syntax.string_of_term ctxt t));
 
+fun s_not @{const True} = @{const False}
+  | s_not @{const False} = @{const True}
+  | s_not (@{const Not} $ t) = t
+  | s_not (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
+  | s_not t = HOLogic.mk_not t
+
 fun factor_out_types ctxt massage destU U T =
   (case try destU U of
     SOME (U1, U2) => if U1 = T then massage T U2 else invalid_map ctxt
@@ -200,22 +207,24 @@
   let
     val thy = Proof_Context.theory_of ctxt;
 
-    fun fld t =
+    fun fld conds t =
       (case Term.strip_comb t of
-        (Const (@{const_name Let}, _), [arg1, arg2]) => fld (betapply (arg2, arg1))
-      | (Const (@{const_name If}, _), _ :: branches) => fold_rev fld branches
+        (Const (@{const_name Let}, _), [arg1, arg2]) => fld conds (betapply (arg2, arg1))
+      | (Const (@{const_name If}, _), [cond, then_branch, else_branch]) =>
+        fld (cond :: conds) then_branch o fld (s_not cond :: conds) else_branch
       | (Const (c, _), args as _ :: _) =>
         let val n = num_binder_types (Sign.the_const_type thy c) in
           (case fastype_of1 (bound_Ts, nth args (n - 1)) of
             Type (s, Ts) =>
             (case dest_case ctxt s Ts t of
-              NONE => f t
-            | SOME (conds, branches) => fold_rev fld branches)
-          | _ => f t)
+              NONE => f conds t
+            | SOME (conds', branches) =>
+              fold_rev (uncurry fld) (map (fn cond => cond :: conds) conds' ~~ branches))
+          | _ => f conds t)
         end
-      | _ => f t)
+      | _ => f conds t)
   in
-    fld
+    fld []
   end;
 
 fun case_of ctxt = ctr_sugar_of ctxt #> Option.map (fst o dest_Const o #casex);
@@ -332,7 +341,8 @@
 fun massage_corec_code_rhs ctxt massage_ctr =
   massage_let_if_case ctxt (K false) (uncurry massage_ctr o Term.strip_comb);
 
-fun fold_rev_corec_code_rhs ctxt f = fold_rev_let_if_case ctxt (uncurry f o Term.strip_comb);
+fun fold_rev_corec_code_rhs ctxt f =
+  fold_rev_let_if_case ctxt (fn conds => uncurry (f conds) o Term.strip_comb);
 
 fun indexed xs h = let val h' = h + length xs in (h upto h' - 1, h') end;
 fun indexedd xss = fold_map indexed xss;