src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML

   val ignore_consts : string list -> theory -> theory
   val keep_functions : string list -> theory -> theory
   val keep_function : theory -> string -> bool
   val processed_specs : theory -> string -> (string * thm list) list option
   val store_processed_specs : (string * (string * thm list) list) -> theory -> theory
-  
+
   val get_specification : Predicate_Compile_Aux.options -> theory -> term -> thm list
   val obtain_specification_graph :
     Predicate_Compile_Aux.options -> theory -> term -> thm list Term_Graph.T
-    
+
   val present_graph : thm list Term_Graph.T -> unit
   val normalize_equation : theory -> thm -> thm
 end;
 
 structure Predicate_Compile_Data : PREDICATE_COMPILE_DATA =

 
 fun defining_term_of_introrule_term t =
   let
     val _ $ u = Logic.strip_imp_concl t
   in fst (strip_comb u) end
-(*  
+(*
   in case pred of
     Const (c, T) => c
     | _ => raise TERM ("defining_const_of_introrule_term failed: Not a constant", [t])
   end
 *)
 val defining_term_of_introrule = defining_term_of_introrule_term o prop_of
 
 fun defining_const_of_introrule th =
-  case defining_term_of_introrule th
-   of Const (c, _) => c
-    | _ => raise TERM ("defining_const_of_introrule failed: Not a constant", [prop_of th])
+  (case defining_term_of_introrule th of
+    Const (c, _) => c
+  | _ => raise TERM ("defining_const_of_introrule failed: Not a constant", [prop_of th]))
 
 (*TODO*)
 fun is_introlike_term _ = true
 
 val is_introlike = is_introlike_term o prop_of
 
 fun check_equation_format_term (t as (Const ("==", _) $ u $ _)) =
-  (case strip_comb u of
-    (Const (_, T), args) =>
-      if (length (binder_types T) = length args) then
-        true
-      else
-        raise TERM ("check_equation_format_term failed: Number of arguments mismatch", [t])
-  | _ => raise TERM ("check_equation_format_term failed: Not a constant", [t]))
+      (case strip_comb u of
+        (Const (_, T), args) =>
+          if (length (binder_types T) = length args) then
+            true
+          else
+            raise TERM ("check_equation_format_term failed: Number of arguments mismatch", [t])
+      | _ => raise TERM ("check_equation_format_term failed: Not a constant", [t]))
   | check_equation_format_term t =
-    raise TERM ("check_equation_format_term failed: Not an equation", [t])
+      raise TERM ("check_equation_format_term failed: Not an equation", [t])
 
 val check_equation_format = check_equation_format_term o prop_of
 
 
 fun defining_term_of_equation_term (Const ("==", _) $ u $ _) = fst (strip_comb u)
   | defining_term_of_equation_term t =
-    raise TERM ("defining_const_of_equation_term failed: Not an equation", [t])
+      raise TERM ("defining_const_of_equation_term failed: Not an equation", [t])
 
 val defining_term_of_equation = defining_term_of_equation_term o prop_of
 
 fun defining_const_of_equation th =
-  case defining_term_of_equation th
-   of Const (c, _) => c
-    | _ => raise TERM ("defining_const_of_equation failed: Not a constant", [prop_of th])
+  (case defining_term_of_equation th of
+    Const (c, _) => c
+  | _ => raise TERM ("defining_const_of_equation failed: Not a constant", [prop_of th]))
 
 
 
 
 (* Normalizing equations *)
 
 fun mk_meta_equation th =
-  case prop_of th of
-    Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => th RS @{thm eq_reflection}
-  | _ => th
+  (case prop_of th of
+    Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _) =>
+      th RS @{thm eq_reflection}
+  | _ => th)
 
 val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp}
 
 fun full_fun_cong_expand th =
   let

 
 fun declare_names s xs ctxt =
   let
     val res = Name.invent_names ctxt s xs
   in (res, fold Name.declare (map fst res) ctxt) end
