src/HOL/Statespace/distinct_tree_prover.ML
author hoelzl
Tue Mar 26 12:20:58 2013 +0100 (2013-03-26)
changeset 51526 155263089e7b
parent 45740 132a3e1c0fe5
child 51701 1e29891759c4
permissions -rw-r--r--
move SEQ.thy and Lim.thy to Limits.thy
wenzelm@29269
     1
(*  Title:      HOL/Statespace/distinct_tree_prover.ML
schirmer@25171
     2
    Author:     Norbert Schirmer, TU Muenchen
schirmer@25171
     3
*)
schirmer@25171
     4
schirmer@25408
     5
signature DISTINCT_TREE_PROVER =
schirmer@25408
     6
sig
wenzelm@45355
     7
  datatype direction = Left | Right
wenzelm@29302
     8
  val mk_tree : ('a -> term) -> typ -> 'a list -> term
wenzelm@29302
     9
  val dest_tree : term -> term list
wenzelm@45355
    10
  val find_tree : term -> term -> direction list option
schirmer@25408
    11
wenzelm@29302
    12
  val neq_to_eq_False : thm
wenzelm@45355
    13
  val distinctTreeProver : thm -> direction list -> direction list -> thm
wenzelm@45355
    14
  val neq_x_y : Proof.context -> term -> term -> string -> thm option
wenzelm@29302
    15
  val distinctFieldSolver : string list -> solver
wenzelm@42368
    16
  val distinctTree_tac : string list -> Proof.context -> int -> tactic
wenzelm@29302
    17
  val distinct_implProver : thm -> cterm -> thm
wenzelm@29302
    18
  val subtractProver : term -> cterm -> thm -> thm
wenzelm@29302
    19
  val distinct_simproc : string list -> simproc
wenzelm@45355
    20
wenzelm@29302
    21
  val discharge : thm list -> thm -> thm
schirmer@25408
    22
end;
schirmer@25408
    23
schirmer@25408
    24
structure DistinctTreeProver : DISTINCT_TREE_PROVER =
schirmer@25171
    25
struct
wenzelm@39159
    26
wenzelm@45356
    27
val neq_to_eq_False = @{thm neq_to_eq_False};
schirmer@25171
    28
wenzelm@45355
    29
datatype direction = Left | Right;
schirmer@25408
    30
wenzelm@45355
    31
fun treeT T = Type (@{type_name tree}, [T]);
wenzelm@45740
    32
wenzelm@45355
    33
fun mk_tree' e T n [] = Const (@{const_name Tip}, treeT T)
schirmer@25171
    34
  | mk_tree' e T n xs =
schirmer@25171
    35
     let
schirmer@25171
    36
       val m = (n - 1) div 2;
schirmer@25171
    37
       val (xsl,x::xsr) = chop m xs;
schirmer@25171
    38
       val l = mk_tree' e T m xsl;
schirmer@25171
    39
       val r = mk_tree' e T (n-(m+1)) xsr;
wenzelm@45355
    40
     in
wenzelm@45355
    41
       Const (@{const_name Node}, treeT T --> T --> HOLogic.boolT--> treeT T --> treeT T) $
wenzelm@45740
    42
         l $ e x $ @{term False} $ r
schirmer@25171
    43
     end
schirmer@25171
    44
wenzelm@45355
    45
fun mk_tree e T xs = mk_tree' e T (length xs) xs;
schirmer@25171
    46
wenzelm@45355
    47
fun dest_tree (Const (@{const_name Tip}, _)) = []
wenzelm@45355
    48
  | dest_tree (Const (@{const_name Node}, _) $ l $ e $ _ $ r) = dest_tree l @ e :: dest_tree r
wenzelm@45355
    49
  | dest_tree t = raise TERM ("dest_tree", [t]);
schirmer@25171
    50
schirmer@25408
    51
schirmer@25171
    52
wenzelm@45355
    53
fun lin_find_tree e (Const (@{const_name Tip}, _)) = NONE
wenzelm@45355
    54
  | lin_find_tree e (Const (@{const_name Node}, _) $ l $ x $ _ $ r) =
wenzelm@45355
    55
      if e aconv x
schirmer@25171
    56
      then SOME []
wenzelm@45355
    57
      else
wenzelm@45355
    58
        (case lin_find_tree e l of
wenzelm@45355
    59
          SOME path => SOME (Left :: path)
wenzelm@45355
    60
        | NONE =>
wenzelm@45355
    61
            (case lin_find_tree e r of
wenzelm@45355
    62
              SOME path => SOME (Right :: path)
wenzelm@45355
    63
            | NONE => NONE))
wenzelm@45355
    64
  | lin_find_tree e t = raise TERM ("find_tree: input not a tree", [t])
schirmer@25171
    65
wenzelm@45355
    66
fun bin_find_tree order e (Const (@{const_name Tip}, _)) = NONE
wenzelm@45355
    67
  | bin_find_tree order e (Const (@{const_name Node}, _) $ l $ x $ _ $ r) =
wenzelm@45355
    68
      (case order (e, x) of
wenzelm@45355
    69
        EQUAL => SOME []
wenzelm@45355
    70
      | LESS => Option.map (cons Left) (bin_find_tree order e l)
wenzelm@45355
    71
      | GREATER => Option.map (cons Right) (bin_find_tree order e r))
wenzelm@45355
    72
  | bin_find_tree order e t = raise TERM ("find_tree: input not a tree", [t])
schirmer@25171
    73
schirmer@25171
    74
fun find_tree e t =
wenzelm@35408
    75
  (case bin_find_tree Term_Ord.fast_term_ord e t of
wenzelm@45355
    76
    NONE => lin_find_tree e t
wenzelm@45355
    77
  | x => x);
wenzelm@45355
    78
schirmer@25171
    79
wenzelm@45355
    80
fun index_tree (Const (@{const_name Tip}, _)) path tab = tab
wenzelm@45355
    81
  | index_tree (Const (@{const_name Node}, _) $ l $ x $ _ $ r) path tab =
wenzelm@45355
    82
      tab
wenzelm@45355
    83
      |> Termtab.update_new (x, path)
wenzelm@45355
    84
      |> index_tree l (path @ [Left])
wenzelm@45355
    85
      |> index_tree r (path @ [Right])
wenzelm@45355
    86
  | index_tree t _ _ = raise TERM ("index_tree: input not a tree", [t])
schirmer@25171
    87
wenzelm@45355
    88
fun split_common_prefix xs [] = ([], xs, [])
wenzelm@45355
    89
  | split_common_prefix [] ys = ([], [], ys)
wenzelm@45355
    90
  | split_common_prefix (xs as (x :: xs')) (ys as (y :: ys')) =
wenzelm@45355
    91
      if x = y
wenzelm@45355
    92
      then let val (ps, xs'', ys'') = split_common_prefix xs' ys' in (x :: ps, xs'', ys'') end
wenzelm@45355
    93
      else ([], xs, ys)
schirmer@25171
    94
schirmer@25171
    95
schirmer@25171
    96
(* Wrapper around Thm.instantiate. The type instiations of instTs are applied to
schirmer@25171
    97
 * the right hand sides of insts
schirmer@25171
    98
 *)
schirmer@25171
    99
fun instantiate instTs insts =
schirmer@25171
   100
  let
wenzelm@45355
   101
    val instTs' = map (fn (T, U) => (dest_TVar (typ_of T), typ_of U)) instTs;
schirmer@25171
   102
    fun substT x = (case AList.lookup (op =) instTs' x of NONE => TVar x | SOME T' => T');
schirmer@25171
   103
    fun mapT_and_recertify ct =
schirmer@25171
   104
      let
schirmer@25171
   105
        val thy = theory_of_cterm ct;
schirmer@25171
   106
      in (cterm_of thy (Term.map_types (Term.map_type_tvar substT) (term_of ct))) end;
schirmer@25171
   107
    val insts' = map (apfst mapT_and_recertify) insts;
wenzelm@45355
   108
  in Thm.instantiate (instTs, insts') end;
schirmer@25171
   109
schirmer@25171
   110
fun tvar_clash ixn S S' = raise TYPE ("Type variable " ^
schirmer@25171
   111
  quote (Term.string_of_vname ixn) ^ " has two distinct sorts",
schirmer@25171
   112
  [TVar (ixn, S), TVar (ixn, S')], []);
schirmer@25171
   113
schirmer@25171
   114
fun lookup (tye, (ixn, S)) =
schirmer@25171
   115
  (case AList.lookup (op =) tye ixn of
schirmer@25171
   116
    NONE => NONE
schirmer@25171
   117
  | SOME (S', T) => if S = S' then SOME T else tvar_clash ixn S S');
schirmer@25171
   118
schirmer@25171
   119
val naive_typ_match =
schirmer@25171
   120
  let
schirmer@25171
   121
    fun match (TVar (v, S), T) subs =
schirmer@25171
   122
          (case lookup (subs, (v, S)) of
schirmer@25171
   123
            NONE => ((v, (S, T))::subs)
schirmer@25171
   124
          | SOME _ => subs)
schirmer@25171
   125
      | match (Type (a, Ts), Type (b, Us)) subs =
schirmer@25171
   126
          if a <> b then raise Type.TYPE_MATCH
schirmer@25171
   127
          else matches (Ts, Us) subs
schirmer@25171
   128
      | match (TFree x, TFree y) subs =
schirmer@25171
   129
          if x = y then subs else raise Type.TYPE_MATCH
schirmer@25171
   130
      | match _ _ = raise Type.TYPE_MATCH
schirmer@25171
   131
    and matches (T :: Ts, U :: Us) subs = matches (Ts, Us) (match (T, U) subs)
schirmer@25171
   132
      | matches _ subs = subs;
schirmer@25171
   133
  in match end;
schirmer@25171
   134
schirmer@25171
   135
wenzelm@45355
   136
(* expects that relevant type variables are already contained in
schirmer@25171
   137
 * term variables. First instantiation of variables is returned without further
schirmer@25171
   138
 * checking.
schirmer@25171
   139
 *)
wenzelm@45355
   140
fun naive_cterm_first_order_match (t, ct) env =
schirmer@25171
   141
  let
wenzelm@45355
   142
    val thy = theory_of_cterm ct;
wenzelm@45355
   143
    fun mtch (env as (tyinsts, insts)) =
wenzelm@45355
   144
      fn (Var (ixn, T), ct) =>
wenzelm@45355
   145
          (case AList.lookup (op =) insts ixn of
wenzelm@45355
   146
            NONE => (naive_typ_match (T, typ_of (ctyp_of_term ct)) tyinsts, (ixn, ct) :: insts)
wenzelm@45355
   147
          | SOME _ => env)
wenzelm@45355
   148
       | (f $ t, ct) =>
wenzelm@45355
   149
          let val (cf, ct') = Thm.dest_comb ct;
wenzelm@45355
   150
          in mtch (mtch env (f, cf)) (t, ct') end
wenzelm@45355
   151
       | _ => env;
wenzelm@45355
   152
  in mtch env (t, ct) end;
schirmer@25171
   153
schirmer@25171
   154
schirmer@25171
   155
fun discharge prems rule =
schirmer@25171
   156
  let
wenzelm@45355
   157
    val thy = theory_of_thm (hd prems);
wenzelm@45355
   158
    val (tyinsts,insts) =
wenzelm@45355
   159
      fold naive_cterm_first_order_match (prems_of rule ~~ map cprop_of prems) ([], []);
schirmer@25171
   160
wenzelm@45355
   161
    val tyinsts' =
wenzelm@45355
   162
      map (fn (v, (S, U)) => (ctyp_of thy (TVar (v, S)), ctyp_of thy U)) tyinsts;
wenzelm@45355
   163
    val insts' =
wenzelm@45355
   164
      map (fn (idxn, ct) => (cterm_of thy (Var (idxn, typ_of (ctyp_of_term ct))), ct)) insts;
wenzelm@45355
   165
    val rule' = Thm.instantiate (tyinsts', insts') rule;
wenzelm@45355
   166
  in fold Thm.elim_implies prems rule' end;
schirmer@25171
   167
schirmer@25171
   168
local
schirmer@25171
   169
wenzelm@45355
   170
val (l_in_set_root, x_in_set_root, r_in_set_root) =
wenzelm@45355
   171
  let
wenzelm@45355
   172
    val (Node_l_x_d, r) =
wenzelm@45356
   173
      cprop_of @{thm in_set_root}
wenzelm@45355
   174
      |> Thm.dest_comb |> #2
wenzelm@45355
   175
      |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb;
wenzelm@45355
   176
    val (Node_l, x) = Node_l_x_d |> Thm.dest_comb |> #1 |> Thm.dest_comb;
wenzelm@45355
   177
    val l = Node_l |> Thm.dest_comb |> #2;
wenzelm@45355
   178
  in (l,x,r) end;
schirmer@25171
   179
wenzelm@45355
   180
val (x_in_set_left, r_in_set_left) =
wenzelm@45355
   181
  let
wenzelm@45355
   182
    val (Node_l_x_d, r) =
wenzelm@45356
   183
      cprop_of @{thm in_set_left}
wenzelm@45355
   184
      |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
wenzelm@45355
   185
      |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb;
wenzelm@45355
   186
    val x = Node_l_x_d |> Thm.dest_comb |> #1 |> Thm.dest_comb |> #2;
wenzelm@45355
   187
  in (x, r) end;
wenzelm@45355
   188
wenzelm@45355
   189
val (x_in_set_right, l_in_set_right) =
wenzelm@45355
   190
  let
wenzelm@45355
   191
    val (Node_l, x) =
wenzelm@45356
   192
      cprop_of @{thm in_set_right}
wenzelm@45355
   193
      |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
wenzelm@45355
   194
      |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
wenzelm@45355
   195
      |> Thm.dest_comb |> #1 |> Thm.dest_comb |> #1
wenzelm@45355
   196
      |> Thm.dest_comb;
wenzelm@45355
   197
    val l = Node_l |> Thm.dest_comb |> #2;
wenzelm@45355
   198
  in (x, l) end;
schirmer@25171
   199
schirmer@25171
   200
in
schirmer@25171
   201
(*
schirmer@25171
   202
1. First get paths x_path y_path of x and y in the tree.
schirmer@25171
   203
2. For the common prefix descend into the tree according to the path
schirmer@25171
   204
   and lemmas all_distinct_left/right
schirmer@25171
   205
3. If one restpath is empty use distinct_left/right,
schirmer@25171
   206
   otherwise all_distinct_left_right
schirmer@25171
   207
*)
schirmer@25171
   208
schirmer@25171
   209
fun distinctTreeProver dist_thm x_path y_path =
schirmer@25171
   210
  let
schirmer@25171
   211
    fun dist_subtree [] thm = thm
wenzelm@45355
   212
      | dist_subtree (p :: ps) thm =
wenzelm@45355
   213
         let
wenzelm@45356
   214
           val rule =
wenzelm@45356
   215
            (case p of Left => @{thm all_distinct_left} | Right => @{thm all_distinct_right})
schirmer@25171
   216
         in dist_subtree ps (discharge [thm] rule) end;
schirmer@25171
   217
wenzelm@45355
   218
    val (ps, x_rest, y_rest) = split_common_prefix x_path y_path;
schirmer@25171
   219
    val dist_subtree_thm = dist_subtree ps dist_thm;
schirmer@25171
   220
    val subtree = cprop_of dist_subtree_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
wenzelm@45355
   221
    val (_, [l, _, _, r]) = Drule.strip_comb subtree;
wenzelm@45355
   222
schirmer@25171
   223
    fun in_set ps tree =
schirmer@25171
   224
      let
wenzelm@45355
   225
        val (_, [l, x, _, r]) = Drule.strip_comb tree;
schirmer@25171
   226
        val xT = ctyp_of_term x;
wenzelm@45355
   227
      in
wenzelm@45355
   228
        (case ps of
wenzelm@45355
   229
          [] =>
wenzelm@45355
   230
            instantiate
wenzelm@45355
   231
              [(ctyp_of_term x_in_set_root, xT)]
wenzelm@45356
   232
              [(l_in_set_root, l), (x_in_set_root, x), (r_in_set_root, r)] @{thm in_set_root}
wenzelm@45355
   233
        | Left :: ps' =>
wenzelm@45355
   234
            let
wenzelm@45355
   235
              val in_set_l = in_set ps' l;
wenzelm@45355
   236
              val in_set_left' =
wenzelm@45355
   237
                instantiate
wenzelm@45355
   238
                  [(ctyp_of_term x_in_set_left, xT)]
wenzelm@45356
   239
                  [(x_in_set_left, x), (r_in_set_left, r)] @{thm in_set_left};
wenzelm@45355
   240
            in discharge [in_set_l] in_set_left' end
wenzelm@45355
   241
        | Right :: ps' =>
wenzelm@45355
   242
            let
wenzelm@45355
   243
              val in_set_r = in_set ps' r;
wenzelm@45355
   244
              val in_set_right' =
wenzelm@45355
   245
                instantiate
wenzelm@45355
   246
                  [(ctyp_of_term x_in_set_right, xT)]
wenzelm@45356
   247
                  [(x_in_set_right, x), (l_in_set_right, l)] @{thm in_set_right};
wenzelm@45355
   248
            in discharge [in_set_r] in_set_right' end)
wenzelm@45355
   249
      end;
schirmer@25171
   250
wenzelm@45355
   251
  fun in_set' [] = raise TERM ("distinctTreeProver", [])
wenzelm@45355
   252
    | in_set' (Left :: ps) = in_set ps l
wenzelm@45355
   253
    | in_set' (Right :: ps) = in_set ps r;
wenzelm@45355
   254
wenzelm@45356
   255
  fun distinct_lr node_in_set Left = discharge [dist_subtree_thm, node_in_set] @{thm distinct_left}
wenzelm@45356
   256
    | distinct_lr node_in_set Right = discharge [dist_subtree_thm, node_in_set] @{thm distinct_right}
schirmer@25171
   257
wenzelm@45355
   258
  val (swap, neq) =
wenzelm@45355
   259
    (case x_rest of
wenzelm@45355
   260
      [] =>
wenzelm@45355
   261
        let val y_in_set = in_set' y_rest;
wenzelm@45355
   262
        in (false, distinct_lr y_in_set (hd y_rest)) end
wenzelm@45355
   263
    | xr :: xrs =>
wenzelm@45355
   264
        (case y_rest of
wenzelm@45355
   265
          [] =>
wenzelm@45355
   266
            let val x_in_set = in_set' x_rest;
wenzelm@45355
   267
            in (true, distinct_lr x_in_set (hd x_rest)) end
wenzelm@45355
   268
        | yr :: yrs =>
wenzelm@45355
   269
            let
wenzelm@45355
   270
              val x_in_set = in_set' x_rest;
wenzelm@45355
   271
              val y_in_set = in_set' y_rest;
wenzelm@45355
   272
            in
wenzelm@45355
   273
              (case xr of
wenzelm@45356
   274
                Left =>
wenzelm@45356
   275
                  (false, discharge [dist_subtree_thm, x_in_set, y_in_set] @{thm distinct_left_right})
wenzelm@45356
   276
              | Right =>
wenzelm@45356
   277
                  (true, discharge [dist_subtree_thm, y_in_set, x_in_set] @{thm distinct_left_right}))
wenzelm@45355
   278
           end));
wenzelm@45356
   279
  in if swap then discharge [neq] @{thm swap_neq} else neq end;
schirmer@25171
   280
schirmer@25171
   281
wenzelm@45356
   282
fun deleteProver dist_thm [] = @{thm delete_root} OF [dist_thm]
schirmer@25171
   283
  | deleteProver dist_thm (p::ps) =
wenzelm@45355
   284
      let
wenzelm@45356
   285
        val dist_rule =
wenzelm@45356
   286
          (case p of Left => @{thm all_distinct_left} | Right => @{thm all_distinct_right});
wenzelm@45355
   287
        val dist_thm' = discharge [dist_thm] dist_rule;
wenzelm@45356
   288
        val del_rule = (case p of Left => @{thm delete_left} | Right => @{thm delete_right});
wenzelm@45355
   289
        val del = deleteProver dist_thm' ps;
wenzelm@45355
   290
      in discharge [dist_thm, del] del_rule end;
schirmer@25171
   291
schirmer@25171
   292
local
wenzelm@45355
   293
  val (alpha, v) =
schirmer@25171
   294
    let
wenzelm@45355
   295
      val ct =
wenzelm@45356
   296
        @{thm subtract_Tip} |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
wenzelm@45355
   297
        |> Thm.dest_comb |> #2;
schirmer@25171
   298
      val [alpha] = ct |> Thm.ctyp_of_term |> Thm.dest_ctyp;
schirmer@25171
   299
    in (alpha, #1 (dest_Var (term_of ct))) end;
schirmer@25171
   300
in
schirmer@25171
   301
wenzelm@45355
   302
fun subtractProver (Const (@{const_name Tip}, T)) ct dist_thm =
wenzelm@45355
   303
      let
wenzelm@45355
   304
        val ct' = dist_thm |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
wenzelm@45355
   305
        val thy = theory_of_cterm ct;
wenzelm@45355
   306
        val [alphaI] = #2 (dest_Type T);
wenzelm@45355
   307
      in
wenzelm@45355
   308
        Thm.instantiate
wenzelm@45355
   309
          ([(alpha, ctyp_of thy alphaI)],
wenzelm@45356
   310
           [(cterm_of thy (Var (v, treeT alphaI)), ct')]) @{thm subtract_Tip}
wenzelm@45355
   311
      end
wenzelm@45355
   312
  | subtractProver (Const (@{const_name Node}, nT) $ l $ x $ d $ r) ct dist_thm =
wenzelm@45355
   313
      let
wenzelm@45355
   314
        val ct' = dist_thm |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
wenzelm@45355
   315
        val (_, [cl, _, _, cr]) = Drule.strip_comb ct;
wenzelm@45355
   316
        val ps = the (find_tree x (term_of ct'));
wenzelm@45355
   317
        val del_tree = deleteProver dist_thm ps;
wenzelm@45356
   318
        val dist_thm' = discharge [del_tree, dist_thm] @{thm delete_Some_all_distinct};
wenzelm@45355
   319
        val sub_l = subtractProver (term_of cl) cl (dist_thm');
wenzelm@45355
   320
        val sub_r =
wenzelm@45355
   321
          subtractProver (term_of cr) cr
wenzelm@45356
   322
            (discharge [sub_l, dist_thm'] @{thm subtract_Some_all_distinct_res});
wenzelm@45356
   323
      in discharge [del_tree, sub_l, sub_r] @{thm subtract_Node} end;
wenzelm@45355
   324
wenzelm@45355
   325
end;
wenzelm@45355
   326
schirmer@25171
   327
fun distinct_implProver dist_thm ct =
schirmer@25171
   328
  let
schirmer@25171
   329
    val ctree = ct |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
schirmer@25171
   330
    val sub = subtractProver (term_of ctree) ctree dist_thm;
wenzelm@45356
   331
  in @{thm subtract_Some_all_distinct} OF [sub, dist_thm] end;
schirmer@25171
   332
schirmer@25171
   333
fun get_fst_success f [] = NONE
wenzelm@45355
   334
  | get_fst_success f (x :: xs) =
wenzelm@45355
   335
      (case f x of
wenzelm@45355
   336
        NONE => get_fst_success f xs
wenzelm@45355
   337
      | SOME v => SOME v);
schirmer@25171
   338
schirmer@25171
   339
fun neq_x_y ctxt x y name =
schirmer@25171
   340
  (let
wenzelm@42361
   341
    val dist_thm = the (try (Proof_Context.get_thm ctxt) name);
schirmer@25171
   342
    val ctree = cprop_of dist_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
schirmer@25171
   343
    val tree = term_of ctree;
schirmer@25171
   344
    val x_path = the (find_tree x tree);
schirmer@25171
   345
    val y_path = the (find_tree y tree);
schirmer@25171
   346
    val thm = distinctTreeProver dist_thm x_path y_path;
wenzelm@45355
   347
  in SOME thm
wenzelm@45355
   348
  end handle Option.Option => NONE);
schirmer@25171
   349
wenzelm@42368
   350
fun distinctTree_tac names ctxt = SUBGOAL (fn (goal, i) =>
wenzelm@42368
   351
    (case goal of
wenzelm@42368
   352
      Const (@{const_name Trueprop}, _) $
wenzelm@42368
   353
          (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ x $ y)) =>
wenzelm@42368
   354
        (case get_fst_success (neq_x_y ctxt x y) names of
wenzelm@42368
   355
          SOME neq => rtac neq i
wenzelm@42368
   356
        | NONE => no_tac)
wenzelm@42368
   357
    | _ => no_tac))
schirmer@25171
   358
wenzelm@45355
   359
fun distinctFieldSolver names =
wenzelm@45355
   360
  mk_solver "distinctFieldSolver" (distinctTree_tac names o Simplifier.the_context);
schirmer@25171
   361
schirmer@25171
   362
fun distinct_simproc names =
wenzelm@38715
   363
  Simplifier.simproc_global @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"]
wenzelm@45355
   364
    (fn thy => fn ss => fn (Const (@{const_name HOL.eq}, _) $ x $ y) =>
wenzelm@45355
   365
      (case try Simplifier.the_context ss of
wenzelm@45355
   366
        SOME ctxt =>
wenzelm@45356
   367
          Option.map (fn neq => @{thm neq_to_eq_False} OF [neq])
wenzelm@45355
   368
            (get_fst_success (neq_x_y ctxt x y) names)
wenzelm@45355
   369
      | NONE => NONE));
schirmer@25171
   370
wenzelm@45355
   371
end;
wenzelm@45355
   372
schirmer@25171
   373
end;