Merge
authorpaulson <lp15@cam.ac.uk>
Wed, 09 Mar 2016 17:22:43 +0000 (2016-03-09)
changeset 62541 b351da9b4c7d
parent 62540 f2fc5485e3b0 (current diff)
parent 62539 00f8bca4aba0 (diff)
child 62579 bfa38c2e751f
Merge
--- a/NEWS	Wed Mar 09 17:16:08 2016 +0000
+++ b/NEWS	Wed Mar 09 17:22:43 2016 +0000
@@ -54,7 +54,6 @@
 resemble the f.split naming convention, INCOMPATIBILITY.
 
 * Multiset membership is now expressed using set_mset rather than count.
-ASCII infix syntax ":#" has been discontinued.
 
   - Expressions "count M a > 0" and similar simplify to membership
     by default.
--- a/src/HOL/Library/Multiset.thy	Wed Mar 09 17:16:08 2016 +0000
+++ b/src/HOL/Library/Multiset.thy	Wed Mar 09 17:22:43 2016 +0000
@@ -113,11 +113,27 @@
 definition set_mset :: "'a multiset \<Rightarrow> 'a set"
   where "set_mset M = {x. count M x > 0}"
 
-abbreviation Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<in>#" 50)
-  where "a \<in># M \<equiv> a \<in> set_mset M"
-
-abbreviation not_Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<notin>#" 50)
-  where "a \<notin># M \<equiv> a \<notin> set_mset M"
+abbreviation Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool"
+  where "Melem a M \<equiv> a \<in> set_mset M"
+
+notation
+  Melem  ("op \<in>#") and
+  Melem  ("(_/ \<in># _)" [51, 51] 50)
+
+notation  (ASCII)
+  Melem  ("op :#") and
+  Melem  ("(_/ :# _)" [51, 51] 50)
+
+abbreviation not_Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool"
+  where "not_Melem a M \<equiv> a \<notin> set_mset M"
+
+notation
+  not_Melem  ("op \<notin>#") and
+  not_Melem  ("(_/ \<notin># _)" [51, 51] 50)
+
+notation  (ASCII)
+  not_Melem  ("op ~:#") and
+  not_Melem  ("(_/ ~:# _)" [51, 51] 50)
 
 context
 begin
@@ -134,6 +150,10 @@
   "_MBall"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<forall>_\<in>#_./ _)" [0, 0, 10] 10)
   "_MBex"        :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<exists>_\<in>#_./ _)" [0, 0, 10] 10)
 
+syntax  (ASCII)
+  "_MBall"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<forall>_:#_./ _)" [0, 0, 10] 10)
+  "_MBex"        :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<exists>_:#_./ _)" [0, 0, 10] 10)
+
 translations
   "\<forall>x\<in>#A. P" \<rightleftharpoons> "CONST Multiset.Ball A (\<lambda>x. P)"
   "\<exists>x\<in>#A. P" \<rightleftharpoons> "CONST Multiset.Bex A (\<lambda>x. P)"
--- a/src/Pure/proofterm.ML	Wed Mar 09 17:16:08 2016 +0000
+++ b/src/Pure/proofterm.ML	Wed Mar 09 17:22:43 2016 +0000
@@ -1057,7 +1057,7 @@
 
 fun of_sort_proof thy hyps =
   Sorts.of_sort_derivation (Sign.classes_of thy)
