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