merged

--- a/NEWS	Mon May 30 20:58:16 2016 +0200
+++ b/NEWS	Mon May 30 20:58:54 2016 +0200
@@ -104,6 +104,13 @@
 
 *** HOL ***
 
+* Command 'code_reflect' accepts empty constructor lists for datatypes,
+which renders those abstract effectively.
+
+* Command 'export_code' checks given constants for abstraction violations:
+a small guarantee that given constants specify a safe interface for the
+generated code.
+
 * Probability/Random_Permutations.thy contains some theory about 
 choosing a permutation of a set uniformly at random and folding over a 
 list in random order.
@@ -231,10 +238,11 @@
 for polynomials over factorial rings.  INCOMPATIBILITY.
 
 * Library/Sublist.thy: added function "prefixes" and renamed
- prefixeq -> prefix
- prefix -> strict_prefix
- suffixeq -> suffix
- suffix -> strict_suffix
+  prefixeq -> prefix
+  prefix -> strict_prefix
+  suffixeq -> suffix
+  suffix -> strict_suffix
+  Added theory of longest common prefixes.
 
 * Dropped various legacy fact bindings, whose replacements are often
 of a more general type also:

--- a/src/Doc/Codegen/Evaluation.thy	Mon May 30 20:58:16 2016 +0200
+++ b/src/Doc/Codegen/Evaluation.thy	Mon May 30 20:58:54 2016 +0200
@@ -344,7 +344,7 @@
 \<close>
 
 code_reflect %quote Rat
-  datatypes rat = Frct
+  datatypes rat
   functions Fract
     "(plus :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(minus :: rat \<Rightarrow> rat \<Rightarrow> rat)"
     "(times :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(divide :: rat \<Rightarrow> rat \<Rightarrow> rat)"

--- a/src/HOL/Code_Numeral.thy	Mon May 30 20:58:16 2016 +0200
+++ b/src/HOL/Code_Numeral.thy	Mon May 30 20:58:54 2016 +0200
@@ -893,9 +893,9 @@
   "Nat (integer_of_natural n) = n"
   by transfer simp
 
-lemma [code abstract]:
-  "integer_of_natural (natural_of_nat n) = of_nat n"
-  by simp
+lemma [code]:
+  "natural_of_nat n = natural_of_integer (integer_of_nat n)"
+  by transfer simp
 
 lemma [code abstract]:
   "integer_of_natural (natural_of_integer k) = max 0 k"
@@ -969,7 +969,11 @@
 lifting_forget natural.lifting
 
 code_reflect Code_Numeral
-  datatypes natural = _
-  functions integer_of_natural natural_of_integer
+  datatypes natural
+  functions "Code_Numeral.Suc" "0 :: natural" "1 :: natural"
+    "plus :: natural \<Rightarrow> _" "minus :: natural \<Rightarrow> _"
+    "times :: natural \<Rightarrow> _" "divide :: natural \<Rightarrow> _"
+    "Divides.mod :: natural \<Rightarrow> _"
+    integer_of_natural natural_of_integer
 
 end

--- a/src/HOL/Library/Sublist.thy	Mon May 30 20:58:16 2016 +0200
+++ b/src/HOL/Library/Sublist.thy	Mon May 30 20:58:54 2016 +0200
@@ -127,6 +127,10 @@
   "prefix (xs\<^sub>1::'a list) ys \<Longrightarrow> prefix xs\<^sub>2 ys \<Longrightarrow> prefix xs\<^sub>1 xs\<^sub>2 \<or> prefix xs\<^sub>2 xs\<^sub>1"
   unfolding prefix_def by (force simp: append_eq_append_conv2)
 
+lemma prefix_length_prefix:
+  "prefix ps xs \<Longrightarrow> prefix qs xs \<Longrightarrow> length ps \<le> length qs \<Longrightarrow> prefix ps qs"
+by (auto simp: prefix_def) (metis append_Nil2 append_eq_append_conv_if)
+
 lemma set_mono_prefix: "prefix xs ys \<Longrightarrow> set xs \<subseteq> set ys"
   by (auto simp add: prefix_def)
 
