--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Statespace/distinct_tree_prover.ML Wed Oct 24 18:36:09 2007 +0200
@@ -0,0 +1,349 @@
+(* Title: distinct_tree_prover.thy
+ ID: $Id$
+ Author: Norbert Schirmer, TU Muenchen
+*)
+
+structure DistinctTreeProver =
+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"
+
+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]);
+
+datatype Direction = Left | Right
+
+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 Term.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) (PureThy.Name 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 HOL.thy "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;
\ No newline at end of file