src/HOL/Statespace/distinct_tree_prover.ML
changeset 25171 4a9c25bffc9b
child 25408 156f6f7082b8
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Statespace/distinct_tree_prover.ML	Wed Oct 24 18:36:09 2007 +0200
     1.3 @@ -0,0 +1,349 @@
     1.4 +(*  Title:      distinct_tree_prover.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Norbert Schirmer, TU Muenchen
     1.7 +*)
     1.8 +
     1.9 +structure DistinctTreeProver =
    1.10 +struct
    1.11 +val all_distinct_left = thm "DistinctTreeProver.all_distinct_left";
    1.12 +val all_distinct_right = thm "DistinctTreeProver.all_distinct_right";
    1.13 +
    1.14 +val distinct_left = thm "DistinctTreeProver.distinct_left";
    1.15 +val distinct_right = thm "DistinctTreeProver.distinct_right";
    1.16 +val distinct_left_right = thm "DistinctTreeProver.distinct_left_right";
    1.17 +val in_set_root = thm "DistinctTreeProver.in_set_root";
    1.18 +val in_set_left = thm "DistinctTreeProver.in_set_left";
    1.19 +val in_set_right = thm "DistinctTreeProver.in_set_right";
    1.20 +
    1.21 +val swap_neq = thm "DistinctTreeProver.swap_neq";
    1.22 +val neq_to_eq_False = thm "DistinctTreeProver.neq_to_eq_False"
    1.23 +
    1.24 +fun treeT T = Type ("DistinctTreeProver.tree",[T]);
    1.25 +fun mk_tree' e T n []     = Const ("DistinctTreeProver.tree.Tip",treeT T)
    1.26 +  | mk_tree' e T n xs =
    1.27 +     let
    1.28 +       val m = (n - 1) div 2;
    1.29 +       val (xsl,x::xsr) = chop m xs;
    1.30 +       val l = mk_tree' e T m xsl;
    1.31 +       val r = mk_tree' e T (n-(m+1)) xsr;
    1.32 +     in Const ("DistinctTreeProver.tree.Node",
    1.33 +                treeT T --> T --> HOLogic.boolT--> treeT T --> treeT T) $ 
    1.34 +          l$ e x $ HOLogic.false_const $ r 
    1.35 +     end
    1.36 +
    1.37 +fun mk_tree e T xs = mk_tree' e T (length xs) xs;         
    1.38 +
    1.39 +fun dest_tree (Const ("DistinctTreeProver.tree.Tip",_)) = []
    1.40 +  | dest_tree (Const ("DistinctTreeProver.tree.Node",_)$l$e$_$r) = dest_tree l @ e :: dest_tree r
    1.41 +  | dest_tree t = raise TERM ("DistinctTreeProver.dest_tree",[t]);
    1.42 +
    1.43 +datatype Direction = Left | Right 
    1.44 +
    1.45 +fun lin_find_tree e (Const ("DistinctTreeProver.tree.Tip",_)) = NONE
    1.46 +  | lin_find_tree e (Const ("DistinctTreeProver.tree.Node",_) $ l$ x $ _ $ r) =
    1.47 +      if e aconv x 
    1.48 +      then SOME []
    1.49 +      else (case lin_find_tree e l of
    1.50 +              SOME path => SOME (Left::path)
    1.51 +            | NONE => (case lin_find_tree e r of
    1.52 +                        SOME path => SOME (Right::path)
    1.53 +                       | NONE => NONE))
    1.54 +  | lin_find_tree e t = raise TERM ("find_tree: input not a tree",[t])
    1.55 +
    1.56 +fun bin_find_tree order e (Const ("DistinctTreeProver.tree.Tip",_)) = NONE
    1.57 +  | bin_find_tree order e (Const ("DistinctTreeProver.tree.Node",_) $ l$ x $ _ $ r) =
    1.58 +      (case order (e,x) of
    1.59 +         EQUAL => SOME []
    1.60 +       | LESS => Option.map (cons Left) (bin_find_tree order e l)
    1.61 +       | GREATER => Option.map (cons Right) (bin_find_tree order e r))
    1.62 +  | bin_find_tree order e t = raise TERM ("find_tree: input not a tree",[t])
    1.63 +
    1.64 +fun find_tree e t =
    1.65 +  (case bin_find_tree Term.fast_term_ord e t of
    1.66 +     NONE => lin_find_tree e t
    1.67 +   | x => x);
    1.68 +
    1.69 + 
    1.70 +fun index_tree (Const ("DistinctTreeProver.tree.Tip",_)) path tab = tab
    1.71 +  | index_tree (Const ("DistinctTreeProver.tree.Node",_) $ l$ x $ _ $ r) path tab =
    1.72 +      tab 
    1.73 +      |> Termtab.update_new (x,path) 
    1.74 +      |> index_tree l (path@[Left])
    1.75 +      |> index_tree r (path@[Right])
    1.76 +  | index_tree t _ _ = raise TERM ("index_tree: input not a tree",[t])
    1.77 +
    1.78 +fun split_common_prefix xs [] = ([],xs,[])
    1.79 +  | split_common_prefix [] ys = ([],[],ys)
    1.80 +  | split_common_prefix (xs as (x::xs')) (ys as (y::ys')) =
    1.81 +     if x=y 
    1.82 +     then let val (ps,xs'',ys'') = split_common_prefix xs' ys' in (x::ps,xs'',ys'') end
    1.83 +     else ([],xs,ys)
    1.84 +
    1.85 +
    1.86 +(* Wrapper around Thm.instantiate. The type instiations of instTs are applied to
    1.87 + * the right hand sides of insts
    1.88 + *)
    1.89 +fun instantiate instTs insts =
    1.90 +  let
    1.91 +    val instTs' = map (fn (T,U) => (dest_TVar (typ_of T),typ_of U)) instTs;
    1.92 +    fun substT x = (case AList.lookup (op =) instTs' x of NONE => TVar x | SOME T' => T');
    1.93 +    fun mapT_and_recertify ct =
    1.94 +      let
    1.95 +        val thy = theory_of_cterm ct;
    1.96 +      in (cterm_of thy (Term.map_types (Term.map_type_tvar substT) (term_of ct))) end;
    1.97 +    val insts' = map (apfst mapT_and_recertify) insts;
    1.98 +  in Thm.instantiate (instTs,insts') end;
    1.99 +
   1.100 +fun tvar_clash ixn S S' = raise TYPE ("Type variable " ^
   1.101 +  quote (Term.string_of_vname ixn) ^ " has two distinct sorts",
   1.102 +  [TVar (ixn, S), TVar (ixn, S')], []);
   1.103 +
   1.104 +fun lookup (tye, (ixn, S)) =
   1.105 +  (case AList.lookup (op =) tye ixn of
   1.106 +    NONE => NONE
   1.107 +  | SOME (S', T) => if S = S' then SOME T else tvar_clash ixn S S');
   1.108 +
   1.109 +val naive_typ_match =
   1.110 +  let
   1.111 +    fun match (TVar (v, S), T) subs =
   1.112 +          (case lookup (subs, (v, S)) of
   1.113 +            NONE => ((v, (S, T))::subs)
   1.114 +          | SOME _ => subs)
   1.115 +      | match (Type (a, Ts), Type (b, Us)) subs =
   1.116 +          if a <> b then raise Type.TYPE_MATCH
   1.117 +          else matches (Ts, Us) subs
   1.118 +      | match (TFree x, TFree y) subs =
   1.119 +          if x = y then subs else raise Type.TYPE_MATCH
   1.120 +      | match _ _ = raise Type.TYPE_MATCH
   1.121 +    and matches (T :: Ts, U :: Us) subs = matches (Ts, Us) (match (T, U) subs)
   1.122 +      | matches _ subs = subs;
   1.123 +  in match end;
   1.124 +
   1.125 +
   1.126 +(* expects that relevant type variables are already contained in 
   1.127 + * term variables. First instantiation of variables is returned without further
   1.128 + * checking.
   1.129 + *)
   1.130 +fun naive_cterm_first_order_match (t,ct) env =
   1.131 +  let
   1.132 +    val thy = (theory_of_cterm ct);
   1.133 +    fun mtch (env as (tyinsts,insts)) = fn
   1.134 +         (Var(ixn,T),ct) =>
   1.135 +           (case AList.lookup (op =) insts ixn of
   1.136 +             NONE => (naive_typ_match (T,typ_of (ctyp_of_term ct)) tyinsts,
   1.137 +                      (ixn, ct)::insts)
   1.138 +            | SOME _ => env)
   1.139 +        | (f$t,ct) => let val (cf,ct') = Thm.dest_comb ct;
   1.140 +                      in mtch (mtch env (f,cf)) (t,ct') end
   1.141 +        | _ => env
   1.142 +  in mtch env (t,ct) end;
   1.143 +
   1.144 +
   1.145 +fun mp prem rule = implies_elim rule prem;
   1.146 +
   1.147 +fun discharge prems rule =
   1.148 +  let
   1.149 +     val thy = theory_of_thm (hd prems);
   1.150 +     val (tyinsts,insts) =  
   1.151 +           fold naive_cterm_first_order_match (prems_of rule ~~ map cprop_of prems) ([],[]);
   1.152 +
   1.153 +     val tyinsts' = map (fn (v,(S,U)) => (ctyp_of thy (TVar (v,S)),ctyp_of thy U)) 
   1.154 +                     tyinsts;
   1.155 +     val insts' = map (fn (idxn,ct) => (cterm_of thy (Var (idxn,typ_of (ctyp_of_term ct))),ct))  
   1.156 +                     insts;
   1.157 +     val rule' = Thm.instantiate (tyinsts',insts') rule;
   1.158 +   in fold mp prems rule' end;
   1.159 +
   1.160 +local
   1.161 +
   1.162 +val (l_in_set_root,x_in_set_root,r_in_set_root) =
   1.163 +  let val (Node_l_x_d,r) = (cprop_of in_set_root) 
   1.164 +                         |> Thm.dest_comb |> #2 
   1.165 +                         |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb;
   1.166 +      val (Node_l,x) = Node_l_x_d |> Thm.dest_comb |> #1 |> Thm.dest_comb;
   1.167 +      val l = Node_l |> Thm.dest_comb |> #2;
   1.168 +  in (l,x,r) end
   1.169 +val (x_in_set_left,r_in_set_left) = 
   1.170 +  let val (Node_l_x_d,r) = (cprop_of in_set_left) 
   1.171 +                         |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
   1.172 +                         |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb;
   1.173 +      val x = Node_l_x_d |> Thm.dest_comb |> #1 |> Thm.dest_comb |> #2;
   1.174 +  in (x,r) end
   1.175 +
   1.176 +val (x_in_set_right,l_in_set_right) = 
   1.177 +  let val (Node_l,x) = (cprop_of in_set_right) 
   1.178 +                         |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
   1.179 +                         |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 
   1.180 +                         |> Thm.dest_comb |> #1 |> Thm.dest_comb |> #1 
   1.181 +                         |> Thm.dest_comb
   1.182 +      val l = Node_l |> Thm.dest_comb |> #2;
   1.183 +  in (x,l) end
   1.184 +
   1.185 +in
   1.186 +(*
   1.187 +1. First get paths x_path y_path of x and y in the tree.
   1.188 +2. For the common prefix descend into the tree according to the path
   1.189 +   and lemmas all_distinct_left/right
   1.190 +3. If one restpath is empty use distinct_left/right,
   1.191 +   otherwise all_distinct_left_right
   1.192 +*)
   1.193 +
   1.194 +fun distinctTreeProver dist_thm x_path y_path =
   1.195 +  let
   1.196 +    fun dist_subtree [] thm = thm
   1.197 +      | dist_subtree (p::ps) thm =
   1.198 +         let 
   1.199 +           val rule = (case p of Left => all_distinct_left | Right => all_distinct_right)
   1.200 +         in dist_subtree ps (discharge [thm] rule) end;
   1.201 +
   1.202 +    val (ps,x_rest,y_rest) = split_common_prefix x_path y_path;
   1.203 +    val dist_subtree_thm = dist_subtree ps dist_thm;
   1.204 +    val subtree = cprop_of dist_subtree_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
   1.205 +    val (_,[l,_,_,r]) = Drule.strip_comb subtree;
   1.206 +    
   1.207 +    fun in_set ps tree =
   1.208 +      let
   1.209 +        val (_,[l,x,_,r]) = Drule.strip_comb tree;
   1.210 +        val xT = ctyp_of_term x;
   1.211 +      in (case ps of
   1.212 +            [] => instantiate 
   1.213 +                    [(ctyp_of_term x_in_set_root,xT)]
   1.214 +                    [(l_in_set_root,l),(x_in_set_root,x),(r_in_set_root,r)] in_set_root
   1.215 +          | (Left::ps') => 
   1.216 +               let
   1.217 +                  val in_set_l = in_set ps' l;
   1.218 +                  val in_set_left' = instantiate [(ctyp_of_term x_in_set_left,xT)]
   1.219 +                                      [(x_in_set_left,x),(r_in_set_left,r)] in_set_left;
   1.220 +               in discharge [in_set_l] in_set_left' end
   1.221 +          | (Right::ps') => 
   1.222 +               let
   1.223 +                  val in_set_r = in_set ps' r;
   1.224 +                  val in_set_right' = instantiate [(ctyp_of_term x_in_set_right,xT)] 
   1.225 +                                      [(x_in_set_right,x),(l_in_set_right,l)] in_set_right;
   1.226 +               in discharge [in_set_r] in_set_right' end)
   1.227 +      end 
   1.228 +       
   1.229 +  fun in_set' [] = raise TERM ("distinctTreeProver",[])
   1.230 +    | in_set' (Left::ps) = in_set ps l
   1.231 +    | in_set' (Right::ps) = in_set ps r;
   1.232 +
   1.233 +  fun distinct_lr node_in_set Left  = discharge [dist_subtree_thm,node_in_set] distinct_left 
   1.234 +    | distinct_lr node_in_set Right = discharge [dist_subtree_thm,node_in_set] distinct_right 
   1.235 +
   1.236 +  val (swap,neq) = 
   1.237 +       (case x_rest of
   1.238 +         [] => let 
   1.239 +                 val y_in_set = in_set' y_rest;
   1.240 +               in (false,distinct_lr y_in_set (hd y_rest)) end
   1.241 +       | (xr::xrs) => 
   1.242 +           (case y_rest of
   1.243 +             [] => let 
   1.244 +                     val x_in_set = in_set' x_rest;
   1.245 +               in (true,distinct_lr x_in_set (hd x_rest)) end
   1.246 +           | (yr::yrs) =>
   1.247 +               let
   1.248 +                 val x_in_set = in_set' x_rest;
   1.249 +                 val y_in_set = in_set' y_rest;
   1.250 +               in (case xr of
   1.251 +                    Left => (false,
   1.252 +                             discharge [dist_subtree_thm,x_in_set,y_in_set] distinct_left_right)
   1.253 +                   |Right => (true,
   1.254 +                             discharge [dist_subtree_thm,y_in_set,x_in_set] distinct_left_right))
   1.255 +               end
   1.256 +        ))
   1.257 +  in if swap then discharge [neq] swap_neq else neq
   1.258 +  end  
   1.259 +
   1.260 +
   1.261 +val delete_root = thm "DistinctTreeProver.delete_root";
   1.262 +val delete_left = thm "DistinctTreeProver.delete_left";
   1.263 +val delete_right = thm "DistinctTreeProver.delete_right";
   1.264 +
   1.265 +fun deleteProver dist_thm [] = delete_root OF [dist_thm]
   1.266 +  | deleteProver dist_thm (p::ps) =
   1.267 +     let
   1.268 +       val dist_rule = (case p of Left => all_distinct_left | Right => all_distinct_right);
   1.269 +       val dist_thm' = discharge [dist_thm] dist_rule 
   1.270 +       val del_rule = (case p of Left => delete_left | Right => delete_right)
   1.271 +       val del = deleteProver dist_thm' ps;
   1.272 +     in discharge [dist_thm, del] del_rule end;
   1.273 +
   1.274 +val subtract_Tip = thm "DistinctTreeProver.subtract_Tip";
   1.275 +val subtract_Node = thm "DistinctTreeProver.subtract_Node";
   1.276 +val delete_Some_all_distinct = thm "DistinctTreeProver.delete_Some_all_distinct";
   1.277 +val subtract_Some_all_distinct_res = thm "DistinctTreeProver.subtract_Some_all_distinct_res";
   1.278 +
   1.279 +local
   1.280 +  val (alpha,v) = 
   1.281 +    let
   1.282 +      val ct = subtract_Tip |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 
   1.283 +               |> Thm.dest_comb |> #2
   1.284 +      val [alpha] = ct |> Thm.ctyp_of_term |> Thm.dest_ctyp;
   1.285 +    in (alpha, #1 (dest_Var (term_of ct))) end;
   1.286 +in
   1.287 +fun subtractProver (Const ("DistinctTreeProver.tree.Tip",T)) ct dist_thm =
   1.288 +    let 
   1.289 +      val ct' = dist_thm |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
   1.290 +      val thy = theory_of_cterm ct;
   1.291 +      val [alphaI] = #2 (dest_Type T);
   1.292 +    in Thm.instantiate ([(alpha,ctyp_of thy alphaI)],
   1.293 +                        [(cterm_of thy (Var (v,treeT alphaI)),ct')]) subtract_Tip
   1.294 +    end
   1.295 +  | subtractProver (Const ("DistinctTreeProver.tree.Node",nT)$l$x$d$r) ct dist_thm =
   1.296 +    let
   1.297 +      val ct' = dist_thm |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
   1.298 +      val (_,[cl,_,_,cr]) = Drule.strip_comb ct;
   1.299 +      val ps = the (find_tree x (term_of ct'));
   1.300 +      val del_tree = deleteProver dist_thm ps;
   1.301 +      val dist_thm' = discharge [del_tree, dist_thm] delete_Some_all_distinct; 
   1.302 +      val sub_l = subtractProver (term_of cl) cl (dist_thm');
   1.303 +      val sub_r = subtractProver (term_of cr) cr 
   1.304 +                    (discharge [sub_l, dist_thm'] subtract_Some_all_distinct_res);
   1.305 +    in discharge [del_tree, sub_l, sub_r] subtract_Node end
   1.306 +end
   1.307 +
   1.308 +val subtract_Some_all_distinct = thm "DistinctTreeProver.subtract_Some_all_distinct";
   1.309 +fun distinct_implProver dist_thm ct =
   1.310 +  let
   1.311 +    val ctree = ct |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
   1.312 +    val sub = subtractProver (term_of ctree) ctree dist_thm;
   1.313 +  in subtract_Some_all_distinct OF [sub, dist_thm] end;
   1.314 +
   1.315 +fun get_fst_success f [] = NONE
   1.316 +  | get_fst_success f (x::xs) = (case f x of NONE => get_fst_success f xs 
   1.317 +                                 | SOME v => SOME v);
   1.318 +
   1.319 +fun neq_x_y ctxt x y name =
   1.320 +  (let
   1.321 +    val dist_thm = the (try (ProofContext.get_thm ctxt) (PureThy.Name name)); 
   1.322 +    val ctree = cprop_of dist_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
   1.323 +    val tree = term_of ctree;
   1.324 +    val x_path = the (find_tree x tree);
   1.325 +    val y_path = the (find_tree y tree);
   1.326 +    val thm = distinctTreeProver dist_thm x_path y_path;
   1.327 +  in SOME thm  
   1.328 +  end handle Option => NONE)
   1.329 +
   1.330 +fun distinctTree_tac names ctxt 
   1.331 +      (Const ("Trueprop",_) $ (Const ("Not", _) $ (Const ("op =", _) $ x $ y)), i) =
   1.332 +  (case get_fst_success (neq_x_y ctxt x y) names of
   1.333 +     SOME neq => rtac neq i
   1.334 +   | NONE => no_tac)
   1.335 +  | distinctTree_tac _ _ _ = no_tac;
   1.336 +
   1.337 +fun distinctFieldSolver names = mk_solver' "distinctFieldSolver"
   1.338 +     (fn ss => case #context (#1 (rep_ss ss)) of
   1.339 +                 SOME ctxt => SUBGOAL (distinctTree_tac names ctxt)
   1.340 +                | NONE => fn i => no_tac)
   1.341 +
   1.342 +fun distinct_simproc names =
   1.343 +  Simplifier.simproc HOL.thy "DistinctTreeProver.distinct_simproc" ["x = y"]
   1.344 +    (fn thy => fn ss => fn (Const ("op =",_)$x$y) =>
   1.345 +        case #context (#1 (rep_ss ss)) of
   1.346 +        SOME ctxt => Option.map (fn neq => neq_to_eq_False OF [neq]) 
   1.347 +                      (get_fst_success (neq_x_y ctxt x y) names)
   1.348 +       | NONE => NONE
   1.349 +    )
   1.350 +
   1.351 +end
   1.352 +end;
   1.353 \ No newline at end of file