@@ -226,6 +230,128 @@
 by (cases ys rule: rev_cases) auto
 
 
+subsection \<open>Longest Common Prefix\<close>
+
+definition Longest_common_prefix :: "'a list set \<Rightarrow> 'a list" where
+"Longest_common_prefix L = (GREATEST ps WRT length. \<forall>xs \<in> L. prefix ps xs)"
+
+lemma Longest_common_prefix_ex: "L \<noteq> {} \<Longrightarrow>
+  \<exists>ps. (\<forall>xs \<in> L. prefix ps xs) \<and> (\<forall>qs. (\<forall>xs \<in> L. prefix qs xs) \<longrightarrow> size qs \<le> size ps)"
+  (is "_ \<Longrightarrow> \<exists>ps. ?P L ps")
+proof(induction "LEAST n. \<exists>xs \<in>L. n = length xs" arbitrary: L)
+  case 0
+  have "[] : L" using "0.hyps" LeastI[of "\<lambda>n. \<exists>xs\<in>L. n = length xs"] \<open>L \<noteq> {}\<close>
+    by auto
+  hence "?P L []" by(auto)
+  thus ?case ..
+next
+  case (Suc n)
+  let ?EX = "\<lambda>n. \<exists>xs\<in>L. n = length xs"
+  obtain x xs where xxs: "x#xs \<in> L" "size xs = n" using Suc.prems Suc.hyps(2)
+    by(metis LeastI_ex[of ?EX] Suc_length_conv ex_in_conv)
+  hence "[] \<notin> L" using Suc.hyps(2) by auto
+  show ?case
+  proof (cases "\<forall>xs \<in> L. \<exists>ys. xs = x#ys")
+    case True
+    let ?L = "{ys. x#ys \<in> L}"
+    have 1: "(LEAST n. \<exists>xs \<in> ?L. n = length xs) = n"
+      using xxs Suc.prems Suc.hyps(2) Least_le[of "?EX"]
+      by - (rule Least_equality, fastforce+)
+    have 2: "?L \<noteq> {}" using \<open>x # xs \<in> L\<close> by auto
+    from Suc.hyps(1)[OF 1[symmetric] 2] obtain ps where IH: "?P ?L ps" ..
+    { fix qs
+      assume "\<forall>qs. (\<forall>xa. x # xa \<in> L \<longrightarrow> prefix qs xa) \<longrightarrow> length qs \<le> length ps"
+      and "\<forall>xs\<in>L. prefix qs xs"
+      hence "length (tl qs) \<le> length ps"
+        by (metis Cons_prefix_Cons hd_Cons_tl list.sel(2) Nil_prefix) 
+      hence "length qs \<le> Suc (length ps)" by auto
+    }
+    hence "?P L (x#ps)" using True IH by auto
+    thus ?thesis ..
+  next
+    case False
+    then obtain y ys where yys: "x\<noteq>y" "y#ys \<in> L" using \<open>[] \<notin> L\<close>
+      by (auto) (metis list.exhaust)
+    have "\<forall>qs. (\<forall>xs\<in>L. prefix qs xs) \<longrightarrow> qs = []" using yys \<open>x#xs \<in> L\<close>
+      by auto (metis Cons_prefix_Cons prefix_Cons)
+    hence "?P L []" by auto
+    thus ?thesis ..
+  qed
+qed
+
+lemma Longest_common_prefix_unique: "L \<noteq> {} \<Longrightarrow>
+  \<exists>! ps. (\<forall>xs \<in> L. prefix ps xs) \<and> (\<forall>qs. (\<forall>xs \<in> L. prefix qs xs) \<longrightarrow> size qs \<le> size ps)"
+by(rule ex_ex1I[OF Longest_common_prefix_ex];
+   meson equals0I prefix_length_prefix prefix_order.antisym)
+
+lemma Longest_common_prefix_eq:
+ "\<lbrakk> L \<noteq> {};  \<forall>xs \<in> L. prefix ps xs;
+    \<forall>qs. (\<forall>xs \<in> L. prefix qs xs) \<longrightarrow> size qs \<le> size ps \<rbrakk>
+  \<Longrightarrow> Longest_common_prefix L = ps"
+unfolding Longest_common_prefix_def GreatestM_def
+by(rule some1_equality[OF Longest_common_prefix_unique]) auto
+
+lemma Longest_common_prefix_prefix:
+  "xs \<in> L \<Longrightarrow> prefix (Longest_common_prefix L) xs"
+unfolding Longest_common_prefix_def GreatestM_def
+by(rule someI2_ex[OF Longest_common_prefix_ex]) auto
+
+lemma Longest_common_prefix_longest:
+  "L \<noteq> {} \<Longrightarrow> \<forall>xs\<in>L. prefix ps xs \<Longrightarrow> length ps \<le> length(Longest_common_prefix L)"
+unfolding Longest_common_prefix_def GreatestM_def
+by(rule someI2_ex[OF Longest_common_prefix_ex]) auto
+
+lemma Longest_common_prefix_max_prefix:
+  "L \<noteq> {} \<Longrightarrow> \<forall>xs\<in>L. prefix ps xs \<Longrightarrow> prefix ps (Longest_common_prefix L)"
+by(metis Longest_common_prefix_prefix Longest_common_prefix_longest
+     prefix_length_prefix ex_in_conv)
+
+lemma Longest_common_prefix_Nil: "[] \<in> L \<Longrightarrow> Longest_common_prefix L = []"
+using Longest_common_prefix_prefix prefix_Nil by blast
+
+lemma Longest_common_prefix_image_Cons: "L \<noteq> {} \<Longrightarrow>
+  Longest_common_prefix (op # x ` L) = x # Longest_common_prefix L"
+apply(rule Longest_common_prefix_eq)
+  apply(simp)
+ apply (simp add: Longest_common_prefix_prefix)
+apply simp
+by(metis Longest_common_prefix_longest[of L] Cons_prefix_Cons Nitpick.size_list_simp(2)
+     Suc_le_mono hd_Cons_tl order.strict_implies_order zero_less_Suc)
+
+lemma Longest_common_prefix_eq_Cons: assumes "L \<noteq> {}" "[] \<notin> L"  "\<forall>xs\<in>L. hd xs = x"
+shows "Longest_common_prefix L = x # Longest_common_prefix {ys. x#ys \<in> L}"
+proof -
+  have "L = op # x ` {ys. x#ys \<in> L}" using assms(2,3)
+    by (auto simp: image_def)(metis hd_Cons_tl)
+  thus ?thesis
+    by (metis Longest_common_prefix_image_Cons image_is_empty assms(1))
+qed
+
+lemma Longest_common_prefix_eq_Nil:
+  "\<lbrakk>x#ys \<in> L; y#zs \<in> L; x \<noteq> y \<rbrakk> \<Longrightarrow> Longest_common_prefix L = []"
+by (metis Longest_common_prefix_prefix list.inject prefix_Cons)
+
+
+fun longest_common_prefix :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"longest_common_prefix (x#xs) (y#ys) =
+  (if x=y then x # longest_common_prefix xs ys else [])" |
+"longest_common_prefix _ _ = []"
+
+lemma longest_common_prefix_prefix1:
+  "prefix (longest_common_prefix xs ys) xs"
+by(induction xs ys rule: longest_common_prefix.induct) auto
+
+lemma longest_common_prefix_prefix2:
+  "prefix (longest_common_prefix xs ys) ys"
+by(induction xs ys rule: longest_common_prefix.induct) auto
+
+lemma longest_common_prefix_max_prefix:
+  "\<lbrakk> prefix ps xs; prefix ps ys \<rbrakk>
+   \<Longrightarrow> prefix ps (longest_common_prefix xs ys)"
+by(induction xs ys arbitrary: ps rule: longest_common_prefix.induct)
+  (auto simp: prefix_Cons)
+
+
 subsection \<open>Parallel lists\<close>
 
 definition parallel :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"  (infixl "\<parallel>" 50)

--- a/src/HOL/List.thy	Mon May 30 20:58:16 2016 +0200
+++ b/src/HOL/List.thy	Mon May 30 20:58:54 2016 +0200
@@ -1002,6 +1002,12 @@
  (ys = [] & zs = x#xs | (EX ys'. ys = x#ys' & ys'@zs = xs))"
 by(cases ys) auto
 
+lemma longest_common_prefix:
+  "\<exists>ps xs' ys'. xs = ps @ xs' \<and> ys = ps @ ys'
+       \<and> (xs' = [] \<or> ys' = [] \<or> hd xs' \<noteq> hd ys')"
+by (induct xs ys rule: list_induct2')
+   (blast, blast, blast,
+    metis (no_types, hide_lams) append_Cons append_Nil list.sel(1))
 
 text \<open>Trivial rules for solving \<open>@\<close>-equations automatically.\<close>
 
@@ -1961,6 +1967,12 @@
   "xs @ [x] = ys \<longleftrightarrow> (ys \<noteq> [] & butlast ys = xs & last ys = x)"
 by fastforce
 
+corollary longest_common_suffix:
+  "\<exists>ss xs' ys'. xs = xs' @ ss \<and> ys = ys' @ ss
+       \<and> (xs' = [] \<or> ys' = [] \<or> last xs' \<noteq> last ys')"
+using longest_common_prefix[of "rev xs" "rev ys"]
+unfolding rev_swap rev_append by (metis last_rev rev_is_Nil_conv)
+
 
 subsubsection \<open>@{const take} and @{const drop}\<close>
 

--- a/src/Tools/Code/code_ml.ML	Mon May 30 20:58:16 2016 +0200
+++ b/src/Tools/Code/code_ml.ML	Mon May 30 20:58:54 2016 +0200
@@ -772,13 +772,18 @@
     fun modify_funs stmts = single (SOME
       (Code_Namespace.Opaque, ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst)))
     fun modify_datatypes stmts =
-      map_filter
-        (fn (Type_Constructor tyco, (export, Code_Thingol.Datatype stmt)) => SOME (export, (tyco, stmt)) | _ => NONE) stmts
-      |> split_list
-      |> apfst Code_Namespace.join_exports
-      |> apsnd ML_Datas
-      |> SOME
-      |> single;
+      let
+        val datas = map_filter
+          (fn (Type_Constructor tyco, (export, Code_Thingol.Datatype stmt)) => SOME (export, (tyco, stmt)) | _ => NONE) stmts
+      in
+        if null datas then [] (*for abstract types wrt. code_reflect*)
+        else datas
+          |> split_list
+          |> apfst Code_Namespace.join_exports
+          |> apsnd ML_Datas
+          |> SOME
+          |> single
+      end;
     fun modify_class stmts =
       the_single (map_filter
         (fn (Type_Class class, (export, Code_Thingol.Class stmt)) => SOME (export, (class, stmt)) | _ => NONE) stmts)

--- a/src/Tools/Code/code_runtime.ML	Mon May 30 20:58:16 2016 +0200
+++ b/src/Tools/Code/code_runtime.ML	Mon May 30 20:58:54 2016 +0200
@@ -375,20 +375,21 @@
 
 fun check_datatype thy tyco some_consts =
   let
-    val constrs = (map fst o snd o fst o Code.get_type thy) tyco;
-    val _ = case some_consts
-     of SOME consts =>
+    val declared_constrs = (map fst o snd o fst o Code.get_type thy) tyco;
+    val constrs = case some_consts
+     of SOME [] => []
+      | SOME consts =>
           let
-            val missing_constrs = subtract (op =) consts constrs;
+            val missing_constrs = subtract (op =) consts declared_constrs;
             val _ = if null missing_constrs then []
               else error ("Missing constructor(s) " ^ commas_quote missing_constrs
                 ^ " for datatype " ^ quote tyco);
-            val false_constrs = subtract (op =) constrs consts;
+            val false_constrs = subtract (op =) declared_constrs consts;
             val _ = if null false_constrs then []
               else error ("Non-constructor(s) " ^ commas_quote false_constrs
                 ^ " for datatype " ^ quote tyco)
-          in () end
-      | NONE => ();
+          in consts end
+      | NONE => declared_constrs;
   in (tyco, constrs) end;
 
 fun add_eval_tyco (tyco, tyco') thy =
@@ -465,16 +466,16 @@
 local
 
 val parse_datatype =
-  Parse.name --| @{keyword "="} --
+  Parse.name -- Scan.optional (@{keyword "="} |--
     (((Parse.sym_ident || Parse.string) >> (fn "_" => NONE | _ => Scan.fail ()))
-    || ((Parse.term ::: (Scan.repeat (@{keyword "|"} |-- Parse.term))) >> SOME));
+    || ((Parse.term ::: (Scan.repeat (@{keyword "|"} |-- Parse.term))) >> SOME))) (SOME []);
 
 in
 
 val _ =
   Outer_Syntax.command @{command_keyword code_reflect}
     "enrich runtime environment with generated code"
-    (Parse.name -- Scan.optional (@{keyword "datatypes"} |-- Parse.!!!  (parse_datatype
+    (Parse.name -- Scan.optional (@{keyword "datatypes"} |-- Parse.!!! (parse_datatype
       ::: Scan.repeat (@{keyword "and"} |-- parse_datatype))) []
     -- Scan.optional (@{keyword "functions"} |-- Parse.!!!  (Scan.repeat1 Parse.name)) []
     -- Scan.option (@{keyword "file"} |-- Parse.!!! Parse.name)

--- a/src/Tools/Code/code_thingol.ML	Mon May 30 20:58:16 2016 +0200
+++ b/src/Tools/Code/code_thingol.ML	Mon May 30 20:58:54 2016 +0200
@@ -786,11 +786,23 @@
 
 (* program generation *)
 
+fun check_abstract_constructors thy consts =
+  case filter (Code.is_abstr thy) consts of
+    [] => ()
+  | abstrs => error ("Cannot export abstract constructor(s): "
+      ^ commas (map (Code.string_of_const thy) abstrs));
+
 fun invoke_generation_for_consts ctxt { ignore_cache, permissive } { algebra, eqngr } consts =
-  Code_Preproc.timed "translating program" #ctxt
-  (fn { ctxt, algebra, eqngr, consts } => invoke_generation ignore_cache ctxt
-    (fold_map (ensure_const ctxt algebra eqngr permissive)) consts)
-    { ctxt = ctxt, algebra = algebra, eqngr = eqngr, consts = consts };
+  let
+    val thy = Proof_Context.theory_of ctxt;
+    val _ = if permissive then ()
+      else check_abstract_constructors thy consts;
+  in
+    Code_Preproc.timed "translating program" #ctxt
+    (fn { ctxt, algebra, eqngr, consts } => invoke_generation ignore_cache ctxt
+      (fold_map (ensure_const ctxt algebra eqngr permissive)) consts)
+      { ctxt = ctxt, algebra = algebra, eqngr = eqngr, consts = consts }
+  end;
 
 fun invoke_generation_for_consts' ctxt ignore_cache_and_permissive consts =
   invoke_generation_for_consts ctxt
@@ -914,7 +926,8 @@
     val thy = Proof_Context.theory_of ctxt;
     fun consts_of thy' =
       fold (fn (c, (_, NONE)) => cons c | _ => I)
-        (#constants (Consts.dest (Sign.consts_of thy'))) [];
+        (#constants (Consts.dest (Sign.consts_of thy'))) []
+      |> filter_out (Code.is_abstr thy);
     fun belongs_here thy' c = forall
       (fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy');
     fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy');
@@ -934,8 +947,10 @@
   let
     val (consts, consts_permissive) =
       read_const_exprs_internal ctxt const_exprs;
-    val consts' = implemented_deps
-      (consts_program_permissive ctxt consts_permissive);
+    val consts' = 
+      consts_program_permissive ctxt consts_permissive
+      |> implemented_deps
+      |> filter_out (Code.is_abstr (Proof_Context.theory_of ctxt));
   in union (op =) consts' consts end;