# HG changeset patch
# User wenzelm
# Date 1320584964 -3600
# Node ID c0704e988526e2e52113b892e9c6292300d10368
# Parent  a2157057024c577c5f2892c588d93050e89269b6
misc tuning and modernization;

diff -r a2157057024c -r c0704e988526 src/HOL/Statespace/DistinctTreeProver.thy
--- a/src/HOL/Statespace/DistinctTreeProver.thy	Sun Nov 06 13:25:41 2011 +0100
+++ b/src/HOL/Statespace/DistinctTreeProver.thy	Sun Nov 06 14:09:24 2011 +0100
@@ -51,8 +51,7 @@
 certificate that the content of the nodes is distinct. We use the
 following lemmas to achieve this.  *} 
 
-lemma all_distinct_left:
-"all_distinct (Node l x b r) \<Longrightarrow> all_distinct l"
+lemma all_distinct_left: "all_distinct (Node l x b r) \<Longrightarrow> all_distinct l"
   by simp
 
 lemma all_distinct_right: "all_distinct (Node l x b r) \<Longrightarrow> all_distinct r"
@@ -164,8 +163,8 @@
   qed
 qed
 
-lemma delete_Some_all_distinct: 
-"\<And>t'. \<lbrakk>delete x t = Some t'; all_distinct t\<rbrakk> \<Longrightarrow> all_distinct t'"
+lemma delete_Some_all_distinct:
+  "\<And>t'. \<lbrakk>delete x t = Some t'; all_distinct t\<rbrakk> \<Longrightarrow> all_distinct t'"
 proof (induct t)
   case Tip thus ?case by simp
 next
diff -r a2157057024c -r c0704e988526 src/HOL/Statespace/distinct_tree_prover.ML
--- a/src/HOL/Statespace/distinct_tree_prover.ML	Sun Nov 06 13:25:41 2011 +0100
+++ b/src/HOL/Statespace/distinct_tree_prover.ML	Sun Nov 06 14:09:24 2011 +0100
@@ -4,20 +4,20 @@
 
 signature DISTINCT_TREE_PROVER =
 sig
