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