-   {class_relation = fn typ => fn (prf, c1) => fn c2 =>
+   {class_relation = fn typ => fn _ => fn (prf, c1) => fn c2 =>
       if c1 = c2 then prf
       else canonical_instance [typ] (classrel_proof thy (c1, c2)) %% prf,
     type_constructor = fn (a, typs) => fn dom => fn c =>
--- a/src/Pure/sorts.ML	Wed Mar 09 17:16:08 2016 +0000
+++ b/src/Pure/sorts.ML	Wed Mar 09 17:22:43 2016 +0000
@@ -55,7 +55,7 @@
   val meet_sort_typ: algebra -> typ * sort -> typ -> typ   (*exception CLASS_ERROR*)
   val of_sort: algebra -> typ * sort -> bool
   val of_sort_derivation: algebra ->
-    {class_relation: typ -> 'a * class -> class -> 'a,
+    {class_relation: typ -> bool -> 'a * class -> class -> 'a,
      type_constructor: string * typ list -> ('a * class) list list -> class -> 'a,
      type_variable: typ -> ('a * class) list} ->
     typ * sort -> 'a list   (*exception CLASS_ERROR*)
@@ -403,9 +403,10 @@
         if S1 = S2 then map fst D1
         else
           S2 |> map (fn c2 =>
-            (case D1 |> find_first (fn (_, c1) => class_le algebra (c1, c2)) of
-              SOME d1 => class_relation T d1 c2
-            | NONE => raise CLASS_ERROR (No_Subsort (S1, S2))))
+            (case D1 |> filter (fn (_, c1) => class_le algebra (c1, c2)) of
+              [d1] => class_relation T true d1 c2
+            | (d1 :: _ :: _) => class_relation T false d1 c2
+            | [] => raise CLASS_ERROR (No_Subsort (S1, S2))))
       end;
 
     fun derive (_, []) = []
--- a/src/Tools/Code/code_ml.ML	Wed Mar 09 17:16:08 2016 +0000
+++ b/src/Tools/Code/code_ml.ML	Wed Mar 09 17:22:43 2016 +0000
@@ -87,12 +87,13 @@
           ((str o deresolve_inst) inst ::
             (if is_pseudo_fun (Class_Instance inst) then [str "()"]
             else map_filter (print_dicts is_pseudo_fun BR) dss))
-      | print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
-          [str (if k = 1 then Name.enforce_case true v ^ "_"
-            else Name.enforce_case true v ^ string_of_int (i+1) ^ "_")]
+      | print_plain_dict is_pseudo_fun fxy (Dict_Var { var, index, length }) =
+          [str (if length = 1 then Name.enforce_case true var ^ "_"
+            else Name.enforce_case true var ^ string_of_int (index + 1) ^ "_")]
     and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
     val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
-      (map_index (fn (i, _) => Dict ([], Dict_Var (v, (i, length sort)))) sort));
+      (map_index (fn (i, _) =>
+        Dict ([], Dict_Var { var = v, index = i, length = length sort })) sort));
     fun print_term is_pseudo_fun some_thm vars fxy (IConst const) =
           print_app is_pseudo_fun some_thm vars fxy (const, [])
       | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
@@ -398,12 +399,13 @@
           brackify BR ((str o deresolve_inst) inst ::
             (if is_pseudo_fun (Class_Instance inst) then [str "()"]
             else map_filter (print_dicts is_pseudo_fun BR) dss))
-      | print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
-          str (if k = 1 then "_" ^ Name.enforce_case true v
-            else "_" ^ Name.enforce_case true v ^ string_of_int (i+1))
+      | print_plain_dict is_pseudo_fun fxy (Dict_Var { var, index, length }) =
+          str (if length = 1 then "_" ^ Name.enforce_case true var
+            else "_" ^ Name.enforce_case true var ^ string_of_int (index + 1))
     and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
     val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
-      (map_index (fn (i, _) => Dict ([], Dict_Var (v, (i, length sort)))) sort));
+      (map_index (fn (i, _) =>
+        Dict ([], Dict_Var { var = v, index = i, length = length sort })) sort));
     fun print_term is_pseudo_fun some_thm vars fxy (IConst const) =
           print_app is_pseudo_fun some_thm vars fxy (const, [])
       | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
--- a/src/Tools/Code/code_preproc.ML	Wed Mar 09 17:16:08 2016 +0000
+++ b/src/Tools/Code/code_preproc.ML	Wed Mar 09 17:22:43 2016 +0000
@@ -476,7 +476,7 @@
 fun dicts_of ctxt (proj_sort, algebra) (T, sort) =
   let
     val thy = Proof_Context.theory_of ctxt;
-    fun class_relation (x, _) _ = x;
+    fun class_relation _ (x, _) _ = x;
     fun type_constructor (tyco, _) xs class =
       inst_params thy tyco (Sorts.complete_sort algebra [class])
         @ (maps o maps) fst xs;
--- a/src/Tools/Code/code_thingol.ML	Wed Mar 09 17:16:08 2016 +0000
+++ b/src/Tools/Code/code_thingol.ML	Wed Mar 09 17:22:43 2016 +0000
@@ -19,7 +19,7 @@
       Dict of (class * class) list * plain_dict
   and plain_dict = 
       Dict_Const of (string * class) * dict list list
-    | Dict_Var of vname * (int * int);
+    | Dict_Var of { var: vname, index: int, length: int };
   datatype itype =
       `%% of string * itype list
     | ITyVar of vname;
@@ -132,7 +132,7 @@
     Dict of (class * class) list * plain_dict
 and plain_dict = 
     Dict_Const of (string * class) * dict list list
-  | Dict_Var of vname * (int * int);
+  | Dict_Var of { var: vname, index: int, length: int };
 
 datatype itype =
     `%% of string * itype list
@@ -482,7 +482,7 @@
         val sort' = proj_sort sort;
       in map_index (fn (n, class) => (Weakening ([], Local (v, (n, sort'))), class)) sort' end;
     val typarg_witnesses = Sorts.of_sort_derivation algebra
-      {class_relation = K (Sorts.classrel_derivation algebra class_relation),
+      {class_relation = fn _ => fn _ => Sorts.classrel_derivation algebra class_relation,
        type_constructor = type_constructor,
        type_variable = type_variable} (ty, proj_sort sort)
       handle Sorts.CLASS_ERROR e => not_wellsorted ctxt permissive some_thm deps ty sort e;
@@ -760,8 +760,8 @@
           ensure_inst ctxt algbr eqngr permissive inst
           ##>> (fold_map o fold_map) mk_dict dss
           #>> (fn (inst, dss) => Dict_Const (inst, dss))
-      | mk_plain_dict (Local (v, (n, sort))) =
-          pair (Dict_Var (unprefix "'" v, (n, length sort)))
+      | mk_plain_dict (Local (v, (index, sort))) =
+          pair (Dict_Var { var = unprefix "'" v, index = index, length = length sort })
   in
     construct_dictionaries ctxt algbr permissive some_thm (ty, sort)
     #-> (fn typarg_witnesses => fold_map mk_dict typarg_witnesses)
--- a/src/Tools/nbe.ML	Wed Mar 09 17:16:08 2016 +0000
+++ b/src/Tools/nbe.ML	Wed Mar 09 17:22:43 2016 +0000
@@ -311,8 +311,8 @@
           assemble_classrels classrels (assemble_plain_dict x)
     and assemble_plain_dict (Dict_Const (inst, dss)) =
           assemble_constapp (Class_Instance inst) dss []
-      | assemble_plain_dict (Dict_Var (v, (n, _))) =
-          nbe_dict v n
+      | assemble_plain_dict (Dict_Var { var, index, ... }) =
+          nbe_dict var index
 
     fun assemble_iterm constapp =
       let