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