# HG changeset patch
# User wenzelm
# Date 1357661406 -3600
# Node ID ac53370dfae1cbb080e3c5e479905518680dbf23
# Parent  205d12333fdc7035db3516b71197776ca11b33b6
more tolerant set/pred rule declaration to improve "tool compliance", notably for "context assumes";

diff -r 205d12333fdc -r ac53370dfae1 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Tue Jan 08 16:25:22 2013 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Tue Jan 08 17:10:06 2013 +0100
@@ -156,7 +156,7 @@
 (* where s and p are parameters                            *)
 (***********************************************************)
 
-structure PredSetConvData = Generic_Data
+structure Data = Generic_Data
 (
   type T =
     {(* rules for converting predicates to sets *)
@@ -269,13 +269,15 @@
 
 (**** declare rules for converting predicates to sets ****)
 
-fun add ctxt thm (tab as {to_set_simps, to_pred_simps, set_arities, pred_arities}) =
-  case prop_of thm of
+exception Malformed of string;
+
+fun add context thm (tab as {to_set_simps, to_pred_simps, set_arities, pred_arities}) =
+  (case prop_of thm of
     Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, Type (_, [T, _])) $ lhs $ rhs) =>
       (case body_type T of
          @{typ bool} =>
            let
-             val thy = Context.theory_of ctxt;
+             val thy = Context.theory_of context;
              fun factors_of t fs = case strip_abs_body t of
                  Const (@{const_name Set.member}, _) $ u $ S =>
                    if is_Free S orelse is_Var S then
@@ -289,7 +291,7 @@
                  Abs _ => (case strip_abs_body rhs of
                      Const (@{const_name Set.member}, _) $ u $ S =>
                        (strip_comb S, SOME (HOLogic.flat_tuple_paths u))
-                   | _ => error "member symbol on right-hand side expected")
+                   | _ => raise Malformed "member symbol on right-hand side expected")
                | _ => (strip_comb rhs, NONE))
            in
              case (name_type_of h, name_type_of h') of
@@ -308,13 +310,16 @@
                       (T', (map (AList.lookup op = fs) ts', fs'))) set_arities,
                     pred_arities = Symtab.insert_list op = (s,
                       (T, (pfs, fs'))) pred_arities}
-             | _ => error "set / predicate constant expected"
+             | _ => raise Malformed "set / predicate constant expected"
            end
-       | _ => error "equation between predicates expected")
-  | _ => error "equation expected";
+       | _ => raise Malformed "equation between predicates expected")
+  | _ => raise Malformed "equation expected")
+  handle Malformed msg =>
+    (warning ("Ignoring malformed set / predicate conversion rule: " ^ msg ^
+      "\n" ^ Display.string_of_thm (Context.proof_of context) thm); tab);
 
 val pred_set_conv_att = Thm.declaration_attribute
-  (fn thm => fn ctxt => PredSetConvData.map (add ctxt thm) ctxt);
+  (fn thm => fn ctxt => Data.map (add ctxt thm) ctxt);
 
 
 (**** convert theorem in set notation to predicate notation ****)
@@ -340,7 +345,7 @@
   let
     val thy = Context.theory_of ctxt;
     val {to_pred_simps, set_arities, pred_arities, ...} =
-      fold (add ctxt) thms (PredSetConvData.get ctxt);
+      fold (add ctxt) thms (Data.get ctxt);
     val fs = filter (is_Var o fst)
       (infer_arities thy set_arities (NONE, prop_of thm) []);
     (* instantiate each set parameter with {(x, y). p x y} *)
@@ -363,7 +368,7 @@
   let
     val thy = Context.theory_of ctxt;
     val {to_set_simps, pred_arities, ...} =
-      fold (add ctxt) thms (PredSetConvData.get ctxt);
+      fold (add ctxt) thms (Data.get ctxt);
     val fs = filter (is_Var o fst)
       (infer_arities thy pred_arities (NONE, prop_of thm) []);
     (* instantiate each predicate parameter with %x y. (x, y) : s *)
@@ -397,7 +402,7 @@
 fun codegen_preproc thy =
   let
     val {to_pred_simps, set_arities, pred_arities, ...} =
-      PredSetConvData.get (Context.Theory thy);
+      Data.get (Context.Theory thy);
     fun preproc thm =
       if exists_Const (fn (s, _) => case Symtab.lookup set_arities s of
           NONE => false
@@ -422,7 +427,7 @@
   let
     val thy = Proof_Context.theory_of lthy;
     val {set_arities, pred_arities, to_pred_simps, ...} =
-      PredSetConvData.get (Context.Proof lthy);
+      Data.get (Context.Proof lthy);
     fun infer (Abs (_, _, t)) = infer t
       | infer (Const (@{const_name Set.member}, _) $ t $ u) =
           infer_arities thy set_arities (SOME (HOLogic.flat_tuple_paths t), u)