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