more work on BNF sugar

--- a/src/HOL/Codatatype/Tools/bnf_comp.ML	Thu Aug 30 09:47:46 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp.ML	Thu Aug 30 09:47:46 2012 +0200
@@ -68,7 +68,6 @@
 
 val bdTN = "bdT";
 
-val compN = "comp_"
 fun mk_killN n = "kill" ^ string_of_int n ^ "_";
 fun mk_liftN n = "lift" ^ string_of_int n ^ "_";
 fun mk_permuteN src dest =

--- a/src/HOL/Codatatype/Tools/bnf_def.ML	Thu Aug 30 09:47:46 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML	Thu Aug 30 09:47:46 2012 +0200
@@ -528,7 +528,7 @@
 
 (* Define new BNFs *)
 
-fun prepare_bnf const_policy mk_fact_policy qualify prep_term Ds_opt
+fun prepare_def const_policy mk_fact_policy qualify prep_term Ds_opt
   ((((raw_b, raw_map), raw_sets), raw_bd_Abs), raw_wits) no_defs_lthy =
   let
     val fact_policy = mk_fact_policy no_defs_lthy;
@@ -1167,14 +1167,14 @@
   in
     (map2 (Skip_Proof.prove lthy [] []) goals (map (unfold_defs_tac lthy defs) tacs))
     |> (fn thms => after_qed (map single thms @ wit_thms) lthy)
-  end) oo prepare_bnf const_policy fact_policy qualify
+  end) oo prepare_def const_policy fact_policy qualify
   (fn ctxt => singleton (Type_Infer_Context.infer_types ctxt)) Ds;
 
 val bnf_def_cmd = (fn (goals, wit_goals, after_qed, lthy, defs) =>
   Proof.unfolding ([[(defs, [])]])
     (Proof.theorem NONE (snd oo after_qed)
       (map (single o rpair []) goals @ map (map (rpair [])) wit_goals) lthy)) oo
-  prepare_bnf Do_Inline user_policy I Syntax.read_term NONE;
+  prepare_def Do_Inline user_policy I Syntax.read_term NONE;
 
 fun print_bnfs ctxt =
   let

--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Thu Aug 30 09:47:46 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Thu Aug 30 09:47:46 2012 +0200
@@ -30,6 +30,7 @@
   val hsetN: string
   val hset_recN: string
   val inductN: string
+  val injectN: string
   val isNodeN: string
   val iterN: string
   val iter_uniqueN: string
@@ -154,7 +155,8 @@
 val fld_unfN = fldN ^ "_" ^ unfN
 val unf_fldN = unfN ^ "_" ^ fldN
 fun mk_nchotomyN s = s ^ "_nchotomy"
-fun mk_injectN s = s ^ "_inject"
+val injectN = "inject"
+fun mk_injectN s = s ^ "_" ^ injectN
 fun mk_exhaustN s = s ^ "_exhaust"
 val fld_injectN = mk_injectN fldN
 val fld_exhaustN = mk_exhaustN fldN

--- a/src/HOL/Codatatype/Tools/bnf_sugar.ML	Thu Aug 30 09:47:46 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_sugar.ML	Thu Aug 30 09:47:46 2012 +0200
@@ -7,43 +7,76 @@
 
 signature BNF_SUGAR =
 sig
-  val prepare_sugar : (Proof.context -> 'b -> term) ->
-    (((typ * 'b list) * binding list) * binding list list) * 'b -> local_theory ->
-    term list * local_theory
 end;
 
 structure BNF_Sugar : BNF_SUGAR =
 struct
 
 open BNF_Util
+open BNF_FP_Util
 
-fun prepare_sugar prep_term ((((raw_T, raw_ctors), raw_dtors), raw_storss), raw_recur) lthy =
+val distinctN = "distinct";
+
+fun prepare_sugar prep_typ prep_term ((((raw_T, raw_ctors), raw_dtors), raw_storss), raw_recur)
+  lthy =
   let
-    val ctors = map (prep_term lthy) raw_ctors;
+    (* TODO: sanity checks on arguments *)
 
-    (* TODO: sanity checks on arguments *)
+    val T as Type (T_name, _) = prep_typ lthy raw_T;
+    val b = Binding.qualified_name T_name;
+
+    val ctors = map (prep_term lthy) raw_ctors;
     val ctor_Tss = map (binder_types o fastype_of) ctors;
-    val (ctor_argss, _) = lthy |>
-      mk_Freess "x" ctor_Tss;
 
-    val goal_distincts =
+    val ((xss, yss), _) = lthy |>
+      mk_Freess "x" ctor_Tss
+      ||>> mk_Freess "y" ctor_Tss;
+
+    val goal_injects =
       let
-        fun mk_goal t u = HOLogic.mk_Trueprop (HOLogic.mk_not (HOLogic.mk_eq (t, u)))
-        fun mk_goals [] = []
-          | mk_goals (t :: ts) = fold_rev (cons o mk_goal t) ts (mk_goals ts)
+        fun mk_goal _ [] [] = NONE
+          | mk_goal ctor xs ys =
+            SOME (HOLogic.mk_Trueprop (HOLogic.mk_eq
+              (HOLogic.mk_eq (Term.list_comb (ctor, xs), Term.list_comb (ctor, ys)),
+               Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) xs ys))));
       in
-        mk_goals (map2 (curry Term.list_comb) ctors ctor_argss)
+        map_filter I (map3 mk_goal ctors xss yss)
       end;
 
-    val goals = goal_distincts;
+    val goal_half_distincts =
+      let
+        fun mk_goal t u = HOLogic.mk_Trueprop (HOLogic.mk_not (HOLogic.mk_eq (t, u)));
+        fun mk_goals [] = []
+          | mk_goals (t :: ts) = fold_rev (cons o mk_goal t) ts (mk_goals ts);
+      in
+        mk_goals (map2 (curry Term.list_comb) ctors xss)
+      end;
+
+    val goals = [goal_injects, goal_half_distincts];
+
+    fun after_qed thmss lthy =
+      let
+        val [inject_thms, half_distinct_thms] = thmss;
+
+        val other_half_distinct_thms = map (fn thm => thm RS not_sym) half_distinct_thms;
+
+        fun note thmN thms =
+          snd o Local_Theory.note
+            ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), thms);
+      in
+        lthy
+        |> note injectN inject_thms
+        |> note distinctN (half_distinct_thms @ other_half_distinct_thms)
+      end;
   in
-    (goals, lthy)
+    (goals, after_qed, lthy)
   end;
 
 val parse_binding_list = Parse.$$$ "[" |--  Parse.list Parse.binding --| Parse.$$$ "]";
 
-val bnf_sugar_cmd = (fn (goals, lthy) =>
-  Proof.theorem NONE (K I) (map (single o rpair []) goals) lthy) oo prepare_sugar Syntax.read_term;
+val bnf_sugar_cmd = (fn (goalss, after_qed, lthy) =>
+  Proof.theorem NONE after_qed (map (map (rpair [])) goalss) lthy) oo
+  prepare_sugar Syntax.read_typ Syntax.read_term;
 
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_spec "bnf_sugar"} "adds sugar on top of a BNF"