src/HOL/Statespace/distinct_tree_prover.ML
changeset 45355 c0704e988526
parent 43596 78211f66cf8d
child 45356 e79402612266
     1.1 --- a/src/HOL/Statespace/distinct_tree_prover.ML	Sun Nov 06 13:25:41 2011 +0100
     1.2 +++ b/src/HOL/Statespace/distinct_tree_prover.ML	Sun Nov 06 14:09:24 2011 +0100
     1.3 @@ -4,20 +4,20 @@
     1.4  
     1.5  signature DISTINCT_TREE_PROVER =
     1.6  sig
     1.7 -  datatype Direction = Left | Right
     1.8 +  datatype direction = Left | Right
     1.9    val mk_tree : ('a -> term) -> typ -> 'a list -> term
    1.10    val dest_tree : term -> term list
    1.11 -  val find_tree : term -> term -> Direction list option 
    1.12 +  val find_tree : term -> term -> direction list option
    1.13  
    1.14    val neq_to_eq_False : thm
    1.15 -  val distinctTreeProver : thm -> Direction list -> Direction list -> thm
    1.16 -  val neq_x_y : Proof.context -> term -> term -> string -> thm option   
    1.17 +  val distinctTreeProver : thm -> direction list -> direction list -> thm
    1.18 +  val neq_x_y : Proof.context -> term -> term -> string -> thm option
    1.19    val distinctFieldSolver : string list -> solver
    1.20    val distinctTree_tac : string list -> Proof.context -> int -> tactic
    1.21    val distinct_implProver : thm -> cterm -> thm
    1.22    val subtractProver : term -> cterm -> thm -> thm
    1.23    val distinct_simproc : string list -> simproc
    1.24 -  
    1.25 +
    1.26    val discharge : thm list -> thm -> thm
    1.27  end;
    1.28  
    1.29 @@ -37,68 +37,70 @@
    1.30  val swap_neq = @{thm DistinctTreeProver.swap_neq};
    1.31  val neq_to_eq_False = @{thm DistinctTreeProver.neq_to_eq_False};
    1.32  
    1.33 -datatype Direction = Left | Right 
    1.34 +datatype direction = Left | Right;
    1.35  
    1.36 -fun treeT T = Type ("DistinctTreeProver.tree",[T]);
    1.37 -fun mk_tree' e T n []     = Const ("DistinctTreeProver.tree.Tip",treeT T)
    1.38 +fun treeT T = Type (@{type_name tree}, [T]);
    1.39 +fun mk_tree' e T n [] = Const (@{const_name Tip}, treeT T)
    1.40    | mk_tree' e T n xs =
    1.41       let
    1.42         val m = (n - 1) div 2;
    1.43         val (xsl,x::xsr) = chop m xs;
    1.44         val l = mk_tree' e T m xsl;
    1.45         val r = mk_tree' e T (n-(m+1)) xsr;
    1.46 -     in Const ("DistinctTreeProver.tree.Node",
    1.47 -                treeT T --> T --> HOLogic.boolT--> treeT T --> treeT T) $ 
    1.48 -          l$ e x $ HOLogic.false_const $ r 
    1.49 +     in
    1.50 +       Const (@{const_name Node}, treeT T --> T --> HOLogic.boolT--> treeT T --> treeT T) $
    1.51 +         l $ e x $ HOLogic.false_const $ r
    1.52       end
    1.53  
    1.54 -fun mk_tree e T xs = mk_tree' e T (length xs) xs;         
    1.55 +fun mk_tree e T xs = mk_tree' e T (length xs) xs;
    1.56  
    1.57 -fun dest_tree (Const ("DistinctTreeProver.tree.Tip",_)) = []
    1.58 -  | dest_tree (Const ("DistinctTreeProver.tree.Node",_)$l$e$_$r) = dest_tree l @ e :: dest_tree r
    1.59 -  | dest_tree t = raise TERM ("DistinctTreeProver.dest_tree",[t]);
    1.60 +fun dest_tree (Const (@{const_name Tip}, _)) = []
    1.61 +  | dest_tree (Const (@{const_name Node}, _) $ l $ e $ _ $ r) = dest_tree l @ e :: dest_tree r
    1.62 +  | dest_tree t = raise TERM ("dest_tree", [t]);
    1.63  
    1.64  
    1.65  
    1.66 -fun lin_find_tree e (Const ("DistinctTreeProver.tree.Tip",_)) = NONE
    1.67 -  | lin_find_tree e (Const ("DistinctTreeProver.tree.Node",_) $ l$ x $ _ $ r) =
    1.68 -      if e aconv x 
    1.69 +fun lin_find_tree e (Const (@{const_name Tip}, _)) = NONE
    1.70 +  | lin_find_tree e (Const (@{const_name Node}, _) $ l $ x $ _ $ r) =
    1.71 +      if e aconv x
    1.72        then SOME []
    1.73 -      else (case lin_find_tree e l of
    1.74 -              SOME path => SOME (Left::path)
    1.75 -            | NONE => (case lin_find_tree e r of
    1.76 -                        SOME path => SOME (Right::path)
    1.77 -                       | NONE => NONE))
    1.78 -  | lin_find_tree e t = raise TERM ("find_tree: input not a tree",[t])
    1.79 +      else
    1.80 +        (case lin_find_tree e l of
    1.81 +          SOME path => SOME (Left :: path)
    1.82 +        | NONE =>
    1.83 +            (case lin_find_tree e r of
    1.84 +              SOME path => SOME (Right :: path)
    1.85 +            | NONE => NONE))
    1.86 +  | lin_find_tree e t = raise TERM ("find_tree: input not a tree", [t])
    1.87  
    1.88 -fun bin_find_tree order e (Const ("DistinctTreeProver.tree.Tip",_)) = NONE
    1.89 -  | bin_find_tree order e (Const ("DistinctTreeProver.tree.Node",_) $ l$ x $ _ $ r) =
    1.90 -      (case order (e,x) of
    1.91 -         EQUAL => SOME []
    1.92 -       | LESS => Option.map (cons Left) (bin_find_tree order e l)
    1.93 -       | GREATER => Option.map (cons Right) (bin_find_tree order e r))
    1.94 -  | bin_find_tree order e t = raise TERM ("find_tree: input not a tree",[t])
    1.95 +fun bin_find_tree order e (Const (@{const_name Tip}, _)) = NONE
    1.96 +  | bin_find_tree order e (Const (@{const_name Node}, _) $ l $ x $ _ $ r) =
    1.97 +      (case order (e, x) of
    1.98 +        EQUAL => SOME []
    1.99 +      | LESS => Option.map (cons Left) (bin_find_tree order e l)
   1.100 +      | GREATER => Option.map (cons Right) (bin_find_tree order e r))
   1.101 +  | bin_find_tree order e t = raise TERM ("find_tree: input not a tree", [t])
   1.102  
   1.103  fun find_tree e t =
   1.104    (case bin_find_tree Term_Ord.fast_term_ord e t of
   1.105 -     NONE => lin_find_tree e t
   1.106 -   | x => x);
   1.107 +    NONE => lin_find_tree e t
   1.108 +  | x => x);
   1.109 +
   1.110  
   1.111 - 
   1.112 -fun index_tree (Const ("DistinctTreeProver.tree.Tip",_)) path tab = tab
   1.113 -  | index_tree (Const ("DistinctTreeProver.tree.Node",_) $ l$ x $ _ $ r) path tab =
   1.114 -      tab 
   1.115 -      |> Termtab.update_new (x,path) 
   1.116 -      |> index_tree l (path@[Left])
   1.117 -      |> index_tree r (path@[Right])
   1.118 -  | index_tree t _ _ = raise TERM ("index_tree: input not a tree",[t])
   1.119 +fun index_tree (Const (@{const_name Tip}, _)) path tab = tab
   1.120 +  | index_tree (Const (@{const_name Node}, _) $ l $ x $ _ $ r) path tab =
   1.121 +      tab
   1.122 +      |> Termtab.update_new (x, path)
   1.123 +      |> index_tree l (path @ [Left])
   1.124 +      |> index_tree r (path @ [Right])
   1.125 +  | index_tree t _ _ = raise TERM ("index_tree: input not a tree", [t])
   1.126  
   1.127 -fun split_common_prefix xs [] = ([],xs,[])
   1.128 -  | split_common_prefix [] ys = ([],[],ys)
   1.129 -  | split_common_prefix (xs as (x::xs')) (ys as (y::ys')) =
   1.130 -     if x=y 
   1.131 -     then let val (ps,xs'',ys'') = split_common_prefix xs' ys' in (x::ps,xs'',ys'') end
   1.132 -     else ([],xs,ys)
   1.133 +fun split_common_prefix xs [] = ([], xs, [])
   1.134 +  | split_common_prefix [] ys = ([], [], ys)
   1.135 +  | split_common_prefix (xs as (x :: xs')) (ys as (y :: ys')) =
   1.136 +      if x = y
   1.137 +      then let val (ps, xs'', ys'') = split_common_prefix xs' ys' in (x :: ps, xs'', ys'') end
   1.138 +      else ([], xs, ys)
   1.139  
   1.140  
   1.141  (* Wrapper around Thm.instantiate. The type instiations of instTs are applied to
   1.142 @@ -106,14 +108,14 @@
   1.143   *)
   1.144  fun instantiate instTs insts =
   1.145    let
   1.146 -    val instTs' = map (fn (T,U) => (dest_TVar (typ_of T),typ_of U)) instTs;
   1.147 +    val instTs' = map (fn (T, U) => (dest_TVar (typ_of T), typ_of U)) instTs;
   1.148      fun substT x = (case AList.lookup (op =) instTs' x of NONE => TVar x | SOME T' => T');
   1.149      fun mapT_and_recertify ct =
   1.150        let
   1.151          val thy = theory_of_cterm ct;
   1.152        in (cterm_of thy (Term.map_types (Term.map_type_tvar substT) (term_of ct))) end;
   1.153      val insts' = map (apfst mapT_and_recertify) insts;
   1.154 -  in Thm.instantiate (instTs,insts') end;
   1.155 +  in Thm.instantiate (instTs, insts') end;
   1.156  
   1.157  fun tvar_clash ixn S S' = raise TYPE ("Type variable " ^
   1.158    quote (Term.string_of_vname ixn) ^ " has two distinct sorts",
   1.159 @@ -141,62 +143,69 @@
   1.160    in match end;
   1.161  
   1.162  
   1.163 -(* expects that relevant type variables are already contained in 
   1.164 +(* expects that relevant type variables are already contained in
   1.165   * term variables. First instantiation of variables is returned without further
   1.166   * checking.
   1.167   *)
   1.168 -fun naive_cterm_first_order_match (t,ct) env =
   1.169 +fun naive_cterm_first_order_match (t, ct) env =
   1.170    let
   1.171 -    val thy = (theory_of_cterm ct);
   1.172 -    fun mtch (env as (tyinsts,insts)) = fn
   1.173 -         (Var(ixn,T),ct) =>
   1.174 -           (case AList.lookup (op =) insts ixn of
   1.175 -             NONE => (naive_typ_match (T,typ_of (ctyp_of_term ct)) tyinsts,
   1.176 -                      (ixn, ct)::insts)
   1.177 -            | SOME _ => env)
   1.178 -        | (f$t,ct) => let val (cf,ct') = Thm.dest_comb ct;
   1.179 -                      in mtch (mtch env (f,cf)) (t,ct') end
   1.180 -        | _ => env
   1.181 -  in mtch env (t,ct) end;
   1.182 +    val thy = theory_of_cterm ct;
   1.183 +    fun mtch (env as (tyinsts, insts)) =
   1.184 +      fn (Var (ixn, T), ct) =>
   1.185 +          (case AList.lookup (op =) insts ixn of
   1.186 +            NONE => (naive_typ_match (T, typ_of (ctyp_of_term ct)) tyinsts, (ixn, ct) :: insts)
   1.187 +          | SOME _ => env)
   1.188 +       | (f $ t, ct) =>
   1.189 +          let val (cf, ct') = Thm.dest_comb ct;
   1.190 +          in mtch (mtch env (f, cf)) (t, ct') end
   1.191 +       | _ => env;
   1.192 +  in mtch env (t, ct) end;
   1.193  
   1.194  
   1.195  fun discharge prems rule =
   1.196    let
   1.197 -     val thy = theory_of_thm (hd prems);
   1.198 -     val (tyinsts,insts) =  
   1.199 -           fold naive_cterm_first_order_match (prems_of rule ~~ map cprop_of prems) ([],[]);
   1.200 +    val thy = theory_of_thm (hd prems);
   1.201 +    val (tyinsts,insts) =
   1.202 +      fold naive_cterm_first_order_match (prems_of rule ~~ map cprop_of prems) ([], []);
   1.203  
   1.204 -     val tyinsts' = map (fn (v,(S,U)) => (ctyp_of thy (TVar (v,S)),ctyp_of thy U)) 
   1.205 -                     tyinsts;
   1.206 -     val insts' = map (fn (idxn,ct) => (cterm_of thy (Var (idxn,typ_of (ctyp_of_term ct))),ct))  
   1.207 -                     insts;
   1.208 -     val rule' = Thm.instantiate (tyinsts',insts') rule;
   1.209 -   in fold Thm.elim_implies prems rule' end;
   1.210 +    val tyinsts' =
   1.211 +      map (fn (v, (S, U)) => (ctyp_of thy (TVar (v, S)), ctyp_of thy U)) tyinsts;
   1.212 +    val insts' =
   1.213 +      map (fn (idxn, ct) => (cterm_of thy (Var (idxn, typ_of (ctyp_of_term ct))), ct)) insts;
   1.214 +    val rule' = Thm.instantiate (tyinsts', insts') rule;
   1.215 +  in fold Thm.elim_implies prems rule' end;
   1.216  
   1.217  local
   1.218  
   1.219 -val (l_in_set_root,x_in_set_root,r_in_set_root) =
   1.220 -  let val (Node_l_x_d,r) = (cprop_of in_set_root) 
   1.221 -                         |> Thm.dest_comb |> #2 
   1.222 -                         |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb;
   1.223 -      val (Node_l,x) = Node_l_x_d |> Thm.dest_comb |> #1 |> Thm.dest_comb;
   1.224 -      val l = Node_l |> Thm.dest_comb |> #2;
   1.225 -  in (l,x,r) end
   1.226 -val (x_in_set_left,r_in_set_left) = 
   1.227 -  let val (Node_l_x_d,r) = (cprop_of in_set_left) 
   1.228 -                         |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
   1.229 -                         |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb;
   1.230 -      val x = Node_l_x_d |> Thm.dest_comb |> #1 |> Thm.dest_comb |> #2;
   1.231 -  in (x,r) end
   1.232 +val (l_in_set_root, x_in_set_root, r_in_set_root) =
   1.233 +  let
   1.234 +    val (Node_l_x_d, r) =
   1.235 +      cprop_of in_set_root
   1.236 +      |> Thm.dest_comb |> #2
   1.237 +      |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb;
   1.238 +    val (Node_l, x) = Node_l_x_d |> Thm.dest_comb |> #1 |> Thm.dest_comb;
   1.239 +    val l = Node_l |> Thm.dest_comb |> #2;
   1.240 +  in (l,x,r) end;
   1.241  
   1.242 -val (x_in_set_right,l_in_set_right) = 
   1.243 -  let val (Node_l,x) = (cprop_of in_set_right) 
   1.244 -                         |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
   1.245 -                         |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 
   1.246 -                         |> Thm.dest_comb |> #1 |> Thm.dest_comb |> #1 
   1.247 -                         |> Thm.dest_comb
   1.248 -      val l = Node_l |> Thm.dest_comb |> #2;
   1.249 -  in (x,l) end
   1.250 +val (x_in_set_left, r_in_set_left) =
   1.251 +  let
   1.252 +    val (Node_l_x_d, r) =
   1.253 +      cprop_of in_set_left
   1.254 +      |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
   1.255 +      |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb;
   1.256 +    val x = Node_l_x_d |> Thm.dest_comb |> #1 |> Thm.dest_comb |> #2;
   1.257 +  in (x, r) end;
   1.258 +
   1.259 +val (x_in_set_right, l_in_set_right) =
   1.260 +  let
   1.261 +    val (Node_l, x) =
   1.262 +      cprop_of in_set_right
   1.263 +      |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
   1.264 +      |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
   1.265 +      |> Thm.dest_comb |> #1 |> Thm.dest_comb |> #1
   1.266 +      |> Thm.dest_comb;
   1.267 +    val l = Node_l |> Thm.dest_comb |> #2;
   1.268 +  in (x, l) end;
   1.269  
   1.270  in
   1.271  (*
   1.272 @@ -210,118 +219,128 @@
   1.273  fun distinctTreeProver dist_thm x_path y_path =
   1.274    let
   1.275      fun dist_subtree [] thm = thm
   1.276 -      | dist_subtree (p::ps) thm =
   1.277 -         let 
   1.278 +      | dist_subtree (p :: ps) thm =
   1.279 +         let
   1.280             val rule = (case p of Left => all_distinct_left | Right => all_distinct_right)
   1.281           in dist_subtree ps (discharge [thm] rule) end;
   1.282  
   1.283 -    val (ps,x_rest,y_rest) = split_common_prefix x_path y_path;
   1.284 +    val (ps, x_rest, y_rest) = split_common_prefix x_path y_path;
   1.285      val dist_subtree_thm = dist_subtree ps dist_thm;
   1.286      val subtree = cprop_of dist_subtree_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
   1.287 -    val (_,[l,_,_,r]) = Drule.strip_comb subtree;
   1.288 -    
   1.289 +    val (_, [l, _, _, r]) = Drule.strip_comb subtree;
   1.290 +
   1.291      fun in_set ps tree =
   1.292        let
   1.293 -        val (_,[l,x,_,r]) = Drule.strip_comb tree;
   1.294 +        val (_, [l, x, _, r]) = Drule.strip_comb tree;
   1.295          val xT = ctyp_of_term x;
   1.296 -      in (case ps of
   1.297 -            [] => instantiate 
   1.298 -                    [(ctyp_of_term x_in_set_root,xT)]
   1.299 -                    [(l_in_set_root,l),(x_in_set_root,x),(r_in_set_root,r)] in_set_root
   1.300 -          | (Left::ps') => 
   1.301 -               let
   1.302 -                  val in_set_l = in_set ps' l;
   1.303 -                  val in_set_left' = instantiate [(ctyp_of_term x_in_set_left,xT)]
   1.304 -                                      [(x_in_set_left,x),(r_in_set_left,r)] in_set_left;
   1.305 -               in discharge [in_set_l] in_set_left' end
   1.306 -          | (Right::ps') => 
   1.307 -               let
   1.308 -                  val in_set_r = in_set ps' r;
   1.309 -                  val in_set_right' = instantiate [(ctyp_of_term x_in_set_right,xT)] 
   1.310 -                                      [(x_in_set_right,x),(l_in_set_right,l)] in_set_right;
   1.311 -               in discharge [in_set_r] in_set_right' end)
   1.312 -      end 
   1.313 -       
   1.314 -  fun in_set' [] = raise TERM ("distinctTreeProver",[])
   1.315 -    | in_set' (Left::ps) = in_set ps l
   1.316 -    | in_set' (Right::ps) = in_set ps r;
   1.317 +      in
   1.318 +        (case ps of
   1.319 +          [] =>
   1.320 +            instantiate
   1.321 +              [(ctyp_of_term x_in_set_root, xT)]
   1.322 +              [(l_in_set_root, l), (x_in_set_root, x), (r_in_set_root, r)] in_set_root
   1.323 +        | Left :: ps' =>
   1.324 +            let
   1.325 +              val in_set_l = in_set ps' l;
   1.326 +              val in_set_left' =
   1.327 +                instantiate
   1.328 +                  [(ctyp_of_term x_in_set_left, xT)]
   1.329 +                  [(x_in_set_left, x), (r_in_set_left, r)] in_set_left;
   1.330 +            in discharge [in_set_l] in_set_left' end
   1.331 +        | Right :: ps' =>
   1.332 +            let
   1.333 +              val in_set_r = in_set ps' r;
   1.334 +              val in_set_right' =
   1.335 +                instantiate
   1.336 +                  [(ctyp_of_term x_in_set_right, xT)]
   1.337 +                  [(x_in_set_right, x), (l_in_set_right, l)] in_set_right;
   1.338 +            in discharge [in_set_r] in_set_right' end)
   1.339 +      end;
   1.340  
   1.341 -  fun distinct_lr node_in_set Left  = discharge [dist_subtree_thm,node_in_set] distinct_left 
   1.342 -    | distinct_lr node_in_set Right = discharge [dist_subtree_thm,node_in_set] distinct_right 
   1.343 +  fun in_set' [] = raise TERM ("distinctTreeProver", [])
   1.344 +    | in_set' (Left :: ps) = in_set ps l
   1.345 +    | in_set' (Right :: ps) = in_set ps r;
   1.346 +
   1.347 +  fun distinct_lr node_in_set Left  = discharge [dist_subtree_thm,node_in_set] distinct_left
   1.348 +    | distinct_lr node_in_set Right = discharge [dist_subtree_thm,node_in_set] distinct_right
   1.349  
   1.350 -  val (swap,neq) = 
   1.351 -       (case x_rest of
   1.352 -         [] => let 
   1.353 -                 val y_in_set = in_set' y_rest;
   1.354 -               in (false,distinct_lr y_in_set (hd y_rest)) end
   1.355 -       | (xr::xrs) => 
   1.356 -           (case y_rest of
   1.357 -             [] => let 
   1.358 -                     val x_in_set = in_set' x_rest;
   1.359 -               in (true,distinct_lr x_in_set (hd x_rest)) end
   1.360 -           | (yr::yrs) =>
   1.361 -               let
   1.362 -                 val x_in_set = in_set' x_rest;
   1.363 -                 val y_in_set = in_set' y_rest;
   1.364 -               in (case xr of
   1.365 -                    Left => (false,
   1.366 -                             discharge [dist_subtree_thm,x_in_set,y_in_set] distinct_left_right)
   1.367 -                   |Right => (true,
   1.368 -                             discharge [dist_subtree_thm,y_in_set,x_in_set] distinct_left_right))
   1.369 -               end
   1.370 -        ))
   1.371 -  in if swap then discharge [neq] swap_neq else neq
   1.372 -  end  
   1.373 +  val (swap, neq) =
   1.374 +    (case x_rest of
   1.375 +      [] =>
   1.376 +        let val y_in_set = in_set' y_rest;
   1.377 +        in (false, distinct_lr y_in_set (hd y_rest)) end
   1.378 +    | xr :: xrs =>
   1.379 +        (case y_rest of
   1.380 +          [] =>
   1.381 +            let val x_in_set = in_set' x_rest;
   1.382 +            in (true, distinct_lr x_in_set (hd x_rest)) end
   1.383 +        | yr :: yrs =>
   1.384 +            let
   1.385 +              val x_in_set = in_set' x_rest;
   1.386 +              val y_in_set = in_set' y_rest;
   1.387 +            in
   1.388 +              (case xr of
   1.389 +                Left => (false, discharge [dist_subtree_thm,x_in_set,y_in_set] distinct_left_right)
   1.390 +              | Right => (true, discharge [dist_subtree_thm,y_in_set,x_in_set] distinct_left_right))
   1.391 +           end));
   1.392 +  in if swap then discharge [neq] swap_neq else neq end;
   1.393  
   1.394  
   1.395 -val delete_root = @{thm DistinctTreeProver.delete_root};
   1.396 -val delete_left = @{thm DistinctTreeProver.delete_left};
   1.397 -val delete_right = @{thm DistinctTreeProver.delete_right};
   1.398 +val delete_root = @{thm delete_root};
   1.399 +val delete_left = @{thm delete_left};
   1.400 +val delete_right = @{thm delete_right};
   1.401  
   1.402  fun deleteProver dist_thm [] = delete_root OF [dist_thm]
   1.403    | deleteProver dist_thm (p::ps) =
   1.404 -     let
   1.405 -       val dist_rule = (case p of Left => all_distinct_left | Right => all_distinct_right);
   1.406 -       val dist_thm' = discharge [dist_thm] dist_rule 
   1.407 -       val del_rule = (case p of Left => delete_left | Right => delete_right)
   1.408 -       val del = deleteProver dist_thm' ps;
   1.409 -     in discharge [dist_thm, del] del_rule end;
   1.410 +      let
   1.411 +        val dist_rule = (case p of Left => all_distinct_left | Right => all_distinct_right);
   1.412 +        val dist_thm' = discharge [dist_thm] dist_rule;
   1.413 +        val del_rule = (case p of Left => delete_left | Right => delete_right);
   1.414 +        val del = deleteProver dist_thm' ps;
   1.415 +      in discharge [dist_thm, del] del_rule end;
   1.416  
   1.417 -val subtract_Tip = @{thm DistinctTreeProver.subtract_Tip};
   1.418 -val subtract_Node = @{thm DistinctTreeProver.subtract_Node};
   1.419 -val delete_Some_all_distinct = @{thm DistinctTreeProver.delete_Some_all_distinct};
   1.420 -val subtract_Some_all_distinct_res = @{thm DistinctTreeProver.subtract_Some_all_distinct_res};
   1.421 +val subtract_Tip = @{thm subtract_Tip};
   1.422 +val subtract_Node = @{thm subtract_Node};
   1.423 +val delete_Some_all_distinct = @{thm delete_Some_all_distinct};
   1.424 +val subtract_Some_all_distinct_res = @{thm subtract_Some_all_distinct_res};
   1.425  
   1.426  local
   1.427 -  val (alpha,v) = 
   1.428 +  val (alpha, v) =
   1.429      let
   1.430 -      val ct = subtract_Tip |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 
   1.431 -               |> Thm.dest_comb |> #2
   1.432 +      val ct =
   1.433 +        subtract_Tip |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
   1.434 +        |> Thm.dest_comb |> #2;
   1.435        val [alpha] = ct |> Thm.ctyp_of_term |> Thm.dest_ctyp;
   1.436      in (alpha, #1 (dest_Var (term_of ct))) end;
   1.437  in
   1.438 -fun subtractProver (Const ("DistinctTreeProver.tree.Tip",T)) ct dist_thm =
   1.439 -    let 
   1.440 -      val ct' = dist_thm |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
   1.441 -      val thy = theory_of_cterm ct;
   1.442 -      val [alphaI] = #2 (dest_Type T);
   1.443 -    in Thm.instantiate ([(alpha,ctyp_of thy alphaI)],
   1.444 -                        [(cterm_of thy (Var (v,treeT alphaI)),ct')]) subtract_Tip
   1.445 -    end
   1.446 -  | subtractProver (Const ("DistinctTreeProver.tree.Node",nT)$l$x$d$r) ct dist_thm =
   1.447 -    let
   1.448 -      val ct' = dist_thm |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
   1.449 -      val (_,[cl,_,_,cr]) = Drule.strip_comb ct;
   1.450 -      val ps = the (find_tree x (term_of ct'));
   1.451 -      val del_tree = deleteProver dist_thm ps;
   1.452 -      val dist_thm' = discharge [del_tree, dist_thm] delete_Some_all_distinct; 
   1.453 -      val sub_l = subtractProver (term_of cl) cl (dist_thm');
   1.454 -      val sub_r = subtractProver (term_of cr) cr 
   1.455 -                    (discharge [sub_l, dist_thm'] subtract_Some_all_distinct_res);
   1.456 -    in discharge [del_tree, sub_l, sub_r] subtract_Node end
   1.457 -end
   1.458  
   1.459 -val subtract_Some_all_distinct = @{thm DistinctTreeProver.subtract_Some_all_distinct};
   1.460 +fun subtractProver (Const (@{const_name Tip}, T)) ct dist_thm =
   1.461 +      let
   1.462 +        val ct' = dist_thm |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
   1.463 +        val thy = theory_of_cterm ct;
   1.464 +        val [alphaI] = #2 (dest_Type T);
   1.465 +      in
   1.466 +        Thm.instantiate
   1.467 +          ([(alpha, ctyp_of thy alphaI)],
   1.468 +           [(cterm_of thy (Var (v, treeT alphaI)), ct')]) subtract_Tip
   1.469 +      end
   1.470 +  | subtractProver (Const (@{const_name Node}, nT) $ l $ x $ d $ r) ct dist_thm =
   1.471 +      let
   1.472 +        val ct' = dist_thm |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
   1.473 +        val (_, [cl, _, _, cr]) = Drule.strip_comb ct;
   1.474 +        val ps = the (find_tree x (term_of ct'));
   1.475 +        val del_tree = deleteProver dist_thm ps;
   1.476 +        val dist_thm' = discharge [del_tree, dist_thm] delete_Some_all_distinct;
   1.477 +        val sub_l = subtractProver (term_of cl) cl (dist_thm');
   1.478 +        val sub_r =
   1.479 +          subtractProver (term_of cr) cr
   1.480 +            (discharge [sub_l, dist_thm'] subtract_Some_all_distinct_res);
   1.481 +      in discharge [del_tree, sub_l, sub_r] subtract_Node end;
   1.482 +
   1.483 +end;
   1.484 +
   1.485 +val subtract_Some_all_distinct = @{thm subtract_Some_all_distinct};
   1.486 +
   1.487  fun distinct_implProver dist_thm ct =
   1.488    let
   1.489      val ctree = ct |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
   1.490 @@ -329,8 +348,10 @@
   1.491    in subtract_Some_all_distinct OF [sub, dist_thm] end;
   1.492  
   1.493  fun get_fst_success f [] = NONE
   1.494 -  | get_fst_success f (x::xs) = (case f x of NONE => get_fst_success f xs 
   1.495 -                                 | SOME v => SOME v);
   1.496 +  | get_fst_success f (x :: xs) =
   1.497 +      (case f x of
   1.498 +        NONE => get_fst_success f xs
   1.499 +      | SOME v => SOME v);
   1.500  
   1.501  fun neq_x_y ctxt x y name =
   1.502    (let
   1.503 @@ -340,8 +361,8 @@
   1.504      val x_path = the (find_tree x tree);
   1.505      val y_path = the (find_tree y tree);
   1.506      val thm = distinctTreeProver dist_thm x_path y_path;
   1.507 -  in SOME thm  
   1.508 -  end handle Option => NONE)
   1.509 +  in SOME thm
   1.510 +  end handle Option.Option => NONE);
   1.511  
   1.512  fun distinctTree_tac names ctxt = SUBGOAL (fn (goal, i) =>
   1.513      (case goal of
   1.514 @@ -352,17 +373,18 @@
   1.515          | NONE => no_tac)
   1.516      | _ => no_tac))
   1.517  
   1.518 -fun distinctFieldSolver names = mk_solver "distinctFieldSolver"
   1.519 -     (distinctTree_tac names o Simplifier.the_context)
   1.520 +fun distinctFieldSolver names =
   1.521 +  mk_solver "distinctFieldSolver" (distinctTree_tac names o Simplifier.the_context);
   1.522  
   1.523  fun distinct_simproc names =
   1.524    Simplifier.simproc_global @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"]
   1.525 -    (fn thy => fn ss => fn (Const (@{const_name HOL.eq},_)$x$y) =>
   1.526 -        case try Simplifier.the_context ss of
   1.527 -        SOME ctxt => Option.map (fn neq => neq_to_eq_False OF [neq]) 
   1.528 -                      (get_fst_success (neq_x_y ctxt x y) names)
   1.529 -       | NONE => NONE
   1.530 -    )
   1.531 +    (fn thy => fn ss => fn (Const (@{const_name HOL.eq}, _) $ x $ y) =>
   1.532 +      (case try Simplifier.the_context ss of
   1.533 +        SOME ctxt =>
   1.534 +          Option.map (fn neq => neq_to_eq_False OF [neq])
   1.535 +            (get_fst_success (neq_x_y ctxt x y) names)
   1.536 +      | NONE => NONE));
   1.537  
   1.538 -end
   1.539 +end;
   1.540 +
   1.541  end;
   1.542 \ No newline at end of file