src/HOL/Codatatype/Tools/bnf_sugar.ML

--- 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"