# HG changeset patch
# User blanchet
# Date 1366822192 -7200
# Node ID bbcdd8519253b3b0fdcf5e60e5d8619207cb0bbb
# Parent  f19a4d0ab1bf261116a7bb79c4f39db283748a4d
honor user-specified name for relator + generalize syntax

diff -r f19a4d0ab1bf -r bbcdd8519253 src/HOL/BNF/Tools/bnf_comp.ML
--- a/src/HOL/BNF/Tools/bnf_comp.ML	Wed Apr 24 17:47:22 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML	Wed Apr 24 18:49:52 2013 +0200
@@ -262,7 +262,7 @@
 
     val (bnf', lthy') =
       bnf_def const_policy (K Dont_Note) qualify tacs wit_tac (SOME (oDs @ flat Dss)) Binding.empty
-        [] (((((b, mapx), sets), bd), wits), SOME rel) lthy;
+        Binding.empty [] (((((b, mapx), sets), bd), wits), SOME rel) lthy;
   in
     (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
   end;
@@ -360,7 +360,7 @@
 
     val (bnf', lthy') =
       bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME (killedAs @ Ds)) Binding.empty
-        [] (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
+        Binding.empty [] (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
   in
     (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
   end;
@@ -443,8 +443,8 @@
     fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
 
     val (bnf', lthy') =
-      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty []
-        (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
+      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty Binding.empty
+        [] (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
 
   in
     (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
@@ -520,8 +520,8 @@
     fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
 
     val (bnf', lthy') =
-      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty []
-        (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
+      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty Binding.empty
+        [] (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
   in
     (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
   end;
@@ -663,7 +663,7 @@
     fun wit_tac _ = mk_simple_wit_tac (map unfold_all (wit_thms_of_bnf bnf));
 
     val (bnf', lthy') = bnf_def Hardly_Inline (user_policy Dont_Note) I tacs wit_tac (SOME deads)
-      Binding.empty []
+      Binding.empty Binding.empty []
       (((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), SOME bnf_rel) lthy;
   in
     ((bnf', deads), lthy')
diff -r f19a4d0ab1bf -r bbcdd8519253 src/HOL/BNF/Tools/bnf_def.ML
--- a/src/HOL/BNF/Tools/bnf_def.ML	Wed Apr 24 17:47:22 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Wed Apr 24 18:49:52 2013 +0200
@@ -94,7 +94,8 @@
   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 ->
-    binding list -> ((((binding * term) * term list) * term) * term list) * term option ->
+    binding -> binding list ->
+    ((((binding * term) * term list) * term) * term list) * term option ->
     local_theory -> BNF * local_theory
 end;
 
@@ -544,7 +545,7 @@
 
 (* Define new BNFs *)
 
-fun prepare_def const_policy mk_fact_policy qualify prep_term Ds_opt map_b set_bs
+fun prepare_def const_policy mk_fact_policy qualify prep_term Ds_opt map_b rel_b set_bs
   (((((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;
@@ -766,7 +767,9 @@
           (Term.list_comb (fold_rev Term.absfree Rs' O_Gr, sQs)))
       | SOME raw_rel => prep_term no_defs_lthy raw_rel);
 
-    val rel_bind_def = (fn () => Binding.suffix_name ("_" ^ relN) b, rel_rhs);
+    val rel_bind_def =
+      (fn () => if Binding.is_empty rel_b then Binding.suffix_name ("_" ^ relN) b else rel_b,
+       rel_rhs);
 
     val ((bnf_rel_term, raw_rel_def), (lthy, lthy_old)) =
       lthy
@@ -1261,7 +1264,7 @@
 fun mk_conjunction_balanced' [] = @{prop True}
   | mk_conjunction_balanced' ts = Logic.mk_conjunction_balanced ts;
 
-fun bnf_def const_policy fact_policy qualify tacs wit_tac Ds =
+fun bnf_def const_policy fact_policy qualify tacs wit_tac Ds map_b rel_b set_bs =
   (fn (_, goals, wit_goalss, after_qed, lthy, one_step_defs) =>
   let
     val wits_tac =
@@ -1277,13 +1280,14 @@
     map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] [])
       goals (map (mk_unfold_thms_then_tac lthy one_step_defs) tacs)
     |> (fn thms => after_qed (map single thms @ wit_thms) lthy)
-  end) oooo prepare_def const_policy fact_policy qualify (K I) Ds;
+  end) oo prepare_def const_policy fact_policy qualify (K I) Ds map_b rel_b set_bs;
 
 val bnf_def_cmd = (fn (key, goals, wit_goals, after_qed, lthy, defs) =>
   Proof.unfolding ([[(defs, [])]])
     (Proof.theorem NONE (snd o register_bnf key oo after_qed)
       (map (single o rpair []) goals @ map (map (rpair [])) wit_goals) lthy)) oo
-  prepare_def Do_Inline (user_policy Note_Some) I Syntax.read_term NONE Binding.empty [];
+  prepare_def Do_Inline (user_policy Note_Some) I Syntax.read_term NONE Binding.empty Binding.empty
+    [];
 
 fun print_bnfs ctxt =
   let
diff -r f19a4d0ab1bf -r bbcdd8519253 src/HOL/BNF/Tools/bnf_fp.ML
--- a/src/HOL/BNF/Tools/bnf_fp.ML	Wed Apr 24 17:47:22 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp.ML	Wed Apr 24 18:49:52 2013 +0200
@@ -141,9 +141,10 @@
   val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
 
   val fp_bnf: (mixfix list -> (string * sort) list option -> binding list -> binding list ->
-      binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory -> 'a) ->
-    binding list -> mixfix list -> binding list -> binding list list -> (string * sort) list ->
-    ((string * sort) * typ) list -> local_theory -> BNF_Def.BNF list * 'a
+      binding list -> binding list list -> typ list * typ list list -> BNF_Def.BNF list ->
+      local_theory -> 'a) ->
+    binding list -> mixfix list -> binding list -> binding list -> binding list list ->
+    (string * sort) list -> ((string * sort) * typ) list -> local_theory -> BNF_Def.BNF list * 'a
 end;
 
 structure BNF_FP : BNF_FP =
@@ -386,8 +387,8 @@
   | fp_sort lhss (SOME resBs) Ass =
     (subtract (op =) lhss (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs)) @ lhss;
 
-fun mk_fp_bnf timer construct_fp resBs bs map_bs set_bss sort lhss bnfs deadss livess unfold_set
-    lthy =
+fun mk_fp_bnf timer construct_fp resBs bs map_bs rel_bs set_bss sort lhss bnfs deadss livess
+    unfold_set lthy =
   let
     val name = mk_common_name (map Binding.name_of bs);
     fun qualify i =
@@ -415,14 +416,14 @@
 
     val timer = time (timer "Normalization & sealing of BNFs");
 
-    val res = construct_fp resBs bs map_bs set_bss (map TFree resDs, deadss) bnfs'' lthy'';
+    val res = construct_fp resBs bs map_bs rel_bs set_bss (map TFree resDs, deadss) bnfs'' lthy'';
 
     val timer = time (timer "FP construction in total");
   in
     timer; (bnfs'', res)
   end;
 
-fun fp_bnf construct_fp bs mixfixes map_bs set_bss resBs eqs lthy =
+fun fp_bnf construct_fp bs mixfixes map_bs rel_bs set_bss resBs eqs lthy =
   let
     val timer = time (Timer.startRealTimer ());
     val (lhss, rhss) = split_list eqs;
@@ -432,8 +433,8 @@
       (fold_map2 (fn b => bnf_of_typ Smart_Inline (qualify b) sort) bs rhss
         (empty_unfolds, lthy));
   in
-    mk_fp_bnf timer (construct_fp mixfixes) (SOME resBs) bs map_bs set_bss sort lhss bnfs Dss Ass
-      unfold_set lthy'
+    mk_fp_bnf timer (construct_fp mixfixes) (SOME resBs) bs map_bs rel_bs set_bss sort lhss bnfs Dss
+      Ass unfold_set lthy'
   end;
 
 end;
diff -r f19a4d0ab1bf -r bbcdd8519253 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Apr 24 17:47:22 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Apr 24 18:49:52 2013 +0200
@@ -8,15 +8,15 @@
 signature BNF_FP_DEF_SUGAR =
 sig
   val datatypes: bool ->
-    (mixfix list -> (string * sort) list option -> binding list -> binding list ->
+    (mixfix list -> (string * sort) list option -> binding list -> binding list -> binding list ->
       binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
       BNF_FP.fp_result * local_theory) ->
-    (bool * bool) * ((((binding * (binding * (typ * sort)) list) * binding) * mixfix) *
+    (bool * bool) * (((((binding * (typ * sort)) list * binding) * (binding * binding)) * mixfix) *
       ((((binding * binding) * (binding * typ) list) * (binding * term) list) *
         mixfix) list) list ->
     local_theory -> local_theory
   val parse_datatype_cmd: bool ->
-    (mixfix list -> (string * sort) list option -> binding list -> binding list ->
+    (mixfix list -> (string * sort) list option -> binding list -> binding list -> binding list ->
       binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
       BNF_FP.fp_result * local_theory) ->
     (local_theory -> local_theory) parser
@@ -130,9 +130,10 @@
   reassoc_conjs (thm RS @{thm conj_assoc[THEN iffD1]})
   handle THM _ => thm;
 
-fun map_binding_of ((((b, _), _), _), _) = b;
-fun type_args_named_constrained_of ((((_, ncAs), _), _), _) = ncAs;
-fun type_binding_of (((_, b), _), _) = b;
+fun type_args_named_constrained_of ((((ncAs, _), _), _), _) = ncAs;
+fun type_binding_of ((((_, b), _), _), _) = b;
+fun map_binding_of (((_, (b, _)), _), _) = b;
+fun rel_binding_of (((_, (_, b)), _), _) = b;
 fun mixfix_of ((_, mx), _) = mx;
 fun ctr_specs_of (_, ctr_specs) = ctr_specs;
 
@@ -159,6 +160,7 @@
     val fp_b_names = map Binding.name_of fp_bs;
     val fp_common_name = mk_common_name fp_b_names;
     val map_bs = map map_binding_of specs;
+    val rel_bs = map rel_binding_of specs;
 
     fun prepare_type_arg (_, (ty, c)) =
       let val TFree (s, _) = prepare_typ no_defs_lthy0 ty in
@@ -244,7 +246,7 @@
     val (pre_bnfs, ((fp_bnfs as any_fp_bnf :: _, dtors0, ctors0, fp_folds0, fp_recs0, fp_induct,
            fp_strong_induct, dtor_ctors, ctor_dtors, ctor_injects, fp_map_thms, fp_set_thmss,
            fp_rel_thms, fp_fold_thms, fp_rec_thms), lthy)) =
-      fp_bnf construct_fp fp_bs mixfixes map_bs set_bss (map dest_TFree unsorted_As) fp_eqs
+      fp_bnf construct_fp fp_bs mixfixes map_bs rel_bs set_bss (map dest_TFree unsorted_As) fp_eqs
         no_defs_lthy0;
 
     val timer = time (Timer.startRealTimer ());
@@ -1196,13 +1198,31 @@
   @{keyword "("} |-- Parse.!!! (Parse.list1 parse_type_arg_named_constrained --| @{keyword ")"}) ||
   Scan.succeed [];
 
-val parse_single_spec =
-  parse_opt_binding_colon -- parse_type_args_named_constrained -- Parse.binding --
-  Parse.opt_mixfix -- (@{keyword "="} |-- Parse.enum1 "|" (parse_opt_binding_colon --
-      Parse.binding -- Scan.repeat parse_ctr_arg -- Scan.optional parse_defaults [] --
-    Parse.opt_mixfix));
+val parse_map_rel_binding = Parse.short_ident --| @{keyword ":"} -- Parse.binding;
+
+val no_map_rel = (Binding.empty, Binding.empty);
+
+(* "map" and "rel" are purposedly not registered as keywords, because they are short and nice names
+   that we don't want them to be highlighted everywhere because of some obscure feature of the BNF
+   package. *)
+fun extract_map_rel ("map", b) = apfst (K b)
+  | extract_map_rel ("rel", b) = apsnd (K b)
+  | extract_map_rel (s, _) = error ("Expected \"map\" or \"rel\" instead of " ^ quote s);
 
-val parse_datatype = parse_wrap_options -- Parse.and_list1 parse_single_spec;
+val parse_map_rel_bindings =
+  @{keyword "("} |-- Scan.repeat parse_map_rel_binding --| @{keyword ")"}
+    >> (fn ps => fold extract_map_rel ps no_map_rel) ||
+  Scan.succeed no_map_rel;
+
+val parse_ctr_spec =
+  parse_opt_binding_colon -- Parse.binding -- Scan.repeat parse_ctr_arg --
+  Scan.optional parse_defaults [] -- Parse.opt_mixfix;
+
+val parse_spec =
+  parse_type_args_named_constrained -- Parse.binding -- parse_map_rel_bindings --
+  Parse.opt_mixfix -- (@{keyword "="} |-- Parse.enum1 "|" parse_ctr_spec);
+
+val parse_datatype = parse_wrap_options -- Parse.and_list1 parse_spec;
 
 fun parse_datatype_cmd lfp construct_fp = parse_datatype >> datatype_cmd lfp construct_fp;
 
diff -r f19a4d0ab1bf -r bbcdd8519253 src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Apr 24 17:47:22 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Apr 24 18:49:52 2013 +0200
@@ -10,8 +10,8 @@
 signature BNF_GFP =
 sig
   val construct_gfp: mixfix list -> (string * sort) list option -> binding list -> binding list ->
-    binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
-    BNF_FP.fp_result * local_theory
+    binding list -> binding list list -> typ list * typ list list -> BNF_Def.BNF list ->
+    local_theory -> BNF_FP.fp_result * local_theory
 end;
 
 structure BNF_GFP : BNF_GFP =
@@ -55,7 +55,7 @@
      ((i, I), nth (nth lwitss i) nwit) :: maps (tree_to_coind_wits lwitss) subtrees;
 
 (*all BNFs have the same lives*)
-fun construct_gfp mixfixes resBs bs map_bs set_bss (resDs, Dss) bnfs lthy =
+fun construct_gfp mixfixes resBs bs map_bs rel_bs set_bss (resDs, Dss) bnfs lthy =
   let
     val timer = time (Timer.startRealTimer ());
 
@@ -2894,13 +2894,13 @@
         val wit_tac = mk_wit_tac n dtor_ctor_thms (flat dtor_set_thmss) (maps wit_thms_of_bnf bnfs);
 
         val (Jbnfs, lthy) =
-          fold_map8 (fn tacs => fn b => fn map_b => fn set_bs => fn mapx => fn sets => fn T =>
-              fn (thms, wits) => fn lthy =>
+          fold_map9 (fn tacs => fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets =>
+              fn T => fn (thms, wits) => fn lthy =>
             bnf_def Dont_Inline (user_policy Note_Some) I tacs (wit_tac thms) (SOME deads) map_b
-              set_bs (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE)
-              lthy
+              rel_b set_bs
+              (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE) lthy
             |> register_bnf (Local_Theory.full_name lthy b))
-          tacss bs map_bs set_bss fs_maps setss_by_bnf Ts all_witss lthy;
+          tacss bs map_bs rel_bs set_bss fs_maps setss_by_bnf Ts all_witss lthy;
 
         val fold_maps = fold_thms lthy (map (fn bnf =>
           mk_unabs_def m (map_def_of_bnf bnf RS meta_eq_to_obj_eq)) Jbnfs);
diff -r f19a4d0ab1bf -r bbcdd8519253 src/HOL/BNF/Tools/bnf_lfp.ML
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Wed Apr 24 17:47:22 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Wed Apr 24 18:49:52 2013 +0200
@@ -9,8 +9,8 @@
 signature BNF_LFP =
 sig
   val construct_lfp: mixfix list -> (string * sort) list option -> binding list -> binding list ->
-    binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
-    BNF_FP.fp_result * local_theory
+    binding list -> binding list list -> typ list * typ list list -> BNF_Def.BNF list ->
+    local_theory -> BNF_FP.fp_result * local_theory
 end;
 
 structure BNF_LFP : BNF_LFP =
@@ -26,7 +26,7 @@
 open BNF_LFP_Tactics
 
 (*all BNFs have the same lives*)
-fun construct_lfp mixfixes resBs bs map_bs set_bss (resDs, Dss) bnfs lthy =
+fun construct_lfp mixfixes resBs bs map_bs rel_bs set_bss (resDs, Dss) bnfs lthy =
   let
     val timer = time (Timer.startRealTimer ());
 
@@ -1734,12 +1734,13 @@
         fun wit_tac _ = mk_wit_tac n (flat ctor_set_thmss) (maps wit_thms_of_bnf bnfs);
 
         val (Ibnfs, lthy) =
-          fold_map8 (fn tacs => fn b => fn map_b => fn set_bs => fn mapx => fn sets => fn T =>
-              fn wits => fn lthy =>
-            bnf_def Dont_Inline (user_policy Note_Some) I tacs wit_tac (SOME deads) map_b set_bs
-              (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE) lthy
+          fold_map9 (fn tacs => fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets =>
+              fn T => fn wits => fn lthy =>
+            bnf_def Dont_Inline (user_policy Note_Some) I tacs wit_tac (SOME deads) map_b rel_b
+              set_bs (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE)
+              lthy
             |> register_bnf (Local_Theory.full_name lthy b))
-          tacss bs map_bs set_bss fs_maps setss_by_bnf Ts ctor_witss lthy;
+          tacss bs map_bs rel_bs set_bss fs_maps setss_by_bnf Ts ctor_witss lthy;
 
         val fold_maps = fold_thms lthy (map (fn bnf =>
           mk_unabs_def m (map_def_of_bnf bnf RS meta_eq_to_obj_eq)) Ibnfs);
diff -r f19a4d0ab1bf -r bbcdd8519253 src/HOL/BNF/Tools/bnf_util.ML
--- a/src/HOL/BNF/Tools/bnf_util.ML	Wed Apr 24 17:47:22 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML	Wed Apr 24 18:49:52 2013 +0200
@@ -43,6 +43,9 @@
   val fold_map8: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j * 'i) ->
     'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> 'i ->
     'j list * 'i
+  val fold_map9: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k * 'j) ->
+    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
+    'i list -> 'j -> 'k list * 'j
   val splice: 'a list -> 'a list -> 'a list
   val transpose: 'a list list -> 'a list list
   val seq_conds: (bool -> 'a -> 'b) -> int -> int -> 'a list -> 'b list
@@ -286,6 +289,15 @@
     in (x :: xs, acc'') end
   | fold_map8 _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
 
+fun fold_map9 _ [] [] [] [] [] [] [] [] [] acc = ([], acc)
+  | fold_map9 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
+      (x9::x9s) acc =
+    let
+      val (x, acc') = f x1 x2 x3 x4 x5 x6 x7 x8 x9 acc;
+      val (xs, acc'') = fold_map9 f x1s x2s x3s x4s x5s x6s x7s x8s x9s acc';
+    in (x :: xs, acc'') end
+  | fold_map9 _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
+
 (*stolen from ~~/src/HOL/Tools/SMT/smt_utils.ML*)
 fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt);
 fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt);