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