moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
authorblanchet
Tue Nov 12 13:47:24 2013 +0100 (2013-11-12)
changeset 54398100c0eaf63d5
parent 54397 f4b4fa25ce56
child 54399 60cd3ebf2d94
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
src/HOL/Ctr_Sugar.thy
src/HOL/Datatype.thy
src/HOL/Inductive.thy
src/HOL/Tools/Datatype/datatype_prop.ML
src/HOL/Tools/case_translation.ML
     1.1 --- a/src/HOL/Ctr_Sugar.thy	Tue Nov 12 13:47:24 2013 +0100
     1.2 +++ b/src/HOL/Ctr_Sugar.thy	Tue Nov 12 13:47:24 2013 +0100
     1.3 @@ -8,13 +8,28 @@
     1.4  header {* Wrapping Existing Freely Generated Type's Constructors *}
     1.5  
     1.6  theory Ctr_Sugar
     1.7 -imports Main
     1.8 +imports HOL
     1.9  keywords
    1.10 +  "print_case_translations" :: diag and
    1.11    "wrap_free_constructors" :: thy_goal and
    1.12    "no_discs_sels" and
    1.13    "rep_compat"
    1.14  begin
    1.15  
    1.16 +consts
    1.17 +  case_guard :: "bool \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b"
    1.18 +  case_nil :: "'a \<Rightarrow> 'b"
    1.19 +  case_cons :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    1.20 +  case_elem :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b"
    1.21 +  case_abs :: "('c \<Rightarrow> 'b) \<Rightarrow> 'b"
    1.22 +declare [[coercion_args case_guard - + -]]
    1.23 +declare [[coercion_args case_cons - -]]
    1.24 +declare [[coercion_args case_abs -]]
    1.25 +declare [[coercion_args case_elem - +]]
    1.26 +
    1.27 +ML_file "Tools/case_translation.ML"
    1.28 +setup Case_Translation.setup
    1.29 +
    1.30  lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
    1.31  by (erule iffI) (erule contrapos_pn)
    1.32  
     2.1 --- a/src/HOL/Datatype.thy	Tue Nov 12 13:47:24 2013 +0100
     2.2 +++ b/src/HOL/Datatype.thy	Tue Nov 12 13:47:24 2013 +0100
     2.3 @@ -499,7 +499,7 @@
     2.4  
     2.5  (*Dependent version*)
     2.6  lemma dprod_subset_Sigma2:
     2.7 -     "(dprod (Sigma A B) (Sigma C D)) <= 
     2.8 +     "(dprod (Sigma A B) (Sigma C D)) <=
     2.9        Sigma (uprod A C) (Split (%x y. uprod (B x) (D y)))"
    2.10  by auto
    2.11  
    2.12 @@ -522,4 +522,3 @@
    2.13  setup Datatype_Realizer.setup
    2.14  
    2.15  end
    2.16 -
     3.1 --- a/src/HOL/Inductive.thy	Tue Nov 12 13:47:24 2013 +0100
     3.2 +++ b/src/HOL/Inductive.thy	Tue Nov 12 13:47:24 2013 +0100
     3.3 @@ -4,12 +4,12 @@
     3.4  
     3.5  header {* Knaster-Tarski Fixpoint Theorem and inductive definitions *}
     3.6  
     3.7 -theory Inductive 
     3.8 -imports Complete_Lattices
     3.9 +theory Inductive
    3.10 +imports Complete_Lattices Ctr_Sugar
    3.11  keywords
    3.12    "inductive" "coinductive" :: thy_decl and
    3.13    "inductive_cases" "inductive_simps" :: thy_script and "monos" and
    3.14 -  "print_inductives" "print_case_translations" :: diag and
    3.15 +  "print_inductives" :: diag and
    3.16    "rep_datatype" :: thy_goal and
    3.17    "primrec" :: thy_decl
    3.18  begin
    3.19 @@ -30,7 +30,7 @@
    3.20  
    3.21  subsection{* Proof of Knaster-Tarski Theorem using @{term lfp} *}
    3.22  
    3.23 -text{*@{term "lfp f"} is the least upper bound of 
    3.24 +text{*@{term "lfp f"} is the least upper bound of
    3.25        the set @{term "{u. f(u) \<le> u}"} *}
    3.26  
    3.27  lemma lfp_lowerbound: "f A \<le> A ==> lfp f \<le> A"
    3.28 @@ -273,21 +273,6 @@
    3.29  ML_file "Tools/Datatype/datatype_aux.ML"
    3.30  ML_file "Tools/Datatype/datatype_prop.ML"
    3.31  ML_file "Tools/Datatype/datatype_data.ML" setup Datatype_Data.setup
    3.32 -
    3.33 -consts
    3.34 -  case_guard :: "bool \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b"
    3.35 -  case_nil :: "'a \<Rightarrow> 'b"
    3.36 -  case_cons :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    3.37 -  case_elem :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b"
    3.38 -  case_abs :: "('c \<Rightarrow> 'b) \<Rightarrow> 'b"
    3.39 -declare [[coercion_args case_guard - + -]]
    3.40 -declare [[coercion_args case_cons - -]]
    3.41 -declare [[coercion_args case_abs -]]
    3.42 -declare [[coercion_args case_elem - +]]
    3.43 -
    3.44 -ML_file "Tools/case_translation.ML"
    3.45 -setup Case_Translation.setup
    3.46 -
    3.47  ML_file "Tools/Datatype/rep_datatype.ML"
    3.48  ML_file "Tools/Datatype/datatype_codegen.ML" setup Datatype_Codegen.setup
    3.49  ML_file "Tools/Datatype/primrec.ML"
     4.1 --- a/src/HOL/Tools/Datatype/datatype_prop.ML	Tue Nov 12 13:47:24 2013 +0100
     4.2 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Tue Nov 12 13:47:24 2013 +0100
     4.3 @@ -29,17 +29,8 @@
     4.4  type descr = Datatype_Aux.descr;
     4.5  
     4.6  
     4.7 -fun indexify_names names =
     4.8 -  let
     4.9 -    fun index (x :: xs) tab =
    4.10 -        (case AList.lookup (op =) tab x of
    4.11 -          NONE =>
    4.12 -            if member (op =) xs x
    4.13 -            then (x ^ "1") :: index xs ((x, 2) :: tab)
    4.14 -            else x :: index xs tab
    4.15 -        | SOME i => (x ^ string_of_int i) :: index xs ((x, i + 1) :: tab))
    4.16 -      | index [] _ = [];
    4.17 -  in index names [] end;
    4.18 +val indexify_names = Case_Translation.indexify_names;
    4.19 +val make_tnames = Case_Translation.make_tnames;
    4.20  
    4.21  fun make_tnames Ts =
    4.22    let
     5.1 --- a/src/HOL/Tools/case_translation.ML	Tue Nov 12 13:47:24 2013 +0100
     5.2 +++ b/src/HOL/Tools/case_translation.ML	Tue Nov 12 13:47:24 2013 +0100
     5.3 @@ -8,6 +8,9 @@
     5.4  
     5.5  signature CASE_TRANSLATION =
     5.6  sig
     5.7 +  val indexify_names: string list -> string list
     5.8 +  val make_tnames: typ list -> string list
     5.9 +
    5.10    datatype config = Error | Warning | Quiet
    5.11    val case_tr: bool -> Proof.context -> term list -> term
    5.12    val lookup_by_constr: Proof.context -> string * typ -> (term * term list) option
    5.13 @@ -25,6 +28,30 @@
    5.14  structure Case_Translation: CASE_TRANSLATION =
    5.15  struct
    5.16  
    5.17 +(** general utilities **)
    5.18 +
    5.19 +fun indexify_names names =
    5.20 +  let
    5.21 +    fun index (x :: xs) tab =
    5.22 +        (case AList.lookup (op =) tab x of
    5.23 +          NONE =>
    5.24 +            if member (op =) xs x
    5.25 +            then (x ^ "1") :: index xs ((x, 2) :: tab)
    5.26 +            else x :: index xs tab
    5.27 +        | SOME i => (x ^ string_of_int i) :: index xs ((x, i + 1) :: tab))
    5.28 +      | index [] _ = [];
    5.29 +  in index names [] end;
    5.30 +
    5.31 +fun make_tnames Ts =
    5.32 +  let
    5.33 +    fun type_name (TFree (name, _)) = unprefix "'" name
    5.34 +      | type_name (Type (name, _)) =
    5.35 +          let val name' = Long_Name.base_name name
    5.36 +          in if Symbol_Pos.is_identifier name' then name' else "x" end;
    5.37 +  in indexify_names (map type_name Ts) end;
    5.38 +
    5.39 +
    5.40 +
    5.41  (** data management **)
    5.42  
    5.43  datatype data = Data of
    5.44 @@ -228,8 +255,7 @@
    5.45      val (_, T) = dest_Const c;
    5.46      val Ts = binder_types T;
    5.47      val (names, _) =
    5.48 -      fold_map Name.variant
    5.49 -        (Datatype_Prop.make_tnames (map Logic.unvarifyT_global Ts)) used;
    5.50 +      fold_map Name.variant (make_tnames (map Logic.unvarifyT_global Ts)) used;
    5.51      val ty = body_type T;
    5.52      val ty_theta = Type.raw_match (ty, colty) Vartab.empty
    5.53        handle Type.TYPE_MATCH => raise CASE_ERROR ("type mismatch", ~1);