# 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