adapted FP code to new relator approach

--- a/src/HOL/Codatatype/Examples/Misc_Data.thy	Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Misc_Data.thy	Thu Sep 20 02:42:48 2012 +0200
@@ -20,6 +20,8 @@
   @{typ "('a \<Rightarrow> 'a) + ('a + 'b) + 'c"} (BNF_Comp.empty_unfold, lthy)))
 *}
 
+print_theorems
+
 data 'a lst = Nl | Cns 'a "'a lst"
 
 thm pre_lst.rel_unfold

--- a/src/HOL/Codatatype/Tools/bnf_comp.ML	Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp.ML	Thu Sep 20 02:42:48 2012 +0200
@@ -267,7 +267,7 @@
 
     val (bnf', lthy') =
       bnf_def const_policy (K Derive_Some_Facts) qualify tacs wit_tac (SOME (oDs @ flat Dss))
-        (((((b, mapx), sets), bd), wits), rel) lthy;
+        (((((b, mapx), sets), bd), wits), SOME rel) lthy;
 
     val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (rel_def_of_bnf bnf')
       unfold;
@@ -365,7 +365,7 @@
 
     val (bnf', lthy') =
       bnf_def Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME (killedAs @ Ds))
-        (((((b, mapx), sets), Term.absdummy T bd), wits), rel) lthy;
+        (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
 
     val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (rel_def_of_bnf bnf')
       unfold;
@@ -453,7 +453,7 @@
 
     val (bnf', lthy') =
       bnf_def Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME Ds)
-        (((((b, mapx), sets), Term.absdummy T bd), wits), rel) lthy;
+        (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
 
     val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (rel_def_of_bnf bnf')
       unfold;
@@ -531,7 +531,7 @@
 
     val (bnf', lthy') =
       bnf_def Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME Ds)
-        (((((b, mapx), sets), Term.absdummy T bd), wits), rel) lthy;
+        (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
 
     val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (rel_def_of_bnf bnf')
       unfold;
@@ -673,7 +673,7 @@
     val policy = user_policy Derive_All_Facts;
 
     val (bnf', lthy') = bnf_def Hardly_Inline policy I tacs wit_tac (SOME deads)
-      (((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), bnf_rel) lthy;
+      (((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), SOME bnf_rel) lthy;
   in
     ((bnf', deads), lthy')
   end;

--- a/src/HOL/Codatatype/Tools/bnf_def.ML	Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML	Thu Sep 20 02:42:48 2012 +0200
@@ -90,7 +90,7 @@
   val bnf_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
     ({prems: thm list, context: Proof.context} -> tactic) list ->
     ({prems: thm list, context: Proof.context} -> tactic) -> typ list option ->
-    ((((binding * term) * term list) * term) * term list) * term -> local_theory ->
+    ((((binding * term) * term list) * term) * term list) * term option -> local_theory ->
     BNF * local_theory
 end;
 
@@ -533,7 +533,7 @@
 (* Define new BNFs *)
 
 fun prepare_def const_policy mk_fact_policy qualify prep_term Ds_opt
-  (((((raw_b, raw_map), raw_sets), raw_bd_Abs), raw_wits), raw_rel) no_defs_lthy =
+  (((((raw_b, raw_map), raw_sets), raw_bd_Abs), raw_wits), raw_rel_opt) no_defs_lthy =
   let
     val fact_policy = mk_fact_policy no_defs_lthy;
     val b = qualify raw_b;
@@ -546,7 +546,6 @@
       Abs (_, T, t) => (T, t)
     | _ => error "Bad bound constant");
     val wit_rhss = map (prep_term no_defs_lthy) raw_wits;
-    val rel_rhs = prep_term no_defs_lthy raw_rel;
 
     fun err T =
       error ("Trying to register the type " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^
@@ -560,20 +559,6 @@
         | T => err T)
       else (b, Local_Theory.full_name no_defs_lthy b);
 
-    val map_bind_def = (fn () => Binding.suffix_name ("_" ^ mapN) b, map_rhs);
-    val set_binds_defs =
-      let
-        val bs = if live = 1 then [fn () => Binding.suffix_name ("_" ^ setN) b]
-          else map (fn i => fn () => Binding.suffix_name ("_" ^ mk_setN i) b) (1 upto live)
-      in map2 pair bs set_rhss end;
-    val bd_bind_def = (fn () => Binding.suffix_name ("_" ^ bdN) b, bd_rhs);
-    val wit_binds_defs =
-      let
-        val bs = if nwits = 1 then [fn () => Binding.suffix_name ("_" ^ witN) b]
-          else map (fn i => fn () => Binding.suffix_name ("_" ^ mk_witN i) b) (1 upto nwits);
-      in map2 pair bs wit_rhss end;
-    val rel_bind_def = (fn () => Binding.suffix_name ("_" ^ relN) b, rel_rhs);
-
     fun maybe_define (b, rhs) lthy =
       let
         val inline =
@@ -591,31 +576,40 @@
               lthy)
           end
       end;
-    fun maybe_restore lthy0 lthy = lthy |> not (pointer_eq (lthy0, lthy)) ? Local_Theory.restore;
+
+    fun maybe_restore lthy_old lthy =
+      lthy |> not (pointer_eq (lthy_old, lthy)) ? Local_Theory.restore;
 
-    val ((((((bnf_map_term, raw_map_def),
+    val map_bind_def = (fn () => Binding.suffix_name ("_" ^ mapN) b, map_rhs);
+    val set_binds_defs =
+      let
+        val bs = if live = 1 then [fn () => Binding.suffix_name ("_" ^ setN) b]
+          else map (fn i => fn () => Binding.suffix_name ("_" ^ mk_setN i) b) (1 upto live)
+      in map2 pair bs set_rhss end;
+    val bd_bind_def = (fn () => Binding.suffix_name ("_" ^ bdN) b, bd_rhs);
+    val wit_binds_defs =
+      let
+        val bs = if nwits = 1 then [fn () => Binding.suffix_name ("_" ^ witN) b]
+          else map (fn i => fn () => Binding.suffix_name ("_" ^ mk_witN i) b) (1 upto nwits);
+      in map2 pair bs wit_rhss end;
+
+    val (((((bnf_map_term, raw_map_def),
       (bnf_set_terms, raw_set_defs)),
       (bnf_bd_term, raw_bd_def)),
-      (bnf_wit_terms, raw_wit_defs)),
-      (bnf_rel_term, raw_rel_def)), (lthy1, lthy0)) =
+      (bnf_wit_terms, raw_wit_defs)), (lthy, lthy_old)) =
         no_defs_lthy
         |> maybe_define map_bind_def
         ||>> apfst split_list o fold_map maybe_define set_binds_defs
         ||>> maybe_define bd_bind_def
         ||>> apfst split_list o fold_map maybe_define wit_binds_defs
-        ||>> maybe_define rel_bind_def
         ||> `(maybe_restore no_defs_lthy);
 
-    val phi = Proof_Context.export_morphism lthy0 lthy1;
+    val phi = Proof_Context.export_morphism lthy_old lthy;
 
     val bnf_map_def = Morphism.thm phi raw_map_def;
     val bnf_set_defs = map (Morphism.thm phi) raw_set_defs;
     val bnf_bd_def = Morphism.thm phi raw_bd_def;
     val bnf_wit_defs = map (Morphism.thm phi) raw_wit_defs;
-    val bnf_rel_def = Morphism.thm phi raw_rel_def;
-
-    val one_step_defs =
-      filter_out_refl (bnf_map_def :: bnf_bd_def :: bnf_set_defs @ bnf_wit_defs @ [bnf_rel_def]);
 
     val bnf_map = Morphism.term phi bnf_map_term;
 
@@ -635,7 +629,6 @@
     val bnf_bd =
       Term.subst_TVars (Term.add_tvar_namesT bdT [] ~~ CA_params) (Morphism.term phi bnf_bd_term);
     val bnf_wits = map (normalize_wit CA_params CA alphas o Morphism.term phi) bnf_wit_terms;
-    val bnf_rel = Morphism.term phi bnf_rel_term;
 
     (*TODO: assert Ds = (TVars of bnf_map) \ (alphas @ betas) as sets*)
     val deads = (case Ds_opt of
@@ -649,7 +642,7 @@
     (*TODO: check type of bnf_rel*)
 
     val ((((((((((As', Bs'), Cs), Ds), B1Ts), B2Ts), domTs), ranTs), ranTs'), ranTs''),
-      (Ts, T)) = lthy1
+      (Ts, T)) = lthy
       |> mk_TFrees live
       ||>> mk_TFrees live
       ||>> mk_TFrees live
@@ -669,8 +662,6 @@
     fun mk_bnf_t As' = Term.subst_atomic_types ((deads ~~ Ds) @ (alphas ~~ As'));
     fun mk_bnf_T As' = Term.typ_subst_atomic ((deads ~~ Ds) @ (alphas ~~ As'));
 
-    fun mk_bnf_rel setRTs CA' CB' = normalize_rel lthy1 setRTs CA' CB' bnf_rel;
-
     val (setRTs, RTs) = map_split (`HOLogic.mk_setT o HOLogic.mk_prodT) (As' ~~ Bs');
     val setRTsAsCs = map (HOLogic.mk_setT o HOLogic.mk_prodT) (As' ~~ Cs);
     val setRTsBsCs = map (HOLogic.mk_setT o HOLogic.mk_prodT) (Bs' ~~ Cs);
@@ -691,11 +682,10 @@
     val bnf_sets_Bs = map (mk_bnf_t Bs') bnf_sets;
     val bnf_bd_As = mk_bnf_t As' bnf_bd;
     val bnf_wit_As = map (apsnd (mk_bnf_t As')) bnf_wits;
-    val relAsBs = mk_bnf_rel setRTs CA' CB';
 
     val ((((((((((((((((((((((((fs, fs_copy), gs), hs), (x, x')), (y, y')), (z, z')), zs), As),
-      As_copy), Xs), B1s), B2s), f1s), f2s), e1s), e2s), p1s), p2s), bs), Rs), Rs_copy), Ss),
-      (Qs, Qs')), _) = lthy1
+      As_copy), Xs), B1s), B2s), f1s), f2s), e1s), e2s), p1s), p2s), bs), (Rs, Rs')), Rs_copy), Ss),
+      (Qs, Qs')), _) = lthy
       |> mk_Frees "f" (map2 (curry (op -->)) As' Bs')
       ||>> mk_Frees "f" (map2 (curry (op -->)) As' Bs')
       ||>> mk_Frees "g" (map2 (curry (op -->)) Bs' Cs)
@@ -716,29 +706,54 @@
       ||>> mk_Frees "p1" (map2 (curry (op -->)) domTs B1Ts)
       ||>> mk_Frees "p2" (map2 (curry (op -->)) domTs B2Ts)
       ||>> mk_Frees "b" As'
-      ||>> mk_Frees "R" setRTs
+      ||>> mk_Frees' "R" setRTs
       ||>> mk_Frees "R" setRTs
       ||>> mk_Frees "S" setRTsBsCs
       ||>> mk_Frees' "Q" QTs;
 
+    (*Gr (in R1 .. Rn) (map fst .. fst)^-1 O Gr (in R1 .. Rn) (map snd .. snd)*)
+    val rel_O_Gr_rhs =
+      let
+        val map1 = Term.list_comb (mk_bnf_map RTs As', map fst_const RTs);
+        val map2 = Term.list_comb (mk_bnf_map RTs Bs', map snd_const RTs);
+        val bnf_in = mk_in (map Free Rs') (map (mk_bnf_t RTs) bnf_sets) CRs';
+      in
+        mk_rel_comp (mk_converse (mk_Gr bnf_in map1), mk_Gr bnf_in map2)
+      end;
+
+    val rel_rhs = (case raw_rel_opt of
+        NONE => fold_rev Term.absfree Rs' rel_O_Gr_rhs
+      | SOME raw_rel => prep_term no_defs_lthy raw_rel);
+
+    val rel_bind_def = (fn () => Binding.suffix_name ("_" ^ relN) b, rel_rhs);
+
+    val ((bnf_rel_term, raw_rel_def), (lthy, lthy_old)) =
+      lthy
+      |> maybe_define rel_bind_def
+      ||> `(maybe_restore lthy);
+
+    val phi = Proof_Context.export_morphism lthy_old lthy;
+
+    val bnf_rel_def = Morphism.thm phi raw_rel_def;
+
+    val bnf_rel = Morphism.term phi bnf_rel_term;
+
+    fun mk_bnf_rel setRTs CA' CB' = normalize_rel lthy setRTs CA' CB' bnf_rel;
+
+    val relAsBs = mk_bnf_rel setRTs CA' CB';
+
     val pred_rhs = fold absfree (y' :: x' :: rev Qs') (HOLogic.mk_mem (HOLogic.mk_prod (x, y),
       Term.list_comb (relAsBs, map3 (fn Q => fn T => fn U =>
         HOLogic.Collect_const (HOLogic.mk_prodT (T, U)) $ HOLogic.mk_split Q)
         Qs As' Bs')));
     val pred_bind_def = (fn () => Binding.suffix_name ("_" ^ predN) b, pred_rhs);
 
-    val ((bnf_pred_term, raw_pred_def), (lthy3, lthy2)) =
-      lthy1
+    val ((bnf_pred_term, raw_pred_def), (lthy, lthy_old)) =
+      lthy
       |> maybe_define pred_bind_def
-      ||> `(maybe_restore lthy1);
+      ||> `(maybe_restore lthy);
 
-    val _ = case filter_out_refl (raw_map_def :: raw_set_defs @ [raw_bd_def] @
-        raw_wit_defs @ [raw_rel_def, raw_pred_def]) of
-        [] => ()
-      | defs => Proof_Display.print_consts true lthy2 (K false)
-          (map (dest_Free o fst o Logic.dest_equals o prop_of) defs);
-
-    val phi = Proof_Context.export_morphism lthy2 lthy3;
+    val phi = Proof_Context.export_morphism lthy_old lthy;
 
     val bnf_pred_def =
       if fact_policy <> Derive_Some_Facts then
@@ -748,10 +763,16 @@
 
     val bnf_pred = Morphism.term phi bnf_pred_term;
 
-    fun mk_bnf_pred QTs CA' CB' = normalize_pred lthy3 QTs CA' CB' bnf_pred;
+    fun mk_bnf_pred QTs CA' CB' = normalize_pred lthy QTs CA' CB' bnf_pred;
 
     val pred = mk_bnf_pred QTs CA' CB';
 
+    val _ = case filter_out_refl (raw_map_def :: raw_set_defs @ [raw_bd_def] @
+        raw_wit_defs @ [raw_rel_def, raw_pred_def]) of
+        [] => ()
+      | defs => Proof_Display.print_consts true lthy_old (K false)
+          (map (dest_Free o fst o Logic.dest_equals o prop_of) defs);
+
     val map_id_goal =
       let
         val bnf_map_app_id = Term.list_comb (bnf_map_AsAs, map HOLogic.id_const As');
@@ -845,15 +866,7 @@
       end;
 
     val rel_O_Gr_goal =
-      let
-        val map1 = Term.list_comb (mk_bnf_map RTs As', map fst_const RTs);
-        val map2 = Term.list_comb (mk_bnf_map RTs Bs', map snd_const RTs);
-        val bnf_in = mk_in Rs (map (mk_bnf_t RTs) bnf_sets) CRs';
-        (*Gr (in R1 .. Rn) (map fst .. fst)^-1 O Gr (in R1 .. Rn) (map snd .. snd)*)
-        val rhs = mk_rel_comp (mk_converse (mk_Gr bnf_in map1), mk_Gr bnf_in map2);
-      in
-        fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (relAsBs, Rs), rhs))
-      end;
+      fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (relAsBs, Rs), rel_O_Gr_rhs));
 
     val goals = zip_goals map_id_goal map_comp_goal map_cong_goal set_naturals_goal
       card_order_bd_goal cinfinite_bd_goal set_bds_goal in_bd_goal map_wpull_goal rel_O_Gr_goal;
@@ -1157,8 +1170,11 @@
               else
                 I))
       end;
+
+    val one_step_defs =
+      filter_out_refl (bnf_map_def :: bnf_bd_def :: bnf_set_defs @ bnf_wit_defs @ [bnf_rel_def]);
   in
-    (key, goals, wit_goalss, after_qed, lthy3, one_step_defs)
+    (key, goals, wit_goalss, after_qed, lthy, one_step_defs)
   end;
 
 fun register_bnf key (bnf, lthy) =
@@ -1227,6 +1243,7 @@
   Outer_Syntax.local_theory_to_proof @{command_spec "bnf_def"} "define a BNF for an existing type"
     ((parse_opt_binding_colon -- Parse.term --
        (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Parse.term --
-       (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Parse.term) >> bnf_def_cmd);
+       (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Scan.option Parse.term)
+       >> bnf_def_cmd);
 
 end;

--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Thu Sep 20 02:42:48 2012 +0200
@@ -2669,10 +2669,7 @@
           map3 (K ooo mk_wpull_tac m coalg_thePull_thm mor_thePull_fst_thm mor_thePull_snd_thm
             mor_thePull_pick_thm) unique_mor_thms (transpose pick_col_thmss) hset_defss;
 
-        (* ### *)
-        fun rel_O_Gr_tac {context = ctxt, ...} = Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt);
-
-        val rel_O_gr_tacs = replicate n rel_O_Gr_tac;
+        val rel_O_gr_tacs = replicate n (K (rtac refl 1));
 
         val tacss = map10 zip_goals map_id_tacs map_comp_tacs map_cong_tacs set_nat_tacss
           bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs rel_O_gr_tacs;
@@ -2864,7 +2861,7 @@
         val (Jbnfs, lthy) =
           fold_map6 (fn tacs => fn b => fn mapx => fn sets => fn T => fn (thms, wits) => fn lthy =>
             bnf_def Dont_Inline policy I tacs (wit_tac thms) (SOME deads)
-              (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), @{term True}(*###*)) lthy
+              (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE) lthy
             |> register_bnf (Local_Theory.full_name lthy b))
           tacss bs fs_maps setss_by_bnf Ts all_witss lthy;
 

--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Thu Sep 20 02:42:48 2012 +0200
@@ -1670,10 +1670,7 @@
           in_incl_min_alg_thms card_of_min_alg_thms;
         val map_wpull_tacs = map (K o mk_wpull_tac) map_wpull_thms;
 
-        (* ### *)
-        fun rel_O_Gr_tac {context = ctxt, ...} = Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt);
-
-        val rel_O_gr_tacs = replicate n rel_O_Gr_tac;
+        val rel_O_gr_tacs = replicate n (K (rtac refl 1));
 
         val tacss = map10 zip_goals map_id_tacs map_comp_tacs map_cong_tacs set_nat_tacss
           bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs rel_O_gr_tacs;
@@ -1710,7 +1707,7 @@
         val (Ibnfs, lthy) =
           fold_map6 (fn tacs => fn b => fn mapx => fn sets => fn T => fn wits => fn lthy =>
             bnf_def Dont_Inline policy I tacs wit_tac (SOME deads)
-              (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), @{term True}(*###*)) lthy
+              (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE) lthy
             |> register_bnf (Local_Theory.full_name lthy b))
           tacss bs fs_maps setss_by_bnf Ts fld_witss lthy;