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