--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Datatype_Records.thy Thu Feb 15 13:04:36 2018 +0100
@@ -0,0 +1,67 @@
+section \<open>Records based on BNF/datatype machinery\<close>
+
+theory Datatype_Records
+imports Main
+keywords "datatype_record" :: thy_decl
+begin
+
+no_syntax
+ "_constify" :: "id => ident" ("_")
+ "_constify" :: "longid => ident" ("_")
+
+ "_field_type" :: "ident => type => field_type" ("(2_ ::/ _)")
+ "" :: "field_type => field_types" ("_")
+ "_field_types" :: "field_type => field_types => field_types" ("_,/ _")
+ "_record_type" :: "field_types => type" ("(3\<lparr>_\<rparr>)")
+ "_record_type_scheme" :: "field_types => type => type" ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
+
+ "_field" :: "ident => 'a => field" ("(2_ =/ _)")
+ "" :: "field => fields" ("_")
+ "_fields" :: "field => fields => fields" ("_,/ _")
+ "_record" :: "fields => 'a" ("(3\<lparr>_\<rparr>)")
+ "_record_scheme" :: "fields => 'a => 'a" ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
+
+ "_field_update" :: "ident => 'a => field_update" ("(2_ :=/ _)")
+ "" :: "field_update => field_updates" ("_")
+ "_field_updates" :: "field_update => field_updates => field_updates" ("_,/ _")
+ "_record_update" :: "'a => field_updates => 'b" ("_/(3\<lparr>_\<rparr>)" [900, 0] 900)
+
+no_syntax (ASCII)
+ "_record_type" :: "field_types => type" ("(3'(| _ |'))")
+ "_record_type_scheme" :: "field_types => type => type" ("(3'(| _,/ (2... ::/ _) |'))")
+ "_record" :: "fields => 'a" ("(3'(| _ |'))")
+ "_record_scheme" :: "fields => 'a => 'a" ("(3'(| _,/ (2... =/ _) |'))")
+ "_record_update" :: "'a => field_updates => 'b" ("_/(3'(| _ |'))" [900, 0] 900)
+
+(* copied and adapted from Record.thy *)
+
+nonterminal
+ field and
+ fields and
+ field_update and
+ field_updates
+
+syntax
+ "_constify" :: "id => ident" ("_")
+ "_constify" :: "longid => ident" ("_")
+
+ "_datatype_field" :: "ident => 'a => field" ("(2_ =/ _)")
+ "" :: "field => fields" ("_")
+ "_datatype_fields" :: "field => fields => fields" ("_,/ _")
+ "_datatype_record" :: "fields => 'a" ("(3\<lparr>_\<rparr>)")
+ "_datatype_field_update" :: "ident => 'a => field_update" ("(2_ :=/ _)")
+ "" :: "field_update => field_updates" ("_")
+ "_datatype_field_updates" :: "field_update => field_updates => field_updates" ("_,/ _")
+ "_datatype_record_update" :: "'a => field_updates => 'b" ("_/(3\<lparr>_\<rparr>)" [900, 0] 900)
+
+syntax (ASCII)
+ "_datatype_record" :: "fields => 'a" ("(3'(| _ |'))")
+ "_datatype_record_scheme" :: "fields => 'a => 'a" ("(3'(| _,/ (2... =/ _) |'))")
+ "_datatype_record_update" :: "'a => field_updates => 'b" ("_/(3'(| _ |'))" [900, 0] 900)
+
+named_theorems datatype_record_update
+
+ML_file "datatype_records.ML"
+setup \<open>Datatype_Records.setup\<close>
+
+end
\ No newline at end of file
--- a/src/HOL/Library/Sublist.thy Thu Feb 15 12:11:00 2018 +0100
+++ b/src/HOL/Library/Sublist.thy Thu Feb 15 13:04:36 2018 +0100
@@ -147,6 +147,9 @@
lemma filter_mono_prefix: "prefix xs ys \<Longrightarrow> prefix (filter P xs) (filter P ys)"
by (auto simp: prefix_def)
+lemma sorted_antimono_prefix: "prefix xs ys \<Longrightarrow> sorted ys \<Longrightarrow> sorted xs"
+by (metis sorted_append prefix_def)
+
lemma prefix_length_less: "strict_prefix xs ys \<Longrightarrow> length xs < length ys"
by (auto simp: strict_prefix_def prefix_def)
@@ -526,6 +529,9 @@
lemma set_mono_suffix: "suffix xs ys \<Longrightarrow> set xs \<subseteq> set ys"
by (auto simp: suffix_def)
+lemma sorted_antimono_suffix: "suffix xs ys \<Longrightarrow> sorted ys \<Longrightarrow> sorted xs"
+by (metis sorted_append suffix_def)
+
lemma suffix_ConsD2: "suffix (x # xs) (y # ys) \<Longrightarrow> suffix xs ys"
proof -
assume "suffix (x # xs) (y # ys)"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/datatype_records.ML Thu Feb 15 13:04:36 2018 +0100
@@ -0,0 +1,182 @@
+signature DATATYPE_RECORDS = sig
+ type ctr_options = string -> bool
+ type ctr_options_cmd = Proof.context -> string -> bool
+
+ val default_ctr_options: ctr_options
+ val default_ctr_options_cmd: ctr_options_cmd
+
+ val mk_update_defs: string -> local_theory -> local_theory
+
+ val bnf_record: binding -> ctr_options -> (binding option * (typ * sort)) list ->
+ (binding * typ) list -> local_theory -> local_theory
+
+ val bnf_record_cmd: binding -> ctr_options_cmd ->
+ (binding option * (string * string option)) list -> (binding * string) list -> local_theory ->
+ local_theory
+
+ val setup: theory -> theory
+end
+
+structure Datatype_Records : DATATYPE_RECORDS = struct
+
+type ctr_options = string -> bool
+type ctr_options_cmd = Proof.context -> string -> bool
+
+val default_ctr_options = Plugin_Name.default_filter
+val default_ctr_options_cmd = K Plugin_Name.default_filter
+
+type data = string Symtab.table
+
+structure Data = Theory_Data
+(
+ type T = data
+ val empty = Symtab.empty
+ val merge = Symtab.merge op =
+ val extend = I
+)
+
+fun mk_update_defs typ_name lthy =
+ let
+ val short_name = Long_Name.base_name typ_name
+
+ val {ctrs, casex, selss, ...} = the (Ctr_Sugar.ctr_sugar_of lthy typ_name)
+ val ctr = case ctrs of [ctr] => ctr | _ => error "BNF_Record.mk_update_defs: expected only single constructor"
+ val sels = case selss of [sels] => sels | _ => error "BNF_Record.mk_update_defs: expected selectors"
+ val ctr_dummy = Const (fst (dest_Const ctr), dummyT)
+ val casex_dummy = Const (fst (dest_Const casex), dummyT)
+
+ val len = length sels
+
+ fun mk_name sel =
+ Binding.name ("update_" ^ Long_Name.base_name (fst (dest_Const sel)))
+
+ fun mk_t idx =
+ let
+ val body =
+ fold_rev (fn pos => fn t => t $ (if len - pos = idx + 1 then Bound len $ Bound pos else Bound pos)) (0 upto len - 1) ctr_dummy
+ |> fold_rev (fn idx => fn t => Abs ("x" ^ Value.print_int idx, dummyT, t)) (1 upto len)
+ in
+ Abs ("f", dummyT, casex_dummy $ body)
+ end
+
+ fun define name t =
+ Local_Theory.define ((name, NoSyn), ((Binding.empty, @{attributes [datatype_record_update, code]}), t)) #> snd
+
+ val lthy' =
+ Local_Theory.map_background_naming (Name_Space.qualified_path false (Binding.name short_name)) lthy
+
+ fun insert sel =
+ Symtab.insert op = (fst (dest_Const sel), Local_Theory.full_name lthy' (mk_name sel))
+ in
+ lthy'
+ |> @{fold 2} define (map mk_name sels) (Syntax.check_terms lthy (map mk_t (0 upto len - 1)))
+ |> Local_Theory.background_theory (Data.map (fold insert sels))
+ |> Local_Theory.restore_background_naming lthy
+ end
+
+fun bnf_record binding opts tyargs args lthy =
+ let
+ val constructor =
+ (((Binding.empty, Binding.map_name (fn c => "make_" ^ c) binding), args), NoSyn)
+
+ val datatyp =
+ ((tyargs, binding), NoSyn)
+
+ val dtspec =
+ ((opts, false),
+ [(((datatyp, [constructor]), (Binding.empty, Binding.empty, Binding.empty)), [])])
+
+ val lthy' =
+ BNF_FP_Def_Sugar.co_datatypes BNF_Util.Least_FP BNF_LFP.construct_lfp dtspec lthy
+ |> mk_update_defs (Local_Theory.full_name lthy binding)
+ in
+ lthy'
+ end
+
+fun bnf_record_cmd binding opts tyargs args lthy =
+ bnf_record binding (opts lthy)
+ (map (apsnd (apfst (Syntax.parse_typ lthy) o apsnd (Typedecl.read_constraint lthy))) tyargs)
+ (map (apsnd (Syntax.parse_typ lthy)) args) lthy
+
+(* syntax *)
+(* copied and adapted from record.ML *)
+
+val read_const =
+ dest_Const oo Proof_Context.read_const {proper = true, strict = true}
+
+fun field_tr ((Const (\<^syntax_const>\<open>_datatype_field\<close>, _) $ Const (name, _) $ arg)) = (name, arg)
+ | field_tr t = raise TERM ("field_tr", [t]);
+
+fun fields_tr (Const (\<^syntax_const>\<open>_datatype_fields\<close>, _) $ t $ u) = field_tr t :: fields_tr u
+ | fields_tr t = [field_tr t];
+
+fun record_fields_tr ctxt t =
+ let
+ val assns = map (apfst (read_const ctxt)) (fields_tr t)
+
+ val typ_name =
+ snd (fst (hd assns))
+ |> domain_type
+ |> dest_Type
+ |> fst
+
+ val assns' = map (apfst fst) assns
+
+ val {ctrs, selss, ...} = the (Ctr_Sugar.ctr_sugar_of ctxt typ_name)
+ val ctr = case ctrs of [ctr] => ctr | _ => error "BNF_Record.record_fields_tr: expected only single constructor"
+ val sels = case selss of [sels] => sels | _ => error "BNF_Record.record_fields_tr: expected selectors"
+ val ctr_dummy = Const (fst (dest_Const ctr), dummyT)
+
+ fun mk_arg name =
+ case AList.lookup op = assns' name of
+ NONE => error ("BNF_Record.record_fields_tr: missing field " ^ name)
+ | SOME t => t
+ in
+ if length assns = length sels then
+ list_comb (ctr_dummy, map (mk_arg o fst o dest_Const) sels)
+ else
+ error ("BNF_Record.record_fields_tr: expected " ^ Value.print_int (length sels) ^ " field(s)")
+ end
+
+fun field_update_tr ctxt (Const (\<^syntax_const>\<open>_datatype_field_update\<close>, _) $ Const (name, _) $ arg) =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val (name, _) = read_const ctxt name
+ in
+ case Symtab.lookup (Data.get thy) name of
+ NONE => raise Fail ("not a valid record field: " ^ name)
+ | SOME s => Const (s, dummyT) $ Abs (Name.uu_, dummyT, arg)
+ end
+ | field_update_tr _ t = raise TERM ("field_update_tr", [@{print} t]);
+
+fun field_updates_tr ctxt (Const (\<^syntax_const>\<open>_datatype_field_updates\<close>, _) $ t $ u) =
+ field_update_tr ctxt t :: field_updates_tr ctxt u
+ | field_updates_tr ctxt t = [field_update_tr ctxt t];
+
+fun record_tr ctxt [t] = record_fields_tr ctxt t
+ | record_tr _ ts = raise TERM ("record_tr", ts);
+
+fun record_update_tr ctxt [t, u] = fold (curry op $) (field_updates_tr ctxt u) t
+ | record_update_tr _ ts = raise TERM ("record_update_tr", ts);
+
+val parse_ctr_options =
+ Scan.optional (@{keyword "("} |-- Parse.list1 (Plugin_Name.parse_filter >> K) --| @{keyword ")"} >>
+ (fn fs => fold I fs default_ctr_options_cmd)) default_ctr_options_cmd
+
+val parser =
+ (parse_ctr_options -- BNF_Util.parse_type_args_named_constrained -- Parse.binding) --
+ (\<^keyword>\<open>=\<close> |-- Scan.repeat1 (Parse.binding -- (Parse.$$$ "::" |-- Parse.!!! Parse.typ)))
+
+val _ =
+ Outer_Syntax.local_theory
+ @{command_keyword datatype_record}
+ "Defines a record based on the BNF/datatype machinery"
+ (parser >> (fn (((ctr_options, tyargs), binding), args) =>
+ bnf_record_cmd binding ctr_options tyargs args))
+
+val setup =
+ (Sign.parse_translation
+ [(\<^syntax_const>\<open>_datatype_record_update\<close>, record_update_tr),
+ (\<^syntax_const>\<open>_datatype_record\<close>, record_tr)]);
+
+end
\ No newline at end of file
--- a/src/HOL/ROOT Thu Feb 15 12:11:00 2018 +0100
+++ b/src/HOL/ROOT Thu Feb 15 13:04:36 2018 +0100
@@ -34,6 +34,8 @@
Product_Lexorder
Product_Order
Subseq_Order
+ (*conflicting syntax*)
+ Datatype_Records
(*data refinements and dependent applications*)
AList_Mapping
Code_Binary_Nat
@@ -539,6 +541,7 @@
Computations
Conditional_Parametricity_Examples
Cubic_Quartic
+ Datatype_Record_Examples
Dedekind_Real
Erdoes_Szekeres
Eval_Examples
@@ -573,6 +576,7 @@
Primrec
Pythagoras
Quicksort
+ Radix_Sort
Records
Reflection_Examples
Refute_Examples
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Datatype_Record_Examples.thy Thu Feb 15 13:04:36 2018 +0100
@@ -0,0 +1,48 @@
+theory Datatype_Record_Examples
+imports "HOL-Library.Datatype_Records"
+begin
+
+text \<open>Standard usage\<close>
+
+datatype_record ('a, 'b) foo =
+ field_1 :: 'a
+ field_2 :: 'b
+
+lemma "\<lparr> field_1 = 3, field_2 = () \<rparr> = (make_foo 3 () :: (nat, unit) foo)" ..
+
+lemma "(make_foo a b) \<lparr> field_1 := y \<rparr> = make_foo y b"
+ by (simp add: datatype_record_update)
+
+lemma "(make_foo a b) \<lparr> foo.field_1 := y \<rparr> = make_foo y b"
+ by (simp add: datatype_record_update)
+
+text \<open>Existing datatypes\<close>
+
+datatype x = X (a: int) (b: int)
+
+lemma "\<lparr> a = 1, b = 2 \<rparr> = X 1 2" ..
+
+local_setup \<open>Datatype_Records.mk_update_defs @{type_name x}\<close>
+
+lemma "(X 1 2) \<lparr> b := 3 \<rparr> = X 1 3"
+ by (simp add: datatype_record_update)
+
+text \<open>Nested recursion\<close>
+
+datatype_record 'a container =
+ content :: "'a option"
+
+datatype 'a contrived = Contrived "'a contrived container"
+
+term "Contrived \<lparr> content = None \<rparr>"
+
+text \<open>Supports features of @{command datatype}\<close>
+
+datatype_record (plugins del: code) (dead 'a :: finite, b_set: 'b) rec =
+ field_1 :: 'a
+ field_2 :: 'b
+
+lemma "b_set \<lparr> field_1 = True, field_2 = False \<rparr> = {False}"
+ by simp
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Radix_Sort.thy Thu Feb 15 13:04:36 2018 +0100
@@ -0,0 +1,74 @@
+(* Author: Tobias Nipkow *)
+
+theory Radix_Sort
+imports
+ "HOL-Library.Multiset"
+ "HOL-Library.List_lexord"
+ "HOL-Library.Sublist"
+begin
+
+fun radix_sort :: "nat \<Rightarrow> 'a::linorder list list \<Rightarrow> 'a list list" where
+"radix_sort 0 xss = xss" |
+"radix_sort (Suc n) xss = radix_sort n (sort_key (\<lambda>xs. xs ! n) xss)"
+
+abbreviation "sorted_from i xss \<equiv> sorted (map (drop i) xss)"
+
+definition "cols xss k = (\<forall>xs \<in> set xss. length xs = k)"
+
+lemma mset_radix_sort: "mset (radix_sort k xss) = mset xss"
+by(induction k arbitrary: xss) (auto)
+
+lemma cols_sort_key: "cols xss n \<Longrightarrow> cols (sort_key f xss) n"
+by(simp add: cols_def)
+
+lemma sorted_from_Suc2: "\<lbrakk> cols xss n; i < n;
+ sorted (map (\<lambda>xs. xs!i) xss); \<forall>xs \<in> set xss. sorted_from (i+1) [ys \<leftarrow> xss. ys!i = xs!i] \<rbrakk>
+ \<Longrightarrow> sorted_from i xss"
+proof(induction xss rule: induct_list012)
+ case 1 show ?case by simp
+next
+ case 2 show ?case by simp
+next
+ case (3 xs1 xs2 xss)
+ have lxs1: "length xs1 = n" and lxs2: "length xs2 = n"
+ using "3.prems"(1) by(auto simp: cols_def)
+ have *: "drop i xs1 \<le> drop i xs2"
+ proof -
+ have "drop i xs1 = xs1!i # drop (i+1) xs1"
+ using \<open>i < n\<close> by (simp add: Cons_nth_drop_Suc lxs1)
+ also have "\<dots> \<le> xs2!i # drop (i+1) xs2" using "3.prems"(3,4) by(auto)
+ also have "\<dots> = drop i xs2"
+ using \<open>i < n\<close> by (simp add: Cons_nth_drop_Suc lxs2)
+ finally show ?thesis .
+ qed
+ have "sorted_from i (xs2 # xss)"
+ proof(rule "3.IH"[OF _ "3.prems"(2)])
+ show "cols (xs2 # xss) n" using "3.prems"(1) by(simp add: cols_def)
+ show "sorted (map (\<lambda>xs. xs ! i) (xs2 # xss))" using "3.prems"(3) by simp
+ show "\<forall>xs\<in>set (xs2 # xss). sorted_from (i+1) [ys\<leftarrow>xs2 # xss . ys ! i = xs ! i]"
+ using "3.prems"(4)
+ sorted_antimono_suffix[OF map_mono_suffix[OF filter_mono_suffix[OF suffix_ConsI[OF suffix_order.order.refl]]]]
+ by fastforce
+ qed
+ with * show ?case by (auto)
+qed
+
+lemma sorted_from_radix_sort_step:
+ "\<lbrakk> cols xss n; i < n; sorted_from (Suc i) xss \<rbrakk> \<Longrightarrow> sorted_from i (sort_key (\<lambda>xs. xs ! i) xss)"
+apply (rule sorted_from_Suc2)
+apply (auto simp add: sort_key_stable[of _ xss "%xs. xs!i"] sorted_filter cols_def)
+done
+
+lemma sorted_from_radix_sort:
+ "cols xss n \<Longrightarrow> i \<le> n \<Longrightarrow> sorted_from i xss \<Longrightarrow> sorted_from 0 (radix_sort i xss)"
+apply(induction i arbitrary: xss)
+ apply(simp add: sort_key_const)
+apply(simp add: sorted_from_radix_sort_step cols_sort_key)
+done
+
+lemma sorted_radix_sort: "cols xss n \<Longrightarrow> sorted (radix_sort n xss)"
+apply(frule sorted_from_radix_sort[OF _ le_refl])
+ apply(auto simp add: cols_def sorted_equals_nth_mono)
+done
+
+end