-  
+
 fun split_all_pairs thy th =
   let
     val ctxt = Proof_Context.init_global thy  (* FIXME proper context!? *)
     val ((_, [th']), _) = Variable.import true [th] ctxt
     val t = prop_of th'
-    val frees = Term.add_frees t [] 
+    val frees = Term.add_frees t []
     val freenames = Term.add_free_names t []
     val nctxt = Name.make_context freenames
     fun mk_tuple_rewrites (x, T) nctxt =
       let
         val Ts = HOLogic.flatten_tupleT T
         val (xTs, nctxt') = declare_names x Ts nctxt
         val paths = HOLogic.flat_tupleT_paths T
       in ((Free (x, T), HOLogic.mk_ptuple paths T (map Free xTs)), nctxt') end
-    val (rewr, _) = fold_map mk_tuple_rewrites frees nctxt 
+    val (rewr, _) = fold_map mk_tuple_rewrites frees nctxt
     val t' = Pattern.rewrite_term thy rewr [] t
     val th'' =
       Goal.prove ctxt (Term.add_free_names t' []) [] t'
         (fn _ => ALLGOALS Skip_Proof.cheat_tac)
     val th''' = Local_Defs.unfold ctxt [@{thm split_conv}, @{thm fst_conv}, @{thm snd_conv}] th''

 fun inline_equations thy th =
   let
     val ctxt = Proof_Context.init_global thy
     val inline_defs = Predicate_Compile_Inline_Defs.get ctxt
     val th' = (Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps inline_defs)) th
-    (*val _ = print_step options 
+    (*val _ = print_step options
       ("Inlining " ^ (Syntax.string_of_term_global thy (prop_of th))
        ^ "with " ^ (commas (map ((Syntax.string_of_term_global thy) o prop_of) inline_defs))
        ^" to " ^ (Syntax.string_of_term_global thy (prop_of th')))*)
   in
     th'

         if is_introlike th andalso defining_const_of_introrule th = fst (dest_Const t) then
           SOME th
         else
           NONE
     fun filter_defs ths = map_filter filtering (map (normalize thy o Thm.transfer thy) ths)
-    val spec = case filter_defs (Predicate_Compile_Alternative_Defs.get ctxt) of
-      [] => (case Spec_Rules.retrieve ctxt t of
-          [] => error ("No specification for " ^ (Syntax.string_of_term_global thy t))
-        | ((_, (_, ths)) :: _) => filter_defs ths)
-    | ths => rev ths
+    val spec =
+      (case filter_defs (Predicate_Compile_Alternative_Defs.get ctxt) of
+        [] =>
+          (case Spec_Rules.retrieve ctxt t of
+            [] => error ("No specification for " ^ Syntax.string_of_term_global thy t)
+          | ((_, (_, ths)) :: _) => filter_defs ths)
+      | ths => rev ths)
     val _ =
       if show_intermediate_results options then
         tracing ("Specification for " ^ (Syntax.string_of_term_global thy t) ^ ":\n" ^
           commas (map (Display.string_of_thm_global thy) spec))
       else ()
   in
     spec
   end
 
 val logic_operator_names =
-  [@{const_name "=="}, 
+  [@{const_name "=="},
    @{const_name "==>"},
    @{const_name Trueprop},
    @{const_name Not},
    @{const_name HOL.eq},
    @{const_name HOL.implies},
    @{const_name All},
-   @{const_name Ex}, 
+   @{const_name Ex},
    @{const_name HOL.conj},
    @{const_name HOL.disj}]
 
-fun special_cases (c, _) = member (op =) [
-  @{const_name Product_Type.Unity},
-  @{const_name False},
-  @{const_name Suc}, @{const_name Nat.zero_nat_inst.zero_nat},
-  @{const_name Nat.one_nat_inst.one_nat},
-  @{const_name Orderings.less}, @{const_name Orderings.less_eq},
-  @{const_name Groups.zero},
-  @{const_name Groups.one},  @{const_name Groups.plus},
-  @{const_name Nat.ord_nat_inst.less_eq_nat},
-  @{const_name Nat.ord_nat_inst.less_nat},
-(* FIXME
-  @{const_name number_nat_inst.number_of_nat},
-*)
-  @{const_name Num.Bit0},
-  @{const_name Num.Bit1},
-  @{const_name Num.One},
-  @{const_name Int.zero_int_inst.zero_int},
-  @{const_name List.filter},
-  @{const_name HOL.If},
-  @{const_name Groups.minus}
-  ] c
+fun special_cases (c, _) =
+  member (op =)
+   [@{const_name Product_Type.Unity},
+    @{const_name False},
+    @{const_name Suc}, @{const_name Nat.zero_nat_inst.zero_nat},
+    @{const_name Nat.one_nat_inst.one_nat},
+    @{const_name Orderings.less}, @{const_name Orderings.less_eq},
+    @{const_name Groups.zero},
+    @{const_name Groups.one},  @{const_name Groups.plus},
+    @{const_name Nat.ord_nat_inst.less_eq_nat},
+    @{const_name Nat.ord_nat_inst.less_nat},
+  (* FIXME
+    @{const_name number_nat_inst.number_of_nat},
+  *)
+    @{const_name Num.Bit0},
+    @{const_name Num.Bit1},
+    @{const_name Num.One},
+    @{const_name Int.zero_int_inst.zero_int},
+    @{const_name List.filter},
+    @{const_name HOL.If},
+    @{const_name Groups.minus}] c
 
 
 fun obtain_specification_graph options thy t =
   let
     val ctxt = Proof_Context.init_global thy

       |> maps (Term_Graph.immediate_succs gr)
       |> subtract eq_cname consts
       |> map (the o Termtab.lookup mapping)
       |> distinct (eq_list eq_cname);
     val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss;
-    
+
     fun namify consts = map string_of_const consts
       |> commas;
     val prgr = map (fn (consts, constss) =>
-      { name = namify consts, ID = namify consts, dir = "", unfold = true,
-        path = "", parents = map namify constss, content = [] }) conn;
-  in Graph_Display.display_graph prgr end;
-
-
-end;
+      {name = namify consts, ID = namify consts, dir = "", unfold = true,
+       path = "", parents = map namify constss, content = [] }) conn
+  in Graph_Display.display_graph prgr end
+
+end