# HG changeset patch
# User blanchet
# Date 1346312866 -7200
# Node ID f379cf5d71bdcbc002890e48a7b584f8037cbdff
# Parent  fc4decdba5ceb9aa0306b34c4a98b2b71a700c16
more work on BNF sugar -- up to derivation of nchotomy

diff -r fc4decdba5ce -r f379cf5d71bd etc/isar-keywords.el
--- a/etc/isar-keywords.el	Thu Aug 30 09:47:46 2012 +0200
+++ b/etc/isar-keywords.el	Thu Aug 30 09:47:46 2012 +0200
@@ -35,6 +35,7 @@
     "bnf_codata"
     "bnf_data"
     "bnf_def"
+    "bnf_sugar"
     "boogie_end"
     "boogie_open"
     "boogie_status"
@@ -576,6 +577,7 @@
 (defconst isar-keywords-theory-goal
   '("ax_specification"
     "bnf_def"
+    "bnf_sugar"
     "boogie_vc"
     "code_pred"
     "corollary"
diff -r fc4decdba5ce -r f379cf5d71bd src/HOL/Codatatype/Codatatype.thy
--- a/src/HOL/Codatatype/Codatatype.thy	Thu Aug 30 09:47:46 2012 +0200
+++ b/src/HOL/Codatatype/Codatatype.thy	Thu Aug 30 09:47:46 2012 +0200
@@ -14,6 +14,7 @@
 keywords
   "bnf_sugar" :: thy_goal
 uses
+  "Tools/bnf_sugar_tactics.ML"
   "Tools/bnf_sugar.ML"
 begin
 
diff -r fc4decdba5ce -r f379cf5d71bd src/HOL/Codatatype/Tools/bnf_fp_util.ML
--- 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
@@ -20,6 +20,7 @@
   val coiterN: string
   val coiter_uniqueN: string
   val corecN: string
+  val exhaustN: string
   val fldN: string
   val fld_coiterN: string
   val fld_exhaustN: string
@@ -39,6 +40,7 @@
   val map_uniqueN: string
   val min_algN: string
   val morN: string
+  val nchotomyN: string
   val pred_coinductN: string
   val pred_coinduct_uptoN: string
   val recN: string
@@ -79,6 +81,8 @@
   val mk_Field: term -> term
   val mk_union: term * term -> term
 
+  val mk_disjIN: int -> int -> thm
+
   val mk_tactics: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list
 
   val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
@@ -154,10 +158,12 @@
 
 val fld_unfN = fldN ^ "_" ^ unfN
 val unf_fldN = unfN ^ "_" ^ fldN
-fun mk_nchotomyN s = s ^ "_nchotomy"
+val nchotomyN = "nchotomy"
+fun mk_nchotomyN s = s ^ "_" ^ nchotomyN
 val injectN = "inject"
 fun mk_injectN s = s ^ "_" ^ injectN
-fun mk_exhaustN s = s ^ "_exhaust"
+val exhaustN = "exhaust"
+fun mk_exhaustN s = s ^ "_" ^ exhaustN
 val fld_injectN = mk_injectN fldN
 val fld_exhaustN = mk_exhaustN fldN
 val unf_injectN = mk_injectN unfN
@@ -184,6 +190,11 @@
 
 val mk_union = HOLogic.mk_binop @{const_name sup};
 
+fun mk_disjIN 1 1 = @{thm TrueE[OF TrueI]}
+  | mk_disjIN _ 1 = disjI1
+  | mk_disjIN 2 2 = disjI2
+  | mk_disjIN n m = (mk_disjIN (n - 1) (m - 1)) RS disjI2;
+
 (*dangerous; use with monotonic, converging functions only!*)
 fun fixpoint eq f X = if subset eq (f X, X) then X else fixpoint eq f (f X);
 
diff -r fc4decdba5ce -r f379cf5d71bd src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML	Thu Aug 30 09:47:46 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML	Thu Aug 30 09:47:46 2012 +0200
@@ -124,6 +124,7 @@
 
 open BNF_Tactics
 open BNF_Util
+open BNF_FP_Util
 open BNF_GFP_Util
 
 fun mk_coalg_set_tac coalg_def =
diff -r fc4decdba5ce -r f379cf5d71bd src/HOL/Codatatype/Tools/bnf_gfp_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_gfp_util.ML	Thu Aug 30 09:47:46 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp_util.ML	Thu Aug 30 09:47:46 2012 +0200
@@ -47,7 +47,6 @@
   val mk_sum_case: term -> term -> term
   val mk_sum_caseN: term list -> term
 
-  val mk_disjIN: int -> int -> thm
   val mk_specN: int -> thm -> thm
   val mk_sum_casesN: int -> int -> thm
   val mk_sumEN: int -> thm
@@ -193,11 +192,6 @@
       A $ f1 $ f2 $ b1 $ b2
   end;
 
-fun mk_disjIN 1 1 = @{thm TrueE[OF TrueI]}
-  | mk_disjIN _ 1 = disjI1
-  | mk_disjIN 2 2 = disjI2
-  | mk_disjIN n m = (mk_disjIN (n - 1) (m - 1)) RS disjI2;
-
 fun mk_sumTN Ts = Library.foldr1 (mk_sumT) Ts;
 
 fun Inl_const LT RT = Const (@{const_name Inl}, LT --> mk_sumT (LT, RT));
diff -r fc4decdba5ce -r f379cf5d71bd 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
@@ -14,33 +14,51 @@
 
 open BNF_Util
 open BNF_FP_Util
+open BNF_Sugar_Tactics
 
 val distinctN = "distinct";
 
-fun prepare_sugar prep_typ prep_term ((((raw_T, raw_ctors), raw_dtors), raw_storss), raw_recur)
+fun prepare_sugar prep_term (((raw_ctors, raw_dtors), raw_storss), raw_recur)
   lthy =
   let
     (* 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 ((xss, yss), _) = lthy |>
+    val T as Type (T_name, _) = body_type (fastype_of (hd ctors));
+    val b = Binding.qualified_name T_name;
+
+    val n = length ctors;
+
+    val ((((xss, yss), (v, v')), p), _) = lthy |>
       mk_Freess "x" ctor_Tss
-      ||>> mk_Freess "y" ctor_Tss;
+      ||>> mk_Freess "y" ctor_Tss
+      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "v") T
+      ||>> yield_singleton (mk_Frees "P") HOLogic.boolT;
+
+    val xs_ctors = map2 (curry Term.list_comb) ctors xss;
+    val ys_ctors = map2 (curry Term.list_comb) ctors yss;
+
+    val goal_exhaust =
+      let
+        fun mk_imp_p Q = Logic.list_implies (Q, HOLogic.mk_Trueprop p);
+        fun mk_prem xs_ctor xs =
+          fold_rev Logic.all xs
+            (mk_imp_p [HOLogic.mk_Trueprop (HOLogic.mk_eq (v, xs_ctor))]);
+      in
+        mk_imp_p (map2 mk_prem xs_ctors xss)
+      end;
 
     val goal_injects =
       let
-        fun mk_goal _ [] [] = NONE
-          | mk_goal ctor xs ys =
+        fun mk_goal _ _ [] [] = NONE
+          | mk_goal xs_ctor ys_ctor xs ys =
             SOME (HOLogic.mk_Trueprop (HOLogic.mk_eq
-              (HOLogic.mk_eq (Term.list_comb (ctor, xs), Term.list_comb (ctor, ys)),
+              (HOLogic.mk_eq (xs_ctor, ys_ctor),
                Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) xs ys))));
       in
-        map_filter I (map3 mk_goal ctors xss yss)
+        map_filter I (map4 mk_goal xs_ctors ys_ctors xss yss)
       end;
 
     val goal_half_distincts =
@@ -49,24 +67,37 @@
         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)
+        mk_goals xs_ctors
       end;
 
-    val goals = [goal_injects, goal_half_distincts];
+    val goals = [[goal_exhaust], goal_injects, goal_half_distincts];
 
     fun after_qed thmss lthy =
       let
-        val [inject_thms, half_distinct_thms] = thmss;
+        val [[exhaust_thm], inject_thms, half_distinct_thms] = thmss;
 
         val other_half_distinct_thms = map (fn thm => thm RS not_sym) half_distinct_thms;
 
+        val nchotomy_thm =
+          let
+            fun mk_disjunct xs_ctor xs = list_exists_free xs (HOLogic.mk_eq (v, xs_ctor))
+            val goal =
+              HOLogic.mk_Trueprop
+                (HOLogic.mk_all (fst v', snd v',
+                   Library.foldr1 HOLogic.mk_disj (map2 mk_disjunct xs_ctors xss)));
+          in
+            Skip_Proof.prove lthy [] [] goal (fn _ => mk_nchotomy_tac n exhaust_thm)
+          end;
+
         fun note thmN thms =
           snd o Local_Theory.note
             ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), thms);
       in
         lthy
+        |> note distinctN (half_distinct_thms @ other_half_distinct_thms)
+        |> note exhaustN [exhaust_thm]
         |> note injectN inject_thms
-        |> note distinctN (half_distinct_thms @ other_half_distinct_thms)
+        |> note nchotomyN [nchotomy_thm]
       end;
   in
     (goals, after_qed, lthy)
@@ -76,11 +107,11 @@
 
 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;
+  prepare_sugar Syntax.read_term;
 
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_spec "bnf_sugar"} "adds sugar on top of a BNF"
-    ((Parse.typ -- (Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]") --
+    (((Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]") --
       parse_binding_list -- (Parse.$$$ "[" |-- Parse.list parse_binding_list --| Parse.$$$ "]") --
       Parse.term) >> bnf_sugar_cmd);
 
diff -r fc4decdba5ce -r f379cf5d71bd src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML	Thu Aug 30 09:47:46 2012 +0200
@@ -0,0 +1,22 @@
+(*  Title:      HOL/Codatatype/Tools/bnf_sugar_tactics.ML
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2012
+
+Tactics for sugar on top of a BNF.
+*)
+
+signature BNF_SUGAR_TACTICS =
+sig
+  val mk_nchotomy_tac: int -> thm -> tactic
+end;
+
+structure BNF_Sugar_Tactics : BNF_SUGAR_TACTICS =
+struct
+
+open BNF_FP_Util
+
+fun mk_nchotomy_tac n exhaust =
+  (rtac allI THEN' rtac exhaust THEN'
+   EVERY' (maps (fn i => [rtac (mk_disjIN n i), REPEAT_DETERM o rtac exI, atac]) (1 upto n))) 1;
+
+end;
diff -r fc4decdba5ce -r f379cf5d71bd src/HOL/Tools/Datatype/rep_datatype.ML
--- a/src/HOL/Tools/Datatype/rep_datatype.ML	Thu Aug 30 09:47:46 2012 +0200
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Thu Aug 30 09:47:46 2012 +0200
@@ -589,7 +589,7 @@
       (case map_filter (fn (tyco, _) =>
           if Symtab.defined (Datatype_Data.get_all thy) tyco then SOME tyco else NONE) raw_cs of
         [] => ()
-      | tycos => error ("Type(s) " ^ commas_quote tycos ^ " already represented inductivly"));
+      | tycos => error ("Type(s) " ^ commas_quote tycos ^ " already represented inductively"));
     val raw_vss = maps (map (map snd o fst) o snd) raw_cs;
     val ms =
       (case distinct (op =) (map length raw_vss) of