# HG changeset patch
# User blanchet
# Date 1384260444 -3600
# Node ID 100c0eaf63d5c9bb0b80ff8962cd652cc0e2ca8c
# Parent  f4b4fa25ce567bd2ba626e75cf3cf6ac858067ee
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it

diff -r f4b4fa25ce56 -r 100c0eaf63d5 src/HOL/Ctr_Sugar.thy
--- a/src/HOL/Ctr_Sugar.thy	Tue Nov 12 13:47:24 2013 +0100
+++ b/src/HOL/Ctr_Sugar.thy	Tue Nov 12 13:47:24 2013 +0100
@@ -8,13 +8,28 @@
 header {* Wrapping Existing Freely Generated Type's Constructors *}
 
 theory Ctr_Sugar
-imports Main
+imports HOL
 keywords
+  "print_case_translations" :: diag and
   "wrap_free_constructors" :: thy_goal and
   "no_discs_sels" and
   "rep_compat"
 begin
 
+consts
+  case_guard :: "bool \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b"
+  case_nil :: "'a \<Rightarrow> 'b"
+  case_cons :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+  case_elem :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b"
+  case_abs :: "('c \<Rightarrow> 'b) \<Rightarrow> 'b"
+declare [[coercion_args case_guard - + -]]
+declare [[coercion_args case_cons - -]]
+declare [[coercion_args case_abs -]]
+declare [[coercion_args case_elem - +]]
+
+ML_file "Tools/case_translation.ML"
+setup Case_Translation.setup
+
 lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
 by (erule iffI) (erule contrapos_pn)
 
diff -r f4b4fa25ce56 -r 100c0eaf63d5 src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Tue Nov 12 13:47:24 2013 +0100
+++ b/src/HOL/Datatype.thy	Tue Nov 12 13:47:24 2013 +0100
@@ -499,7 +499,7 @@
 
 (*Dependent version*)
 lemma dprod_subset_Sigma2:
-     "(dprod (Sigma A B) (Sigma C D)) <= 
+     "(dprod (Sigma A B) (Sigma C D)) <=
       Sigma (uprod A C) (Split (%x y. uprod (B x) (D y)))"
 by auto
 
@@ -522,4 +522,3 @@
 setup Datatype_Realizer.setup
 
 end
-
diff -r f4b4fa25ce56 -r 100c0eaf63d5 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Tue Nov 12 13:47:24 2013 +0100
+++ b/src/HOL/Inductive.thy	Tue Nov 12 13:47:24 2013 +0100
@@ -4,12 +4,12 @@
 
 header {* Knaster-Tarski Fixpoint Theorem and inductive definitions *}
 
-theory Inductive 
-imports Complete_Lattices
+theory Inductive
+imports Complete_Lattices Ctr_Sugar
 keywords
   "inductive" "coinductive" :: thy_decl and
   "inductive_cases" "inductive_simps" :: thy_script and "monos" and
-  "print_inductives" "print_case_translations" :: diag and
+  "print_inductives" :: diag and
   "rep_datatype" :: thy_goal and
   "primrec" :: thy_decl
 begin
@@ -30,7 +30,7 @@
 
 subsection{* Proof of Knaster-Tarski Theorem using @{term lfp} *}
 
-text{*@{term "lfp f"} is the least upper bound of 
+text{*@{term "lfp f"} is the least upper bound of
       the set @{term "{u. f(u) \<le> u}"} *}
 
 lemma lfp_lowerbound: "f A \<le> A ==> lfp f \<le> A"
@@ -273,21 +273,6 @@
 ML_file "Tools/Datatype/datatype_aux.ML"
 ML_file "Tools/Datatype/datatype_prop.ML"
 ML_file "Tools/Datatype/datatype_data.ML" setup Datatype_Data.setup
-
-consts
-  case_guard :: "bool \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b"
-  case_nil :: "'a \<Rightarrow> 'b"
-  case_cons :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
-  case_elem :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b"
-  case_abs :: "('c \<Rightarrow> 'b) \<Rightarrow> 'b"
-declare [[coercion_args case_guard - + -]]
-declare [[coercion_args case_cons - -]]
-declare [[coercion_args case_abs -]]
-declare [[coercion_args case_elem - +]]
-
-ML_file "Tools/case_translation.ML"
-setup Case_Translation.setup
-
 ML_file "Tools/Datatype/rep_datatype.ML"
 ML_file "Tools/Datatype/datatype_codegen.ML" setup Datatype_Codegen.setup
 ML_file "Tools/Datatype/primrec.ML"
diff -r f4b4fa25ce56 -r 100c0eaf63d5 src/HOL/Tools/Datatype/datatype_prop.ML
--- a/src/HOL/Tools/Datatype/datatype_prop.ML	Tue Nov 12 13:47:24 2013 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Tue Nov 12 13:47:24 2013 +0100
@@ -29,17 +29,8 @@
 type descr = Datatype_Aux.descr;
 
 
-fun indexify_names names =
-  let
-    fun index (x :: xs) tab =
-        (case AList.lookup (op =) tab x of
-          NONE =>
-            if member (op =) xs x
-            then (x ^ "1") :: index xs ((x, 2) :: tab)
-            else x :: index xs tab
-        | SOME i => (x ^ string_of_int i) :: index xs ((x, i + 1) :: tab))
-      | index [] _ = [];
-  in index names [] end;
+val indexify_names = Case_Translation.indexify_names;
+val make_tnames = Case_Translation.make_tnames;
 
 fun make_tnames Ts =
   let
diff -r f4b4fa25ce56 -r 100c0eaf63d5 src/HOL/Tools/case_translation.ML
--- a/src/HOL/Tools/case_translation.ML	Tue Nov 12 13:47:24 2013 +0100
+++ b/src/HOL/Tools/case_translation.ML	Tue Nov 12 13:47:24 2013 +0100
@@ -8,6 +8,9 @@
 
 signature CASE_TRANSLATION =
 sig
+  val indexify_names: string list -> string list
+  val make_tnames: typ list -> string list
+
   datatype config = Error | Warning | Quiet
   val case_tr: bool -> Proof.context -> term list -> term
   val lookup_by_constr: Proof.context -> string * typ -> (term * term list) option
@@ -25,6 +28,30 @@
 structure Case_Translation: CASE_TRANSLATION =
 struct
 
+(** general utilities **)
+
+fun indexify_names names =
+  let
+    fun index (x :: xs) tab =
+        (case AList.lookup (op =) tab x of
+          NONE =>
+            if member (op =) xs x
+            then (x ^ "1") :: index xs ((x, 2) :: tab)
+            else x :: index xs tab
+        | SOME i => (x ^ string_of_int i) :: index xs ((x, i + 1) :: tab))
+      | index [] _ = [];
+  in index names [] end;
+
+fun make_tnames Ts =
+  let
+    fun type_name (TFree (name, _)) = unprefix "'" name
+      | type_name (Type (name, _)) =
+          let val name' = Long_Name.base_name name
+          in if Symbol_Pos.is_identifier name' then name' else "x" end;
+  in indexify_names (map type_name Ts) end;
+
+
+
 (** data management **)
 
 datatype data = Data of
@@ -228,8 +255,7 @@
     val (_, T) = dest_Const c;
     val Ts = binder_types T;
     val (names, _) =
-      fold_map Name.variant
-        (Datatype_Prop.make_tnames (map Logic.unvarifyT_global Ts)) used;
+      fold_map Name.variant (make_tnames (map Logic.unvarifyT_global Ts)) used;
     val ty = body_type T;
     val ty_theta = Type.raw_match (ty, colty) Vartab.empty
       handle Type.TYPE_MATCH => raise CASE_ERROR ("type mismatch", ~1);