(* Title: HOL/Statespace/distinct_tree_prover.ML
Author: Norbert Schirmer, TU Muenchen
*)
signature DISTINCT_TREE_PROVER =
sig
datatype Direction = Left | Right
val mk_tree : ('a -> term) -> typ -> 'a list -> term
val dest_tree : term -> term list
val find_tree : term -> term -> Direction list option
val neq_to_eq_False : thm
val distinctTreeProver : thm -> Direction list -> Direction list -> thm
val neq_x_y : Proof.context -> term -> term -> string -> thm option
val distinctFieldSolver : string list -> solver
val distinctTree_tac : string list -> Proof.context -> term * int -> tactic
val distinct_implProver : thm -> cterm -> thm
val subtractProver : term -> cterm -> thm -> thm
val distinct_simproc : string list -> simproc
val discharge : thm list -> thm -> thm
end;
structure DistinctTreeProver : DISTINCT_TREE_PROVER =
struct
val all_distinct_left = thm "DistinctTreeProver.all_distinct_left";
val all_distinct_right = thm "DistinctTreeProver.all_distinct_right";
val distinct_left = thm "DistinctTreeProver.distinct_left";
val distinct_right = thm "DistinctTreeProver.distinct_right";
val distinct_left_right = thm "DistinctTreeProver.distinct_left_right";
val in_set_root = thm "DistinctTreeProver.in_set_root";
val in_set_left = thm "DistinctTreeProver.in_set_left";
val in_set_right = thm "DistinctTreeProver.in_set_right";
val swap_neq = thm "DistinctTreeProver.swap_neq";
val neq_to_eq_False = thm "DistinctTreeProver.neq_to_eq_False"
datatype Direction = Left | Right
fun treeT T = Type ("DistinctTreeProver.tree",[T]);
fun mk_tree' e T n [] = Const ("DistinctTreeProver.tree.Tip",treeT T)
| mk_tree' e T n xs =
let
val m = (n - 1) div 2;
val (xsl,x::xsr) = chop m xs;
val l = mk_tree' e T m xsl;
val r = mk_tree' e T (n-(m+1)) xsr;
in Const ("DistinctTreeProver.tree.Node",
treeT T --> T --> HOLogic.boolT--> treeT T --> treeT T) $
l$ e x $ HOLogic.false_const $ r
end
fun mk_tree e T xs = mk_tree' e T (length xs) xs;
fun dest_tree (Const ("DistinctTreeProver.tree.Tip",_)) = []
| dest_tree (Const ("DistinctTreeProver.tree.Node",_)$l$e$_$r) = dest_tree l @ e :: dest_tree r
| dest_tree t = raise TERM ("DistinctTreeProver.dest_tree",[t]);
fun lin_find_tree e (Const ("DistinctTreeProver.tree.Tip",_)) = NONE
| lin_find_tree e (Const ("DistinctTreeProver.tree.Node",_) $ l$ x $ _ $ r) =
if e aconv x
then SOME []
else (case lin_find_tree e l of
SOME path => SOME (Left::path)
| NONE => (case lin_find_tree e r of
SOME path => SOME (Right::path)
| NONE => NONE))
| lin_find_tree e t = raise TERM ("find_tree: input not a tree",[t])
fun bin_find_tree order e (Const ("DistinctTreeProver.tree.Tip",_)) = NONE
| bin_find_tree order e (Const ("DistinctTreeProver.tree.Node",_) $ l$ x $ _ $ r) =
(case order (e,x) of
EQUAL => SOME []
| LESS => Option.map (cons Left) (bin_find_tree order e l)
| GREATER => Option.map (cons Right) (bin_find_tree order e r))
| bin_find_tree order e t = raise TERM ("find_tree: input not a tree",[t])
fun find_tree e t =
(case bin_find_tree TermOrd.fast_term_ord e t of
NONE => lin_find_tree e t
| x => x);
fun index_tree (Const ("DistinctTreeProver.tree.Tip",_)) path tab = tab
| index_tree (Const ("DistinctTreeProver.tree.Node",_) $ l$ x $ _ $ r) path tab =
tab
|> Termtab.update_new (x,path)
|> index_tree l (path@[Left])
|> index_tree r (path@[Right])
| index_tree t _ _ = raise TERM ("index_tree: input not a tree",[t])
fun split_common_prefix xs [] = ([],xs,[])
| split_common_prefix [] ys = ([],[],ys)
| split_common_prefix (xs as (x::xs')) (ys as (y::ys')) =
if x=y
then let val (ps,xs'',ys'') = split_common_prefix xs' ys' in (x::ps,xs'',ys'') end
else ([],xs,ys)
(* Wrapper around Thm.instantiate. The type instiations of instTs are applied to
* the right hand sides of insts
*)
fun instantiate instTs insts =
let
val instTs' = map (fn (T,U) => (dest_TVar (typ_of T),typ_of U)) instTs;
fun substT x = (case AList.lookup (op =) instTs' x of NONE => TVar x | SOME T' => T');
fun mapT_and_recertify ct =
let
val thy = theory_of_cterm ct;
in (cterm_of thy (Term.map_types (Term.map_type_tvar substT) (term_of ct))) end;
val insts' = map (apfst mapT_and_recertify) insts;
in Thm.instantiate (instTs,insts') end;
fun tvar_clash ixn S S' = raise TYPE ("Type variable " ^
quote (Term.string_of_vname ixn) ^ " has two distinct sorts",
[TVar (ixn, S), TVar (ixn, S')], []);
fun lookup (tye, (ixn, S)) =
(case AList.lookup (op =) tye ixn of
NONE => NONE
| SOME (S', T) => if S = S' then SOME T else tvar_clash ixn S S');
val naive_typ_match =
let
fun match (TVar (v, S), T) subs =
(case lookup (subs, (v, S)) of
NONE => ((v, (S, T))::subs)
| SOME _ => subs)
| match (Type (a, Ts), Type (b, Us)) subs =
if a <> b then raise Type.TYPE_MATCH
else matches (Ts, Us) subs
| match (TFree x, TFree y) subs =
if x = y then subs else raise Type.TYPE_MATCH
| match _ _ = raise Type.TYPE_MATCH
and matches (T :: Ts, U :: Us) subs = matches (Ts, Us) (match (T, U) subs)
| matches _ subs = subs;
in match end;
(* expects that relevant type variables are already contained in
* term variables. First instantiation of variables is returned without further
* checking.
*)
fun naive_cterm_first_order_match (t,ct) env =
let
val thy = (theory_of_cterm ct);
fun mtch (env as (tyinsts,insts)) = fn
(Var(ixn,T),ct) =>
(case AList.lookup (op =) insts ixn of
NONE => (naive_typ_match (T,typ_of (ctyp_of_term ct)) tyinsts,
(ixn, ct)::insts)
| SOME _ => env)
| (f$t,ct) => let val (cf,ct') = Thm.dest_comb ct;
in mtch (mtch env (f,cf)) (t,ct') end
| _ => env
in mtch env (t,ct) end;
fun mp prem rule = implies_elim rule prem;
fun discharge prems rule =
let
val thy = theory_of_thm (hd prems);
val (tyinsts,insts) =
fold naive_cterm_first_order_match (prems_of rule ~~ map cprop_of prems) ([],[]);
val tyinsts' = map (fn (v,(S,U)) => (ctyp_of thy (TVar (v,S)),ctyp_of thy U))
tyinsts;
val insts' = map (fn (idxn,ct) => (cterm_of thy (Var (idxn,typ_of (ctyp_of_term ct))),ct))
insts;
val rule' = Thm.instantiate (tyinsts',insts') rule;
in fold mp prems rule' end;
local
val (l_in_set_root,x_in_set_root,r_in_set_root) =
let val (Node_l_x_d,r) = (cprop_of in_set_root)
|> Thm.dest_comb |> #2
|> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb;
val (Node_l,x) = Node_l_x_d |> Thm.dest_comb |> #1 |> Thm.dest_comb;
val l = Node_l |> Thm.dest_comb |> #2;
in (l,x,r) end
val (x_in_set_left,r_in_set_left) =
let val (Node_l_x_d,r) = (cprop_of in_set_left)
|> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
|> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb;
val x = Node_l_x_d |> Thm.dest_comb |> #1 |> Thm.dest_comb |> #2;
in (x,r) end
val (x_in_set_right,l_in_set_right) =
let val (Node_l,x) = (cprop_of in_set_right)
|> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
|> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
|> Thm.dest_comb |> #1 |> Thm.dest_comb |> #1
|> Thm.dest_comb
val l = Node_l |> Thm.dest_comb |> #2;
in (x,l) end
in
(*
1. First get paths x_path y_path of x and y in the tree.
2. For the common prefix descend into the tree according to the path
and lemmas all_distinct_left/right
3. If one restpath is empty use distinct_left/right,
otherwise all_distinct_left_right
*)
fun distinctTreeProver dist_thm x_path y_path =
let
fun dist_subtree [] thm = thm
| dist_subtree (p::ps) thm =
let
val rule = (case p of Left => all_distinct_left | Right => all_distinct_right)
in dist_subtree ps (discharge [thm] rule) end;
val (ps,x_rest,y_rest) = split_common_prefix x_path y_path;
val dist_subtree_thm = dist_subtree ps dist_thm;
val subtree = cprop_of dist_subtree_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
val (_,[l,_,_,r]) = Drule.strip_comb subtree;
fun in_set ps tree =
let
val (_,[l,x,_,r]) = Drule.strip_comb tree;
val xT = ctyp_of_term x;
in (case ps of
[] => instantiate
[(ctyp_of_term x_in_set_root,xT)]
[(l_in_set_root,l),(x_in_set_root,x),(r_in_set_root,r)] in_set_root
| (Left::ps') =>
let
val in_set_l = in_set ps' l;
val in_set_left' = instantiate [(ctyp_of_term x_in_set_left,xT)]
[(x_in_set_left,x),(r_in_set_left,r)] in_set_left;
in discharge [in_set_l] in_set_left' end
| (Right::ps') =>
let
val in_set_r = in_set ps' r;
val in_set_right' = instantiate [(ctyp_of_term x_in_set_right,xT)]
[(x_in_set_right,x),(l_in_set_right,l)] in_set_right;
in discharge [in_set_r] in_set_right' end)
end
fun in_set' [] = raise TERM ("distinctTreeProver",[])
| in_set' (Left::ps) = in_set ps l
| in_set' (Right::ps) = in_set ps r;
fun distinct_lr node_in_set Left = discharge [dist_subtree_thm,node_in_set] distinct_left
| distinct_lr node_in_set Right = discharge [dist_subtree_thm,node_in_set] distinct_right
val (swap,neq) =
(case x_rest of
[] => let
val y_in_set = in_set' y_rest;
in (false,distinct_lr y_in_set (hd y_rest)) end
| (xr::xrs) =>
(case y_rest of
[] => let
val x_in_set = in_set' x_rest;
in (true,distinct_lr x_in_set (hd x_rest)) end
| (yr::yrs) =>
let
val x_in_set = in_set' x_rest;
val y_in_set = in_set' y_rest;
in (case xr of
Left => (false,
discharge [dist_subtree_thm,x_in_set,y_in_set] distinct_left_right)
|Right => (true,
discharge [dist_subtree_thm,y_in_set,x_in_set] distinct_left_right))
end
))
in if swap then discharge [neq] swap_neq else neq
end
val delete_root = thm "DistinctTreeProver.delete_root";
val delete_left = thm "DistinctTreeProver.delete_left";
val delete_right = thm "DistinctTreeProver.delete_right";
fun deleteProver dist_thm [] = delete_root OF [dist_thm]
| deleteProver dist_thm (p::ps) =
let
val dist_rule = (case p of Left => all_distinct_left | Right => all_distinct_right);
val dist_thm' = discharge [dist_thm] dist_rule
val del_rule = (case p of Left => delete_left | Right => delete_right)
val del = deleteProver dist_thm' ps;
in discharge [dist_thm, del] del_rule end;
val subtract_Tip = thm "DistinctTreeProver.subtract_Tip";
val subtract_Node = thm "DistinctTreeProver.subtract_Node";
val delete_Some_all_distinct = thm "DistinctTreeProver.delete_Some_all_distinct";
val subtract_Some_all_distinct_res = thm "DistinctTreeProver.subtract_Some_all_distinct_res";
local
val (alpha,v) =
let
val ct = subtract_Tip |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
|> Thm.dest_comb |> #2
val [alpha] = ct |> Thm.ctyp_of_term |> Thm.dest_ctyp;
in (alpha, #1 (dest_Var (term_of ct))) end;
in
fun subtractProver (Const ("DistinctTreeProver.tree.Tip",T)) ct dist_thm =
let
val ct' = dist_thm |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
val thy = theory_of_cterm ct;
val [alphaI] = #2 (dest_Type T);
in Thm.instantiate ([(alpha,ctyp_of thy alphaI)],
[(cterm_of thy (Var (v,treeT alphaI)),ct')]) subtract_Tip
end
| subtractProver (Const ("DistinctTreeProver.tree.Node",nT)$l$x$d$r) ct dist_thm =
let
val ct' = dist_thm |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
val (_,[cl,_,_,cr]) = Drule.strip_comb ct;
val ps = the (find_tree x (term_of ct'));
val del_tree = deleteProver dist_thm ps;
val dist_thm' = discharge [del_tree, dist_thm] delete_Some_all_distinct;
val sub_l = subtractProver (term_of cl) cl (dist_thm');
val sub_r = subtractProver (term_of cr) cr
(discharge [sub_l, dist_thm'] subtract_Some_all_distinct_res);
in discharge [del_tree, sub_l, sub_r] subtract_Node end
end
val subtract_Some_all_distinct = thm "DistinctTreeProver.subtract_Some_all_distinct";
fun distinct_implProver dist_thm ct =
let
val ctree = ct |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
val sub = subtractProver (term_of ctree) ctree dist_thm;
in subtract_Some_all_distinct OF [sub, dist_thm] end;
fun get_fst_success f [] = NONE
| get_fst_success f (x::xs) = (case f x of NONE => get_fst_success f xs
| SOME v => SOME v);
fun neq_x_y ctxt x y name =
(let
val dist_thm = the (try (ProofContext.get_thm ctxt) name);
val ctree = cprop_of dist_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
val tree = term_of ctree;
val x_path = the (find_tree x tree);
val y_path = the (find_tree y tree);
val thm = distinctTreeProver dist_thm x_path y_path;
in SOME thm
end handle Option => NONE)
fun distinctTree_tac names ctxt
(Const ("Trueprop",_) $ (Const ("Not", _) $ (Const ("op =", _) $ x $ y)), i) =
(case get_fst_success (neq_x_y ctxt x y) names of
SOME neq => rtac neq i
| NONE => no_tac)
| distinctTree_tac _ _ _ = no_tac;
fun distinctFieldSolver names = mk_solver' "distinctFieldSolver"
(fn ss => case #context (#1 (rep_ss ss)) of
SOME ctxt => SUBGOAL (distinctTree_tac names ctxt)
| NONE => fn i => no_tac)
fun distinct_simproc names =
Simplifier.simproc @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"]
(fn thy => fn ss => fn (Const ("op =",_)$x$y) =>
case #context (#1 (rep_ss ss)) of
SOME ctxt => Option.map (fn neq => neq_to_eq_False OF [neq])
(get_fst_success (neq_x_y ctxt x y) names)
| NONE => NONE
)
end
end;