misc tuning and modernization;
authorwenzelm
Sun Nov 06 14:09:24 2011 +0100 (2011-11-06)
changeset 45355c0704e988526
parent 45354 a2157057024c
child 45356 e79402612266
misc tuning and modernization;
src/HOL/Statespace/DistinctTreeProver.thy
src/HOL/Statespace/distinct_tree_prover.ML
     1.1 --- a/src/HOL/Statespace/DistinctTreeProver.thy	Sun Nov 06 13:25:41 2011 +0100
     1.2 +++ b/src/HOL/Statespace/DistinctTreeProver.thy	Sun Nov 06 14:09:24 2011 +0100
     1.3 @@ -51,8 +51,7 @@
     1.4  certificate that the content of the nodes is distinct. We use the
     1.5  following lemmas to achieve this.  *} 
     1.6  
     1.7 -lemma all_distinct_left:
     1.8 -"all_distinct (Node l x b r) \<Longrightarrow> all_distinct l"
     1.9 +lemma all_distinct_left: "all_distinct (Node l x b r) \<Longrightarrow> all_distinct l"
    1.10    by simp
    1.11  
    1.12  lemma all_distinct_right: "all_distinct (Node l x b r) \<Longrightarrow> all_distinct r"
    1.13 @@ -164,8 +163,8 @@
    1.14    qed
    1.15  qed
    1.16  
    1.17 -lemma delete_Some_all_distinct: 
    1.18 -"\<And>t'. \<lbrakk>delete x t = Some t'; all_distinct t\<rbrakk> \<Longrightarrow> all_distinct t'"
    1.19 +lemma delete_Some_all_distinct:
    1.20 +  "\<And>t'. \<lbrakk>delete x t = Some t'; all_distinct t\<rbrakk> \<Longrightarrow> all_distinct t'"
    1.21  proof (induct t)
    1.22    case Tip thus ?case by simp
    1.23  next
     2.1 --- a/src/HOL/Statespace/distinct_tree_prover.ML	Sun Nov 06 13:25:41 2011 +0100
     2.2 +++ b/src/HOL/Statespace/distinct_tree_prover.ML	Sun Nov 06 14:09:24 2011 +0100
     2.3 @@ -4,20 +4,20 @@
     2.4  
     2.5  signature DISTINCT_TREE_PROVER =
     2.6  sig
     2.7 -  datatype Direction = Left | Right
     2.8 +  datatype direction = Left | Right
     2.9    val mk_tree : ('a -> term) -> typ -> 'a list -> term
    2.10    val dest_tree : term -> term list
    2.11 -  val find_tree : term -> term -> Direction list option 
    2.12 +  val find_tree : term -> term -> direction list option
    2.13  
    2.14    val neq_to_eq_False : thm
    2.15 -  val distinctTreeProver : thm -> Direction list -> Direction list -> thm
    2.16 -  val neq_x_y : Proof.context -> term -> term -> string -> thm option   
    2.17 +  val distinctTreeProver : thm -> direction list -> direction list -> thm
    2.18 +  val neq_x_y : Proof.context -> term -> term -> string -> thm option
    2.19    val distinctFieldSolver : string list -> solver
    2.20    val distinctTree_tac : string list -> Proof.context -> int -> tactic
    2.21    val distinct_implProver : thm -> cterm -> thm
    2.22    val subtractProver : term -> cterm -> thm -> thm
    2.23    val distinct_simproc : string list -> simproc
    2.24 -  
    2.25 +
    2.26    val discharge : thm list -> thm -> thm
    2.27  end;
    2.28  
    2.29 @@ -37,68 +37,70 @@
    2.30  val swap_neq = @{thm DistinctTreeProver.swap_neq};
    2.31  val neq_to_eq_False = @{thm DistinctTreeProver.neq_to_eq_False};
    2.32  
    2.33 -datatype Direction = Left | Right 
    2.34 +datatype direction = Left | Right;
    2.35  
    2.36 -fun treeT T = Type ("DistinctTreeProver.tree",[T]);
    2.37 -fun mk_tree' e T n []     = Const ("DistinctTreeProver.tree.Tip",treeT T)
    2.38 +fun treeT T = Type (@{type_name tree}, [T]);
    2.39 +fun mk_tree' e T n [] = Const (@{const_name Tip}, treeT T)
    2.40    | mk_tree' e T n xs =
    2.41       let
    2.42         val m = (n - 1) div 2;
    2.43         val (xsl,x::xsr) = chop m xs;
    2.44         val l = mk_tree' e T m xsl;
    2.45         val r = mk_tree' e T (n-(m+1)) xsr;
    2.46 -     in Const ("DistinctTreeProver.tree.Node",
    2.47 -                treeT T --> T --> HOLogic.boolT--> treeT T --> treeT T) $ 
    2.48 -          l$ e x $ HOLogic.false_const $ r 
    2.49 +     in
    2.50 +       Const (@{const_name Node}, treeT T --> T --> HOLogic.boolT--> treeT T --> treeT T) $
    2.51 +         l $ e x $ HOLogic.false_const $ r
    2.52       end
    2.53  
    2.54 -fun mk_tree e T xs = mk_tree' e T (length xs) xs;         
    2.55 +fun mk_tree e T xs = mk_tree' e T (length xs) xs;
    2.56  
    2.57 -fun dest_tree (Const ("DistinctTreeProver.tree.Tip",_)) = []
    2.58 -  | dest_tree (Const ("DistinctTreeProver.tree.Node",_)$l$e$_$r) = dest_tree l @ e :: dest_tree r
    2.59 -  | dest_tree t = raise TERM ("DistinctTreeProver.dest_tree",[t]);
    2.60 +fun dest_tree (Const (@{const_name Tip}, _)) = []
    2.61 +  | dest_tree (Const (@{const_name Node}, _) $ l $ e $ _ $ r) = dest_tree l @ e :: dest_tree r
    2.62 +  | dest_tree t = raise TERM ("dest_tree", [t]);
    2.63  
    2.64  
    2.65  
    2.66 -fun lin_find_tree e (Const ("DistinctTreeProver.tree.Tip",_)) = NONE
    2.67 -  | lin_find_tree e (Const ("DistinctTreeProver.tree.Node",_) $ l$ x $ _ $ r) =
    2.68 -      if e aconv x 
    2.69 +fun lin_find_tree e (Const (@{const_name Tip}, _)) = NONE
    2.70 +  | lin_find_tree e (Const (@{const_name Node}, _) $ l $ x $ _ $ r) =
    2.71 +      if e aconv x
    2.72        then SOME []
    2.73 -      else (case lin_find_tree e l of
    2.74 -              SOME path => SOME (Left::path)
    2.75 -            | NONE => (case lin_find_tree e r of
    2.76 -                        SOME path => SOME (Right::path)
    2.77 -                       | NONE => NONE))
    2.78 -  | lin_find_tree e t = raise TERM ("find_tree: input not a tree",[t])
    2.79 +      else
    2.80 +        (case lin_find_tree e l of
    2.81 +          SOME path => SOME (Left :: path)
    2.82 +        | NONE =>
    2.83 +            (case lin_find_tree e r of
    2.84 +              SOME path => SOME (Right :: path)
    2.85 +            | NONE => NONE))
    2.86 +  | lin_find_tree e t = raise TERM ("find_tree: input not a tree", [t])
    2.87  
    2.88 -fun bin_find_tree order e (Const ("DistinctTreeProver.tree.Tip",_)) = NONE
    2.89 -  | bin_find_tree order e (Const ("DistinctTreeProver.tree.Node",_) $ l$ x $ _ $ r) =
    2.90 -      (case order (e,x) of
    2.91 -         EQUAL => SOME []
    2.92 -       | LESS => Option.map (cons Left) (bin_find_tree order e l)
    2.93 -       | GREATER => Option.map (cons Right) (bin_find_tree order e r))
    2.94 -  | bin_find_tree order e t = raise TERM ("find_tree: input not a tree",[t])
    2.95 +fun bin_find_tree order e (Const (@{const_name Tip}, _)) = NONE
    2.96 +  | bin_find_tree order e (Const (@{const_name Node}, _) $ l $ x $ _ $ r) =
    2.97 +      (case order (e, x) of
    2.98 +        EQUAL => SOME []
    2.99 +      | LESS => Option.map (cons Left) (bin_find_tree order e l)
   2.100 +      | GREATER => Option.map (cons Right) (bin_find_tree order e r))
   2.101 +  | bin_find_tree order e t = raise TERM ("find_tree: input not a tree", [t])
   2.102  
   2.103  fun find_tree e t =
   2.104    (case bin_find_tree Term_Ord.fast_term_ord e t of
   2.105 -     NONE => lin_find_tree e t
   2.106 -   | x => x);
   2.107 +    NONE => lin_find_tree e t
   2.108 +  | x => x);
   2.109 +
   2.110  
   2.111 - 
   2.112 -fun index_tree (Const ("DistinctTreeProver.tree.Tip",_)) path tab = tab
   2.113 -  | index_tree (Const ("DistinctTreeProver.tree.Node",_) $ l$ x $ _ $ r) path tab =
   2.114 -      tab 
   2.115 -      |> Termtab.update_new (x,path) 
   2.116 -      |> index_tree l (path@[Left])
   2.117 -      |> index_tree r (path@[Right])
   2.118 -  | index_tree t _ _ = raise TERM ("index_tree: input not a tree",[t])
   2.119 +fun index_tree (Const (@{const_name Tip}, _)) path tab = tab
   2.120 +  | index_tree (Const (@{const_name Node}, _) $ l $ x $ _ $ r) path tab =
   2.121 +      tab
   2.122 +      |> Termtab.update_new (x, path)
   2.123 +      |> index_tree l (path @ [Left])
   2.124 +      |> index_tree r (path @ [Right])
   2.125 +  | index_tree t _ _ = raise TERM ("index_tree: input not a tree", [t])
   2.126  
   2.127 -fun split_common_prefix xs [] = ([],xs,[])
   2.128 -  | split_common_prefix [] ys = ([],[],ys)
   2.129 -  | split_common_prefix (xs as (x::xs')) (ys as (y::ys')) =
   2.130 -     if x=y 
   2.131 -     then let val (ps,xs'',ys'') = split_common_prefix xs' ys' in (x::ps,xs'',ys'') end
   2.132 -     else ([],xs,ys)
   2.133 +fun split_common_prefix xs [] = ([], xs, [])
   2.134 +  | split_common_prefix [] ys = ([], [], ys)
   2.135 +  | split_common_prefix (xs as (x :: xs')) (ys as (y :: ys')) =
   2.136 +      if x = y
   2.137 +      then let val (ps, xs'', ys'') = split_common_prefix xs' ys' in (x :: ps, xs'', ys'') end
   2.138 +      else ([], xs, ys)
   2.139  
   2.140  
   2.141  (* Wrapper around Thm.instantiate. The type instiations of instTs are applied to
   2.142 @@ -106,14 +108,14 @@
   2.143   *)
   2.144  fun instantiate instTs insts =
   2.145    let
   2.146 -    val instTs' = map (fn (T,U) => (dest_TVar (typ_of T),typ_of U)) instTs;
   2.147 +    val instTs' = map (fn (T, U) => (dest_TVar (typ_of T), typ_of U)) instTs;
   2.148      fun substT x = (case AList.lookup (op =) instTs' x of NONE => TVar x | SOME T' => T');
   2.149      fun mapT_and_recertify ct =
   2.150        let
   2.151          val thy = theory_of_cterm ct;
   2.152        in (cterm_of thy (Term.map_types (Term.map_type_tvar substT) (term_of ct))) end;
   2.153      val insts' = map (apfst mapT_and_recertify) insts;
   2.154 -  in Thm.instantiate (instTs,insts') end;
   2.155 +  in Thm.instantiate (instTs, insts') end;
   2.156  
   2.157  fun tvar_clash ixn S S' = raise TYPE ("Type variable " ^
   2.158    quote (Term.string_of_vname ixn) ^ " has two distinct sorts",
   2.159 @@ -141,62 +143,69 @@
   2.160    in match end;
   2.161  
   2.162  
   2.163 -(* expects that relevant type variables are already contained in 
   2.164 +(* expects that relevant type variables are already contained in
   2.165   * term variables. First instantiation of variables is returned without further
   2.166   * checking.
   2.167   *)
   2.168 -fun naive_cterm_first_order_match (t,ct) env =
   2.169 +fun naive_cterm_first_order_match (t, ct) env =
   2.170    let
   2.171 -    val thy = (theory_of_cterm ct);
   2.172 -    fun mtch (env as (tyinsts,insts)) = fn
   2.173 -         (Var(ixn,T),ct) =>
   2.174 -           (case AList.lookup (op =) insts ixn of
   2.175 -             NONE => (naive_typ_match (T,typ_of (ctyp_of_term ct)) tyinsts,
   2.176 -                      (ixn, ct)::insts)
   2.177 -            | SOME _ => env)
   2.178 -        | (f$t,ct) => let val (cf,ct') = Thm.dest_comb ct;
   2.179 -                      in mtch (mtch env (f,cf)) (t,ct') end
   2.180 -        | _ => env
   2.181 -  in mtch env (t,ct) end;
   2.182 +    val thy = theory_of_cterm ct;
   2.183 +    fun mtch (env as (tyinsts, insts)) =
   2.184 +      fn (Var (ixn, T), ct) =>
   2.185 +          (case AList.lookup (op =) insts ixn of
   2.186 +            NONE => (naive_typ_match (T, typ_of (ctyp_of_term ct)) tyinsts, (ixn, ct) :: insts)
   2.187 +          | SOME _ => env)
   2.188 +       | (f $ t, ct) =>
   2.189 +          let val (cf, ct') = Thm.dest_comb ct;
   2.190 +          in mtch (mtch env (f, cf)) (t, ct') end
   2.191 +       | _ => env;
   2.192 +  in mtch env (t, ct) end;
   2.193  
   2.194  
   2.195  fun discharge prems rule =
   2.196    let
   2.197 -     val thy = theory_of_thm (hd prems);
   2.198 -     val (tyinsts,insts) =  
   2.199 -           fold naive_cterm_first_order_match (prems_of rule ~~ map cprop_of prems) ([],[]);
   2.200 +    val thy = theory_of_thm (hd prems);
   2.201 +    val (tyinsts,insts) =
   2.202 +      fold naive_cterm_first_order_match (prems_of rule ~~ map cprop_of prems) ([], []);
   2.203  
   2.204 -     val tyinsts' = map (fn (v,(S,U)) => (ctyp_of thy (TVar (v,S)),ctyp_of thy U)) 
   2.205 -                     tyinsts;
   2.206 -     val insts' = map (fn (idxn,ct) => (cterm_of thy (Var (idxn,typ_of (ctyp_of_term ct))),ct))  
   2.207 -                     insts;
   2.208 -     val rule' = Thm.instantiate (tyinsts',insts') rule;
   2.209 -   in fold Thm.elim_implies prems rule' end;
   2.210 +    val tyinsts' =
   2.211 +      map (fn (v, (S, U)) => (ctyp_of thy (TVar (v, S)), ctyp_of thy U)) tyinsts;
   2.212 +    val insts' =
   2.213 +      map (fn (idxn, ct) => (cterm_of thy (Var (idxn, typ_of (ctyp_of_term ct))), ct)) insts;
   2.214 +    val rule' = Thm.instantiate (tyinsts', insts') rule;
   2.215 +  in fold Thm.elim_implies prems rule' end;
   2.216  
   2.217  local
   2.218  
   2.219 -val (l_in_set_root,x_in_set_root,r_in_set_root) =
   2.220 -  let val (Node_l_x_d,r) = (cprop_of in_set_root) 
   2.221 -                         |> Thm.dest_comb |> #2 
   2.222 -                         |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb;
   2.223 -      val (Node_l,x) = Node_l_x_d |> Thm.dest_comb |> #1 |> Thm.dest_comb;
   2.224 -      val l = Node_l |> Thm.dest_comb |> #2;
   2.225 -  in (l,x,r) end
   2.226 -val (x_in_set_left,r_in_set_left) = 
   2.227 -  let val (Node_l_x_d,r) = (cprop_of in_set_left) 
   2.228 -                         |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
   2.229 -                         |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb;
   2.230 -      val x = Node_l_x_d |> Thm.dest_comb |> #1 |> Thm.dest_comb |> #2;
   2.231 -  in (x,r) end
   2.232 +val (l_in_set_root, x_in_set_root, r_in_set_root) =
   2.233 +  let
   2.234 +    val (Node_l_x_d, r) =
   2.235 +      cprop_of in_set_root
   2.236 +      |> Thm.dest_comb |> #2
   2.237 +      |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb;
   2.238 +    val (Node_l, x) = Node_l_x_d |> Thm.dest_comb |> #1 |> Thm.dest_comb;
   2.239 +    val l = Node_l |> Thm.dest_comb |> #2;
   2.240 +  in (l,x,r) end;
   2.241  
   2.242 -val (x_in_set_right,l_in_set_right) = 
   2.243 -  let val (Node_l,x) = (cprop_of in_set_right) 
   2.244 -                         |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
   2.245 -                         |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 
   2.246 -                         |> Thm.dest_comb |> #1 |> Thm.dest_comb |> #1 
   2.247 -                         |> Thm.dest_comb
   2.248 -      val l = Node_l |> Thm.dest_comb |> #2;
   2.249 -  in (x,l) end
   2.250 +val (x_in_set_left, r_in_set_left) =
   2.251 +  let
   2.252 +    val (Node_l_x_d, r) =
   2.253 +      cprop_of in_set_left
   2.254 +      |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
   2.255 +      |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb;
   2.256 +    val x = Node_l_x_d |> Thm.dest_comb |> #1 |> Thm.dest_comb |> #2;
   2.257 +  in (x, r) end;
   2.258 +
   2.259 +val (x_in_set_right, l_in_set_right) =
   2.260 +  let
   2.261 +    val (Node_l, x) =
   2.262 +      cprop_of in_set_right
   2.263 +      |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
   2.264 +      |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
   2.265 +      |> Thm.dest_comb |> #1 |> Thm.dest_comb |> #1
   2.266 +      |> Thm.dest_comb;
   2.267 +    val l = Node_l |> Thm.dest_comb |> #2;
   2.268 +  in (x, l) end;
   2.269  
   2.270  in
   2.271  (*
   2.272 @@ -210,118 +219,128 @@
   2.273  fun distinctTreeProver dist_thm x_path y_path =
   2.274    let
   2.275      fun dist_subtree [] thm = thm
   2.276 -      | dist_subtree (p::ps) thm =
   2.277 -         let 
   2.278 +      | dist_subtree (p :: ps) thm =
   2.279 +         let
   2.280             val rule = (case p of Left => all_distinct_left | Right => all_distinct_right)
   2.281           in dist_subtree ps (discharge [thm] rule) end;
   2.282  
   2.283 -    val (ps,x_rest,y_rest) = split_common_prefix x_path y_path;
   2.284 +    val (ps, x_rest, y_rest) = split_common_prefix x_path y_path;
   2.285      val dist_subtree_thm = dist_subtree ps dist_thm;
   2.286      val subtree = cprop_of dist_subtree_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
   2.287 -    val (_,[l,_,_,r]) = Drule.strip_comb subtree;
   2.288 -    
   2.289 +    val (_, [l, _, _, r]) = Drule.strip_comb subtree;
   2.290 +
   2.291      fun in_set ps tree =
   2.292        let
   2.293 -        val (_,[l,x,_,r]) = Drule.strip_comb tree;
   2.294 +        val (_, [l, x, _, r]) = Drule.strip_comb tree;
   2.295          val xT = ctyp_of_term x;
   2.296 -      in (case ps of
   2.297 -            [] => instantiate 
   2.298 -                    [(ctyp_of_term x_in_set_root,xT)]
   2.299 -                    [(l_in_set_root,l),(x_in_set_root,x),(r_in_set_root,r)] in_set_root
   2.300 -          | (Left::ps') => 
   2.301 -               let
   2.302 -                  val in_set_l = in_set ps' l;
   2.303 -                  val in_set_left' = instantiate [(ctyp_of_term x_in_set_left,xT)]
   2.304 -                                      [(x_in_set_left,x),(r_in_set_left,r)] in_set_left;
   2.305 -               in discharge [in_set_l] in_set_left' end
   2.306 -          | (Right::ps') => 
   2.307 -               let
   2.308 -                  val in_set_r = in_set ps' r;
   2.309 -                  val in_set_right' = instantiate [(ctyp_of_term x_in_set_right,xT)] 
   2.310 -                                      [(x_in_set_right,x),(l_in_set_right,l)] in_set_right;
   2.311 -               in discharge [in_set_r] in_set_right' end)
   2.312 -      end 
   2.313 -       
   2.314 -  fun in_set' [] = raise TERM ("distinctTreeProver",[])
   2.315 -    | in_set' (Left::ps) = in_set ps l
   2.316 -    | in_set' (Right::ps) = in_set ps r;
   2.317 +      in
   2.318 +        (case ps of
   2.319 +          [] =>
   2.320 +            instantiate
   2.321 +              [(ctyp_of_term x_in_set_root, xT)]
   2.322 +              [(l_in_set_root, l), (x_in_set_root, x), (r_in_set_root, r)] in_set_root
   2.323 +        | Left :: ps' =>
   2.324 +            let
   2.325 +              val in_set_l = in_set ps' l;
   2.326 +              val in_set_left' =
   2.327 +                instantiate
   2.328 +                  [(ctyp_of_term x_in_set_left, xT)]
   2.329 +                  [(x_in_set_left, x), (r_in_set_left, r)] in_set_left;
   2.330 +            in discharge [in_set_l] in_set_left' end
   2.331 +        | Right :: ps' =>
   2.332 +            let
   2.333 +              val in_set_r = in_set ps' r;
   2.334 +              val in_set_right' =
   2.335 +                instantiate
   2.336 +                  [(ctyp_of_term x_in_set_right, xT)]
   2.337 +                  [(x_in_set_right, x), (l_in_set_right, l)] in_set_right;
   2.338 +            in discharge [in_set_r] in_set_right' end)
   2.339 +      end;
   2.340  
   2.341 -  fun distinct_lr node_in_set Left  = discharge [dist_subtree_thm,node_in_set] distinct_left 
   2.342 -    | distinct_lr node_in_set Right = discharge [dist_subtree_thm,node_in_set] distinct_right 
   2.343 +  fun in_set' [] = raise TERM ("distinctTreeProver", [])
   2.344 +    | in_set' (Left :: ps) = in_set ps l
   2.345 +    | in_set' (Right :: ps) = in_set ps r;
   2.346 +
   2.347 +  fun distinct_lr node_in_set Left  = discharge [dist_subtree_thm,node_in_set] distinct_left
   2.348 +    | distinct_lr node_in_set Right = discharge [dist_subtree_thm,node_in_set] distinct_right
   2.349  
   2.350 -  val (swap,neq) = 
   2.351 -       (case x_rest of
   2.352 -         [] => let 
   2.353 -                 val y_in_set = in_set' y_rest;
   2.354 -               in (false,distinct_lr y_in_set (hd y_rest)) end
   2.355 -       | (xr::xrs) => 
   2.356 -           (case y_rest of
   2.357 -             [] => let 
   2.358 -                     val x_in_set = in_set' x_rest;
   2.359 -               in (true,distinct_lr x_in_set (hd x_rest)) end
   2.360 -           | (yr::yrs) =>
   2.361 -               let
   2.362 -                 val x_in_set = in_set' x_rest;
   2.363 -                 val y_in_set = in_set' y_rest;
   2.364 -               in (case xr of
   2.365 -                    Left => (false,
   2.366 -                             discharge [dist_subtree_thm,x_in_set,y_in_set] distinct_left_right)
   2.367 -                   |Right => (true,
   2.368 -                             discharge [dist_subtree_thm,y_in_set,x_in_set] distinct_left_right))
   2.369 -               end
   2.370 -        ))
   2.371 -  in if swap then discharge [neq] swap_neq else neq
   2.372 -  end  
   2.373 +  val (swap, neq) =
   2.374 +    (case x_rest of
   2.375 +      [] =>
   2.376 +        let val y_in_set = in_set' y_rest;
   2.377 +        in (false, distinct_lr y_in_set (hd y_rest)) end
   2.378 +    | xr :: xrs =>
   2.379 +        (case y_rest of
   2.380 +          [] =>
   2.381 +            let val x_in_set = in_set' x_rest;
   2.382 +            in (true, distinct_lr x_in_set (hd x_rest)) end
   2.383 +        | yr :: yrs =>
   2.384 +            let
   2.385 +              val x_in_set = in_set' x_rest;
   2.386 +              val y_in_set = in_set' y_rest;
   2.387 +            in
   2.388 +              (case xr of
   2.389 +                Left => (false, discharge [dist_subtree_thm,x_in_set,y_in_set] distinct_left_right)
   2.390 +              | Right => (true, discharge [dist_subtree_thm,y_in_set,x_in_set] distinct_left_right))
   2.391 +           end));
   2.392 +  in if swap then discharge [neq] swap_neq else neq end;
   2.393  
   2.394  
   2.395 -val delete_root = @{thm DistinctTreeProver.delete_root};
   2.396 -val delete_left = @{thm DistinctTreeProver.delete_left};
   2.397 -val delete_right = @{thm DistinctTreeProver.delete_right};
   2.398 +val delete_root = @{thm delete_root};
   2.399 +val delete_left = @{thm delete_left};
   2.400 +val delete_right = @{thm delete_right};
   2.401  
   2.402  fun deleteProver dist_thm [] = delete_root OF [dist_thm]
   2.403    | deleteProver dist_thm (p::ps) =
   2.404 -     let
   2.405 -       val dist_rule = (case p of Left => all_distinct_left | Right => all_distinct_right);
   2.406 -       val dist_thm' = discharge [dist_thm] dist_rule 
   2.407 -       val del_rule = (case p of Left => delete_left | Right => delete_right)
   2.408 -       val del = deleteProver dist_thm' ps;
   2.409 -     in discharge [dist_thm, del] del_rule end;
   2.410 +      let
   2.411 +        val dist_rule = (case p of Left => all_distinct_left | Right => all_distinct_right);
   2.412 +        val dist_thm' = discharge [dist_thm] dist_rule;
   2.413 +        val del_rule = (case p of Left => delete_left | Right => delete_right);
   2.414 +        val del = deleteProver dist_thm' ps;
   2.415 +      in discharge [dist_thm, del] del_rule end;
   2.416  
   2.417 -val subtract_Tip = @{thm DistinctTreeProver.subtract_Tip};
   2.418 -val subtract_Node = @{thm DistinctTreeProver.subtract_Node};
   2.419 -val delete_Some_all_distinct = @{thm DistinctTreeProver.delete_Some_all_distinct};
   2.420 -val subtract_Some_all_distinct_res = @{thm DistinctTreeProver.subtract_Some_all_distinct_res};
   2.421 +val subtract_Tip = @{thm subtract_Tip};
   2.422 +val subtract_Node = @{thm subtract_Node};
   2.423 +val delete_Some_all_distinct = @{thm delete_Some_all_distinct};
   2.424 +val subtract_Some_all_distinct_res = @{thm subtract_Some_all_distinct_res};
   2.425  
   2.426  local
   2.427 -  val (alpha,v) = 
   2.428 +  val (alpha, v) =
   2.429      let
   2.430 -      val ct = subtract_Tip |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 
   2.431 -               |> Thm.dest_comb |> #2
   2.432 +      val ct =
   2.433 +        subtract_Tip |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
   2.434 +        |> Thm.dest_comb |> #2;
   2.435        val [alpha] = ct |> Thm.ctyp_of_term |> Thm.dest_ctyp;
   2.436      in (alpha, #1 (dest_Var (term_of ct))) end;
   2.437  in
   2.438 -fun subtractProver (Const ("DistinctTreeProver.tree.Tip",T)) ct dist_thm =
   2.439 -    let 
   2.440 -      val ct' = dist_thm |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
   2.441 -      val thy = theory_of_cterm ct;
   2.442 -      val [alphaI] = #2 (dest_Type T);
   2.443 -    in Thm.instantiate ([(alpha,ctyp_of thy alphaI)],
   2.444 -                        [(cterm_of thy (Var (v,treeT alphaI)),ct')]) subtract_Tip
   2.445 -    end
   2.446 -  | subtractProver (Const ("DistinctTreeProver.tree.Node",nT)$l$x$d$r) ct dist_thm =
   2.447 -    let
   2.448 -      val ct' = dist_thm |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
   2.449 -      val (_,[cl,_,_,cr]) = Drule.strip_comb ct;
   2.450 -      val ps = the (find_tree x (term_of ct'));
   2.451 -      val del_tree = deleteProver dist_thm ps;
   2.452 -      val dist_thm' = discharge [del_tree, dist_thm] delete_Some_all_distinct; 
   2.453 -      val sub_l = subtractProver (term_of cl) cl (dist_thm');
   2.454 -      val sub_r = subtractProver (term_of cr) cr 
   2.455 -                    (discharge [sub_l, dist_thm'] subtract_Some_all_distinct_res);
   2.456 -    in discharge [del_tree, sub_l, sub_r] subtract_Node end
   2.457 -end
   2.458  
   2.459 -val subtract_Some_all_distinct = @{thm DistinctTreeProver.subtract_Some_all_distinct};
   2.460 +fun subtractProver (Const (@{const_name Tip}, T)) ct dist_thm =
   2.461 +      let
   2.462 +        val ct' = dist_thm |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
   2.463 +        val thy = theory_of_cterm ct;
   2.464 +        val [alphaI] = #2 (dest_Type T);
   2.465 +      in
   2.466 +        Thm.instantiate
   2.467 +          ([(alpha, ctyp_of thy alphaI)],
   2.468 +           [(cterm_of thy (Var (v, treeT alphaI)), ct')]) subtract_Tip
   2.469 +      end
   2.470 +  | subtractProver (Const (@{const_name Node}, nT) $ l $ x $ d $ r) ct dist_thm =
   2.471 +      let
   2.472 +        val ct' = dist_thm |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
   2.473 +        val (_, [cl, _, _, cr]) = Drule.strip_comb ct;
   2.474 +        val ps = the (find_tree x (term_of ct'));
   2.475 +        val del_tree = deleteProver dist_thm ps;
   2.476 +        val dist_thm' = discharge [del_tree, dist_thm] delete_Some_all_distinct;
   2.477 +        val sub_l = subtractProver (term_of cl) cl (dist_thm');
   2.478 +        val sub_r =
   2.479 +          subtractProver (term_of cr) cr
   2.480 +            (discharge [sub_l, dist_thm'] subtract_Some_all_distinct_res);
   2.481 +      in discharge [del_tree, sub_l, sub_r] subtract_Node end;
   2.482 +
   2.483 +end;
   2.484 +
   2.485 +val subtract_Some_all_distinct = @{thm subtract_Some_all_distinct};
   2.486 +
   2.487  fun distinct_implProver dist_thm ct =
   2.488    let
   2.489      val ctree = ct |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
   2.490 @@ -329,8 +348,10 @@
   2.491    in subtract_Some_all_distinct OF [sub, dist_thm] end;
   2.492  
   2.493  fun get_fst_success f [] = NONE
   2.494 -  | get_fst_success f (x::xs) = (case f x of NONE => get_fst_success f xs 
   2.495 -                                 | SOME v => SOME v);
   2.496 +  | get_fst_success f (x :: xs) =
   2.497 +      (case f x of
   2.498 +        NONE => get_fst_success f xs
   2.499 +      | SOME v => SOME v);
   2.500  
   2.501  fun neq_x_y ctxt x y name =
   2.502    (let
   2.503 @@ -340,8 +361,8 @@
   2.504      val x_path = the (find_tree x tree);
   2.505      val y_path = the (find_tree y tree);
   2.506      val thm = distinctTreeProver dist_thm x_path y_path;
   2.507 -  in SOME thm  
   2.508 -  end handle Option => NONE)
   2.509 +  in SOME thm
   2.510 +  end handle Option.Option => NONE);
   2.511  
   2.512  fun distinctTree_tac names ctxt = SUBGOAL (fn (goal, i) =>
   2.513      (case goal of
   2.514 @@ -352,17 +373,18 @@
   2.515          | NONE => no_tac)
   2.516      | _ => no_tac))
   2.517  
   2.518 -fun distinctFieldSolver names = mk_solver "distinctFieldSolver"
   2.519 -     (distinctTree_tac names o Simplifier.the_context)
   2.520 +fun distinctFieldSolver names =
   2.521 +  mk_solver "distinctFieldSolver" (distinctTree_tac names o Simplifier.the_context);
   2.522  
   2.523  fun distinct_simproc names =
   2.524    Simplifier.simproc_global @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"]
   2.525 -    (fn thy => fn ss => fn (Const (@{const_name HOL.eq},_)$x$y) =>
   2.526 -        case try Simplifier.the_context ss of
   2.527 -        SOME ctxt => Option.map (fn neq => neq_to_eq_False OF [neq]) 
   2.528 -                      (get_fst_success (neq_x_y ctxt x y) names)
   2.529 -       | NONE => NONE
   2.530 -    )
   2.531 +    (fn thy => fn ss => fn (Const (@{const_name HOL.eq}, _) $ x $ y) =>
   2.532 +      (case try Simplifier.the_context ss of
   2.533 +        SOME ctxt =>
   2.534 +          Option.map (fn neq => neq_to_eq_False OF [neq])
   2.535 +            (get_fst_success (neq_x_y ctxt x y) names)
   2.536 +      | NONE => NONE));
   2.537  
   2.538 -end
   2.539 +end;
   2.540 +
   2.541  end;
   2.542 \ No newline at end of file