-  datatype Direction = Left | Right
+  datatype direction = Left | Right
   val mk_tree : ('a -> term) -> typ -> 'a list -> term
   val dest_tree : term -> term list
-  val find_tree : term -> term -> Direction list option 
+  val find_tree : term -> term -> direction list option
 
   val neq_to_eq_False : thm
-  val distinctTreeProver : thm -> Direction list -> Direction list -> thm
-  val neq_x_y : Proof.context -> term -> term -> string -> thm option   
+  val distinctTreeProver : thm -> direction list -> direction list -> thm
+  val neq_x_y : Proof.context -> term -> term -> string -> thm option
   val distinctFieldSolver : string list -> solver
   val distinctTree_tac : string list -> Proof.context -> int -> tactic
   val distinct_implProver : thm -> cterm -> thm
   val subtractProver : term -> cterm -> thm -> thm
   val distinct_simproc : string list -> simproc
-  
+
   val discharge : thm list -> thm -> thm
 end;
 
@@ -37,68 +37,70 @@
 val swap_neq = @{thm DistinctTreeProver.swap_neq};
 val neq_to_eq_False = @{thm DistinctTreeProver.neq_to_eq_False};
 
-datatype Direction = Left | Right 
+datatype direction = Left | Right;
 
-fun treeT T = Type ("DistinctTreeProver.tree",[T]);
-fun mk_tree' e T n []     = Const ("DistinctTreeProver.tree.Tip",treeT T)
+fun treeT T = Type (@{type_name tree}, [T]);
+fun mk_tree' e T n [] = Const (@{const_name Tip}, treeT T)
   | mk_tree' e T n xs =
      let
        val m = (n - 1) div 2;
        val (xsl,x::xsr) = chop m xs;
        val l = mk_tree' e T m xsl;
        val r = mk_tree' e T (n-(m+1)) xsr;
-     in Const ("DistinctTreeProver.tree.Node",
-                treeT T --> T --> HOLogic.boolT--> treeT T --> treeT T) $ 
-          l$ e x $ HOLogic.false_const $ r 
+     in
+       Const (@{const_name Node}, treeT T --> T --> HOLogic.boolT--> treeT T --> treeT T) $
+         l $ e x $ HOLogic.false_const $ r
      end
 
-fun mk_tree e T xs = mk_tree' e T (length xs) xs;         
+fun mk_tree e T xs = mk_tree' e T (length xs) xs;
 
-fun dest_tree (Const ("DistinctTreeProver.tree.Tip",_)) = []
-  | dest_tree (Const ("DistinctTreeProver.tree.Node",_)$l$e$_$r) = dest_tree l @ e :: dest_tree r
-  | dest_tree t = raise TERM ("DistinctTreeProver.dest_tree",[t]);
+fun dest_tree (Const (@{const_name Tip}, _)) = []
+  | dest_tree (Const (@{const_name Node}, _) $ l $ e $ _ $ r) = dest_tree l @ e :: dest_tree r
+  | dest_tree t = raise TERM ("dest_tree", [t]);
 
 
 
-fun lin_find_tree e (Const ("DistinctTreeProver.tree.Tip",_)) = NONE
-  | lin_find_tree e (Const ("DistinctTreeProver.tree.Node",_) $ l$ x $ _ $ r) =
-      if e aconv x 
+fun lin_find_tree e (Const (@{const_name Tip}, _)) = NONE
+  | lin_find_tree e (Const (@{const_name Node}, _) $ l $ x $ _ $ r) =
+      if e aconv x
       then SOME []
-      else (case lin_find_tree e l of
-              SOME path => SOME (Left::path)
-            | NONE => (case lin_find_tree e r of
-                        SOME path => SOME (Right::path)
-                       | NONE => NONE))
-  | lin_find_tree e t = raise TERM ("find_tree: input not a tree",[t])
+      else
+        (case lin_find_tree e l of
+          SOME path => SOME (Left :: path)
+        | NONE =>
+            (case lin_find_tree e r of
+              SOME path => SOME (Right :: path)
+            | NONE => NONE))
+  | lin_find_tree e t = raise TERM ("find_tree: input not a tree", [t])
 
-fun bin_find_tree order e (Const ("DistinctTreeProver.tree.Tip",_)) = NONE
-  | bin_find_tree order e (Const ("DistinctTreeProver.tree.Node",_) $ l$ x $ _ $ r) =
-      (case order (e,x) of
-         EQUAL => SOME []
-       | LESS => Option.map (cons Left) (bin_find_tree order e l)
-       | GREATER => Option.map (cons Right) (bin_find_tree order e r))
-  | bin_find_tree order e t = raise TERM ("find_tree: input not a tree",[t])
+fun bin_find_tree order e (Const (@{const_name Tip}, _)) = NONE
+  | bin_find_tree order e (Const (@{const_name Node}, _) $ l $ x $ _ $ r) =
+      (case order (e, x) of
+        EQUAL => SOME []
+      | LESS => Option.map (cons Left) (bin_find_tree order e l)
+      | GREATER => Option.map (cons Right) (bin_find_tree order e r))
+  | bin_find_tree order e t = raise TERM ("find_tree: input not a tree", [t])
 
 fun find_tree e t =
   (case bin_find_tree Term_Ord.fast_term_ord e t of
-     NONE => lin_find_tree e t
-   | x => x);
+    NONE => lin_find_tree e t
+  | x => x);
+
 
- 
-fun index_tree (Const ("DistinctTreeProver.tree.Tip",_)) path tab = tab
-  | index_tree (Const ("DistinctTreeProver.tree.Node",_) $ l$ x $ _ $ r) path tab =
-      tab 
-      |> Termtab.update_new (x,path) 
-      |> index_tree l (path@[Left])
-      |> index_tree r (path@[Right])
-  | index_tree t _ _ = raise TERM ("index_tree: input not a tree",[t])
+fun index_tree (Const (@{const_name Tip}, _)) path tab = tab
+  | index_tree (Const (@{const_name Node}, _) $ l $ x $ _ $ r) path tab =
+      tab
+      |> Termtab.update_new (x, path)
+      |> index_tree l (path @ [Left])
+      |> index_tree r (path @ [Right])
+  | index_tree t _ _ = raise TERM ("index_tree: input not a tree", [t])
 
