# HG changeset patch
# User blanchet
# Date 1389276445 -3600
# Node ID e25b4d22082bd5a67bda29c73a90b77f49e3055e
# Parent  f00012c2034405b7136270baf3115d699267609b
for code equations that coincide with ctr equations, make sure the usr's input is preserved for both

diff -r f00012c20344 -r e25b4d22082b src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Thu Jan 09 14:09:44 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Thu Jan 09 15:07:25 2014 +0100
@@ -568,7 +568,7 @@
   end;
 
 fun dissect_coeqn_sel fun_names (basic_ctr_specss : basic_corec_ctr_spec list list) eqn_pos
-    ctr_rhs_opt code_rhs_opt eqn' of_spec_opt eqn =
+    ctr_rhs_opt code_rhs_opt eqn0 of_spec_opt eqn =
   let
     val (lhs, rhs) = HOLogic.dest_eq eqn
       handle TERM _ =>
@@ -585,7 +585,7 @@
         SOME of_spec => the (find_first (curry (op =) of_spec o #ctr) basic_ctr_specs)
       | NONE => filter (exists (curry (op =) sel) o #sels) basic_ctr_specs |> the_single
           handle List.Empty => primcorec_error_eqn "ambiguous selector - use \"of\"" eqn);
-    val user_eqn = drop_All eqn';
+    val user_eqn = drop_All eqn0;
   in
     Sel {
       fun_name = fun_name,
@@ -602,7 +602,7 @@
   end;
 
 fun dissect_coeqn_ctr fun_names sequentials (basic_ctr_specss : basic_corec_ctr_spec list list)
-    eqn_pos eqn' code_rhs_opt prems concl matchedsss =
+    eqn_pos eqn0 code_rhs_opt prems concl matchedsss =
   let
     val (lhs, rhs) = HOLogic.dest_eq concl;
     val (fun_name, fun_args) = strip_comb lhs |>> fst o dest_Free;
@@ -630,12 +630,12 @@
 
     val eqns_data_sel =
       map (dissect_coeqn_sel fun_names basic_ctr_specss eqn_pos
-        (SOME (abstract (List.rev fun_args) rhs)) code_rhs_opt eqn' (SOME ctr)) sel_concls;
+        (SOME (abstract (List.rev fun_args) rhs)) code_rhs_opt eqn0 (SOME ctr)) sel_concls;
   in
     (the_list eqn_data_disc_opt @ eqns_data_sel, matchedsss')
   end;
 
-fun dissect_coeqn_code lthy has_call fun_names basic_ctr_specss eqn_pos eqn' concl matchedsss =
+fun dissect_coeqn_code lthy has_call fun_names basic_ctr_specss eqn_pos eqn0 concl matchedsss =
   let
     val (lhs, (rhs', rhs)) = HOLogic.dest_eq concl ||> `(expand_corec_code_rhs lthy has_call []);
     val (fun_name, fun_args) = strip_comb lhs |>> fst o dest_Free;
@@ -657,16 +657,16 @@
 
     val sequentials = replicate (length fun_names) false;
   in
-    fold_map2 (dissect_coeqn_ctr fun_names sequentials basic_ctr_specss eqn_pos eqn'
+    fold_map2 (dissect_coeqn_ctr fun_names sequentials basic_ctr_specss eqn_pos eqn0
         (SOME (abstract (List.rev fun_args) rhs)))
       ctr_premss ctr_concls matchedsss
   end;
 
 fun dissect_coeqn lthy has_call fun_names sequentials
-    (basic_ctr_specss : basic_corec_ctr_spec list list) (eqn_pos, eqn') of_spec_opt matchedsss =
+    (basic_ctr_specss : basic_corec_ctr_spec list list) (eqn_pos, eqn0) of_spec_opt matchedsss =
   let
-    val eqn = drop_All eqn'
-      handle TERM _ => primcorec_error_eqn "malformed function equation" eqn';
+    val eqn = drop_All eqn0
+      handle TERM _ => primcorec_error_eqn "malformed function equation" eqn0;
     val (prems, concl) = Logic.strip_horn eqn
       |> apfst (map HOLogic.dest_Trueprop) o apsnd HOLogic.dest_Trueprop;
 
@@ -681,20 +681,23 @@
     val ctrs = maps (map #ctr) basic_ctr_specss;
   in
     if member (op =) discs head orelse
-      is_some rhs_opt andalso
-        member (op =) (filter (null o binder_types o fastype_of) ctrs) (the rhs_opt) then
-      dissect_coeqn_disc fun_names sequentials basic_ctr_specss eqn_pos NONE NONE prems concl matchedsss
+        is_some rhs_opt andalso
+          member (op =) (filter (null o binder_types o fastype_of) ctrs) (the rhs_opt) then
+      dissect_coeqn_disc fun_names sequentials basic_ctr_specss eqn_pos NONE NONE prems concl
+        matchedsss
       |>> single
     else if member (op =) sels head then
-      ([dissect_coeqn_sel fun_names basic_ctr_specss eqn_pos NONE NONE eqn' of_spec_opt concl],
+      ([dissect_coeqn_sel fun_names basic_ctr_specss eqn_pos NONE NONE eqn0 of_spec_opt concl],
        matchedsss)
-    else if is_Free head andalso member (op =) fun_names (fst (dest_Free head)) andalso
-      member (op =) ctrs (head_of (unfold_let (the rhs_opt))) then
-      dissect_coeqn_ctr fun_names sequentials basic_ctr_specss eqn_pos eqn' NONE prems concl matchedsss
-    else if is_Free head andalso member (op =) fun_names (fst (dest_Free head)) andalso
-      null prems then
-      dissect_coeqn_code lthy has_call fun_names basic_ctr_specss eqn_pos eqn' concl matchedsss
-      |>> flat
+    else if is_Free head andalso member (op =) fun_names (fst (dest_Free head)) then
+      if member (op =) ctrs (head_of (unfold_let (the rhs_opt))) then
+        dissect_coeqn_ctr fun_names sequentials basic_ctr_specss eqn_pos eqn0
+          (if null prems then SOME eqn0 else NONE) prems concl matchedsss
+      else if null prems then
+        dissect_coeqn_code lthy has_call fun_names basic_ctr_specss eqn_pos eqn0 concl matchedsss
+        |>> flat
+      else
+        primcorec_error_eqn "malformed constructor or code view equation" eqn
     else
       primcorec_error_eqn "malformed function equation" eqn
   end;
@@ -939,7 +942,7 @@
 *)
 
     val excludess'' = map2 (fn sequential => map (fn (idx, goal) =>
-        (idx, (Option.map (Goal.prove lthy [] [] goal #> Thm.close_derivation)
+        (idx, (Option.map (Goal.prove_sorry lthy [] [] goal #> Thm.close_derivation)
            (exclude_tac sequential idx), goal))))
       sequentials excludess';
     val taut_thmss = map (map (apsnd (the o fst)) o filter (is_some o fst o snd)) excludess'';
@@ -960,7 +963,7 @@
       map2 (fn b => fn b' => b orelse b') exhaustives syntactic_exhaustives;
 
     fun map_prove_with_tac tac =
-      map (fn goal => Goal.prove lthy [] [] goal tac |> Thm.close_derivation);
+      map (fn goal => Goal.prove_sorry lthy [] [] goal tac |> Thm.close_derivation);
 
     val nchotomy_goalss =
       map2 (fn false => K [] | true => single o HOLogic.mk_Trueprop o mk_dnf o map #prems)
@@ -1004,7 +1007,7 @@
               | [nchotomy_thm] => fn [goal] =>
                 [mk_primcorec_exhaust_tac lthy ("" (* for "P" *) :: map (fst o dest_Free) fun_args)
                    (length disc_eqns) nchotomy_thm
-                 |> K |> Goal.prove lthy [] [] goal
+                 |> K |> Goal.prove_sorry lthy [] [] goal
                  |> Thm.close_derivation])
             disc_eqnss nchotomy_thmss;
         val nontriv_exhaust_thmss = map (filter_out is_trivial_implies) exhaust_thmss;
@@ -1037,7 +1040,7 @@
                 []
               else
                 mk_primcorec_disc_tac lthy def_thms disc_corec k m excludesss
-                |> K |> Goal.prove lthy [] [] goal
+                |> K |> Goal.prove_sorry lthy [] [] goal
                 |> Thm.close_derivation
                 |> pair (#disc (nth ctr_specs ctr_no))
                 |> pair eqn_pos
@@ -1067,7 +1070,7 @@
           in
             mk_primcorec_sel_tac lthy def_thms distincts sel_splits sel_split_asms nested_map_idents
               nested_map_comps sel_corec k m excludesss
-            |> K |> Goal.prove lthy [] [] goal
+            |> K |> Goal.prove_sorry lthy [] [] goal
             |> Thm.close_derivation
             |> pair sel
             |> pair eqn_pos
@@ -1081,8 +1084,9 @@
             orelse
               filter (curry (op =) ctr o #ctr) sel_eqns
               |> fst o finds ((op =) o apsnd #sel) sels
-              |> exists (null o snd)
-          then [] else
+              |> exists (null o snd) then
+            []
+          else
             let
               val (fun_name, fun_T, fun_args, prems, rhs_opt, eqn_pos) =
                 (find_first (curry (op =) ctr o #ctr) disc_eqns,
@@ -1109,7 +1113,7 @@
             in
               if prems = [@{term False}] then [] else
                 mk_primcorec_ctr_of_dtr_tac lthy m collapse disc_thm_opt sel_thms
-                |> K |> Goal.prove lthy [] [] goal
+                |> K |> Goal.prove_sorry lthy [] [] goal
                 |> Thm.close_derivation
                 |> pair ctr
                 |> pair eqn_pos
@@ -1191,11 +1195,11 @@
                     val raw_code_thm = mk_primcorec_raw_code_of_ctr_tac lthy distincts discIs
                         sel_splits sel_split_asms ms ctr_thms
                         (if exhaustive_code then try the_single nchotomys else NONE)
-                      |> K |> Goal.prove lthy [] [] raw_goal
+                      |> K |> Goal.prove_sorry lthy [] [] raw_goal
                       |> Thm.close_derivation;
                   in
                     mk_primcorec_code_of_raw_code_tac lthy distincts sel_splits raw_code_thm
-                    |> K |> Goal.prove lthy [] [] goal
+                    |> K |> Goal.prove_sorry lthy [] [] goal
                     |> Thm.close_derivation
                     |> single
                   end)
@@ -1227,7 +1231,7 @@
               else
                 mk_primcorec_disc_iff_tac lthy (map (fst o dest_Free) fun_args)
                   (the_single exhaust_thms) (the_single disc_thms) disc_thmss' (flat disc_excludess)
-                |> K |> Goal.prove lthy [] [] goal
+                |> K |> Goal.prove_sorry lthy [] [] goal
                 |> Thm.close_derivation
                 |> pair eqn_pos
                 |> single