splitting large core file into core_data, mode_inference and predicate_compile_proof
authorbulwahn
Thu Oct 21 19:13:09 2010 +0200 (2010-10-21)
changeset 40052ea46574ca815
parent 40051 b6acda4d1c29
child 40053 3fa49ea76cbb
splitting large core file into core_data, mode_inference and predicate_compile_proof
src/HOL/Predicate_Compile.thy
src/HOL/Tools/Predicate_Compile/core_data.ML
src/HOL/Tools/Predicate_Compile/mode_inference.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
     1.1 --- a/src/HOL/Predicate_Compile.thy	Thu Oct 21 19:13:09 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile.thy	Thu Oct 21 19:13:09 2010 +0200
     1.3 @@ -9,6 +9,9 @@
     1.4  uses
     1.5    "Tools/Predicate_Compile/predicate_compile_aux.ML"
     1.6    "Tools/Predicate_Compile/predicate_compile_compilations.ML"
     1.7 +  "Tools/Predicate_Compile/core_data.ML"
     1.8 +  "Tools/Predicate_Compile/mode_inference.ML"
     1.9 +  "Tools/Predicate_Compile/predicate_compile_proof.ML"
    1.10    "Tools/Predicate_Compile/predicate_compile_core.ML"
    1.11    "Tools/Predicate_Compile/predicate_compile_data.ML"
    1.12    "Tools/Predicate_Compile/predicate_compile_fun.ML"
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Thu Oct 21 19:13:09 2010 +0200
     2.3 @@ -0,0 +1,179 @@
     2.4 +
     2.5 +structure Core_Data =
     2.6 +struct
     2.7 +
     2.8 +open Predicate_Compile_Aux;
     2.9 +
    2.10 +(* book-keeping *)
    2.11 +
    2.12 +datatype predfun_data = PredfunData of {
    2.13 +  definition : thm,
    2.14 +  intro : thm,
    2.15 +  elim : thm,
    2.16 +  neg_intro : thm option
    2.17 +};
    2.18 +
    2.19 +fun rep_predfun_data (PredfunData data) = data;
    2.20 +
    2.21 +fun mk_predfun_data (definition, ((intro, elim), neg_intro)) =
    2.22 +  PredfunData {definition = definition, intro = intro, elim = elim, neg_intro = neg_intro}
    2.23 +
    2.24 +datatype pred_data = PredData of {
    2.25 +  intros : (string option * thm) list,
    2.26 +  elim : thm option,
    2.27 +  preprocessed : bool,
    2.28 +  function_names : (compilation * (mode * string) list) list,
    2.29 +  predfun_data : (mode * predfun_data) list,
    2.30 +  needs_random : mode list
    2.31 +};
    2.32 +
    2.33 +fun rep_pred_data (PredData data) = data;
    2.34 +
    2.35 +fun mk_pred_data (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random))) =
    2.36 +  PredData {intros = intros, elim = elim, preprocessed = preprocessed,
    2.37 +    function_names = function_names, predfun_data = predfun_data, needs_random = needs_random}
    2.38 +
    2.39 +fun map_pred_data f (PredData {intros, elim, preprocessed, function_names, predfun_data, needs_random}) =
    2.40 +  mk_pred_data (f (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random))))
    2.41 +
    2.42 +fun eq_option eq (NONE, NONE) = true
    2.43 +  | eq_option eq (SOME x, SOME y) = eq (x, y)
    2.44 +  | eq_option eq _ = false
    2.45 +
    2.46 +fun eq_pred_data (PredData d1, PredData d2) = 
    2.47 +  eq_list (eq_pair (op =) Thm.eq_thm) (#intros d1, #intros d2) andalso
    2.48 +  eq_option Thm.eq_thm (#elim d1, #elim d2)
    2.49 +
    2.50 +structure PredData = Theory_Data
    2.51 +(
    2.52 +  type T = pred_data Graph.T;
    2.53 +  val empty = Graph.empty;
    2.54 +  val extend = I;
    2.55 +  val merge = Graph.merge eq_pred_data;
    2.56 +);
    2.57 +
    2.58 +(* queries *)
    2.59 +
    2.60 +fun lookup_pred_data ctxt name =
    2.61 +  Option.map rep_pred_data (try (Graph.get_node (PredData.get (ProofContext.theory_of ctxt))) name)
    2.62 +
    2.63 +fun the_pred_data ctxt name = case lookup_pred_data ctxt name
    2.64 + of NONE => error ("No such predicate " ^ quote name)  
    2.65 +  | SOME data => data;
    2.66 +
    2.67 +val is_registered = is_some oo lookup_pred_data
    2.68 +
    2.69 +val all_preds_of = Graph.keys o PredData.get o ProofContext.theory_of
    2.70 +
    2.71 +val intros_of = map snd o #intros oo the_pred_data
    2.72 +
    2.73 +val names_of = map fst o #intros oo the_pred_data
    2.74 +
    2.75 +fun the_elim_of ctxt name = case #elim (the_pred_data ctxt name)
    2.76 + of NONE => error ("No elimination rule for predicate " ^ quote name)
    2.77 +  | SOME thm => thm
    2.78 +  
    2.79 +val has_elim = is_some o #elim oo the_pred_data
    2.80 +
    2.81 +fun function_names_of compilation ctxt name =
    2.82 +  case AList.lookup (op =) (#function_names (the_pred_data ctxt name)) compilation of
    2.83 +    NONE => error ("No " ^ string_of_compilation compilation
    2.84 +      ^ " functions defined for predicate " ^ quote name)
    2.85 +  | SOME fun_names => fun_names
    2.86 +
    2.87 +fun function_name_of compilation ctxt name mode =
    2.88 +  case AList.lookup eq_mode
    2.89 +    (function_names_of compilation ctxt name) mode of
    2.90 +    NONE => error ("No " ^ string_of_compilation compilation
    2.91 +      ^ " function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ quote name)
    2.92 +  | SOME function_name => function_name
    2.93 +
    2.94 +fun modes_of compilation ctxt name = map fst (function_names_of compilation ctxt name)
    2.95 +
    2.96 +fun all_modes_of compilation ctxt =
    2.97 +  map_filter (fn name => Option.map (pair name) (try (modes_of compilation ctxt) name))
    2.98 +    (all_preds_of ctxt)
    2.99 +
   2.100 +val all_random_modes_of = all_modes_of Random
   2.101 +
   2.102 +fun defined_functions compilation ctxt name = case lookup_pred_data ctxt name of
   2.103 +    NONE => false
   2.104 +  | SOME data => AList.defined (op =) (#function_names data) compilation
   2.105 +
   2.106 +fun needs_random ctxt s m =
   2.107 +  member (op =) (#needs_random (the_pred_data ctxt s)) m
   2.108 +
   2.109 +fun lookup_predfun_data ctxt name mode =
   2.110 +  Option.map rep_predfun_data
   2.111 +    (AList.lookup (op =) (#predfun_data (the_pred_data ctxt name)) mode)
   2.112 +
   2.113 +fun the_predfun_data ctxt name mode =
   2.114 +  case lookup_predfun_data ctxt name mode of
   2.115 +    NONE => error ("No function defined for mode " ^ string_of_mode mode ^
   2.116 +      " of predicate " ^ name)
   2.117 +  | SOME data => data;
   2.118 +
   2.119 +val predfun_definition_of = #definition ooo the_predfun_data
   2.120 +
   2.121 +val predfun_intro_of = #intro ooo the_predfun_data
   2.122 +
   2.123 +val predfun_elim_of = #elim ooo the_predfun_data
   2.124 +
   2.125 +val predfun_neg_intro_of = #neg_intro ooo the_predfun_data
   2.126 +
   2.127 +val intros_graph_of =
   2.128 +  Graph.map (K (map snd o #intros o rep_pred_data)) o PredData.get o ProofContext.theory_of
   2.129 +
   2.130 +(* registration of alternative function names *)
   2.131 +
   2.132 +structure Alt_Compilations_Data = Theory_Data
   2.133 +(
   2.134 +  type T = (mode * (compilation_funs -> typ -> term)) list Symtab.table;
   2.135 +  val empty = Symtab.empty;
   2.136 +  val extend = I;
   2.137 +  fun merge data : T = Symtab.merge (K true) data;
   2.138 +);
   2.139 +
   2.140 +fun alternative_compilation_of_global thy pred_name mode =
   2.141 +  AList.lookup eq_mode (Symtab.lookup_list (Alt_Compilations_Data.get thy) pred_name) mode
   2.142 +
   2.143 +fun alternative_compilation_of ctxt pred_name mode =
   2.144 +  AList.lookup eq_mode
   2.145 +    (Symtab.lookup_list (Alt_Compilations_Data.get (ProofContext.theory_of ctxt)) pred_name) mode
   2.146 +
   2.147 +fun force_modes_and_compilations pred_name compilations =
   2.148 +  let
   2.149 +    (* thm refl is a dummy thm *)
   2.150 +    val modes = map fst compilations
   2.151 +    val (needs_random, non_random_modes) = pairself (map fst)
   2.152 +      (List.partition (fn (m, (fun_name, random)) => random) compilations)
   2.153 +    val non_random_dummys = map (rpair "dummy") non_random_modes
   2.154 +    val all_dummys = map (rpair "dummy") modes
   2.155 +    val dummy_function_names = map (rpair all_dummys) Predicate_Compile_Aux.random_compilations
   2.156 +      @ map (rpair non_random_dummys) Predicate_Compile_Aux.non_random_compilations
   2.157 +    val alt_compilations = map (apsnd fst) compilations
   2.158 +  in
   2.159 +    PredData.map (Graph.new_node
   2.160 +      (pred_name, mk_pred_data ((([], SOME @{thm refl}), true), (dummy_function_names, ([], needs_random)))))
   2.161 +    #> Alt_Compilations_Data.map (Symtab.insert (K false) (pred_name, alt_compilations))
   2.162 +  end
   2.163 +
   2.164 +fun functional_compilation fun_name mode compfuns T =
   2.165 +  let
   2.166 +    val (inpTs, outpTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE))
   2.167 +      mode (binder_types T)
   2.168 +    val bs = map (pair "x") inpTs
   2.169 +    val bounds = map Bound (rev (0 upto (length bs) - 1))
   2.170 +    val f = Const (fun_name, inpTs ---> HOLogic.mk_tupleT outpTs)
   2.171 +  in list_abs (bs, mk_single compfuns (list_comb (f, bounds))) end
   2.172 +
   2.173 +fun register_alternative_function pred_name mode fun_name =
   2.174 +  Alt_Compilations_Data.map (Symtab.insert_list (eq_pair eq_mode (K false))
   2.175 +    (pred_name, (mode, functional_compilation fun_name mode)))
   2.176 +
   2.177 +fun force_modes_and_functions pred_name fun_names =
   2.178 +  force_modes_and_compilations pred_name
   2.179 +    (map (fn (mode, (fun_name, random)) => (mode, (functional_compilation fun_name mode, random)))
   2.180 +    fun_names)
   2.181 +
   2.182 +end;
   2.183 \ No newline at end of file
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/mode_inference.ML	Thu Oct 21 19:13:09 2010 +0200
     3.3 @@ -0,0 +1,643 @@
     3.4 +(*  Title:      HOL/Tools/Predicate_Compile/mode_inference.ML
     3.5 +    Author:     Lukas Bulwahn, TU Muenchen
     3.6 +
     3.7 +Mode inference for the predicate compiler
     3.8 +
     3.9 +*)
    3.10 +
    3.11 +signature MODE_INFERENCE =
    3.12 +sig
    3.13 +  type mode = Predicate_Compile_Aux.mode
    3.14 +  
    3.15 +  (* options *)
    3.16 +  type mode_analysis_options =
    3.17 +  {use_generators : bool,
    3.18 +  reorder_premises : bool,
    3.19 +  infer_pos_and_neg_modes : bool}
    3.20 +  
    3.21 +  (* mode operation *)
    3.22 +  val all_input_of : typ -> mode
    3.23 +  (* mode derivation and operations *)
    3.24 +  datatype mode_derivation = Mode_App of mode_derivation * mode_derivation | Context of mode
    3.25 +    | Mode_Pair of mode_derivation * mode_derivation | Term of mode
    3.26 +
    3.27 +  val head_mode_of : mode_derivation -> mode
    3.28 +  val param_derivations_of : mode_derivation -> mode_derivation list
    3.29 +  val collect_context_modes : mode_derivation -> mode list
    3.30 +  
    3.31 +  type moded_clause = term list * (Predicate_Compile_Aux.indprem * mode_derivation) list
    3.32 +  type 'a pred_mode_table = (string * ((bool * mode) * 'a) list) list
    3.33 + 
    3.34 +  (* mode inference operations *)
    3.35 +  val all_derivations_of :
    3.36 +    Proof.context -> (string * mode list) list -> string list -> term
    3.37 +      -> (mode_derivation * string list) list
    3.38 +  (* TODO: move all_modes creation to infer_modes *) 
    3.39 +  val infer_modes : 
    3.40 +    mode_analysis_options -> Predicate_Compile_Aux.options ->
    3.41 +     (string -> mode list) * (string -> mode list)
    3.42 +       * (string -> mode -> bool) -> Proof.context -> (string * typ) list ->
    3.43 +      (string * mode list) list ->
    3.44 +      string list -> (string * (Term.term list * Predicate_Compile_Aux.indprem list) list) list ->
    3.45 +      ((moded_clause list pred_mode_table * (string * mode list) list) * string list)
    3.46 +  
    3.47 +  (* mode and term operations -- to be moved to Predicate_Compile_Aux *) 
    3.48 +  val collect_non_invertible_subterms :
    3.49 +    Proof.context -> term -> string list * term list ->  (term * (string list * term list))
    3.50 +  val is_all_input : mode -> bool
    3.51 +  val term_vs : term -> string list
    3.52 +  val terms_vs : term list -> string list
    3.53 +  
    3.54 +end;
    3.55 +
    3.56 +structure Mode_Inference : MODE_INFERENCE =
    3.57 +struct
    3.58 +
    3.59 +open Predicate_Compile_Aux;
    3.60 +open Core_Data;
    3.61 +
    3.62 +(* derivation trees for modes of premises *)
    3.63 +
    3.64 +datatype mode_derivation = Mode_App of mode_derivation * mode_derivation | Context of mode
    3.65 +  | Mode_Pair of mode_derivation * mode_derivation | Term of mode
    3.66 +
    3.67 +fun string_of_derivation (Mode_App (m1, m2)) =
    3.68 +  "App (" ^ string_of_derivation m1 ^ ", " ^ string_of_derivation m2 ^ ")"
    3.69 +  | string_of_derivation (Mode_Pair (m1, m2)) =
    3.70 +  "Pair (" ^ string_of_derivation m1 ^ ", " ^ string_of_derivation m2 ^ ")"
    3.71 +  | string_of_derivation (Term m) = "Term (" ^ string_of_mode m ^ ")"
    3.72 +  | string_of_derivation (Context m) = "Context (" ^ string_of_mode m ^ ")"
    3.73 +
    3.74 +fun strip_mode_derivation deriv =
    3.75 +  let
    3.76 +    fun strip (Mode_App (deriv1, deriv2)) ds = strip deriv1 (deriv2 :: ds)
    3.77 +      | strip deriv ds = (deriv, ds)
    3.78 +  in
    3.79 +    strip deriv []
    3.80 +  end
    3.81 +
    3.82 +fun mode_of (Context m) = m
    3.83 +  | mode_of (Term m) = m
    3.84 +  | mode_of (Mode_App (d1, d2)) =
    3.85 +    (case mode_of d1 of Fun (m, m') =>
    3.86 +        (if eq_mode (m, mode_of d2) then m' else raise Fail "mode_of: derivation has mismatching modes")
    3.87 +      | _ => raise Fail "mode_of: derivation has a non-functional mode")
    3.88 +  | mode_of (Mode_Pair (d1, d2)) =
    3.89 +    Pair (mode_of d1, mode_of d2)
    3.90 +
    3.91 +fun head_mode_of deriv = mode_of (fst (strip_mode_derivation deriv))
    3.92 +
    3.93 +fun param_derivations_of deriv =
    3.94 +  let
    3.95 +    val (_, argument_derivs) = strip_mode_derivation deriv
    3.96 +    fun param_derivation (Mode_Pair (m1, m2)) =
    3.97 +        param_derivation m1 @ param_derivation m2
    3.98 +      | param_derivation (Term _) = []
    3.99 +      | param_derivation m = [m]
   3.100 +  in
   3.101 +    maps param_derivation argument_derivs
   3.102 +  end
   3.103 +
   3.104 +fun collect_context_modes (Mode_App (m1, m2)) =
   3.105 +      collect_context_modes m1 @ collect_context_modes m2
   3.106 +  | collect_context_modes (Mode_Pair (m1, m2)) =
   3.107 +      collect_context_modes m1 @ collect_context_modes m2
   3.108 +  | collect_context_modes (Context m) = [m]
   3.109 +  | collect_context_modes (Term _) = []
   3.110 +
   3.111 +type moded_clause = term list * (Predicate_Compile_Aux.indprem * mode_derivation) list
   3.112 +type 'a pred_mode_table = (string * ((bool * mode) * 'a) list) list
   3.113 +
   3.114 +
   3.115 +(** string_of functions **)
   3.116 +
   3.117 +fun string_of_prem ctxt (Prem t) =
   3.118 +    (Syntax.string_of_term ctxt t) ^ "(premise)"
   3.119 +  | string_of_prem ctxt (Negprem t) =
   3.120 +    (Syntax.string_of_term ctxt (HOLogic.mk_not t)) ^ "(negative premise)"
   3.121 +  | string_of_prem ctxt (Sidecond t) =
   3.122 +    (Syntax.string_of_term ctxt t) ^ "(sidecondition)"
   3.123 +  | string_of_prem ctxt _ = raise Fail "string_of_prem: unexpected input"
   3.124 +
   3.125 +fun string_of_clause ctxt pred (ts, prems) =
   3.126 +  (space_implode " --> "
   3.127 +  (map (string_of_prem ctxt) prems)) ^ " --> " ^ pred ^ " "
   3.128 +   ^ (space_implode " " (map (Syntax.string_of_term ctxt) ts))
   3.129 +
   3.130 +type mode_analysis_options =
   3.131 +  {use_generators : bool,
   3.132 +  reorder_premises : bool,
   3.133 +  infer_pos_and_neg_modes : bool}
   3.134 +
   3.135 +fun is_constrt thy =
   3.136 +  let
   3.137 +    val cnstrs = flat (maps
   3.138 +      (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
   3.139 +      (Symtab.dest (Datatype.get_all thy)));
   3.140 +    fun check t = (case strip_comb t of
   3.141 +        (Free _, []) => true
   3.142 +      | (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of
   3.143 +            (SOME (i, Tname), Type (Tname', _)) =>
   3.144 +              length ts = i andalso Tname = Tname' andalso forall check ts
   3.145 +          | _ => false)
   3.146 +      | _ => false)
   3.147 +  in check end;
   3.148 +
   3.149 +(*** check if a type is an equality type (i.e. doesn't contain fun)
   3.150 +  FIXME this is only an approximation ***)
   3.151 +fun is_eqT (Type (s, Ts)) = s <> "fun" andalso forall is_eqT Ts
   3.152 +  | is_eqT _ = true;
   3.153 +
   3.154 +fun term_vs tm = fold_aterms (fn Free (x, T) => cons x | _ => I) tm [];
   3.155 +val terms_vs = distinct (op =) o maps term_vs;
   3.156 +
   3.157 +(** collect all Frees in a term (with duplicates!) **)
   3.158 +fun term_vTs tm =
   3.159 +  fold_aterms (fn Free xT => cons xT | _ => I) tm [];
   3.160 +
   3.161 +fun subsets i j =
   3.162 +  if i <= j then
   3.163 +    let
   3.164 +      fun merge xs [] = xs
   3.165 +        | merge [] ys = ys
   3.166 +        | merge (x::xs) (y::ys) = if length x >= length y then x::merge xs (y::ys)
   3.167 +            else y::merge (x::xs) ys;
   3.168 +      val is = subsets (i+1) j
   3.169 +    in merge (map (fn ks => i::ks) is) is end
   3.170 +  else [[]];
   3.171 +
   3.172 +fun print_failed_mode options thy modes p (pol, m) rs is =
   3.173 +  if show_mode_inference options then
   3.174 +    let
   3.175 +      val _ = tracing ("Clauses " ^ commas (map (fn i => string_of_int (i + 1)) is) ^ " of " ^
   3.176 +        p ^ " violates mode " ^ string_of_mode m)
   3.177 +    in () end
   3.178 +  else ()
   3.179 +
   3.180 +fun error_of p (pol, m) is =
   3.181 +  "  Clauses " ^ commas (map (fn i => string_of_int (i + 1)) is) ^ " of " ^
   3.182 +        p ^ " violates mode " ^ string_of_mode m
   3.183 +
   3.184 +fun is_all_input mode =
   3.185 +  let
   3.186 +    fun is_all_input' (Fun _) = true
   3.187 +      | is_all_input' (Pair (m1, m2)) = is_all_input' m1 andalso is_all_input' m2
   3.188 +      | is_all_input' Input = true
   3.189 +      | is_all_input' Output = false
   3.190 +  in
   3.191 +    forall is_all_input' (strip_fun_mode mode)
   3.192 +  end
   3.193 +
   3.194 +fun all_input_of T =
   3.195 +  let
   3.196 +    val (Ts, U) = strip_type T
   3.197 +    fun input_of (Type (@{type_name Product_Type.prod}, [T1, T2])) = Pair (input_of T1, input_of T2)
   3.198 +      | input_of _ = Input
   3.199 +  in
   3.200 +    if U = HOLogic.boolT then
   3.201 +      fold_rev (curry Fun) (map input_of Ts) Bool
   3.202 +    else
   3.203 +      raise Fail "all_input_of: not a predicate"
   3.204 +  end
   3.205 +
   3.206 +fun find_least ord xs =
   3.207 +  let
   3.208 +    fun find' x y = (case y of NONE => SOME x | SOME y' => if ord (x, y') = LESS then SOME x else y) 
   3.209 +  in
   3.210 +    fold find' xs NONE
   3.211 +  end
   3.212 +  
   3.213 +fun term_vs tm = fold_aterms (fn Free (x, T) => cons x | _ => I) tm [];
   3.214 +val terms_vs = distinct (op =) o maps term_vs;
   3.215 +
   3.216 +fun input_mode T =
   3.217 +  let
   3.218 +    val (Ts, U) = strip_type T
   3.219 +  in
   3.220 +    fold_rev (curry Fun) (map (K Input) Ts) Input
   3.221 +  end
   3.222 +
   3.223 +fun output_mode T =
   3.224 +  let
   3.225 +    val (Ts, U) = strip_type T
   3.226 +  in
   3.227 +    fold_rev (curry Fun) (map (K Output) Ts) Output
   3.228 +  end
   3.229 +
   3.230 +fun is_invertible_function ctxt (Const (f, _)) = is_constr ctxt f
   3.231 +  | is_invertible_function ctxt _ = false
   3.232 +
   3.233 +fun non_invertible_subterms ctxt (t as Free _) = []
   3.234 +  | non_invertible_subterms ctxt t = 
   3.235 +  let
   3.236 +    val (f, args) = strip_comb t
   3.237 +  in
   3.238 +    if is_invertible_function ctxt f then
   3.239 +      maps (non_invertible_subterms ctxt) args
   3.240 +    else
   3.241 +      [t]
   3.242 +  end
   3.243 +
   3.244 +fun collect_non_invertible_subterms ctxt (f as Free _) (names, eqs) = (f, (names, eqs))
   3.245 +  | collect_non_invertible_subterms ctxt t (names, eqs) =
   3.246 +    case (strip_comb t) of (f, args) =>
   3.247 +      if is_invertible_function ctxt f then
   3.248 +          let
   3.249 +            val (args', (names', eqs')) =
   3.250 +              fold_map (collect_non_invertible_subterms ctxt) args (names, eqs)
   3.251 +          in
   3.252 +            (list_comb (f, args'), (names', eqs'))
   3.253 +          end
   3.254 +        else
   3.255 +          let
   3.256 +            val s = Name.variant names "x"
   3.257 +            val v = Free (s, fastype_of t)
   3.258 +          in
   3.259 +            (v, (s :: names, HOLogic.mk_eq (v, t) :: eqs))
   3.260 +          end
   3.261 +(*
   3.262 +  if is_constrt thy t then (t, (names, eqs)) else
   3.263 +    let
   3.264 +      val s = Name.variant names "x"
   3.265 +      val v = Free (s, fastype_of t)
   3.266 +    in (v, (s::names, HOLogic.mk_eq (v, t)::eqs)) end;
   3.267 +*)
   3.268 +
   3.269 +fun is_possible_output ctxt vs t =
   3.270 +  forall
   3.271 +    (fn t => is_eqT (fastype_of t) andalso forall (member (op =) vs) (term_vs t))
   3.272 +      (non_invertible_subterms ctxt t)
   3.273 +  andalso
   3.274 +    (forall (is_eqT o snd)
   3.275 +      (inter (fn ((f', _), f) => f = f') vs (Term.add_frees t [])))
   3.276 +
   3.277 +fun vars_of_destructable_term ctxt (Free (x, _)) = [x]
   3.278 +  | vars_of_destructable_term ctxt t =
   3.279 +  let
   3.280 +    val (f, args) = strip_comb t
   3.281 +  in
   3.282 +    if is_invertible_function ctxt f then
   3.283 +      maps (vars_of_destructable_term ctxt) args
   3.284 +    else
   3.285 +      []
   3.286 +  end
   3.287 +
   3.288 +fun is_constructable vs t = forall (member (op =) vs) (term_vs t)
   3.289 +
   3.290 +fun missing_vars vs t = subtract (op =) vs (term_vs t)
   3.291 +
   3.292 +fun output_terms (Const (@{const_name Pair}, _) $ t1 $ t2, Mode_Pair (d1, d2)) =
   3.293 +    output_terms (t1, d1)  @ output_terms (t2, d2)
   3.294 +  | output_terms (t1 $ t2, Mode_App (d1, d2)) =
   3.295 +    output_terms (t1, d1)  @ output_terms (t2, d2)
   3.296 +  | output_terms (t, Term Output) = [t]
   3.297 +  | output_terms _ = []
   3.298 +
   3.299 +fun lookup_mode modes (Const (s, T)) =
   3.300 +   (case (AList.lookup (op =) modes s) of
   3.301 +      SOME ms => SOME (map (fn m => (Context m, [])) ms)
   3.302 +    | NONE => NONE)
   3.303 +  | lookup_mode modes (Free (x, _)) =
   3.304 +    (case (AList.lookup (op =) modes x) of
   3.305 +      SOME ms => SOME (map (fn m => (Context m , [])) ms)
   3.306 +    | NONE => NONE)
   3.307 +
   3.308 +fun derivations_of (ctxt : Proof.context) modes vs (Const (@{const_name Pair}, _) $ t1 $ t2) (Pair (m1, m2)) =
   3.309 +    map_product
   3.310 +      (fn (m1, mvars1) => fn (m2, mvars2) => (Mode_Pair (m1, m2), union (op =) mvars1 mvars2))
   3.311 +        (derivations_of ctxt modes vs t1 m1) (derivations_of ctxt modes vs t2 m2)
   3.312 +  | derivations_of ctxt modes vs t (m as Fun _) =
   3.313 +    (*let
   3.314 +      val (p, args) = strip_comb t
   3.315 +    in
   3.316 +      (case lookup_mode modes p of
   3.317 +        SOME ms => map_filter (fn (Context m, []) => let
   3.318 +          val ms = strip_fun_mode m
   3.319 +          val (argms, restms) = chop (length args) ms
   3.320 +          val m' = fold_rev (curry Fun) restms Bool
   3.321 +        in
   3.322 +          if forall (fn m => eq_mode (Input, m)) argms andalso eq_mode (m', mode) then
   3.323 +            SOME (fold (curry Mode_App) (map Term argms) (Context m), missing_vars vs t)
   3.324 +          else NONE
   3.325 +        end) ms
   3.326 +      | NONE => (if is_all_input mode then [(Context mode, [])] else []))
   3.327 +    end*)
   3.328 +    (case try (all_derivations_of ctxt modes vs) t  of
   3.329 +      SOME derivs =>
   3.330 +        filter (fn (d, mvars) => eq_mode (mode_of d, m) andalso null (output_terms (t, d))) derivs
   3.331 +    | NONE => (if is_all_input m then [(Context m, [])] else []))
   3.332 +  | derivations_of ctxt modes vs t m =
   3.333 +    if eq_mode (m, Input) then
   3.334 +      [(Term Input, missing_vars vs t)]
   3.335 +    else if eq_mode (m, Output) then
   3.336 +      (if is_possible_output ctxt vs t then [(Term Output, [])] else [])
   3.337 +    else []
   3.338 +and all_derivations_of ctxt modes vs (Const (@{const_name Pair}, _) $ t1 $ t2) =
   3.339 +  let
   3.340 +    val derivs1 = all_derivations_of ctxt modes vs t1
   3.341 +    val derivs2 = all_derivations_of ctxt modes vs t2
   3.342 +  in
   3.343 +    map_product
   3.344 +      (fn (m1, mvars1) => fn (m2, mvars2) => (Mode_Pair (m1, m2), union (op =) mvars1 mvars2))
   3.345 +        derivs1 derivs2
   3.346 +  end
   3.347 +  | all_derivations_of ctxt modes vs (t1 $ t2) =
   3.348 +  let
   3.349 +    val derivs1 = all_derivations_of ctxt modes vs t1
   3.350 +  in
   3.351 +    maps (fn (d1, mvars1) =>
   3.352 +      case mode_of d1 of
   3.353 +        Fun (m', _) => map (fn (d2, mvars2) =>
   3.354 +          (Mode_App (d1, d2), union (op =) mvars1 mvars2)) (derivations_of ctxt modes vs t2 m')
   3.355 +        | _ => raise Fail "all_derivations_of: derivation has an unexpected non-functional mode") derivs1
   3.356 +  end
   3.357 +  | all_derivations_of _ modes vs (Const (s, T)) = the (lookup_mode modes (Const (s, T)))
   3.358 +  | all_derivations_of _ modes vs (Free (x, T)) = the (lookup_mode modes (Free (x, T)))
   3.359 +  | all_derivations_of _ modes vs _ = raise Fail "all_derivations_of: unexpected term"
   3.360 +
   3.361 +fun rev_option_ord ord (NONE, NONE) = EQUAL
   3.362 +  | rev_option_ord ord (NONE, SOME _) = GREATER
   3.363 +  | rev_option_ord ord (SOME _, NONE) = LESS
   3.364 +  | rev_option_ord ord (SOME x, SOME y) = ord (x, y)
   3.365 +
   3.366 +fun random_mode_in_deriv modes t deriv =
   3.367 +  case try dest_Const (fst (strip_comb t)) of
   3.368 +    SOME (s, _) =>
   3.369 +      (case AList.lookup (op =) modes s of
   3.370 +        SOME ms =>
   3.371 +          (case AList.lookup (op =) (map (fn ((p, m), r) => (m, r)) ms) (head_mode_of deriv) of
   3.372 +            SOME r => r
   3.373 +          | NONE => false)
   3.374 +      | NONE => false)
   3.375 +  | NONE => false
   3.376 +
   3.377 +fun number_of_output_positions mode =
   3.378 +  let
   3.379 +    val args = strip_fun_mode mode
   3.380 +    fun contains_output (Fun _) = false
   3.381 +      | contains_output Input = false
   3.382 +      | contains_output Output = true
   3.383 +      | contains_output (Pair (m1, m2)) = contains_output m1 orelse contains_output m2
   3.384 +  in
   3.385 +    length (filter contains_output args)
   3.386 +  end
   3.387 +
   3.388 +fun lex_ord ord1 ord2 (x, x') =
   3.389 +  case ord1 (x, x') of
   3.390 +    EQUAL => ord2 (x, x')
   3.391 +  | ord => ord
   3.392 +
   3.393 +fun lexl_ord [] (x, x') = EQUAL
   3.394 +  | lexl_ord (ord :: ords') (x, x') =
   3.395 +    case ord (x, x') of
   3.396 +      EQUAL => lexl_ord ords' (x, x')
   3.397 +    | ord => ord
   3.398 +
   3.399 +fun deriv_ord' ctxt pol pred modes t1 t2 ((deriv1, mvars1), (deriv2, mvars2)) =
   3.400 +  let
   3.401 +    (* prefer functional modes if it is a function *)
   3.402 +    fun fun_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
   3.403 +      let
   3.404 +        fun is_functional t mode =
   3.405 +          case try (fst o dest_Const o fst o strip_comb) t of
   3.406 +            NONE => false
   3.407 +          | SOME c => is_some (alternative_compilation_of ctxt c mode)
   3.408 +      in
   3.409 +        case (is_functional t1 (head_mode_of deriv1), is_functional t2 (head_mode_of deriv2)) of
   3.410 +          (true, true) => EQUAL
   3.411 +        | (true, false) => LESS
   3.412 +        | (false, true) => GREATER
   3.413 +        | (false, false) => EQUAL
   3.414 +      end
   3.415 +    (* prefer modes without requirement for generating random values *)
   3.416 +    fun mvars_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
   3.417 +      int_ord (length mvars1, length mvars2)
   3.418 +    (* prefer non-random modes *)
   3.419 +    fun random_mode_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
   3.420 +      int_ord (if random_mode_in_deriv modes t1 deriv1 then 1 else 0,
   3.421 +               if random_mode_in_deriv modes t2 deriv2 then 1 else 0)
   3.422 +    (* prefer modes with more input and less output *)
   3.423 +    fun output_mode_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
   3.424 +      int_ord (number_of_output_positions (head_mode_of deriv1),
   3.425 +        number_of_output_positions (head_mode_of deriv2))
   3.426 +    (* prefer recursive calls *)
   3.427 +    fun is_rec_premise t =
   3.428 +      case fst (strip_comb t) of Const (c, T) => c = pred | _ => false
   3.429 +    fun recursive_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
   3.430 +      int_ord (if is_rec_premise t1 then 0 else 1,
   3.431 +        if is_rec_premise t2 then 0 else 1)
   3.432 +    val ord = lexl_ord [mvars_ord, fun_ord, random_mode_ord, output_mode_ord, recursive_ord]
   3.433 +  in
   3.434 +    ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2))
   3.435 +  end
   3.436 +
   3.437 +fun deriv_ord ctxt pol pred modes t = deriv_ord' ctxt pol pred modes t t
   3.438 +
   3.439 +fun premise_ord thy pol pred modes ((prem1, a1), (prem2, a2)) =
   3.440 +  rev_option_ord (deriv_ord' thy pol pred modes (dest_indprem prem1) (dest_indprem prem2)) (a1, a2)
   3.441 +
   3.442 +fun print_mode_list modes =
   3.443 +  tracing ("modes: " ^ (commas (map (fn (s, ms) => s ^ ": " ^
   3.444 +    commas (map (fn (m, r) => string_of_mode m ^ (if r then " random " else " not ")) ms)) modes)))
   3.445 +
   3.446 +fun select_mode_prem (mode_analysis_options : mode_analysis_options) (ctxt : Proof.context) pred
   3.447 +  pol (modes, (pos_modes, neg_modes)) vs ps =
   3.448 +  let
   3.449 +    fun choose_mode_of_prem (Prem t) =
   3.450 +          find_least (deriv_ord ctxt pol pred modes t) (all_derivations_of ctxt pos_modes vs t)
   3.451 +      | choose_mode_of_prem (Sidecond t) = SOME (Context Bool, missing_vars vs t)
   3.452 +      | choose_mode_of_prem (Negprem t) = find_least (deriv_ord ctxt (not pol) pred modes t)
   3.453 +          (filter (fn (d, missing_vars) => is_all_input (head_mode_of d))
   3.454 +             (all_derivations_of ctxt neg_modes vs t))
   3.455 +      | choose_mode_of_prem p = raise Fail ("choose_mode_of_prem: unexpected premise " ^ string_of_prem ctxt p)
   3.456 +  in
   3.457 +    if #reorder_premises mode_analysis_options then
   3.458 +      find_least (premise_ord ctxt pol pred modes) (ps ~~ map choose_mode_of_prem ps)
   3.459 +    else
   3.460 +      SOME (hd ps, choose_mode_of_prem (hd ps))
   3.461 +  end
   3.462 +
   3.463 +fun check_mode_clause' (mode_analysis_options : mode_analysis_options) ctxt pred param_vs (modes :
   3.464 +  (string * ((bool * mode) * bool) list) list) ((pol, mode) : bool * mode) (ts, ps) =
   3.465 +  let
   3.466 +    val vTs = distinct (op =) (fold Term.add_frees (map dest_indprem ps) (fold Term.add_frees ts []))
   3.467 +    val modes' = modes @ (param_vs ~~ map (fn x => [((true, x), false), ((false, x), false)]) (ho_arg_modes_of mode))
   3.468 +    fun retrieve_modes_of_pol pol = map (fn (s, ms) =>
   3.469 +      (s, map_filter (fn ((p, m), r) => if p = pol then SOME m else NONE | _ => NONE) ms))
   3.470 +    val (pos_modes', neg_modes') =
   3.471 +      if #infer_pos_and_neg_modes mode_analysis_options then
   3.472 +        (retrieve_modes_of_pol pol modes', retrieve_modes_of_pol (not pol) modes')
   3.473 +      else
   3.474 +        let
   3.475 +          val modes = map (fn (s, ms) => (s, map (fn ((p, m), r) => m) ms)) modes'
   3.476 +        in (modes, modes) end
   3.477 +    val (in_ts, out_ts) = split_mode mode ts
   3.478 +    val in_vs = union (op =) param_vs (maps (vars_of_destructable_term ctxt) in_ts)
   3.479 +    val out_vs = terms_vs out_ts
   3.480 +    fun known_vs_after p vs = (case p of
   3.481 +        Prem t => union (op =) vs (term_vs t)
   3.482 +      | Sidecond t => union (op =) vs (term_vs t)
   3.483 +      | Negprem t => union (op =) vs (term_vs t)
   3.484 +      | _ => raise Fail "unexpected premise")
   3.485 +    fun check_mode_prems acc_ps rnd vs [] = SOME (acc_ps, vs, rnd)
   3.486 +      | check_mode_prems acc_ps rnd vs ps =
   3.487 +        (case
   3.488 +          (select_mode_prem mode_analysis_options ctxt pred pol (modes', (pos_modes', neg_modes')) vs ps) of
   3.489 +          SOME (p, SOME (deriv, [])) => check_mode_prems ((p, deriv) :: acc_ps) rnd
   3.490 +            (known_vs_after p vs) (filter_out (equal p) ps)
   3.491 +        | SOME (p, SOME (deriv, missing_vars)) =>
   3.492 +          if #use_generators mode_analysis_options andalso pol then
   3.493 +            check_mode_prems ((p, deriv) :: (map
   3.494 +              (fn v => (Generator (v, the (AList.lookup (op =) vTs v)), Term Output))
   3.495 +                (distinct (op =) missing_vars))
   3.496 +                @ acc_ps) true (known_vs_after p vs) (filter_out (equal p) ps)
   3.497 +          else NONE
   3.498 +        | SOME (p, NONE) => NONE
   3.499 +        | NONE => NONE)
   3.500 +  in
   3.501 +    case check_mode_prems [] false in_vs ps of
   3.502 +      NONE => NONE
   3.503 +    | SOME (acc_ps, vs, rnd) =>
   3.504 +      if forall (is_constructable vs) (in_ts @ out_ts) then
   3.505 +        SOME (ts, rev acc_ps, rnd)
   3.506 +      else
   3.507 +        if #use_generators mode_analysis_options andalso pol then
   3.508 +          let
   3.509 +             val generators = map
   3.510 +              (fn v => (Generator (v, the (AList.lookup (op =) vTs v)), Term Output))
   3.511 +                (subtract (op =) vs (terms_vs (in_ts @ out_ts)))
   3.512 +          in
   3.513 +            SOME (ts, rev (generators @ acc_ps), true)
   3.514 +          end
   3.515 +        else
   3.516 +          NONE
   3.517 +  end
   3.518 +
   3.519 +datatype result = Success of bool | Error of string
   3.520 +
   3.521 +fun check_modes_pred' mode_analysis_options options thy param_vs clauses modes (p, (ms : ((bool * mode) * bool) list)) =
   3.522 +  let
   3.523 +    fun split xs =
   3.524 +      let
   3.525 +        fun split' [] (ys, zs) = (rev ys, rev zs)
   3.526 +          | split' ((m, Error z) :: xs) (ys, zs) = split' xs (ys, z :: zs)
   3.527 +          | split' (((m : bool * mode), Success rnd) :: xs) (ys, zs) = split' xs ((m, rnd) :: ys, zs)
   3.528 +       in
   3.529 +         split' xs ([], [])
   3.530 +       end
   3.531 +    val rs = these (AList.lookup (op =) clauses p)
   3.532 +    fun check_mode m =
   3.533 +      let
   3.534 +        val res = Output.cond_timeit false "work part of check_mode for one mode" (fn _ => 
   3.535 +          map (check_mode_clause' mode_analysis_options thy p param_vs modes m) rs)
   3.536 +      in
   3.537 +        Output.cond_timeit false "aux part of check_mode for one mode" (fn _ => 
   3.538 +        case find_indices is_none res of
   3.539 +          [] => Success (exists (fn SOME (_, _, true) => true | _ => false) res)
   3.540 +        | is => (print_failed_mode options thy modes p m rs is; Error (error_of p m is)))
   3.541 +      end
   3.542 +    val _ = if show_mode_inference options then
   3.543 +        tracing ("checking " ^ string_of_int (length ms) ^ " modes ...")
   3.544 +      else ()
   3.545 +    val res = Output.cond_timeit false "check_mode" (fn _ => map (fn (m, _) => (m, check_mode m)) ms)
   3.546 +    val (ms', errors) = split res
   3.547 +  in
   3.548 +    ((p, (ms' : ((bool * mode) * bool) list)), errors)
   3.549 +  end;
   3.550 +
   3.551 +fun get_modes_pred' mode_analysis_options thy param_vs clauses modes (p, ms) =
   3.552 +  let
   3.553 +    val rs = these (AList.lookup (op =) clauses p)
   3.554 +  in
   3.555 +    (p, map (fn (m, rnd) =>
   3.556 +      (m, map
   3.557 +        ((fn (ts, ps, rnd) => (ts, ps)) o the o
   3.558 +          check_mode_clause' mode_analysis_options thy p param_vs modes m) rs)) ms)
   3.559 +  end;
   3.560 +
   3.561 +fun fixp f (x : (string * ((bool * mode) * bool) list) list) =
   3.562 +  let val y = f x
   3.563 +  in if x = y then x else fixp f y end;
   3.564 +
   3.565 +fun fixp_with_state f (x : (string * ((bool * mode) * bool) list) list, state) =
   3.566 +  let
   3.567 +    val (y, state') = f (x, state)
   3.568 +  in
   3.569 +    if x = y then (y, state') else fixp_with_state f (y, state')
   3.570 +  end
   3.571 +
   3.572 +fun string_of_ext_mode ((pol, mode), rnd) =
   3.573 +  string_of_mode mode ^ "(" ^ (if pol then "pos" else "neg") ^ ", "
   3.574 +  ^ (if rnd then "rnd" else "nornd") ^ ")"
   3.575 +
   3.576 +fun print_extra_modes options modes =
   3.577 +  if show_mode_inference options then
   3.578 +    tracing ("Modes of inferred predicates: " ^
   3.579 +      cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map string_of_ext_mode ms)) modes))
   3.580 +  else ()
   3.581 +
   3.582 +fun infer_modes mode_analysis_options options (lookup_mode, lookup_neg_mode, needs_random) ctxt
   3.583 +  preds all_modes param_vs clauses =
   3.584 +  let
   3.585 +    fun appair f (x1, x2) (y1, y2) = (f x1 y1, f x2 y2)
   3.586 +    fun add_needs_random s (false, m) = ((false, m), false)
   3.587 +      | add_needs_random s (true, m) = ((true, m), needs_random s m)
   3.588 +    fun add_polarity_and_random_bit s b ms = map (fn m => add_needs_random s (b, m)) ms
   3.589 +    val prednames = map fst preds
   3.590 +    (* extramodes contains all modes of all constants, should we only use the necessary ones
   3.591 +       - what is the impact on performance? *)
   3.592 +    fun predname_of (Prem t) =
   3.593 +        (case try dest_Const (fst (strip_comb t)) of SOME (c, _) => insert (op =) c | NONE => I)
   3.594 +      | predname_of (Negprem t) =
   3.595 +        (case try dest_Const (fst (strip_comb t)) of SOME (c, _) => insert (op =) c | NONE => I)
   3.596 +      | predname_of _ = I
   3.597 +    val relevant_prednames = fold (fn (_, clauses') =>
   3.598 +      fold (fn (_, ps) => fold Term.add_const_names (map dest_indprem ps)) clauses') clauses []
   3.599 +      |> filter_out (fn name => member (op =) prednames name)
   3.600 +    val extra_modes =
   3.601 +      if #infer_pos_and_neg_modes mode_analysis_options then
   3.602 +        let
   3.603 +          val pos_extra_modes =
   3.604 +            map_filter (fn name => Option.map (pair name) (try lookup_mode name))
   3.605 +            relevant_prednames
   3.606 +          val neg_extra_modes =
   3.607 +            map_filter (fn name => Option.map (pair name) (try lookup_neg_mode name))
   3.608 +              relevant_prednames
   3.609 +        in
   3.610 +          map (fn (s, ms) => (s, (add_polarity_and_random_bit s true ms)
   3.611 +                @ add_polarity_and_random_bit s false (the (AList.lookup (op =) neg_extra_modes s))))
   3.612 +            pos_extra_modes
   3.613 +        end
   3.614 +      else
   3.615 +        map (fn (s, ms) => (s, (add_polarity_and_random_bit s true ms)))
   3.616 +          (map_filter (fn name => Option.map (pair name) (try lookup_mode name))
   3.617 +            relevant_prednames)
   3.618 +    val _ = print_extra_modes options extra_modes
   3.619 +    val start_modes =
   3.620 +      if #infer_pos_and_neg_modes mode_analysis_options then
   3.621 +        map (fn (s, ms) => (s, map (fn m => ((true, m), false)) ms @
   3.622 +          (map (fn m => ((false, m), false)) ms))) all_modes
   3.623 +      else
   3.624 +        map (fn (s, ms) => (s, map (fn m => ((true, m), false)) ms)) all_modes
   3.625 +    fun iteration modes = map
   3.626 +      (check_modes_pred' mode_analysis_options options ctxt param_vs clauses
   3.627 +        (modes @ extra_modes)) modes
   3.628 +    val ((modes : (string * ((bool * mode) * bool) list) list), errors) =
   3.629 +      Output.cond_timeit false "Fixpount computation of mode analysis" (fn () =>
   3.630 +      if show_invalid_clauses options then
   3.631 +        fixp_with_state (fn (modes, errors) =>
   3.632 +          let
   3.633 +            val (modes', new_errors) = split_list (iteration modes)
   3.634 +          in (modes', errors @ flat new_errors) end) (start_modes, [])
   3.635 +        else
   3.636 +          (fixp (fn modes => map fst (iteration modes)) start_modes, []))
   3.637 +    val moded_clauses = map (get_modes_pred' mode_analysis_options ctxt param_vs clauses
   3.638 +      (modes @ extra_modes)) modes
   3.639 +    val need_random = fold (fn (s, ms) => if member (op =) (map fst preds) s then
   3.640 +      cons (s, (map_filter (fn ((true, m), true) => SOME m | _ => NONE) ms)) else I)
   3.641 +      modes []
   3.642 +  in
   3.643 +    ((moded_clauses, need_random), errors)
   3.644 +  end;
   3.645 +
   3.646 +end;
   3.647 \ No newline at end of file
     4.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Oct 21 19:13:09 2010 +0200
     4.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Oct 21 19:13:09 2010 +0200
     4.3 @@ -150,6 +150,7 @@
     4.4    val imp_prems_conv : conv -> conv
     4.5    (* simple transformations *)
     4.6    val split_conjuncts_in_assms : Proof.context -> thm -> thm
     4.7 +  val dest_conjunct_prem : thm -> thm list
     4.8    val expand_tuples : theory -> thm -> thm
     4.9    val case_betapply : theory -> term -> term
    4.10    val eta_contract_ho_arguments : theory -> thm -> thm
    4.11 @@ -157,7 +158,7 @@
    4.12    val remove_pointless_clauses : thm -> thm list
    4.13    val peephole_optimisation : theory -> thm -> thm option
    4.14    val define_quickcheck_predicate :
    4.15 -    term -> theory -> (((string * typ) * (string * typ) list) * thm) * theory 
    4.16 +    term -> theory -> (((string * typ) * (string * typ) list) * thm) * theory
    4.17  end;
    4.18  
    4.19  structure Predicate_Compile_Aux : PREDICATE_COMPILE_AUX =
    4.20 @@ -854,7 +855,14 @@
    4.21    in
    4.22      singleton (Variable.export ctxt' ctxt) (split_conjs 1 (Thm.nprems_of fixed_th) fixed_th)
    4.23    end
    4.24 -  
    4.25 +
    4.26 +fun dest_conjunct_prem th =
    4.27 +  case HOLogic.dest_Trueprop (prop_of th) of
    4.28 +    (Const (@{const_name HOL.conj}, _) $ t $ t') =>
    4.29 +      dest_conjunct_prem (th RS @{thm conjunct1})
    4.30 +        @ dest_conjunct_prem (th RS @{thm conjunct2})
    4.31 +    | _ => [th]
    4.32 +
    4.33  fun expand_tuples thy intro =
    4.34    let
    4.35      val ctxt = ProofContext.init_global thy
     5.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Oct 21 19:13:09 2010 +0200
     5.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Oct 21 19:13:09 2010 +0200
     5.3 @@ -78,35 +78,16 @@
     5.4    type moded_clause = term list * (Predicate_Compile_Aux.indprem * mode_derivation) list
     5.5    type 'a pred_mode_table = (string * ((bool * mode) * 'a) list) list
     5.6  
     5.7 -  val infer_modes : 
     5.8 -    mode_analysis_options -> options ->
     5.9 -     (string -> Predicate_Compile_Aux.mode list) * (string -> Predicate_Compile_Aux.mode list)
    5.10 -       * (string -> Predicate_Compile_Aux.mode -> bool) -> Proof.context -> (string * typ) list ->
    5.11 -      (string * mode list) list ->
    5.12 -      string list -> (string * (Term.term list * Predicate_Compile_Aux.indprem list) list) list ->
    5.13 -      ((moded_clause list pred_mode_table * (string * mode list) list) * string list)
    5.14 +
    5.15  end;
    5.16  
    5.17  structure Predicate_Compile_Core : PREDICATE_COMPILE_CORE =
    5.18  struct
    5.19  
    5.20  open Predicate_Compile_Aux;
    5.21 -
    5.22 -(** auxiliary **)
    5.23 -
    5.24 -(* debug stuff *)
    5.25 -
    5.26 -fun print_tac options s = 
    5.27 -  if show_proof_trace options then Tactical.print_tac s else Seq.single;
    5.28 -
    5.29 -fun assert b = if not b then raise Fail "Assertion failed" else warning "Assertion holds"
    5.30 -
    5.31 -datatype assertion = Max_number_of_subgoals of int
    5.32 -fun assert_tac (Max_number_of_subgoals i) st =
    5.33 -  if (nprems_of st <= i) then Seq.single st
    5.34 -  else raise Fail ("assert_tac: Numbers of subgoals mismatch at goal state :"
    5.35 -    ^ "\n" ^ Pretty.string_of (Pretty.chunks
    5.36 -      (Goal_Display.pretty_goals_without_context st)));
    5.37 +open Core_Data;
    5.38 +open Mode_Inference;
    5.39 +open Predicate_Compile_Proof;
    5.40  
    5.41  (** fundamentals **)
    5.42  
    5.43 @@ -149,181 +130,12 @@
    5.44  
    5.45  val strip_intro_concl = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o prop_of)
    5.46  
    5.47 -(* derivation trees for modes of premises *)
    5.48 -
    5.49 -datatype mode_derivation = Mode_App of mode_derivation * mode_derivation | Context of mode
    5.50 -  | Mode_Pair of mode_derivation * mode_derivation | Term of mode
    5.51 -
    5.52 -fun string_of_derivation (Mode_App (m1, m2)) =
    5.53 -  "App (" ^ string_of_derivation m1 ^ ", " ^ string_of_derivation m2 ^ ")"
    5.54 -  | string_of_derivation (Mode_Pair (m1, m2)) =
    5.55 -  "Pair (" ^ string_of_derivation m1 ^ ", " ^ string_of_derivation m2 ^ ")"
    5.56 -  | string_of_derivation (Term m) = "Term (" ^ string_of_mode m ^ ")"
    5.57 -  | string_of_derivation (Context m) = "Context (" ^ string_of_mode m ^ ")"
    5.58 -
    5.59 -fun strip_mode_derivation deriv =
    5.60 -  let
    5.61 -    fun strip (Mode_App (deriv1, deriv2)) ds = strip deriv1 (deriv2 :: ds)
    5.62 -      | strip deriv ds = (deriv, ds)
    5.63 -  in
    5.64 -    strip deriv []
    5.65 -  end
    5.66 -
    5.67 -fun mode_of (Context m) = m
    5.68 -  | mode_of (Term m) = m
    5.69 -  | mode_of (Mode_App (d1, d2)) =
    5.70 -    (case mode_of d1 of Fun (m, m') =>
    5.71 -        (if eq_mode (m, mode_of d2) then m' else raise Fail "mode_of: derivation has mismatching modes")
    5.72 -      | _ => raise Fail "mode_of: derivation has a non-functional mode")
    5.73 -  | mode_of (Mode_Pair (d1, d2)) =
    5.74 -    Pair (mode_of d1, mode_of d2)
    5.75 -
    5.76 -fun head_mode_of deriv = mode_of (fst (strip_mode_derivation deriv))
    5.77 -
    5.78 -fun param_derivations_of deriv =
    5.79 -  let
    5.80 -    val (_, argument_derivs) = strip_mode_derivation deriv
    5.81 -    fun param_derivation (Mode_Pair (m1, m2)) =
    5.82 -        param_derivation m1 @ param_derivation m2
    5.83 -      | param_derivation (Term _) = []
    5.84 -      | param_derivation m = [m]
    5.85 -  in
    5.86 -    maps param_derivation argument_derivs
    5.87 -  end
    5.88 -
    5.89 -fun collect_context_modes (Mode_App (m1, m2)) =
    5.90 -      collect_context_modes m1 @ collect_context_modes m2
    5.91 -  | collect_context_modes (Mode_Pair (m1, m2)) =
    5.92 -      collect_context_modes m1 @ collect_context_modes m2
    5.93 -  | collect_context_modes (Context m) = [m]
    5.94 -  | collect_context_modes (Term _) = []
    5.95 -
    5.96  (* representation of inferred clauses with modes *)
    5.97  
    5.98  type moded_clause = term list * (indprem * mode_derivation) list
    5.99  
   5.100  type 'a pred_mode_table = (string * ((bool * mode) * 'a) list) list
   5.101  
   5.102 -(* book-keeping *)
   5.103 -
   5.104 -datatype predfun_data = PredfunData of {
   5.105 -  definition : thm,
   5.106 -  intro : thm,
   5.107 -  elim : thm,
   5.108 -  neg_intro : thm option
   5.109 -};
   5.110 -
   5.111 -fun rep_predfun_data (PredfunData data) = data;
   5.112 -
   5.113 -fun mk_predfun_data (definition, ((intro, elim), neg_intro)) =
   5.114 -  PredfunData {definition = definition, intro = intro, elim = elim, neg_intro = neg_intro}
   5.115 -
   5.116 -datatype pred_data = PredData of {
   5.117 -  intros : (string option * thm) list,
   5.118 -  elim : thm option,
   5.119 -  preprocessed : bool,
   5.120 -  function_names : (compilation * (mode * string) list) list,
   5.121 -  predfun_data : (mode * predfun_data) list,
   5.122 -  needs_random : mode list
   5.123 -};
   5.124 -
   5.125 -fun rep_pred_data (PredData data) = data;
   5.126 -
   5.127 -fun mk_pred_data (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random))) =
   5.128 -  PredData {intros = intros, elim = elim, preprocessed = preprocessed,
   5.129 -    function_names = function_names, predfun_data = predfun_data, needs_random = needs_random}
   5.130 -
   5.131 -fun map_pred_data f (PredData {intros, elim, preprocessed, function_names, predfun_data, needs_random}) =
   5.132 -  mk_pred_data (f (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random))))
   5.133 -
   5.134 -fun eq_option eq (NONE, NONE) = true
   5.135 -  | eq_option eq (SOME x, SOME y) = eq (x, y)
   5.136 -  | eq_option eq _ = false
   5.137 -
   5.138 -fun eq_pred_data (PredData d1, PredData d2) = 
   5.139 -  eq_list (eq_pair (op =) Thm.eq_thm) (#intros d1, #intros d2) andalso
   5.140 -  eq_option Thm.eq_thm (#elim d1, #elim d2)
   5.141 -
   5.142 -structure PredData = Theory_Data
   5.143 -(
   5.144 -  type T = pred_data Graph.T;
   5.145 -  val empty = Graph.empty;
   5.146 -  val extend = I;
   5.147 -  val merge = Graph.merge eq_pred_data;
   5.148 -);
   5.149 -
   5.150 -(* queries *)
   5.151 -
   5.152 -fun lookup_pred_data ctxt name =
   5.153 -  Option.map rep_pred_data (try (Graph.get_node (PredData.get (ProofContext.theory_of ctxt))) name)
   5.154 -
   5.155 -fun the_pred_data ctxt name = case lookup_pred_data ctxt name
   5.156 - of NONE => error ("No such predicate " ^ quote name)  
   5.157 -  | SOME data => data;
   5.158 -
   5.159 -val is_registered = is_some oo lookup_pred_data
   5.160 -
   5.161 -val all_preds_of = Graph.keys o PredData.get o ProofContext.theory_of
   5.162 -
   5.163 -val intros_of = map snd o #intros oo the_pred_data
   5.164 -
   5.165 -val names_of = map fst o #intros oo the_pred_data
   5.166 -
   5.167 -fun the_elim_of ctxt name = case #elim (the_pred_data ctxt name)
   5.168 - of NONE => error ("No elimination rule for predicate " ^ quote name)
   5.169 -  | SOME thm => thm
   5.170 -  
   5.171 -val has_elim = is_some o #elim oo the_pred_data
   5.172 -
   5.173 -fun function_names_of compilation ctxt name =
   5.174 -  case AList.lookup (op =) (#function_names (the_pred_data ctxt name)) compilation of
   5.175 -    NONE => error ("No " ^ string_of_compilation compilation
   5.176 -      ^ " functions defined for predicate " ^ quote name)
   5.177 -  | SOME fun_names => fun_names
   5.178 -
   5.179 -fun function_name_of compilation ctxt name mode =
   5.180 -  case AList.lookup eq_mode
   5.181 -    (function_names_of compilation ctxt name) mode of
   5.182 -    NONE => error ("No " ^ string_of_compilation compilation
   5.183 -      ^ " function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ quote name)
   5.184 -  | SOME function_name => function_name
   5.185 -
   5.186 -fun modes_of compilation ctxt name = map fst (function_names_of compilation ctxt name)
   5.187 -
   5.188 -fun all_modes_of compilation ctxt =
   5.189 -  map_filter (fn name => Option.map (pair name) (try (modes_of compilation ctxt) name))
   5.190 -    (all_preds_of ctxt)
   5.191 -
   5.192 -val all_random_modes_of = all_modes_of Random
   5.193 -
   5.194 -fun defined_functions compilation ctxt name = case lookup_pred_data ctxt name of
   5.195 -    NONE => false
   5.196 -  | SOME data => AList.defined (op =) (#function_names data) compilation
   5.197 -
   5.198 -fun needs_random ctxt s m =
   5.199 -  member (op =) (#needs_random (the_pred_data ctxt s)) m
   5.200 -
   5.201 -fun lookup_predfun_data ctxt name mode =
   5.202 -  Option.map rep_predfun_data
   5.203 -    (AList.lookup (op =) (#predfun_data (the_pred_data ctxt name)) mode)
   5.204 -
   5.205 -fun the_predfun_data ctxt name mode =
   5.206 -  case lookup_predfun_data ctxt name mode of
   5.207 -    NONE => error ("No function defined for mode " ^ string_of_mode mode ^
   5.208 -      " of predicate " ^ name)
   5.209 -  | SOME data => data;
   5.210 -
   5.211 -val predfun_definition_of = #definition ooo the_predfun_data
   5.212 -
   5.213 -val predfun_intro_of = #intro ooo the_predfun_data
   5.214 -
   5.215 -val predfun_elim_of = #elim ooo the_predfun_data
   5.216 -
   5.217 -val predfun_neg_intro_of = #neg_intro ooo the_predfun_data
   5.218 -
   5.219 -val intros_graph_of =
   5.220 -  Graph.map (K (map snd o #intros o rep_pred_data)) o PredData.get o ProofContext.theory_of
   5.221 -
   5.222  (* diagnostic display functions *)
   5.223  
   5.224  fun print_modes options modes =
   5.225 @@ -342,19 +154,6 @@
   5.226      val _ = tracing (cat_lines (map print_pred pred_mode_table))
   5.227    in () end;
   5.228  
   5.229 -fun string_of_prem ctxt (Prem t) =
   5.230 -    (Syntax.string_of_term ctxt t) ^ "(premise)"
   5.231 -  | string_of_prem ctxt (Negprem t) =
   5.232 -    (Syntax.string_of_term ctxt (HOLogic.mk_not t)) ^ "(negative premise)"
   5.233 -  | string_of_prem ctxt (Sidecond t) =
   5.234 -    (Syntax.string_of_term ctxt t) ^ "(sidecondition)"
   5.235 -  | string_of_prem ctxt _ = raise Fail "string_of_prem: unexpected input"
   5.236 -
   5.237 -fun string_of_clause ctxt pred (ts, prems) =
   5.238 -  (space_implode " --> "
   5.239 -  (map (string_of_prem ctxt) prems)) ^ " --> " ^ pred ^ " "
   5.240 -   ^ (space_implode " " (map (Syntax.string_of_term ctxt) ts))
   5.241 -
   5.242  fun print_compiled_terms options ctxt =
   5.243    if show_compilation options then
   5.244      print_pred_mode_table (fn _ => fn _ => Syntax.string_of_term ctxt)
   5.245 @@ -585,13 +384,6 @@
   5.246      val cases = map mk_case intros
   5.247    in Logic.list_implies (assm :: cases, prop) end;
   5.248  
   5.249 -fun dest_conjunct_prem th =
   5.250 -  case HOLogic.dest_Trueprop (prop_of th) of
   5.251 -    (Const (@{const_name HOL.conj}, _) $ t $ t') =>
   5.252 -      dest_conjunct_prem (th RS @{thm conjunct1})
   5.253 -        @ dest_conjunct_prem (th RS @{thm conjunct2})
   5.254 -    | _ => [th]
   5.255 -
   5.256  fun prove_casesrule ctxt (pred, (pre_cases_rule, nparams)) cases_rule =
   5.257    let
   5.258      val thy = ProofContext.theory_of ctxt
   5.259 @@ -755,58 +547,6 @@
   5.260      PredData.map (Graph.map_node name (map_pred_data set))
   5.261    end
   5.262  
   5.263 -(* registration of alternative function names *)
   5.264 -
   5.265 -structure Alt_Compilations_Data = Theory_Data
   5.266 -(
   5.267 -  type T = (mode * (compilation_funs -> typ -> term)) list Symtab.table;
   5.268 -  val empty = Symtab.empty;
   5.269 -  val extend = I;
   5.270 -  fun merge data : T = Symtab.merge (K true) data;
   5.271 -);
   5.272 -
   5.273 -fun alternative_compilation_of_global thy pred_name mode =
   5.274 -  AList.lookup eq_mode (Symtab.lookup_list (Alt_Compilations_Data.get thy) pred_name) mode
   5.275 -
   5.276 -fun alternative_compilation_of ctxt pred_name mode =
   5.277 -  AList.lookup eq_mode
   5.278 -    (Symtab.lookup_list (Alt_Compilations_Data.get (ProofContext.theory_of ctxt)) pred_name) mode
   5.279 -
   5.280 -fun force_modes_and_compilations pred_name compilations =
   5.281 -  let
   5.282 -    (* thm refl is a dummy thm *)
   5.283 -    val modes = map fst compilations
   5.284 -    val (needs_random, non_random_modes) = pairself (map fst)
   5.285 -      (List.partition (fn (m, (fun_name, random)) => random) compilations)
   5.286 -    val non_random_dummys = map (rpair "dummy") non_random_modes
   5.287 -    val all_dummys = map (rpair "dummy") modes
   5.288 -    val dummy_function_names = map (rpair all_dummys) Predicate_Compile_Aux.random_compilations
   5.289 -      @ map (rpair non_random_dummys) Predicate_Compile_Aux.non_random_compilations
   5.290 -    val alt_compilations = map (apsnd fst) compilations
   5.291 -  in
   5.292 -    PredData.map (Graph.new_node
   5.293 -      (pred_name, mk_pred_data ((([], SOME @{thm refl}), true), (dummy_function_names, ([], needs_random)))))
   5.294 -    #> Alt_Compilations_Data.map (Symtab.insert (K false) (pred_name, alt_compilations))
   5.295 -  end
   5.296 -
   5.297 -fun functional_compilation fun_name mode compfuns T =
   5.298 -  let
   5.299 -    val (inpTs, outpTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE))
   5.300 -      mode (binder_types T)
   5.301 -    val bs = map (pair "x") inpTs
   5.302 -    val bounds = map Bound (rev (0 upto (length bs) - 1))
   5.303 -    val f = Const (fun_name, inpTs ---> HOLogic.mk_tupleT outpTs)
   5.304 -  in list_abs (bs, mk_single compfuns (list_comb (f, bounds))) end
   5.305 -
   5.306 -fun register_alternative_function pred_name mode fun_name =
   5.307 -  Alt_Compilations_Data.map (Symtab.insert_list (eq_pair eq_mode (K false))
   5.308 -    (pred_name, (mode, functional_compilation fun_name mode)))
   5.309 -
   5.310 -fun force_modes_and_functions pred_name fun_names =
   5.311 -  force_modes_and_compilations pred_name
   5.312 -    (map (fn (mode, (fun_name, random)) => (mode, (functional_compilation fun_name mode, random)))
   5.313 -    fun_names)
   5.314 -
   5.315  (* compilation modifiers *)
   5.316  
   5.317  structure Comp_Mod =
   5.318 @@ -1133,524 +873,6 @@
   5.319      | Neg_Generator_DSeq => pos_generator_dseq_comp_modifiers
   5.320      | c => comp_modifiers)
   5.321  
   5.322 -(** mode analysis **)
   5.323 -
   5.324 -type mode_analysis_options =
   5.325 -  {use_generators : bool,
   5.326 -  reorder_premises : bool,
   5.327 -  infer_pos_and_neg_modes : bool}
   5.328 -
   5.329 -fun is_constrt thy =
   5.330 -  let
   5.331 -    val cnstrs = flat (maps
   5.332 -      (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
   5.333 -      (Symtab.dest (Datatype.get_all thy)));
   5.334 -    fun check t = (case strip_comb t of
   5.335 -        (Free _, []) => true
   5.336 -      | (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of
   5.337 -            (SOME (i, Tname), Type (Tname', _)) =>
   5.338 -              length ts = i andalso Tname = Tname' andalso forall check ts
   5.339 -          | _ => false)
   5.340 -      | _ => false)
   5.341 -  in check end;
   5.342 -
   5.343 -(*** check if a type is an equality type (i.e. doesn't contain fun)
   5.344 -  FIXME this is only an approximation ***)
   5.345 -fun is_eqT (Type (s, Ts)) = s <> "fun" andalso forall is_eqT Ts
   5.346 -  | is_eqT _ = true;
   5.347 -
   5.348 -fun term_vs tm = fold_aterms (fn Free (x, T) => cons x | _ => I) tm [];
   5.349 -val terms_vs = distinct (op =) o maps term_vs;
   5.350 -
   5.351 -(** collect all Frees in a term (with duplicates!) **)
   5.352 -fun term_vTs tm =
   5.353 -  fold_aterms (fn Free xT => cons xT | _ => I) tm [];
   5.354 -
   5.355 -fun subsets i j =
   5.356 -  if i <= j then
   5.357 -    let
   5.358 -      fun merge xs [] = xs
   5.359 -        | merge [] ys = ys
   5.360 -        | merge (x::xs) (y::ys) = if length x >= length y then x::merge xs (y::ys)
   5.361 -            else y::merge (x::xs) ys;
   5.362 -      val is = subsets (i+1) j
   5.363 -    in merge (map (fn ks => i::ks) is) is end
   5.364 -  else [[]];
   5.365 -
   5.366 -fun print_failed_mode options thy modes p (pol, m) rs is =
   5.367 -  if show_mode_inference options then
   5.368 -    let
   5.369 -      val _ = tracing ("Clauses " ^ commas (map (fn i => string_of_int (i + 1)) is) ^ " of " ^
   5.370 -        p ^ " violates mode " ^ string_of_mode m)
   5.371 -    in () end
   5.372 -  else ()
   5.373 -
   5.374 -fun error_of p (pol, m) is =
   5.375 -  "  Clauses " ^ commas (map (fn i => string_of_int (i + 1)) is) ^ " of " ^
   5.376 -        p ^ " violates mode " ^ string_of_mode m
   5.377 -
   5.378 -fun is_all_input mode =
   5.379 -  let
   5.380 -    fun is_all_input' (Fun _) = true
   5.381 -      | is_all_input' (Pair (m1, m2)) = is_all_input' m1 andalso is_all_input' m2
   5.382 -      | is_all_input' Input = true
   5.383 -      | is_all_input' Output = false
   5.384 -  in
   5.385 -    forall is_all_input' (strip_fun_mode mode)
   5.386 -  end
   5.387 -
   5.388 -fun all_input_of T =
   5.389 -  let
   5.390 -    val (Ts, U) = strip_type T
   5.391 -    fun input_of (Type (@{type_name Product_Type.prod}, [T1, T2])) = Pair (input_of T1, input_of T2)
   5.392 -      | input_of _ = Input
   5.393 -  in
   5.394 -    if U = HOLogic.boolT then
   5.395 -      fold_rev (curry Fun) (map input_of Ts) Bool
   5.396 -    else
   5.397 -      raise Fail "all_input_of: not a predicate"
   5.398 -  end
   5.399 -
   5.400 -fun find_least ord xs =
   5.401 -  let
   5.402 -    fun find' x y = (case y of NONE => SOME x | SOME y' => if ord (x, y') = LESS then SOME x else y) 
   5.403 -  in
   5.404 -    fold find' xs NONE
   5.405 -  end
   5.406 -  
   5.407 -fun term_vs tm = fold_aterms (fn Free (x, T) => cons x | _ => I) tm [];
   5.408 -val terms_vs = distinct (op =) o maps term_vs;
   5.409 -
   5.410 -fun input_mode T =
   5.411 -  let
   5.412 -    val (Ts, U) = strip_type T
   5.413 -  in
   5.414 -    fold_rev (curry Fun) (map (K Input) Ts) Input
   5.415 -  end
   5.416 -
   5.417 -fun output_mode T =
   5.418 -  let
   5.419 -    val (Ts, U) = strip_type T
   5.420 -  in
   5.421 -    fold_rev (curry Fun) (map (K Output) Ts) Output
   5.422 -  end
   5.423 -
   5.424 -fun is_invertible_function ctxt (Const (f, _)) = is_constr ctxt f
   5.425 -  | is_invertible_function ctxt _ = false
   5.426 -
   5.427 -fun non_invertible_subterms ctxt (t as Free _) = []
   5.428 -  | non_invertible_subterms ctxt t = 
   5.429 -  let
   5.430 -    val (f, args) = strip_comb t
   5.431 -  in
   5.432 -    if is_invertible_function ctxt f then
   5.433 -      maps (non_invertible_subterms ctxt) args
   5.434 -    else
   5.435 -      [t]
   5.436 -  end
   5.437 -
   5.438 -fun collect_non_invertible_subterms ctxt (f as Free _) (names, eqs) = (f, (names, eqs))
   5.439 -  | collect_non_invertible_subterms ctxt t (names, eqs) =
   5.440 -    case (strip_comb t) of (f, args) =>
   5.441 -      if is_invertible_function ctxt f then
   5.442 -          let
   5.443 -            val (args', (names', eqs')) =
   5.444 -              fold_map (collect_non_invertible_subterms ctxt) args (names, eqs)
   5.445 -          in
   5.446 -            (list_comb (f, args'), (names', eqs'))
   5.447 -          end
   5.448 -        else
   5.449 -          let
   5.450 -            val s = Name.variant names "x"
   5.451 -            val v = Free (s, fastype_of t)
   5.452 -          in
   5.453 -            (v, (s :: names, HOLogic.mk_eq (v, t) :: eqs))
   5.454 -          end
   5.455 -(*
   5.456 -  if is_constrt thy t then (t, (names, eqs)) else
   5.457 -    let
   5.458 -      val s = Name.variant names "x"
   5.459 -      val v = Free (s, fastype_of t)
   5.460 -    in (v, (s::names, HOLogic.mk_eq (v, t)::eqs)) end;
   5.461 -*)
   5.462 -
   5.463 -fun is_possible_output ctxt vs t =
   5.464 -  forall
   5.465 -    (fn t => is_eqT (fastype_of t) andalso forall (member (op =) vs) (term_vs t))
   5.466 -      (non_invertible_subterms ctxt t)
   5.467 -  andalso
   5.468 -    (forall (is_eqT o snd)
   5.469 -      (inter (fn ((f', _), f) => f = f') vs (Term.add_frees t [])))
   5.470 -
   5.471 -fun vars_of_destructable_term ctxt (Free (x, _)) = [x]
   5.472 -  | vars_of_destructable_term ctxt t =
   5.473 -  let
   5.474 -    val (f, args) = strip_comb t
   5.475 -  in
   5.476 -    if is_invertible_function ctxt f then
   5.477 -      maps (vars_of_destructable_term ctxt) args
   5.478 -    else
   5.479 -      []
   5.480 -  end
   5.481 -
   5.482 -fun is_constructable vs t = forall (member (op =) vs) (term_vs t)
   5.483 -
   5.484 -fun missing_vars vs t = subtract (op =) vs (term_vs t)
   5.485 -
   5.486 -fun output_terms (Const (@{const_name Pair}, _) $ t1 $ t2, Mode_Pair (d1, d2)) =
   5.487 -    output_terms (t1, d1)  @ output_terms (t2, d2)
   5.488 -  | output_terms (t1 $ t2, Mode_App (d1, d2)) =
   5.489 -    output_terms (t1, d1)  @ output_terms (t2, d2)
   5.490 -  | output_terms (t, Term Output) = [t]
   5.491 -  | output_terms _ = []
   5.492 -
   5.493 -fun lookup_mode modes (Const (s, T)) =
   5.494 -   (case (AList.lookup (op =) modes s) of
   5.495 -      SOME ms => SOME (map (fn m => (Context m, [])) ms)
   5.496 -    | NONE => NONE)
   5.497 -  | lookup_mode modes (Free (x, _)) =
   5.498 -    (case (AList.lookup (op =) modes x) of
   5.499 -      SOME ms => SOME (map (fn m => (Context m , [])) ms)
   5.500 -    | NONE => NONE)
   5.501 -
   5.502 -fun derivations_of (ctxt : Proof.context) modes vs (Const (@{const_name Pair}, _) $ t1 $ t2) (Pair (m1, m2)) =
   5.503 -    map_product
   5.504 -      (fn (m1, mvars1) => fn (m2, mvars2) => (Mode_Pair (m1, m2), union (op =) mvars1 mvars2))
   5.505 -        (derivations_of ctxt modes vs t1 m1) (derivations_of ctxt modes vs t2 m2)
   5.506 -  | derivations_of ctxt modes vs t (m as Fun _) =
   5.507 -    (*let
   5.508 -      val (p, args) = strip_comb t
   5.509 -    in
   5.510 -      (case lookup_mode modes p of
   5.511 -        SOME ms => map_filter (fn (Context m, []) => let
   5.512 -          val ms = strip_fun_mode m
   5.513 -          val (argms, restms) = chop (length args) ms
   5.514 -          val m' = fold_rev (curry Fun) restms Bool
   5.515 -        in
   5.516 -          if forall (fn m => eq_mode (Input, m)) argms andalso eq_mode (m', mode) then
   5.517 -            SOME (fold (curry Mode_App) (map Term argms) (Context m), missing_vars vs t)
   5.518 -          else NONE
   5.519 -        end) ms
   5.520 -      | NONE => (if is_all_input mode then [(Context mode, [])] else []))
   5.521 -    end*)
   5.522 -    (case try (all_derivations_of ctxt modes vs) t  of
   5.523 -      SOME derivs =>
   5.524 -        filter (fn (d, mvars) => eq_mode (mode_of d, m) andalso null (output_terms (t, d))) derivs
   5.525 -    | NONE => (if is_all_input m then [(Context m, [])] else []))
   5.526 -  | derivations_of ctxt modes vs t m =
   5.527 -    if eq_mode (m, Input) then
   5.528 -      [(Term Input, missing_vars vs t)]
   5.529 -    else if eq_mode (m, Output) then
   5.530 -      (if is_possible_output ctxt vs t then [(Term Output, [])] else [])
   5.531 -    else []
   5.532 -and all_derivations_of ctxt modes vs (Const (@{const_name Pair}, _) $ t1 $ t2) =
   5.533 -  let
   5.534 -    val derivs1 = all_derivations_of ctxt modes vs t1
   5.535 -    val derivs2 = all_derivations_of ctxt modes vs t2
   5.536 -  in
   5.537 -    map_product
   5.538 -      (fn (m1, mvars1) => fn (m2, mvars2) => (Mode_Pair (m1, m2), union (op =) mvars1 mvars2))
   5.539 -        derivs1 derivs2
   5.540 -  end
   5.541 -  | all_derivations_of ctxt modes vs (t1 $ t2) =
   5.542 -  let
   5.543 -    val derivs1 = all_derivations_of ctxt modes vs t1
   5.544 -  in
   5.545 -    maps (fn (d1, mvars1) =>
   5.546 -      case mode_of d1 of
   5.547 -        Fun (m', _) => map (fn (d2, mvars2) =>
   5.548 -          (Mode_App (d1, d2), union (op =) mvars1 mvars2)) (derivations_of ctxt modes vs t2 m')
   5.549 -        | _ => raise Fail "all_derivations_of: derivation has an unexpected non-functional mode") derivs1
   5.550 -  end
   5.551 -  | all_derivations_of _ modes vs (Const (s, T)) = the (lookup_mode modes (Const (s, T)))
   5.552 -  | all_derivations_of _ modes vs (Free (x, T)) = the (lookup_mode modes (Free (x, T)))
   5.553 -  | all_derivations_of _ modes vs _ = raise Fail "all_derivations_of: unexpected term"
   5.554 -
   5.555 -fun rev_option_ord ord (NONE, NONE) = EQUAL
   5.556 -  | rev_option_ord ord (NONE, SOME _) = GREATER
   5.557 -  | rev_option_ord ord (SOME _, NONE) = LESS
   5.558 -  | rev_option_ord ord (SOME x, SOME y) = ord (x, y)
   5.559 -
   5.560 -fun random_mode_in_deriv modes t deriv =
   5.561 -  case try dest_Const (fst (strip_comb t)) of
   5.562 -    SOME (s, _) =>
   5.563 -      (case AList.lookup (op =) modes s of
   5.564 -        SOME ms =>
   5.565 -          (case AList.lookup (op =) (map (fn ((p, m), r) => (m, r)) ms) (head_mode_of deriv) of
   5.566 -            SOME r => r
   5.567 -          | NONE => false)
   5.568 -      | NONE => false)
   5.569 -  | NONE => false
   5.570 -
   5.571 -fun number_of_output_positions mode =
   5.572 -  let
   5.573 -    val args = strip_fun_mode mode
   5.574 -    fun contains_output (Fun _) = false
   5.575 -      | contains_output Input = false
   5.576 -      | contains_output Output = true
   5.577 -      | contains_output (Pair (m1, m2)) = contains_output m1 orelse contains_output m2
   5.578 -  in
   5.579 -    length (filter contains_output args)
   5.580 -  end
   5.581 -
   5.582 -fun lex_ord ord1 ord2 (x, x') =
   5.583 -  case ord1 (x, x') of
   5.584 -    EQUAL => ord2 (x, x')
   5.585 -  | ord => ord
   5.586 -
   5.587 -fun lexl_ord [] (x, x') = EQUAL
   5.588 -  | lexl_ord (ord :: ords') (x, x') =
   5.589 -    case ord (x, x') of
   5.590 -      EQUAL => lexl_ord ords' (x, x')
   5.591 -    | ord => ord
   5.592 -
   5.593 -fun deriv_ord' ctxt pol pred modes t1 t2 ((deriv1, mvars1), (deriv2, mvars2)) =
   5.594 -  let
   5.595 -    (* prefer functional modes if it is a function *)
   5.596 -    fun fun_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
   5.597 -      let
   5.598 -        fun is_functional t mode =
   5.599 -          case try (fst o dest_Const o fst o strip_comb) t of
   5.600 -            NONE => false
   5.601 -          | SOME c => is_some (alternative_compilation_of ctxt c mode)
   5.602 -      in
   5.603 -        case (is_functional t1 (head_mode_of deriv1), is_functional t2 (head_mode_of deriv2)) of
   5.604 -          (true, true) => EQUAL
   5.605 -        | (true, false) => LESS
   5.606 -        | (false, true) => GREATER
   5.607 -        | (false, false) => EQUAL
   5.608 -      end
   5.609 -    (* prefer modes without requirement for generating random values *)
   5.610 -    fun mvars_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
   5.611 -      int_ord (length mvars1, length mvars2)
   5.612 -    (* prefer non-random modes *)
   5.613 -    fun random_mode_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
   5.614 -      int_ord (if random_mode_in_deriv modes t1 deriv1 then 1 else 0,
   5.615 -               if random_mode_in_deriv modes t2 deriv2 then 1 else 0)
   5.616 -    (* prefer modes with more input and less output *)
   5.617 -    fun output_mode_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
   5.618 -      int_ord (number_of_output_positions (head_mode_of deriv1),
   5.619 -        number_of_output_positions (head_mode_of deriv2))
   5.620 -    (* prefer recursive calls *)
   5.621 -    fun is_rec_premise t =
   5.622 -      case fst (strip_comb t) of Const (c, T) => c = pred | _ => false
   5.623 -    fun recursive_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
   5.624 -      int_ord (if is_rec_premise t1 then 0 else 1,
   5.625 -        if is_rec_premise t2 then 0 else 1)
   5.626 -    val ord = lexl_ord [mvars_ord, fun_ord, random_mode_ord, output_mode_ord, recursive_ord]
   5.627 -  in
   5.628 -    ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2))
   5.629 -  end
   5.630 -
   5.631 -fun deriv_ord ctxt pol pred modes t = deriv_ord' ctxt pol pred modes t t
   5.632 -
   5.633 -fun premise_ord thy pol pred modes ((prem1, a1), (prem2, a2)) =
   5.634 -  rev_option_ord (deriv_ord' thy pol pred modes (dest_indprem prem1) (dest_indprem prem2)) (a1, a2)
   5.635 -
   5.636 -fun print_mode_list modes =
   5.637 -  tracing ("modes: " ^ (commas (map (fn (s, ms) => s ^ ": " ^
   5.638 -    commas (map (fn (m, r) => string_of_mode m ^ (if r then " random " else " not ")) ms)) modes)))
   5.639 -
   5.640 -fun select_mode_prem (mode_analysis_options : mode_analysis_options) (ctxt : Proof.context) pred
   5.641 -  pol (modes, (pos_modes, neg_modes)) vs ps =
   5.642 -  let
   5.643 -    fun choose_mode_of_prem (Prem t) =
   5.644 -          find_least (deriv_ord ctxt pol pred modes t) (all_derivations_of ctxt pos_modes vs t)
   5.645 -      | choose_mode_of_prem (Sidecond t) = SOME (Context Bool, missing_vars vs t)
   5.646 -      | choose_mode_of_prem (Negprem t) = find_least (deriv_ord ctxt (not pol) pred modes t)
   5.647 -          (filter (fn (d, missing_vars) => is_all_input (head_mode_of d))
   5.648 -             (all_derivations_of ctxt neg_modes vs t))
   5.649 -      | choose_mode_of_prem p = raise Fail ("choose_mode_of_prem: unexpected premise " ^ string_of_prem ctxt p)
   5.650 -  in
   5.651 -    if #reorder_premises mode_analysis_options then
   5.652 -      find_least (premise_ord ctxt pol pred modes) (ps ~~ map choose_mode_of_prem ps)
   5.653 -    else
   5.654 -      SOME (hd ps, choose_mode_of_prem (hd ps))
   5.655 -  end
   5.656 -
   5.657 -fun check_mode_clause' (mode_analysis_options : mode_analysis_options) ctxt pred param_vs (modes :
   5.658 -  (string * ((bool * mode) * bool) list) list) ((pol, mode) : bool * mode) (ts, ps) =
   5.659 -  let
   5.660 -    val vTs = distinct (op =) (fold Term.add_frees (map dest_indprem ps) (fold Term.add_frees ts []))
   5.661 -    val modes' = modes @ (param_vs ~~ map (fn x => [((true, x), false), ((false, x), false)]) (ho_arg_modes_of mode))
   5.662 -    fun retrieve_modes_of_pol pol = map (fn (s, ms) =>
   5.663 -      (s, map_filter (fn ((p, m), r) => if p = pol then SOME m else NONE | _ => NONE) ms))
   5.664 -    val (pos_modes', neg_modes') =
   5.665 -      if #infer_pos_and_neg_modes mode_analysis_options then
   5.666 -        (retrieve_modes_of_pol pol modes', retrieve_modes_of_pol (not pol) modes')
   5.667 -      else
   5.668 -        let
   5.669 -          val modes = map (fn (s, ms) => (s, map (fn ((p, m), r) => m) ms)) modes'
   5.670 -        in (modes, modes) end
   5.671 -    val (in_ts, out_ts) = split_mode mode ts
   5.672 -    val in_vs = union (op =) param_vs (maps (vars_of_destructable_term ctxt) in_ts)
   5.673 -    val out_vs = terms_vs out_ts
   5.674 -    fun known_vs_after p vs = (case p of
   5.675 -        Prem t => union (op =) vs (term_vs t)
   5.676 -      | Sidecond t => union (op =) vs (term_vs t)
   5.677 -      | Negprem t => union (op =) vs (term_vs t)
   5.678 -      | _ => raise Fail "unexpected premise")
   5.679 -    fun check_mode_prems acc_ps rnd vs [] = SOME (acc_ps, vs, rnd)
   5.680 -      | check_mode_prems acc_ps rnd vs ps =
   5.681 -        (case
   5.682 -          (select_mode_prem mode_analysis_options ctxt pred pol (modes', (pos_modes', neg_modes')) vs ps) of
   5.683 -          SOME (p, SOME (deriv, [])) => check_mode_prems ((p, deriv) :: acc_ps) rnd
   5.684 -            (known_vs_after p vs) (filter_out (equal p) ps)
   5.685 -        | SOME (p, SOME (deriv, missing_vars)) =>
   5.686 -          if #use_generators mode_analysis_options andalso pol then
   5.687 -            check_mode_prems ((p, deriv) :: (map
   5.688 -              (fn v => (Generator (v, the (AList.lookup (op =) vTs v)), Term Output))
   5.689 -                (distinct (op =) missing_vars))
   5.690 -                @ acc_ps) true (known_vs_after p vs) (filter_out (equal p) ps)
   5.691 -          else NONE
   5.692 -        | SOME (p, NONE) => NONE
   5.693 -        | NONE => NONE)
   5.694 -  in
   5.695 -    case check_mode_prems [] false in_vs ps of
   5.696 -      NONE => NONE
   5.697 -    | SOME (acc_ps, vs, rnd) =>
   5.698 -      if forall (is_constructable vs) (in_ts @ out_ts) then
   5.699 -        SOME (ts, rev acc_ps, rnd)
   5.700 -      else
   5.701 -        if #use_generators mode_analysis_options andalso pol then
   5.702 -          let
   5.703 -             val generators = map
   5.704 -              (fn v => (Generator (v, the (AList.lookup (op =) vTs v)), Term Output))
   5.705 -                (subtract (op =) vs (terms_vs (in_ts @ out_ts)))
   5.706 -          in
   5.707 -            SOME (ts, rev (generators @ acc_ps), true)
   5.708 -          end
   5.709 -        else
   5.710 -          NONE
   5.711 -  end
   5.712 -
   5.713 -datatype result = Success of bool | Error of string
   5.714 -
   5.715 -fun check_modes_pred' mode_analysis_options options thy param_vs clauses modes (p, (ms : ((bool * mode) * bool) list)) =
   5.716 -  let
   5.717 -    fun split xs =
   5.718 -      let
   5.719 -        fun split' [] (ys, zs) = (rev ys, rev zs)
   5.720 -          | split' ((m, Error z) :: xs) (ys, zs) = split' xs (ys, z :: zs)
   5.721 -          | split' (((m : bool * mode), Success rnd) :: xs) (ys, zs) = split' xs ((m, rnd) :: ys, zs)
   5.722 -       in
   5.723 -         split' xs ([], [])
   5.724 -       end
   5.725 -    val rs = these (AList.lookup (op =) clauses p)
   5.726 -    fun check_mode m =
   5.727 -      let
   5.728 -        val res = Output.cond_timeit false "work part of check_mode for one mode" (fn _ => 
   5.729 -          map (check_mode_clause' mode_analysis_options thy p param_vs modes m) rs)
   5.730 -      in
   5.731 -        Output.cond_timeit false "aux part of check_mode for one mode" (fn _ => 
   5.732 -        case find_indices is_none res of
   5.733 -          [] => Success (exists (fn SOME (_, _, true) => true | _ => false) res)
   5.734 -        | is => (print_failed_mode options thy modes p m rs is; Error (error_of p m is)))
   5.735 -      end
   5.736 -    val _ = if show_mode_inference options then
   5.737 -        tracing ("checking " ^ string_of_int (length ms) ^ " modes ...")
   5.738 -      else ()
   5.739 -    val res = Output.cond_timeit false "check_mode" (fn _ => map (fn (m, _) => (m, check_mode m)) ms)
   5.740 -    val (ms', errors) = split res
   5.741 -  in
   5.742 -    ((p, (ms' : ((bool * mode) * bool) list)), errors)
   5.743 -  end;
   5.744 -
   5.745 -fun get_modes_pred' mode_analysis_options thy param_vs clauses modes (p, ms) =
   5.746 -  let
   5.747 -    val rs = these (AList.lookup (op =) clauses p)
   5.748 -  in
   5.749 -    (p, map (fn (m, rnd) =>
   5.750 -      (m, map
   5.751 -        ((fn (ts, ps, rnd) => (ts, ps)) o the o
   5.752 -          check_mode_clause' mode_analysis_options thy p param_vs modes m) rs)) ms)
   5.753 -  end;
   5.754 -
   5.755 -fun fixp f (x : (string * ((bool * mode) * bool) list) list) =
   5.756 -  let val y = f x
   5.757 -  in if x = y then x else fixp f y end;
   5.758 -
   5.759 -fun fixp_with_state f (x : (string * ((bool * mode) * bool) list) list, state) =
   5.760 -  let
   5.761 -    val (y, state') = f (x, state)
   5.762 -  in
   5.763 -    if x = y then (y, state') else fixp_with_state f (y, state')
   5.764 -  end
   5.765 -
   5.766 -fun string_of_ext_mode ((pol, mode), rnd) =
   5.767 -  string_of_mode mode ^ "(" ^ (if pol then "pos" else "neg") ^ ", "
   5.768 -  ^ (if rnd then "rnd" else "nornd") ^ ")"
   5.769 -
   5.770 -fun print_extra_modes options modes =
   5.771 -  if show_mode_inference options then
   5.772 -    tracing ("Modes of inferred predicates: " ^
   5.773 -      cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map string_of_ext_mode ms)) modes))
   5.774 -  else ()
   5.775 -
   5.776 -fun infer_modes mode_analysis_options options (lookup_mode, lookup_neg_mode, needs_random) ctxt
   5.777 -  preds all_modes param_vs clauses =
   5.778 -  let
   5.779 -    fun appair f (x1, x2) (y1, y2) = (f x1 y1, f x2 y2)
   5.780 -    fun add_needs_random s (false, m) = ((false, m), false)
   5.781 -      | add_needs_random s (true, m) = ((true, m), needs_random s m)
   5.782 -    fun add_polarity_and_random_bit s b ms = map (fn m => add_needs_random s (b, m)) ms
   5.783 -    val prednames = map fst preds
   5.784 -    (* extramodes contains all modes of all constants, should we only use the necessary ones
   5.785 -       - what is the impact on performance? *)
   5.786 -    fun predname_of (Prem t) =
   5.787 -        (case try dest_Const (fst (strip_comb t)) of SOME (c, _) => insert (op =) c | NONE => I)
   5.788 -      | predname_of (Negprem t) =
   5.789 -        (case try dest_Const (fst (strip_comb t)) of SOME (c, _) => insert (op =) c | NONE => I)
   5.790 -      | predname_of _ = I
   5.791 -    val relevant_prednames = fold (fn (_, clauses') =>
   5.792 -      fold (fn (_, ps) => fold Term.add_const_names (map dest_indprem ps)) clauses') clauses []
   5.793 -      |> filter_out (fn name => member (op =) prednames name)
   5.794 -    val extra_modes =
   5.795 -      if #infer_pos_and_neg_modes mode_analysis_options then
   5.796 -        let
   5.797 -          val pos_extra_modes =
   5.798 -            map_filter (fn name => Option.map (pair name) (try lookup_mode name))
   5.799 -            relevant_prednames
   5.800 -          val neg_extra_modes =
   5.801 -            map_filter (fn name => Option.map (pair name) (try lookup_neg_mode name))
   5.802 -              relevant_prednames
   5.803 -        in
   5.804 -          map (fn (s, ms) => (s, (add_polarity_and_random_bit s true ms)
   5.805 -                @ add_polarity_and_random_bit s false (the (AList.lookup (op =) neg_extra_modes s))))
   5.806 -            pos_extra_modes
   5.807 -        end
   5.808 -      else
   5.809 -        map (fn (s, ms) => (s, (add_polarity_and_random_bit s true ms)))
   5.810 -          (map_filter (fn name => Option.map (pair name) (try lookup_mode name))
   5.811 -            relevant_prednames)
   5.812 -    val _ = print_extra_modes options extra_modes
   5.813 -    val start_modes =
   5.814 -      if #infer_pos_and_neg_modes mode_analysis_options then
   5.815 -        map (fn (s, ms) => (s, map (fn m => ((true, m), false)) ms @
   5.816 -          (map (fn m => ((false, m), false)) ms))) all_modes
   5.817 -      else
   5.818 -        map (fn (s, ms) => (s, map (fn m => ((true, m), false)) ms)) all_modes
   5.819 -    fun iteration modes = map
   5.820 -      (check_modes_pred' mode_analysis_options options ctxt param_vs clauses
   5.821 -        (modes @ extra_modes)) modes
   5.822 -    val ((modes : (string * ((bool * mode) * bool) list) list), errors) =
   5.823 -      Output.cond_timeit false "Fixpount computation of mode analysis" (fn () =>
   5.824 -      if show_invalid_clauses options then
   5.825 -        fixp_with_state (fn (modes, errors) =>
   5.826 -          let
   5.827 -            val (modes', new_errors) = split_list (iteration modes)
   5.828 -          in (modes', errors @ flat new_errors) end) (start_modes, [])
   5.829 -        else
   5.830 -          (fixp (fn modes => map fst (iteration modes)) start_modes, []))
   5.831 -    val moded_clauses = map (get_modes_pred' mode_analysis_options ctxt param_vs clauses
   5.832 -      (modes @ extra_modes)) modes
   5.833 -    val need_random = fold (fn (s, ms) => if member (op =) (map fst preds) s then
   5.834 -      cons (s, (map_filter (fn ((true, m), true) => SOME m | _ => NONE) ms)) else I)
   5.835 -      modes []
   5.836 -  in
   5.837 -    ((moded_clauses, need_random), errors)
   5.838 -  end;
   5.839 -
   5.840  (* term construction *)
   5.841  
   5.842  fun mk_v (names, vs) s T = (case AList.lookup (op =) vs s of
   5.843 @@ -2088,11 +1310,6 @@
   5.844        (HOLogic.mk_eq (list_comb (fun_const, in_ts @ additional_arguments), compilation))
   5.845    end;
   5.846  
   5.847 -(** special setup for simpset **)
   5.848 -val HOL_basic_ss' = HOL_basic_ss addsimps (@{thms HOL.simp_thms} @ [@{thm Pair_eq}])
   5.849 -  setSolver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
   5.850 -  setSolver (mk_solver "True_solver" (fn _ => rtac @{thm TrueI}))
   5.851 -
   5.852  (* Definition of executable functions and their intro and elim rules *)
   5.853  
   5.854  fun print_arities arities = tracing ("Arities:\n" ^
   5.855 @@ -2256,483 +1473,6 @@
   5.856      |> fold create_definition modes
   5.857    end;
   5.858  
   5.859 -(* Proving equivalence of term *)
   5.860 -
   5.861 -fun is_Type (Type _) = true
   5.862 -  | is_Type _ = false
   5.863 -
   5.864 -(* returns true if t is an application of an datatype constructor *)
   5.865 -(* which then consequently would be splitted *)
   5.866 -(* else false *)
   5.867 -fun is_constructor thy t =
   5.868 -  if (is_Type (fastype_of t)) then
   5.869 -    (case Datatype.get_info thy ((fst o dest_Type o fastype_of) t) of
   5.870 -      NONE => false
   5.871 -    | SOME info => (let
   5.872 -      val constr_consts = maps (fn (_, (_, _, constrs)) => map fst constrs) (#descr info)
   5.873 -      val (c, _) = strip_comb t
   5.874 -      in (case c of
   5.875 -        Const (name, _) => member (op =) constr_consts name
   5.876 -        | _ => false) end))
   5.877 -  else false
   5.878 -
   5.879 -(* MAJOR FIXME:  prove_params should be simple
   5.880 - - different form of introrule for parameters ? *)
   5.881 -
   5.882 -fun prove_param options ctxt nargs t deriv =
   5.883 -  let
   5.884 -    val  (f, args) = strip_comb (Envir.eta_contract t)
   5.885 -    val mode = head_mode_of deriv
   5.886 -    val param_derivations = param_derivations_of deriv
   5.887 -    val ho_args = ho_args_of mode args
   5.888 -    val f_tac = case f of
   5.889 -      Const (name, T) => simp_tac (HOL_basic_ss addsimps 
   5.890 -         [@{thm eval_pred}, predfun_definition_of ctxt name mode,
   5.891 -         @{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
   5.892 -         @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
   5.893 -    | Free _ =>
   5.894 -      Subgoal.FOCUS_PREMS (fn {context = ctxt, params = params, prems, asms, concl, schematics} =>
   5.895 -        let
   5.896 -          val prems' = maps dest_conjunct_prem (take nargs prems)
   5.897 -        in
   5.898 -          MetaSimplifier.rewrite_goal_tac
   5.899 -            (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
   5.900 -        end) ctxt 1
   5.901 -    | Abs _ => raise Fail "prove_param: No valid parameter term"
   5.902 -  in
   5.903 -    REPEAT_DETERM (rtac @{thm ext} 1)
   5.904 -    THEN print_tac options "prove_param"
   5.905 -    THEN f_tac 
   5.906 -    THEN print_tac options "after prove_param"
   5.907 -    THEN (REPEAT_DETERM (atac 1))
   5.908 -    THEN (EVERY (map2 (prove_param options ctxt nargs) ho_args param_derivations))
   5.909 -    THEN REPEAT_DETERM (rtac @{thm refl} 1)
   5.910 -  end
   5.911 -
   5.912 -fun prove_expr options ctxt nargs (premposition : int) (t, deriv) =
   5.913 -  case strip_comb t of
   5.914 -    (Const (name, T), args) =>
   5.915 -      let
   5.916 -        val mode = head_mode_of deriv
   5.917 -        val introrule = predfun_intro_of ctxt name mode
   5.918 -        val param_derivations = param_derivations_of deriv
   5.919 -        val ho_args = ho_args_of mode args
   5.920 -      in
   5.921 -        print_tac options "before intro rule:"
   5.922 -        THEN rtac introrule 1
   5.923 -        THEN print_tac options "after intro rule"
   5.924 -        (* for the right assumption in first position *)
   5.925 -        THEN rotate_tac premposition 1
   5.926 -        THEN atac 1
   5.927 -        THEN print_tac options "parameter goal"
   5.928 -        (* work with parameter arguments *)
   5.929 -        THEN (EVERY (map2 (prove_param options ctxt nargs) ho_args param_derivations))
   5.930 -        THEN (REPEAT_DETERM (atac 1))
   5.931 -      end
   5.932 -  | (Free _, _) =>
   5.933 -    print_tac options "proving parameter call.."
   5.934 -    THEN Subgoal.FOCUS_PREMS (fn {context = ctxt, params, prems, asms, concl, schematics} =>
   5.935 -        let
   5.936 -          val param_prem = nth prems premposition
   5.937 -          val (param, _) = strip_comb (HOLogic.dest_Trueprop (prop_of param_prem))
   5.938 -          val prems' = maps dest_conjunct_prem (take nargs prems)
   5.939 -          fun param_rewrite prem =
   5.940 -            param = snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of prem)))
   5.941 -          val SOME rew_eq = find_first param_rewrite prems'
   5.942 -          val param_prem' = MetaSimplifier.rewrite_rule
   5.943 -            (map (fn th => th RS @{thm eq_reflection})
   5.944 -              [rew_eq RS @{thm sym}, @{thm split_beta}, @{thm fst_conv}, @{thm snd_conv}])
   5.945 -            param_prem
   5.946 -        in
   5.947 -          rtac param_prem' 1
   5.948 -        end) ctxt 1
   5.949 -    THEN print_tac options "after prove parameter call"
   5.950 -
   5.951 -fun SOLVED tac st = FILTER (fn st' => nprems_of st' = nprems_of st - 1) tac st;
   5.952 -
   5.953 -fun SOLVEDALL tac st = FILTER (fn st' => nprems_of st' = 0) tac st
   5.954 -
   5.955 -fun check_format ctxt st =
   5.956 -  let
   5.957 -    val concl' = Logic.strip_assums_concl (hd (prems_of st))
   5.958 -    val concl = HOLogic.dest_Trueprop concl'
   5.959 -    val expr = fst (strip_comb (fst (PredicateCompFuns.dest_Eval concl)))
   5.960 -    fun valid_expr (Const (@{const_name Predicate.bind}, _)) = true
   5.961 -      | valid_expr (Const (@{const_name Predicate.single}, _)) = true
   5.962 -      | valid_expr _ = false
   5.963 -  in
   5.964 -    if valid_expr expr then
   5.965 -      ((*tracing "expression is valid";*) Seq.single st)
   5.966 -    else
   5.967 -      ((*tracing "expression is not valid";*) Seq.empty) (* error "check_format: wrong format" *)
   5.968 -  end
   5.969 -
   5.970 -fun prove_match options ctxt nargs out_ts =
   5.971 -  let
   5.972 -    val thy = ProofContext.theory_of ctxt
   5.973 -    val eval_if_P =
   5.974 -      @{lemma "P ==> Predicate.eval x z ==> Predicate.eval (if P then x else y) z" by simp} 
   5.975 -    fun get_case_rewrite t =
   5.976 -      if (is_constructor thy t) then let
   5.977 -        val case_rewrites = (#case_rewrites (Datatype.the_info thy
   5.978 -          ((fst o dest_Type o fastype_of) t)))
   5.979 -        in fold (union Thm.eq_thm) (case_rewrites :: map get_case_rewrite (snd (strip_comb t))) [] end
   5.980 -      else []
   5.981 -    val simprules = insert Thm.eq_thm @{thm "unit.cases"} (insert Thm.eq_thm @{thm "prod.cases"}
   5.982 -      (fold (union Thm.eq_thm) (map get_case_rewrite out_ts) []))
   5.983 -  (* replace TRY by determining if it necessary - are there equations when calling compile match? *)
   5.984 -  in
   5.985 -     (* make this simpset better! *)
   5.986 -    asm_full_simp_tac (HOL_basic_ss' addsimps simprules) 1
   5.987 -    THEN print_tac options "after prove_match:"
   5.988 -    THEN (DETERM (TRY 
   5.989 -           (rtac eval_if_P 1
   5.990 -           THEN (SUBPROOF (fn {context = ctxt, params, prems, asms, concl, schematics} =>
   5.991 -             (REPEAT_DETERM (rtac @{thm conjI} 1
   5.992 -             THEN (SOLVED (asm_simp_tac HOL_basic_ss' 1))))
   5.993 -             THEN print_tac options "if condition to be solved:"
   5.994 -             THEN asm_simp_tac HOL_basic_ss' 1
   5.995 -             THEN TRY (
   5.996 -                let
   5.997 -                  val prems' = maps dest_conjunct_prem (take nargs prems)
   5.998 -                in
   5.999 -                  MetaSimplifier.rewrite_goal_tac
  5.1000 -                    (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
  5.1001 -                end
  5.1002 -             THEN REPEAT_DETERM (rtac @{thm refl} 1))
  5.1003 -             THEN print_tac options "after if simp; in SUBPROOF") ctxt 1))))
  5.1004 -    THEN print_tac options "after if simplification"
  5.1005 -  end;
  5.1006 -
  5.1007 -(* corresponds to compile_fun -- maybe call that also compile_sidecond? *)
  5.1008 -
  5.1009 -fun prove_sidecond ctxt t =
  5.1010 -  let
  5.1011 -    fun preds_of t nameTs = case strip_comb t of 
  5.1012 -      (f as Const (name, T), args) =>
  5.1013 -        if is_registered ctxt name then (name, T) :: nameTs
  5.1014 -          else fold preds_of args nameTs
  5.1015 -      | _ => nameTs
  5.1016 -    val preds = preds_of t []
  5.1017 -    val defs = map
  5.1018 -      (fn (pred, T) => predfun_definition_of ctxt pred
  5.1019 -        (all_input_of T))
  5.1020 -        preds
  5.1021 -  in 
  5.1022 -    simp_tac (HOL_basic_ss addsimps
  5.1023 -      (@{thms HOL.simp_thms} @ (@{thm eval_pred} :: defs))) 1 
  5.1024 -    (* need better control here! *)
  5.1025 -  end
  5.1026 -
  5.1027 -fun prove_clause options ctxt nargs mode (_, clauses) (ts, moded_ps) =
  5.1028 -  let
  5.1029 -    val (in_ts, clause_out_ts) = split_mode mode ts;
  5.1030 -    fun prove_prems out_ts [] =
  5.1031 -      (prove_match options ctxt nargs out_ts)
  5.1032 -      THEN print_tac options "before simplifying assumptions"
  5.1033 -      THEN asm_full_simp_tac HOL_basic_ss' 1
  5.1034 -      THEN print_tac options "before single intro rule"
  5.1035 -      THEN Subgoal.FOCUS_PREMS
  5.1036 -             (fn {context = ctxt, params = params, prems, asms, concl, schematics} =>
  5.1037 -              let
  5.1038 -                val prems' = maps dest_conjunct_prem (take nargs prems)
  5.1039 -              in
  5.1040 -                MetaSimplifier.rewrite_goal_tac
  5.1041 -                  (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
  5.1042 -              end) ctxt 1
  5.1043 -      THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
  5.1044 -    | prove_prems out_ts ((p, deriv) :: ps) =
  5.1045 -      let
  5.1046 -        val premposition = (find_index (equal p) clauses) + nargs
  5.1047 -        val mode = head_mode_of deriv
  5.1048 -        val rest_tac =
  5.1049 -          rtac @{thm bindI} 1
  5.1050 -          THEN (case p of Prem t =>
  5.1051 -            let
  5.1052 -              val (_, us) = strip_comb t
  5.1053 -              val (_, out_ts''') = split_mode mode us
  5.1054 -              val rec_tac = prove_prems out_ts''' ps
  5.1055 -            in
  5.1056 -              print_tac options "before clause:"
  5.1057 -              (*THEN asm_simp_tac HOL_basic_ss 1*)
  5.1058 -              THEN print_tac options "before prove_expr:"
  5.1059 -              THEN prove_expr options ctxt nargs premposition (t, deriv)
  5.1060 -              THEN print_tac options "after prove_expr:"
  5.1061 -              THEN rec_tac
  5.1062 -            end
  5.1063 -          | Negprem t =>
  5.1064 -            let
  5.1065 -              val (t, args) = strip_comb t
  5.1066 -              val (_, out_ts''') = split_mode mode args
  5.1067 -              val rec_tac = prove_prems out_ts''' ps
  5.1068 -              val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE)
  5.1069 -              val neg_intro_rule =
  5.1070 -                Option.map (fn name =>
  5.1071 -                  the (predfun_neg_intro_of ctxt name mode)) name
  5.1072 -              val param_derivations = param_derivations_of deriv
  5.1073 -              val params = ho_args_of mode args
  5.1074 -            in
  5.1075 -              print_tac options "before prove_neg_expr:"
  5.1076 -              THEN full_simp_tac (HOL_basic_ss addsimps
  5.1077 -                [@{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
  5.1078 -                 @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
  5.1079 -              THEN (if (is_some name) then
  5.1080 -                  print_tac options "before applying not introduction rule"
  5.1081 -                  THEN Subgoal.FOCUS_PREMS
  5.1082 -                    (fn {context = ctxt, params = params, prems, asms, concl, schematics} =>
  5.1083 -                      rtac (the neg_intro_rule) 1
  5.1084 -                      THEN rtac (nth prems premposition) 1) ctxt 1
  5.1085 -                  THEN print_tac options "after applying not introduction rule"
  5.1086 -                  THEN (EVERY (map2 (prove_param options ctxt nargs) params param_derivations))
  5.1087 -                  THEN (REPEAT_DETERM (atac 1))
  5.1088 -                else
  5.1089 -                  rtac @{thm not_predI'} 1
  5.1090 -                  (* test: *)
  5.1091 -                  THEN dtac @{thm sym} 1
  5.1092 -                  THEN asm_full_simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1)
  5.1093 -                  THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1
  5.1094 -              THEN rec_tac
  5.1095 -            end
  5.1096 -          | Sidecond t =>
  5.1097 -           rtac @{thm if_predI} 1
  5.1098 -           THEN print_tac options "before sidecond:"
  5.1099 -           THEN prove_sidecond ctxt t
  5.1100 -           THEN print_tac options "after sidecond:"
  5.1101 -           THEN prove_prems [] ps)
  5.1102 -      in (prove_match options ctxt nargs out_ts)
  5.1103 -          THEN rest_tac
  5.1104 -      end;
  5.1105 -    val prems_tac = prove_prems in_ts moded_ps
  5.1106 -  in
  5.1107 -    print_tac options "Proving clause..."
  5.1108 -    THEN rtac @{thm bindI} 1
  5.1109 -    THEN rtac @{thm singleI} 1
  5.1110 -    THEN prems_tac
  5.1111 -  end;
  5.1112 -
  5.1113 -fun select_sup 1 1 = []
  5.1114 -  | select_sup _ 1 = [rtac @{thm supI1}]
  5.1115 -  | select_sup n i = (rtac @{thm supI2})::(select_sup (n - 1) (i - 1));
  5.1116 -
  5.1117 -fun prove_one_direction options ctxt clauses preds pred mode moded_clauses =
  5.1118 -  let
  5.1119 -    val T = the (AList.lookup (op =) preds pred)
  5.1120 -    val nargs = length (binder_types T)
  5.1121 -    val pred_case_rule = the_elim_of ctxt pred
  5.1122 -  in
  5.1123 -    REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"}))
  5.1124 -    THEN print_tac options "before applying elim rule"
  5.1125 -    THEN etac (predfun_elim_of ctxt pred mode) 1
  5.1126 -    THEN etac pred_case_rule 1
  5.1127 -    THEN print_tac options "after applying elim rule"
  5.1128 -    THEN (EVERY (map
  5.1129 -           (fn i => EVERY' (select_sup (length moded_clauses) i) i) 
  5.1130 -             (1 upto (length moded_clauses))))
  5.1131 -    THEN (EVERY (map2 (prove_clause options ctxt nargs mode) clauses moded_clauses))
  5.1132 -    THEN print_tac options "proved one direction"
  5.1133 -  end;
  5.1134 -
  5.1135 -(** Proof in the other direction **)
  5.1136 -
  5.1137 -fun prove_match2 options ctxt out_ts =
  5.1138 -  let
  5.1139 -    val thy = ProofContext.theory_of ctxt
  5.1140 -    fun split_term_tac (Free _) = all_tac
  5.1141 -      | split_term_tac t =
  5.1142 -        if (is_constructor thy t) then
  5.1143 -          let
  5.1144 -            val info = Datatype.the_info thy ((fst o dest_Type o fastype_of) t)
  5.1145 -            val num_of_constrs = length (#case_rewrites info)
  5.1146 -            val (_, ts) = strip_comb t
  5.1147 -          in
  5.1148 -            print_tac options ("Term " ^ (Syntax.string_of_term ctxt t) ^ 
  5.1149 -              "splitting with rules \n" ^ Display.string_of_thm ctxt (#split_asm info))
  5.1150 -            THEN TRY ((Splitter.split_asm_tac [#split_asm info] 1)
  5.1151 -              THEN (print_tac options "after splitting with split_asm rules")
  5.1152 -            (* THEN (Simplifier.asm_full_simp_tac HOL_basic_ss 1)
  5.1153 -              THEN (DETERM (TRY (etac @{thm Pair_inject} 1)))*)
  5.1154 -              THEN (REPEAT_DETERM_N (num_of_constrs - 1)
  5.1155 -                (etac @{thm botE} 1 ORELSE etac @{thm botE} 2)))
  5.1156 -            THEN (assert_tac (Max_number_of_subgoals 2))
  5.1157 -            THEN (EVERY (map split_term_tac ts))
  5.1158 -          end
  5.1159 -      else all_tac
  5.1160 -  in
  5.1161 -    split_term_tac (HOLogic.mk_tuple out_ts)
  5.1162 -    THEN (DETERM (TRY ((Splitter.split_asm_tac [@{thm "split_if_asm"}] 1)
  5.1163 -    THEN (etac @{thm botE} 2))))
  5.1164 -  end
  5.1165 -
  5.1166 -(* VERY LARGE SIMILIRATIY to function prove_param 
  5.1167 --- join both functions
  5.1168 -*)
  5.1169 -(* TODO: remove function *)
  5.1170 -
  5.1171 -fun prove_param2 options ctxt t deriv =
  5.1172 -  let
  5.1173 -    val (f, args) = strip_comb (Envir.eta_contract t)
  5.1174 -    val mode = head_mode_of deriv
  5.1175 -    val param_derivations = param_derivations_of deriv
  5.1176 -    val ho_args = ho_args_of mode args
  5.1177 -    val f_tac = case f of
  5.1178 -        Const (name, T) => full_simp_tac (HOL_basic_ss addsimps 
  5.1179 -           (@{thm eval_pred}::(predfun_definition_of ctxt name mode)
  5.1180 -           :: @{thm "Product_Type.split_conv"}::[])) 1
  5.1181 -      | Free _ => all_tac
  5.1182 -      | _ => error "prove_param2: illegal parameter term"
  5.1183 -  in
  5.1184 -    print_tac options "before simplification in prove_args:"
  5.1185 -    THEN f_tac
  5.1186 -    THEN print_tac options "after simplification in prove_args"
  5.1187 -    THEN EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations)
  5.1188 -  end
  5.1189 -
  5.1190 -fun prove_expr2 options ctxt (t, deriv) = 
  5.1191 -  (case strip_comb t of
  5.1192 -      (Const (name, T), args) =>
  5.1193 -        let
  5.1194 -          val mode = head_mode_of deriv
  5.1195 -          val param_derivations = param_derivations_of deriv
  5.1196 -          val ho_args = ho_args_of mode args
  5.1197 -        in
  5.1198 -          etac @{thm bindE} 1
  5.1199 -          THEN (REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"})))
  5.1200 -          THEN print_tac options "prove_expr2-before"
  5.1201 -          THEN etac (predfun_elim_of ctxt name mode) 1
  5.1202 -          THEN print_tac options "prove_expr2"
  5.1203 -          THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations))
  5.1204 -          THEN print_tac options "finished prove_expr2"
  5.1205 -        end
  5.1206 -      | _ => etac @{thm bindE} 1)
  5.1207 -
  5.1208 -fun prove_sidecond2 options ctxt t = let
  5.1209 -  fun preds_of t nameTs = case strip_comb t of 
  5.1210 -    (f as Const (name, T), args) =>
  5.1211 -      if is_registered ctxt name then (name, T) :: nameTs
  5.1212 -        else fold preds_of args nameTs
  5.1213 -    | _ => nameTs
  5.1214 -  val preds = preds_of t []
  5.1215 -  val defs = map
  5.1216 -    (fn (pred, T) => predfun_definition_of ctxt pred 
  5.1217 -      (all_input_of T))
  5.1218 -      preds
  5.1219 -  in
  5.1220 -   (* only simplify the one assumption *)
  5.1221 -   full_simp_tac (HOL_basic_ss' addsimps @{thm eval_pred} :: defs) 1 
  5.1222 -   (* need better control here! *)
  5.1223 -   THEN print_tac options "after sidecond2 simplification"
  5.1224 -   end
  5.1225 -  
  5.1226 -fun prove_clause2 options ctxt pred mode (ts, ps) i =
  5.1227 -  let
  5.1228 -    val pred_intro_rule = nth (intros_of ctxt pred) (i - 1)
  5.1229 -    val (in_ts, clause_out_ts) = split_mode mode ts;
  5.1230 -    val split_ss = HOL_basic_ss' addsimps [@{thm split_eta}, @{thm split_beta},
  5.1231 -      @{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
  5.1232 -    fun prove_prems2 out_ts [] =
  5.1233 -      print_tac options "before prove_match2 - last call:"
  5.1234 -      THEN prove_match2 options ctxt out_ts
  5.1235 -      THEN print_tac options "after prove_match2 - last call:"
  5.1236 -      THEN (etac @{thm singleE} 1)
  5.1237 -      THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1))
  5.1238 -      THEN (asm_full_simp_tac HOL_basic_ss' 1)
  5.1239 -      THEN TRY (
  5.1240 -        (REPEAT_DETERM (etac @{thm Pair_inject} 1))
  5.1241 -        THEN (asm_full_simp_tac HOL_basic_ss' 1)
  5.1242 -        
  5.1243 -        THEN SOLVED (print_tac options "state before applying intro rule:"
  5.1244 -        THEN (rtac pred_intro_rule
  5.1245 -        (* How to handle equality correctly? *)
  5.1246 -        THEN_ALL_NEW (K (print_tac options "state before assumption matching")
  5.1247 -        THEN' (atac ORELSE' ((CHANGED o asm_full_simp_tac split_ss) THEN' (TRY o atac)))
  5.1248 -          THEN' (K (print_tac options "state after pre-simplification:"))
  5.1249 -        THEN' (K (print_tac options "state after assumption matching:")))) 1))
  5.1250 -    | prove_prems2 out_ts ((p, deriv) :: ps) =
  5.1251 -      let
  5.1252 -        val mode = head_mode_of deriv
  5.1253 -        val rest_tac = (case p of
  5.1254 -          Prem t =>
  5.1255 -          let
  5.1256 -            val (_, us) = strip_comb t
  5.1257 -            val (_, out_ts''') = split_mode mode us
  5.1258 -            val rec_tac = prove_prems2 out_ts''' ps
  5.1259 -          in
  5.1260 -            (prove_expr2 options ctxt (t, deriv)) THEN rec_tac
  5.1261 -          end
  5.1262 -        | Negprem t =>
  5.1263 -          let
  5.1264 -            val (_, args) = strip_comb t
  5.1265 -            val (_, out_ts''') = split_mode mode args
  5.1266 -            val rec_tac = prove_prems2 out_ts''' ps
  5.1267 -            val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE)
  5.1268 -            val param_derivations = param_derivations_of deriv
  5.1269 -            val ho_args = ho_args_of mode args
  5.1270 -          in
  5.1271 -            print_tac options "before neg prem 2"
  5.1272 -            THEN etac @{thm bindE} 1
  5.1273 -            THEN (if is_some name then
  5.1274 -                full_simp_tac (HOL_basic_ss addsimps
  5.1275 -                  [predfun_definition_of ctxt (the name) mode]) 1
  5.1276 -                THEN etac @{thm not_predE} 1
  5.1277 -                THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1
  5.1278 -                THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations))
  5.1279 -              else
  5.1280 -                etac @{thm not_predE'} 1)
  5.1281 -            THEN rec_tac
  5.1282 -          end 
  5.1283 -        | Sidecond t =>
  5.1284 -          etac @{thm bindE} 1
  5.1285 -          THEN etac @{thm if_predE} 1
  5.1286 -          THEN prove_sidecond2 options ctxt t
  5.1287 -          THEN prove_prems2 [] ps)
  5.1288 -      in print_tac options "before prove_match2:"
  5.1289 -         THEN prove_match2 options ctxt out_ts
  5.1290 -         THEN print_tac options "after prove_match2:"
  5.1291 -         THEN rest_tac
  5.1292 -      end;
  5.1293 -    val prems_tac = prove_prems2 in_ts ps 
  5.1294 -  in
  5.1295 -    print_tac options "starting prove_clause2"
  5.1296 -    THEN etac @{thm bindE} 1
  5.1297 -    THEN (etac @{thm singleE'} 1)
  5.1298 -    THEN (TRY (etac @{thm Pair_inject} 1))
  5.1299 -    THEN print_tac options "after singleE':"
  5.1300 -    THEN prems_tac
  5.1301 -  end;
  5.1302 - 
  5.1303 -fun prove_other_direction options ctxt pred mode moded_clauses =
  5.1304 -  let
  5.1305 -    fun prove_clause clause i =
  5.1306 -      (if i < length moded_clauses then etac @{thm supE} 1 else all_tac)
  5.1307 -      THEN (prove_clause2 options ctxt pred mode clause i)
  5.1308 -  in
  5.1309 -    (DETERM (TRY (rtac @{thm unit.induct} 1)))
  5.1310 -     THEN (REPEAT_DETERM (CHANGED (rewtac @{thm split_paired_all})))
  5.1311 -     THEN (rtac (predfun_intro_of ctxt pred mode) 1)
  5.1312 -     THEN (REPEAT_DETERM (rtac @{thm refl} 2))
  5.1313 -     THEN (if null moded_clauses then
  5.1314 -         etac @{thm botE} 1
  5.1315 -       else EVERY (map2 prove_clause moded_clauses (1 upto (length moded_clauses))))
  5.1316 -  end;
  5.1317 -
  5.1318 -(** proof procedure **)
  5.1319 -
  5.1320 -fun prove_pred options thy clauses preds pred (pol, mode) (moded_clauses, compiled_term) =
  5.1321 -  let
  5.1322 -    val ctxt = ProofContext.init_global thy
  5.1323 -    val clauses = case AList.lookup (op =) clauses pred of SOME rs => rs | NONE => []
  5.1324 -  in
  5.1325 -    Goal.prove ctxt (Term.add_free_names compiled_term []) [] compiled_term
  5.1326 -      (if not (skip_proof options) then
  5.1327 -        (fn _ =>
  5.1328 -        rtac @{thm pred_iffI} 1
  5.1329 -        THEN print_tac options "after pred_iffI"
  5.1330 -        THEN prove_one_direction options ctxt clauses preds pred mode moded_clauses
  5.1331 -        THEN print_tac options "proved one direction"
  5.1332 -        THEN prove_other_direction options ctxt pred mode moded_clauses
  5.1333 -        THEN print_tac options "proved other direction")
  5.1334 -      else (fn _ => Skip_Proof.cheat_tac thy))
  5.1335 -  end;
  5.1336  
  5.1337  (* composition of mode inference, definition, compilation and proof *)
  5.1338  
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Thu Oct 21 19:13:09 2010 +0200
     6.3 @@ -0,0 +1,525 @@
     6.4 +(*  Title:      HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
     6.5 +    Author:     Lukas Bulwahn, TU Muenchen
     6.6 +
     6.7 +Proof procedure for the compiler from predicates specified by intro/elim rules to equations.
     6.8 +*)
     6.9 +
    6.10 +signature PREDICATE_COMPILE_PROOF =
    6.11 +sig
    6.12 +  type indprem = Predicate_Compile_Aux.indprem;
    6.13 +  type mode = Predicate_Compile_Aux.mode
    6.14 +  val prove_pred : Predicate_Compile_Aux.options -> theory
    6.15 +    -> (string * (term list * indprem list) list) list
    6.16 +    -> (string * typ) list -> string -> bool * mode
    6.17 +    -> (term list * (indprem * Mode_Inference.mode_derivation) list) list * term
    6.18 +    -> Thm.thm
    6.19 +end;
    6.20 +
    6.21 +structure Predicate_Compile_Proof : PREDICATE_COMPILE_PROOF =
    6.22 +struct
    6.23 +
    6.24 +open Predicate_Compile_Aux;
    6.25 +open Core_Data;
    6.26 +open Mode_Inference;
    6.27 +
    6.28 +(* debug stuff *)
    6.29 +
    6.30 +fun print_tac options s = 
    6.31 +  if show_proof_trace options then Tactical.print_tac s else Seq.single;
    6.32 +
    6.33 +(** auxiliary **)
    6.34 +
    6.35 +fun assert b = if not b then raise Fail "Assertion failed" else warning "Assertion holds"
    6.36 +
    6.37 +datatype assertion = Max_number_of_subgoals of int
    6.38 +fun assert_tac (Max_number_of_subgoals i) st =
    6.39 +  if (nprems_of st <= i) then Seq.single st
    6.40 +  else raise Fail ("assert_tac: Numbers of subgoals mismatch at goal state :"
    6.41 +    ^ "\n" ^ Pretty.string_of (Pretty.chunks
    6.42 +      (Goal_Display.pretty_goals_without_context st)));
    6.43 +
    6.44 +
    6.45 +(** special setup for simpset **)
    6.46 +val HOL_basic_ss' = HOL_basic_ss addsimps (@{thms HOL.simp_thms} @ [@{thm Pair_eq}])
    6.47 +  setSolver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
    6.48 +  setSolver (mk_solver "True_solver" (fn _ => rtac @{thm TrueI}))
    6.49 +
    6.50 +(* auxillary functions *)
    6.51 +
    6.52 +fun is_Type (Type _) = true
    6.53 +  | is_Type _ = false
    6.54 +
    6.55 +(* returns true if t is an application of an datatype constructor *)
    6.56 +(* which then consequently would be splitted *)
    6.57 +(* else false *)
    6.58 +fun is_constructor thy t =
    6.59 +  if (is_Type (fastype_of t)) then
    6.60 +    (case Datatype.get_info thy ((fst o dest_Type o fastype_of) t) of
    6.61 +      NONE => false
    6.62 +    | SOME info => (let
    6.63 +      val constr_consts = maps (fn (_, (_, _, constrs)) => map fst constrs) (#descr info)
    6.64 +      val (c, _) = strip_comb t
    6.65 +      in (case c of
    6.66 +        Const (name, _) => member (op =) constr_consts name
    6.67 +        | _ => false) end))
    6.68 +  else false
    6.69 +
    6.70 +(* MAJOR FIXME:  prove_params should be simple
    6.71 + - different form of introrule for parameters ? *)
    6.72 +
    6.73 +fun prove_param options ctxt nargs t deriv =
    6.74 +  let
    6.75 +    val  (f, args) = strip_comb (Envir.eta_contract t)
    6.76 +    val mode = head_mode_of deriv
    6.77 +    val param_derivations = param_derivations_of deriv
    6.78 +    val ho_args = ho_args_of mode args
    6.79 +    val f_tac = case f of
    6.80 +      Const (name, T) => simp_tac (HOL_basic_ss addsimps 
    6.81 +         [@{thm eval_pred}, predfun_definition_of ctxt name mode,
    6.82 +         @{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
    6.83 +         @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
    6.84 +    | Free _ =>
    6.85 +      Subgoal.FOCUS_PREMS (fn {context = ctxt, params = params, prems, asms, concl, schematics} =>
    6.86 +        let
    6.87 +          val prems' = maps dest_conjunct_prem (take nargs prems)
    6.88 +        in
    6.89 +          MetaSimplifier.rewrite_goal_tac
    6.90 +            (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
    6.91 +        end) ctxt 1
    6.92 +    | Abs _ => raise Fail "prove_param: No valid parameter term"
    6.93 +  in
    6.94 +    REPEAT_DETERM (rtac @{thm ext} 1)
    6.95 +    THEN print_tac options "prove_param"
    6.96 +    THEN f_tac 
    6.97 +    THEN print_tac options "after prove_param"
    6.98 +    THEN (REPEAT_DETERM (atac 1))
    6.99 +    THEN (EVERY (map2 (prove_param options ctxt nargs) ho_args param_derivations))
   6.100 +    THEN REPEAT_DETERM (rtac @{thm refl} 1)
   6.101 +  end
   6.102 +
   6.103 +fun prove_expr options ctxt nargs (premposition : int) (t, deriv) =
   6.104 +  case strip_comb t of
   6.105 +    (Const (name, T), args) =>
   6.106 +      let
   6.107 +        val mode = head_mode_of deriv
   6.108 +        val introrule = predfun_intro_of ctxt name mode
   6.109 +        val param_derivations = param_derivations_of deriv
   6.110 +        val ho_args = ho_args_of mode args
   6.111 +      in
   6.112 +        print_tac options "before intro rule:"
   6.113 +        THEN rtac introrule 1
   6.114 +        THEN print_tac options "after intro rule"
   6.115 +        (* for the right assumption in first position *)
   6.116 +        THEN rotate_tac premposition 1
   6.117 +        THEN atac 1
   6.118 +        THEN print_tac options "parameter goal"
   6.119 +        (* work with parameter arguments *)
   6.120 +        THEN (EVERY (map2 (prove_param options ctxt nargs) ho_args param_derivations))
   6.121 +        THEN (REPEAT_DETERM (atac 1))
   6.122 +      end
   6.123 +  | (Free _, _) =>
   6.124 +    print_tac options "proving parameter call.."
   6.125 +    THEN Subgoal.FOCUS_PREMS (fn {context = ctxt, params, prems, asms, concl, schematics} =>
   6.126 +        let
   6.127 +          val param_prem = nth prems premposition
   6.128 +          val (param, _) = strip_comb (HOLogic.dest_Trueprop (prop_of param_prem))
   6.129 +          val prems' = maps dest_conjunct_prem (take nargs prems)
   6.130 +          fun param_rewrite prem =
   6.131 +            param = snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of prem)))
   6.132 +          val SOME rew_eq = find_first param_rewrite prems'
   6.133 +          val param_prem' = MetaSimplifier.rewrite_rule
   6.134 +            (map (fn th => th RS @{thm eq_reflection})
   6.135 +              [rew_eq RS @{thm sym}, @{thm split_beta}, @{thm fst_conv}, @{thm snd_conv}])
   6.136 +            param_prem
   6.137 +        in
   6.138 +          rtac param_prem' 1
   6.139 +        end) ctxt 1
   6.140 +    THEN print_tac options "after prove parameter call"
   6.141 +
   6.142 +fun SOLVED tac st = FILTER (fn st' => nprems_of st' = nprems_of st - 1) tac st;
   6.143 +
   6.144 +fun SOLVEDALL tac st = FILTER (fn st' => nprems_of st' = 0) tac st
   6.145 +
   6.146 +fun check_format ctxt st =
   6.147 +  let
   6.148 +    val concl' = Logic.strip_assums_concl (hd (prems_of st))
   6.149 +    val concl = HOLogic.dest_Trueprop concl'
   6.150 +    val expr = fst (strip_comb (fst (PredicateCompFuns.dest_Eval concl)))
   6.151 +    fun valid_expr (Const (@{const_name Predicate.bind}, _)) = true
   6.152 +      | valid_expr (Const (@{const_name Predicate.single}, _)) = true
   6.153 +      | valid_expr _ = false
   6.154 +  in
   6.155 +    if valid_expr expr then
   6.156 +      ((*tracing "expression is valid";*) Seq.single st)
   6.157 +    else
   6.158 +      ((*tracing "expression is not valid";*) Seq.empty) (* error "check_format: wrong format" *)
   6.159 +  end
   6.160 +
   6.161 +fun prove_match options ctxt nargs out_ts =
   6.162 +  let
   6.163 +    val thy = ProofContext.theory_of ctxt
   6.164 +    val eval_if_P =
   6.165 +      @{lemma "P ==> Predicate.eval x z ==> Predicate.eval (if P then x else y) z" by simp} 
   6.166 +    fun get_case_rewrite t =
   6.167 +      if (is_constructor thy t) then let
   6.168 +        val case_rewrites = (#case_rewrites (Datatype.the_info thy
   6.169 +          ((fst o dest_Type o fastype_of) t)))
   6.170 +        in fold (union Thm.eq_thm) (case_rewrites :: map get_case_rewrite (snd (strip_comb t))) [] end
   6.171 +      else []
   6.172 +    val simprules = insert Thm.eq_thm @{thm "unit.cases"} (insert Thm.eq_thm @{thm "prod.cases"}
   6.173 +      (fold (union Thm.eq_thm) (map get_case_rewrite out_ts) []))
   6.174 +  (* replace TRY by determining if it necessary - are there equations when calling compile match? *)
   6.175 +  in
   6.176 +     (* make this simpset better! *)
   6.177 +    asm_full_simp_tac (HOL_basic_ss' addsimps simprules) 1
   6.178 +    THEN print_tac options "after prove_match:"
   6.179 +    THEN (DETERM (TRY 
   6.180 +           (rtac eval_if_P 1
   6.181 +           THEN (SUBPROOF (fn {context = ctxt, params, prems, asms, concl, schematics} =>
   6.182 +             (REPEAT_DETERM (rtac @{thm conjI} 1
   6.183 +             THEN (SOLVED (asm_simp_tac HOL_basic_ss' 1))))
   6.184 +             THEN print_tac options "if condition to be solved:"
   6.185 +             THEN asm_simp_tac HOL_basic_ss' 1
   6.186 +             THEN TRY (
   6.187 +                let
   6.188 +                  val prems' = maps dest_conjunct_prem (take nargs prems)
   6.189 +                in
   6.190 +                  MetaSimplifier.rewrite_goal_tac
   6.191 +                    (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
   6.192 +                end
   6.193 +             THEN REPEAT_DETERM (rtac @{thm refl} 1))
   6.194 +             THEN print_tac options "after if simp; in SUBPROOF") ctxt 1))))
   6.195 +    THEN print_tac options "after if simplification"
   6.196 +  end;
   6.197 +
   6.198 +(* corresponds to compile_fun -- maybe call that also compile_sidecond? *)
   6.199 +
   6.200 +fun prove_sidecond ctxt t =
   6.201 +  let
   6.202 +    fun preds_of t nameTs = case strip_comb t of 
   6.203 +      (f as Const (name, T), args) =>
   6.204 +        if is_registered ctxt name then (name, T) :: nameTs
   6.205 +          else fold preds_of args nameTs
   6.206 +      | _ => nameTs
   6.207 +    val preds = preds_of t []
   6.208 +    val defs = map
   6.209 +      (fn (pred, T) => predfun_definition_of ctxt pred
   6.210 +        (all_input_of T))
   6.211 +        preds
   6.212 +  in 
   6.213 +    simp_tac (HOL_basic_ss addsimps
   6.214 +      (@{thms HOL.simp_thms} @ (@{thm eval_pred} :: defs))) 1 
   6.215 +    (* need better control here! *)
   6.216 +  end
   6.217 +
   6.218 +fun prove_clause options ctxt nargs mode (_, clauses) (ts, moded_ps) =
   6.219 +  let
   6.220 +    val (in_ts, clause_out_ts) = split_mode mode ts;
   6.221 +    fun prove_prems out_ts [] =
   6.222 +      (prove_match options ctxt nargs out_ts)
   6.223 +      THEN print_tac options "before simplifying assumptions"
   6.224 +      THEN asm_full_simp_tac HOL_basic_ss' 1
   6.225 +      THEN print_tac options "before single intro rule"
   6.226 +      THEN Subgoal.FOCUS_PREMS
   6.227 +             (fn {context = ctxt, params = params, prems, asms, concl, schematics} =>
   6.228 +              let
   6.229 +                val prems' = maps dest_conjunct_prem (take nargs prems)
   6.230 +              in
   6.231 +                MetaSimplifier.rewrite_goal_tac
   6.232 +                  (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
   6.233 +              end) ctxt 1
   6.234 +      THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
   6.235 +    | prove_prems out_ts ((p, deriv) :: ps) =
   6.236 +      let
   6.237 +        val premposition = (find_index (equal p) clauses) + nargs
   6.238 +        val mode = head_mode_of deriv
   6.239 +        val rest_tac =
   6.240 +          rtac @{thm bindI} 1
   6.241 +          THEN (case p of Prem t =>
   6.242 +            let
   6.243 +              val (_, us) = strip_comb t
   6.244 +              val (_, out_ts''') = split_mode mode us
   6.245 +              val rec_tac = prove_prems out_ts''' ps
   6.246 +            in
   6.247 +              print_tac options "before clause:"
   6.248 +              (*THEN asm_simp_tac HOL_basic_ss 1*)
   6.249 +              THEN print_tac options "before prove_expr:"
   6.250 +              THEN prove_expr options ctxt nargs premposition (t, deriv)
   6.251 +              THEN print_tac options "after prove_expr:"
   6.252 +              THEN rec_tac
   6.253 +            end
   6.254 +          | Negprem t =>
   6.255 +            let
   6.256 +              val (t, args) = strip_comb t
   6.257 +              val (_, out_ts''') = split_mode mode args
   6.258 +              val rec_tac = prove_prems out_ts''' ps
   6.259 +              val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE)
   6.260 +              val neg_intro_rule =
   6.261 +                Option.map (fn name =>
   6.262 +                  the (predfun_neg_intro_of ctxt name mode)) name
   6.263 +              val param_derivations = param_derivations_of deriv
   6.264 +              val params = ho_args_of mode args
   6.265 +            in
   6.266 +              print_tac options "before prove_neg_expr:"
   6.267 +              THEN full_simp_tac (HOL_basic_ss addsimps
   6.268 +                [@{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
   6.269 +                 @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
   6.270 +              THEN (if (is_some name) then
   6.271 +                  print_tac options "before applying not introduction rule"
   6.272 +                  THEN Subgoal.FOCUS_PREMS
   6.273 +                    (fn {context = ctxt, params = params, prems, asms, concl, schematics} =>
   6.274 +                      rtac (the neg_intro_rule) 1
   6.275 +                      THEN rtac (nth prems premposition) 1) ctxt 1
   6.276 +                  THEN print_tac options "after applying not introduction rule"
   6.277 +                  THEN (EVERY (map2 (prove_param options ctxt nargs) params param_derivations))
   6.278 +                  THEN (REPEAT_DETERM (atac 1))
   6.279 +                else
   6.280 +                  rtac @{thm not_predI'} 1
   6.281 +                  (* test: *)
   6.282 +                  THEN dtac @{thm sym} 1
   6.283 +                  THEN asm_full_simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1)
   6.284 +                  THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1
   6.285 +              THEN rec_tac
   6.286 +            end
   6.287 +          | Sidecond t =>
   6.288 +           rtac @{thm if_predI} 1
   6.289 +           THEN print_tac options "before sidecond:"
   6.290 +           THEN prove_sidecond ctxt t
   6.291 +           THEN print_tac options "after sidecond:"
   6.292 +           THEN prove_prems [] ps)
   6.293 +      in (prove_match options ctxt nargs out_ts)
   6.294 +          THEN rest_tac
   6.295 +      end;
   6.296 +    val prems_tac = prove_prems in_ts moded_ps
   6.297 +  in
   6.298 +    print_tac options "Proving clause..."
   6.299 +    THEN rtac @{thm bindI} 1
   6.300 +    THEN rtac @{thm singleI} 1
   6.301 +    THEN prems_tac
   6.302 +  end;
   6.303 +
   6.304 +fun select_sup 1 1 = []
   6.305 +  | select_sup _ 1 = [rtac @{thm supI1}]
   6.306 +  | select_sup n i = (rtac @{thm supI2})::(select_sup (n - 1) (i - 1));
   6.307 +
   6.308 +fun prove_one_direction options ctxt clauses preds pred mode moded_clauses =
   6.309 +  let
   6.310 +    val T = the (AList.lookup (op =) preds pred)
   6.311 +    val nargs = length (binder_types T)
   6.312 +    val pred_case_rule = the_elim_of ctxt pred
   6.313 +  in
   6.314 +    REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"}))
   6.315 +    THEN print_tac options "before applying elim rule"
   6.316 +    THEN etac (predfun_elim_of ctxt pred mode) 1
   6.317 +    THEN etac pred_case_rule 1
   6.318 +    THEN print_tac options "after applying elim rule"
   6.319 +    THEN (EVERY (map
   6.320 +           (fn i => EVERY' (select_sup (length moded_clauses) i) i) 
   6.321 +             (1 upto (length moded_clauses))))
   6.322 +    THEN (EVERY (map2 (prove_clause options ctxt nargs mode) clauses moded_clauses))
   6.323 +    THEN print_tac options "proved one direction"
   6.324 +  end;
   6.325 +
   6.326 +(** Proof in the other direction **)
   6.327 +
   6.328 +fun prove_match2 options ctxt out_ts =
   6.329 +  let
   6.330 +    val thy = ProofContext.theory_of ctxt
   6.331 +    fun split_term_tac (Free _) = all_tac
   6.332 +      | split_term_tac t =
   6.333 +        if (is_constructor thy t) then
   6.334 +          let
   6.335 +            val info = Datatype.the_info thy ((fst o dest_Type o fastype_of) t)
   6.336 +            val num_of_constrs = length (#case_rewrites info)
   6.337 +            val (_, ts) = strip_comb t
   6.338 +          in
   6.339 +            print_tac options ("Term " ^ (Syntax.string_of_term ctxt t) ^ 
   6.340 +              "splitting with rules \n" ^ Display.string_of_thm ctxt (#split_asm info))
   6.341 +            THEN TRY ((Splitter.split_asm_tac [#split_asm info] 1)
   6.342 +              THEN (print_tac options "after splitting with split_asm rules")
   6.343 +            (* THEN (Simplifier.asm_full_simp_tac HOL_basic_ss 1)
   6.344 +              THEN (DETERM (TRY (etac @{thm Pair_inject} 1)))*)
   6.345 +              THEN (REPEAT_DETERM_N (num_of_constrs - 1)
   6.346 +                (etac @{thm botE} 1 ORELSE etac @{thm botE} 2)))
   6.347 +            THEN (assert_tac (Max_number_of_subgoals 2))
   6.348 +            THEN (EVERY (map split_term_tac ts))
   6.349 +          end
   6.350 +      else all_tac
   6.351 +  in
   6.352 +    split_term_tac (HOLogic.mk_tuple out_ts)
   6.353 +    THEN (DETERM (TRY ((Splitter.split_asm_tac [@{thm "split_if_asm"}] 1)
   6.354 +    THEN (etac @{thm botE} 2))))
   6.355 +  end
   6.356 +
   6.357 +(* VERY LARGE SIMILIRATIY to function prove_param 
   6.358 +-- join both functions
   6.359 +*)
   6.360 +(* TODO: remove function *)
   6.361 +
   6.362 +fun prove_param2 options ctxt t deriv =
   6.363 +  let
   6.364 +    val (f, args) = strip_comb (Envir.eta_contract t)
   6.365 +    val mode = head_mode_of deriv
   6.366 +    val param_derivations = param_derivations_of deriv
   6.367 +    val ho_args = ho_args_of mode args
   6.368 +    val f_tac = case f of
   6.369 +        Const (name, T) => full_simp_tac (HOL_basic_ss addsimps 
   6.370 +           (@{thm eval_pred}::(predfun_definition_of ctxt name mode)
   6.371 +           :: @{thm "Product_Type.split_conv"}::[])) 1
   6.372 +      | Free _ => all_tac
   6.373 +      | _ => error "prove_param2: illegal parameter term"
   6.374 +  in
   6.375 +    print_tac options "before simplification in prove_args:"
   6.376 +    THEN f_tac
   6.377 +    THEN print_tac options "after simplification in prove_args"
   6.378 +    THEN EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations)
   6.379 +  end
   6.380 +
   6.381 +fun prove_expr2 options ctxt (t, deriv) = 
   6.382 +  (case strip_comb t of
   6.383 +      (Const (name, T), args) =>
   6.384 +        let
   6.385 +          val mode = head_mode_of deriv
   6.386 +          val param_derivations = param_derivations_of deriv
   6.387 +          val ho_args = ho_args_of mode args
   6.388 +        in
   6.389 +          etac @{thm bindE} 1
   6.390 +          THEN (REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"})))
   6.391 +          THEN print_tac options "prove_expr2-before"
   6.392 +          THEN etac (predfun_elim_of ctxt name mode) 1
   6.393 +          THEN print_tac options "prove_expr2"
   6.394 +          THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations))
   6.395 +          THEN print_tac options "finished prove_expr2"
   6.396 +        end
   6.397 +      | _ => etac @{thm bindE} 1)
   6.398 +
   6.399 +fun prove_sidecond2 options ctxt t = let
   6.400 +  fun preds_of t nameTs = case strip_comb t of 
   6.401 +    (f as Const (name, T), args) =>
   6.402 +      if is_registered ctxt name then (name, T) :: nameTs
   6.403 +        else fold preds_of args nameTs
   6.404 +    | _ => nameTs
   6.405 +  val preds = preds_of t []
   6.406 +  val defs = map
   6.407 +    (fn (pred, T) => predfun_definition_of ctxt pred 
   6.408 +      (all_input_of T))
   6.409 +      preds
   6.410 +  in
   6.411 +   (* only simplify the one assumption *)
   6.412 +   full_simp_tac (HOL_basic_ss' addsimps @{thm eval_pred} :: defs) 1 
   6.413 +   (* need better control here! *)
   6.414 +   THEN print_tac options "after sidecond2 simplification"
   6.415 +   end
   6.416 +  
   6.417 +fun prove_clause2 options ctxt pred mode (ts, ps) i =
   6.418 +  let
   6.419 +    val pred_intro_rule = nth (intros_of ctxt pred) (i - 1)
   6.420 +    val (in_ts, clause_out_ts) = split_mode mode ts;
   6.421 +    val split_ss = HOL_basic_ss' addsimps [@{thm split_eta}, @{thm split_beta},
   6.422 +      @{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
   6.423 +    fun prove_prems2 out_ts [] =
   6.424 +      print_tac options "before prove_match2 - last call:"
   6.425 +      THEN prove_match2 options ctxt out_ts
   6.426 +      THEN print_tac options "after prove_match2 - last call:"
   6.427 +      THEN (etac @{thm singleE} 1)
   6.428 +      THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1))
   6.429 +      THEN (asm_full_simp_tac HOL_basic_ss' 1)
   6.430 +      THEN TRY (
   6.431 +        (REPEAT_DETERM (etac @{thm Pair_inject} 1))
   6.432 +        THEN (asm_full_simp_tac HOL_basic_ss' 1)
   6.433 +        
   6.434 +        THEN SOLVED (print_tac options "state before applying intro rule:"
   6.435 +        THEN (rtac pred_intro_rule
   6.436 +        (* How to handle equality correctly? *)
   6.437 +        THEN_ALL_NEW (K (print_tac options "state before assumption matching")
   6.438 +        THEN' (atac ORELSE' ((CHANGED o asm_full_simp_tac split_ss) THEN' (TRY o atac)))
   6.439 +          THEN' (K (print_tac options "state after pre-simplification:"))
   6.440 +        THEN' (K (print_tac options "state after assumption matching:")))) 1))
   6.441 +    | prove_prems2 out_ts ((p, deriv) :: ps) =
   6.442 +      let
   6.443 +        val mode = head_mode_of deriv
   6.444 +        val rest_tac = (case p of
   6.445 +          Prem t =>
   6.446 +          let
   6.447 +            val (_, us) = strip_comb t
   6.448 +            val (_, out_ts''') = split_mode mode us
   6.449 +            val rec_tac = prove_prems2 out_ts''' ps
   6.450 +          in
   6.451 +            (prove_expr2 options ctxt (t, deriv)) THEN rec_tac
   6.452 +          end
   6.453 +        | Negprem t =>
   6.454 +          let
   6.455 +            val (_, args) = strip_comb t
   6.456 +            val (_, out_ts''') = split_mode mode args
   6.457 +            val rec_tac = prove_prems2 out_ts''' ps
   6.458 +            val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE)
   6.459 +            val param_derivations = param_derivations_of deriv
   6.460 +            val ho_args = ho_args_of mode args
   6.461 +          in
   6.462 +            print_tac options "before neg prem 2"
   6.463 +            THEN etac @{thm bindE} 1
   6.464 +            THEN (if is_some name then
   6.465 +                full_simp_tac (HOL_basic_ss addsimps
   6.466 +                  [predfun_definition_of ctxt (the name) mode]) 1
   6.467 +                THEN etac @{thm not_predE} 1
   6.468 +                THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1
   6.469 +                THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations))
   6.470 +              else
   6.471 +                etac @{thm not_predE'} 1)
   6.472 +            THEN rec_tac
   6.473 +          end 
   6.474 +        | Sidecond t =>
   6.475 +          etac @{thm bindE} 1
   6.476 +          THEN etac @{thm if_predE} 1
   6.477 +          THEN prove_sidecond2 options ctxt t
   6.478 +          THEN prove_prems2 [] ps)
   6.479 +      in print_tac options "before prove_match2:"
   6.480 +         THEN prove_match2 options ctxt out_ts
   6.481 +         THEN print_tac options "after prove_match2:"
   6.482 +         THEN rest_tac
   6.483 +      end;
   6.484 +    val prems_tac = prove_prems2 in_ts ps 
   6.485 +  in
   6.486 +    print_tac options "starting prove_clause2"
   6.487 +    THEN etac @{thm bindE} 1
   6.488 +    THEN (etac @{thm singleE'} 1)
   6.489 +    THEN (TRY (etac @{thm Pair_inject} 1))
   6.490 +    THEN print_tac options "after singleE':"
   6.491 +    THEN prems_tac
   6.492 +  end;
   6.493 + 
   6.494 +fun prove_other_direction options ctxt pred mode moded_clauses =
   6.495 +  let
   6.496 +    fun prove_clause clause i =
   6.497 +      (if i < length moded_clauses then etac @{thm supE} 1 else all_tac)
   6.498 +      THEN (prove_clause2 options ctxt pred mode clause i)
   6.499 +  in
   6.500 +    (DETERM (TRY (rtac @{thm unit.induct} 1)))
   6.501 +     THEN (REPEAT_DETERM (CHANGED (rewtac @{thm split_paired_all})))
   6.502 +     THEN (rtac (predfun_intro_of ctxt pred mode) 1)
   6.503 +     THEN (REPEAT_DETERM (rtac @{thm refl} 2))
   6.504 +     THEN (if null moded_clauses then
   6.505 +         etac @{thm botE} 1
   6.506 +       else EVERY (map2 prove_clause moded_clauses (1 upto (length moded_clauses))))
   6.507 +  end;
   6.508 +
   6.509 +(** proof procedure **)
   6.510 +
   6.511 +fun prove_pred options thy clauses preds pred (pol, mode) (moded_clauses, compiled_term) =
   6.512 +  let
   6.513 +    val ctxt = ProofContext.init_global thy
   6.514 +    val clauses = case AList.lookup (op =) clauses pred of SOME rs => rs | NONE => []
   6.515 +  in
   6.516 +    Goal.prove ctxt (Term.add_free_names compiled_term []) [] compiled_term
   6.517 +      (if not (skip_proof options) then
   6.518 +        (fn _ =>
   6.519 +        rtac @{thm pred_iffI} 1
   6.520 +        THEN print_tac options "after pred_iffI"
   6.521 +        THEN prove_one_direction options ctxt clauses preds pred mode moded_clauses
   6.522 +        THEN print_tac options "proved one direction"
   6.523 +        THEN prove_other_direction options ctxt pred mode moded_clauses
   6.524 +        THEN print_tac options "proved other direction")
   6.525 +      else (fn _ => Skip_Proof.cheat_tac thy))
   6.526 +  end;
   6.527 +
   6.528 +end;
   6.529 \ No newline at end of file