-fun split_common_prefix xs [] = ([],xs,[])
-  | split_common_prefix [] ys = ([],[],ys)
-  | split_common_prefix (xs as (x::xs')) (ys as (y::ys')) =
-     if x=y 
-     then let val (ps,xs'',ys'') = split_common_prefix xs' ys' in (x::ps,xs'',ys'') end
-     else ([],xs,ys)
+fun split_common_prefix xs [] = ([], xs, [])
+  | split_common_prefix [] ys = ([], [], ys)
+  | split_common_prefix (xs as (x :: xs')) (ys as (y :: ys')) =
+      if x = y
+      then let val (ps, xs'', ys'') = split_common_prefix xs' ys' in (x :: ps, xs'', ys'') end
+      else ([], xs, ys)
 
 
 (* Wrapper around Thm.instantiate. The type instiations of instTs are applied to
@@ -106,14 +108,14 @@
  *)
 fun instantiate instTs insts =
   let
-    val instTs' = map (fn (T,U) => (dest_TVar (typ_of T),typ_of U)) instTs;
+    val instTs' = map (fn (T, U) => (dest_TVar (typ_of T), typ_of U)) instTs;
     fun substT x = (case AList.lookup (op =) instTs' x of NONE => TVar x | SOME T' => T');
     fun mapT_and_recertify ct =
       let
         val thy = theory_of_cterm ct;
       in (cterm_of thy (Term.map_types (Term.map_type_tvar substT) (term_of ct))) end;
     val insts' = map (apfst mapT_and_recertify) insts;
-  in Thm.instantiate (instTs,insts') end;
+  in Thm.instantiate (instTs, insts') end;
 
 fun tvar_clash ixn S S' = raise TYPE ("Type variable " ^
   quote (Term.string_of_vname ixn) ^ " has two distinct sorts",
@@ -141,62 +143,69 @@
   in match end;
 
 
-(* expects that relevant type variables are already contained in 
+(* expects that relevant type variables are already contained in
  * term variables. First instantiation of variables is returned without further
  * checking.
  *)
-fun naive_cterm_first_order_match (t,ct) env =
+fun naive_cterm_first_order_match (t, ct) env =
   let
-    val thy = (theory_of_cterm ct);
-    fun mtch (env as (tyinsts,insts)) = fn
-         (Var(ixn,T),ct) =>
-           (case AList.lookup (op =) insts ixn of
-             NONE => (naive_typ_match (T,typ_of (ctyp_of_term ct)) tyinsts,
-                      (ixn, ct)::insts)
-            | SOME _ => env)
-        | (f$t,ct) => let val (cf,ct') = Thm.dest_comb ct;
-                      in mtch (mtch env (f,cf)) (t,ct') end
-        | _ => env
-  in mtch env (t,ct) end;
+    val thy = theory_of_cterm ct;
+    fun mtch (env as (tyinsts, insts)) =
+      fn (Var (ixn, T), ct) =>
+          (case AList.lookup (op =) insts ixn of
+            NONE => (naive_typ_match (T, typ_of (ctyp_of_term ct)) tyinsts, (ixn, ct) :: insts)
+          | SOME _ => env)
+       | (f $ t, ct) =>
+          let val (cf, ct') = Thm.dest_comb ct;
+          in mtch (mtch env (f, cf)) (t, ct') end
+       | _ => env;
+  in mtch env (t, ct) end;
 
 
 fun discharge prems rule =
   let
-     val thy = theory_of_thm (hd prems);
-     val (tyinsts,insts) =  
-           fold naive_cterm_first_order_match (prems_of rule ~~ map cprop_of prems) ([],[]);
+    val thy = theory_of_thm (hd prems);
+    val (tyinsts,insts) =
+      fold naive_cterm_first_order_match (prems_of rule ~~ map cprop_of prems) ([], []);
 
-     val tyinsts' = map (fn (v,(S,U)) => (ctyp_of thy (TVar (v,S)),ctyp_of thy U)) 
-                     tyinsts;
-     val insts' = map (fn (idxn,ct) => (cterm_of thy (Var (idxn,typ_of (ctyp_of_term ct))),ct))  
-                     insts;
-     val rule' = Thm.instantiate (tyinsts',insts') rule;
-   in fold Thm.elim_implies prems rule' end;
+    val tyinsts' =
+      map (fn (v, (S, U)) => (ctyp_of thy (TVar (v, S)), ctyp_of thy U)) tyinsts;
+    val insts' =
+      map (fn (idxn, ct) => (cterm_of thy (Var (idxn, typ_of (ctyp_of_term ct))), ct)) insts;
+    val rule' = Thm.instantiate (tyinsts', insts') rule;
+  in fold Thm.elim_implies prems rule' end;
 
 local
 
-val (l_in_set_root,x_in_set_root,r_in_set_root) =
-  let val (Node_l_x_d,r) = (cprop_of in_set_root) 
-                         |> Thm.dest_comb |> #2 
-                         |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb;
-      val (Node_l,x) = Node_l_x_d |> Thm.dest_comb |> #1 |> Thm.dest_comb;
-      val l = Node_l |> Thm.dest_comb |> #2;
-  in (l,x,r) end
-val (x_in_set_left,r_in_set_left) = 
-  let val (Node_l_x_d,r) = (cprop_of in_set_left) 
-                         |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
-                         |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb;
-      val x = Node_l_x_d |> Thm.dest_comb |> #1 |> Thm.dest_comb |> #2;
-  in (x,r) end
+val (l_in_set_root, x_in_set_root, r_in_set_root) =
+  let
+    val (Node_l_x_d, r) =
+      cprop_of in_set_root
+      |> Thm.dest_comb |> #2
+      |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb;
+    val (Node_l, x) = Node_l_x_d |> Thm.dest_comb |> #1 |> Thm.dest_comb;
+    val l = Node_l |> Thm.dest_comb |> #2;
+  in (l,x,r) end;
 
-val (x_in_set_right,l_in_set_right) = 
-  let val (Node_l,x) = (cprop_of in_set_right) 
-                         |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
-                         |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 
-                         |> Thm.dest_comb |> #1 |> Thm.dest_comb |> #1 
-                         |> Thm.dest_comb
-      val l = Node_l |> Thm.dest_comb |> #2;
-  in (x,l) end
+val (x_in_set_left, r_in_set_left) =
+  let
+    val (Node_l_x_d, r) =
+      cprop_of in_set_left
+      |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
+      |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb;
+    val x = Node_l_x_d |> Thm.dest_comb |> #1 |> Thm.dest_comb |> #2;
+  in (x, r) end;
+
+val (x_in_set_right, l_in_set_right) =
+  let
+    val (Node_l, x) =
+      cprop_of in_set_right
+      |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
+      |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
+      |> Thm.dest_comb |> #1 |> Thm.dest_comb |> #1
+      |> Thm.dest_comb;
+    val l = Node_l |> Thm.dest_comb |> #2;
+  in (x, l) end;
 
 in
 (*
@@ -210,118 +219,128 @@
 fun distinctTreeProver dist_thm x_path y_path =
   let
     fun dist_subtree [] thm = thm
-      | dist_subtree (p::ps) thm =
-         let 
+      | dist_subtree (p :: ps) thm =
+         let
            val rule = (case p of Left => all_distinct_left | Right => all_distinct_right)
          in dist_subtree ps (discharge [thm] rule) end;
 
-    val (ps,x_rest,y_rest) = split_common_prefix x_path y_path;
+    val (ps, x_rest, y_rest) = split_common_prefix x_path y_path;
     val dist_subtree_thm = dist_subtree ps dist_thm;
     val subtree = cprop_of dist_subtree_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
-    val (_,[l,_,_,r]) = Drule.strip_comb subtree;
-    
+    val (_, [l, _, _, r]) = Drule.strip_comb subtree;
+
     fun in_set ps tree =
       let
-        val (_,[l,x,_,r]) = Drule.strip_comb tree;
+        val (_, [l, x, _, r]) = Drule.strip_comb tree;
         val xT = ctyp_of_term x;
-      in (case ps of
-            [] => instantiate 
-                    [(ctyp_of_term x_in_set_root,xT)]
-                    [(l_in_set_root,l),(x_in_set_root,x),(r_in_set_root,r)] in_set_root
-          | (Left::ps') => 
-               let
-                  val in_set_l = in_set ps' l;
-                  val in_set_left' = instantiate [(ctyp_of_term x_in_set_left,xT)]
-                                      [(x_in_set_left,x),(r_in_set_left,r)] in_set_left;
-               in discharge [in_set_l] in_set_left' end
-          | (Right::ps') => 
-               let
-                  val in_set_r = in_set ps' r;
-                  val in_set_right' = instantiate [(ctyp_of_term x_in_set_right,xT)] 
-                                      [(x_in_set_right,x),(l_in_set_right,l)] in_set_right;
-               in discharge [in_set_r] in_set_right' end)
-      end 
-       
-  fun in_set' [] = raise TERM ("distinctTreeProver",[])
-    | in_set' (Left::ps) = in_set ps l
-    | in_set' (Right::ps) = in_set ps r;
+      in
+        (case ps of
+          [] =>
+            instantiate
+              [(ctyp_of_term x_in_set_root, xT)]
+              [(l_in_set_root, l), (x_in_set_root, x), (r_in_set_root, r)] in_set_root
+        | Left :: ps' =>
+            let
+              val in_set_l = in_set ps' l;
+              val in_set_left' =
+                instantiate
+                  [(ctyp_of_term x_in_set_left, xT)]
+                  [(x_in_set_left, x), (r_in_set_left, r)] in_set_left;
+            in discharge [in_set_l] in_set_left' end
+        | Right :: ps' =>
+            let
+              val in_set_r = in_set ps' r;
+              val in_set_right' =
+                instantiate
+                  [(ctyp_of_term x_in_set_right, xT)]
+                  [(x_in_set_right, x), (l_in_set_right, l)] in_set_right;
+            in discharge [in_set_r] in_set_right' end)
+      end;
 
-  fun distinct_lr node_in_set Left  = discharge [dist_subtree_thm,node_in_set] distinct_left 
-    | distinct_lr node_in_set Right = discharge [dist_subtree_thm,node_in_set] distinct_right 
+  fun in_set' [] = raise TERM ("distinctTreeProver", [])
+    | in_set' (Left :: ps) = in_set ps l
+    | in_set' (Right :: ps) = in_set ps r;
+
+  fun distinct_lr node_in_set Left  = discharge [dist_subtree_thm,node_in_set] distinct_left
+    | distinct_lr node_in_set Right = discharge [dist_subtree_thm,node_in_set] distinct_right
 
-  val (swap,neq) = 
-       (case x_rest of
-         [] => let 
-                 val y_in_set = in_set' y_rest;
-               in (false,distinct_lr y_in_set (hd y_rest)) end
-       | (xr::xrs) => 
-           (case y_rest of
-             [] => let 
-                     val x_in_set = in_set' x_rest;
-               in (true,distinct_lr x_in_set (hd x_rest)) end
-           | (yr::yrs) =>
-               let
-                 val x_in_set = in_set' x_rest;
-                 val y_in_set = in_set' y_rest;
-               in (case xr of
-                    Left => (false,
-                             discharge [dist_subtree_thm,x_in_set,y_in_set] distinct_left_right)
-                   |Right => (true,
-                             discharge [dist_subtree_thm,y_in_set,x_in_set] distinct_left_right))
-               end
-        ))
-  in if swap then discharge [neq] swap_neq else neq
-  end  
+  val (swap, neq) =
+    (case x_rest of
+      [] =>
+        let val y_in_set = in_set' y_rest;
+        in (false, distinct_lr y_in_set (hd y_rest)) end
+    | xr :: xrs =>
+        (case y_rest of
+          [] =>
+            let val x_in_set = in_set' x_rest;
+            in (true, distinct_lr x_in_set (hd x_rest)) end
+        | yr :: yrs =>
+            let
+              val x_in_set = in_set' x_rest;
+              val y_in_set = in_set' y_rest;
+            in
+              (case xr of
+                Left => (false, discharge [dist_subtree_thm,x_in_set,y_in_set] distinct_left_right)
+              | Right => (true, discharge [dist_subtree_thm,y_in_set,x_in_set] distinct_left_right))
+           end));
+  in if swap then discharge [neq] swap_neq else neq end;
 
 
-val delete_root = @{thm DistinctTreeProver.delete_root};
-val delete_left = @{thm DistinctTreeProver.delete_left};
-val delete_right = @{thm DistinctTreeProver.delete_right};
+val delete_root = @{thm delete_root};
+val delete_left = @{thm delete_left};
+val delete_right = @{thm delete_right};
 
 fun deleteProver dist_thm [] = delete_root OF [dist_thm]
   | deleteProver dist_thm (p::ps) =
-     let
-       val dist_rule = (case p of Left => all_distinct_left | Right => all_distinct_right);
-       val dist_thm' = discharge [dist_thm] dist_rule 
-       val del_rule = (case p of Left => delete_left | Right => delete_right)
-       val del = deleteProver dist_thm' ps;
-     in discharge [dist_thm, del] del_rule end;
+      let
+        val dist_rule = (case p of Left => all_distinct_left | Right => all_distinct_right);
+        val dist_thm' = discharge [dist_thm] dist_rule;
+        val del_rule = (case p of Left => delete_left | Right => delete_right);
+        val del = deleteProver dist_thm' ps;
+      in discharge [dist_thm, del] del_rule end;
 
-val subtract_Tip = @{thm DistinctTreeProver.subtract_Tip};
-val subtract_Node = @{thm DistinctTreeProver.subtract_Node};
-val delete_Some_all_distinct = @{thm DistinctTreeProver.delete_Some_all_distinct};
-val subtract_Some_all_distinct_res = @{thm DistinctTreeProver.subtract_Some_all_distinct_res};
+val subtract_Tip = @{thm subtract_Tip};
+val subtract_Node = @{thm subtract_Node};
+val delete_Some_all_distinct = @{thm delete_Some_all_distinct};
+val subtract_Some_all_distinct_res = @{thm subtract_Some_all_distinct_res};
 
 local
-  val (alpha,v) = 
+  val (alpha, v) =
     let
-      val ct = subtract_Tip |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 
-               |> Thm.dest_comb |> #2
+      val ct =
+        subtract_Tip |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
+        |> Thm.dest_comb |> #2;
       val [alpha] = ct |> Thm.ctyp_of_term |> Thm.dest_ctyp;
     in (alpha, #1 (dest_Var (term_of ct))) end;
 in
-fun subtractProver (Const ("DistinctTreeProver.tree.Tip",T)) ct dist_thm =
-    let 
-      val ct' = dist_thm |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
-      val thy = theory_of_cterm ct;
-      val [alphaI] = #2 (dest_Type T);
-    in Thm.instantiate ([(alpha,ctyp_of thy alphaI)],
-                        [(cterm_of thy (Var (v,treeT alphaI)),ct')]) subtract_Tip
-    end
-  | subtractProver (Const ("DistinctTreeProver.tree.Node",nT)$l$x$d$r) ct dist_thm =
-    let
-      val ct' = dist_thm |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
-      val (_,[cl,_,_,cr]) = Drule.strip_comb ct;
-      val ps = the (find_tree x (term_of ct'));
-      val del_tree = deleteProver dist_thm ps;
-      val dist_thm' = discharge [del_tree, dist_thm] delete_Some_all_distinct; 
-      val sub_l = subtractProver (term_of cl) cl (dist_thm');
-      val sub_r = subtractProver (term_of cr) cr 
-                    (discharge [sub_l, dist_thm'] subtract_Some_all_distinct_res);
-    in discharge [del_tree, sub_l, sub_r] subtract_Node end
-end
 
-val subtract_Some_all_distinct = @{thm DistinctTreeProver.subtract_Some_all_distinct};
+fun subtractProver (Const (@{const_name Tip}, T)) ct dist_thm =
+      let
+        val ct' = dist_thm |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
+        val thy = theory_of_cterm ct;
+        val [alphaI] = #2 (dest_Type T);
+      in
+        Thm.instantiate
+          ([(alpha, ctyp_of thy alphaI)],
+           [(cterm_of thy (Var (v, treeT alphaI)), ct')]) subtract_Tip
+      end
+  | subtractProver (Const (@{const_name Node}, nT) $ l $ x $ d $ r) ct dist_thm =
+      let
+        val ct' = dist_thm |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
+        val (_, [cl, _, _, cr]) = Drule.strip_comb ct;
+        val ps = the (find_tree x (term_of ct'));
+        val del_tree = deleteProver dist_thm ps;
+        val dist_thm' = discharge [del_tree, dist_thm] delete_Some_all_distinct;
+        val sub_l = subtractProver (term_of cl) cl (dist_thm');
+        val sub_r =
+          subtractProver (term_of cr) cr
+            (discharge [sub_l, dist_thm'] subtract_Some_all_distinct_res);
+      in discharge [del_tree, sub_l, sub_r] subtract_Node end;
+
+end;
+
+val subtract_Some_all_distinct = @{thm subtract_Some_all_distinct};
+
 fun distinct_implProver dist_thm ct =
   let
     val ctree = ct |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
@@ -329,8 +348,10 @@
   in subtract_Some_all_distinct OF [sub, dist_thm] end;
 
 fun get_fst_success f [] = NONE
-  | get_fst_success f (x::xs) = (case f x of NONE => get_fst_success f xs 
-                                 | SOME v => SOME v);
+  | get_fst_success f (x :: xs) =
+      (case f x of
+        NONE => get_fst_success f xs
+      | SOME v => SOME v);
 
 fun neq_x_y ctxt x y name =
   (let
@@ -340,8 +361,8 @@
     val x_path = the (find_tree x tree);
     val y_path = the (find_tree y tree);
     val thm = distinctTreeProver dist_thm x_path y_path;
-  in SOME thm  
-  end handle Option => NONE)
+  in SOME thm
+  end handle Option.Option => NONE);
 
 fun distinctTree_tac names ctxt = SUBGOAL (fn (goal, i) =>
     (case goal of
@@ -352,17 +373,18 @@
         | NONE => no_tac)
     | _ => no_tac))
 
-fun distinctFieldSolver names = mk_solver "distinctFieldSolver"
-     (distinctTree_tac names o Simplifier.the_context)
+fun distinctFieldSolver names =
+  mk_solver "distinctFieldSolver" (distinctTree_tac names o Simplifier.the_context);
 
 fun distinct_simproc names =
   Simplifier.simproc_global @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"]
-    (fn thy => fn ss => fn (Const (@{const_name HOL.eq},_)$x$y) =>
-        case try Simplifier.the_context ss of
-        SOME ctxt => Option.map (fn neq => neq_to_eq_False OF [neq]) 
-                      (get_fst_success (neq_x_y ctxt x y) names)
-       | NONE => NONE
-    )
+    (fn thy => fn ss => fn (Const (@{const_name HOL.eq}, _) $ x $ y) =>
+      (case try Simplifier.the_context ss of
+        SOME ctxt =>
+          Option.map (fn neq => neq_to_eq_False OF [neq])
+            (get_fst_success (neq_x_y ctxt x y) names)
+      | NONE => NONE));
 
-end
+end;
+
 end;
\ No newline at end of file