--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/recon_order_clauses.ML Thu Mar 31 19:29:26 2005 +0200
@@ -0,0 +1,492 @@
+
+
+(*----------------------------------------------*)
+(* Reorder clauses for use in binary resolution *)
+(*----------------------------------------------*)
+fun take n [] = []
+| take n (x::xs) = (if n = 0 then [] else (x::(take (n - 1) xs)))
+
+fun drop n [] = []
+| drop n (x::xs) = (if n = 0 then (x::xs) else drop (n-1) xs)
+
+fun remove n [] = []
+| remove n (x::xs) = List.filter (not_equal n) (x::xs);
+
+fun remove_nth n [] = []
+| remove_nth n (x::xs) = (take (n -1) (x::xs))@(drop n (x::xs))
+
+fun get_nth n (x::xs) = hd (drop (n-1) (x::xs))
+
+
+ fun literals (Const("Trueprop",_) $ P) = literals P
+ | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q
+ | literals (Const("Not",_) $ P) = [(false,P)]
+ | literals P = [(true,P)];
+
+ (*number of literals in a term*)
+ val nliterals = length o literals;
+
+exception Not_in_list;
+
+
+
+
+ (* get the literals from a disjunctive clause *)
+
+(*fun get_disj_literals t = if is_disj t then
+ let
+ val {disj1, disj2} = dest_disj t
+ in
+ disj1::(get_disj_literals disj2)
+ end
+ else
+ ([t])
+
+*)
+
+(*
+(* gives horn clause with kth disj as concl (starting at 1) *)
+fun rots (0,th) = (Meson.make_horn Meson.crules th)
+ | rots (k,th) = rots(k-1, assoc_right (th RS disj_comm))
+
+
+
+Goal " (~~P) == P";
+by Auto_tac;
+qed "notnotEq";
+
+Goal "A | A ==> A";
+by Auto_tac;
+qed "rem_dup_disj";
+
+
+
+
+(* New Meson code Versions of make_neg_rule and make_pos_rule that don't insert new *)
+(* assumptions, for ordinary resolution. *)
+
+
+
+
+ val not_conjD = thm "meson_not_conjD";
+ val not_disjD = thm "meson_not_disjD";
+ val not_notD = thm "meson_not_notD";
+ val not_allD = thm "meson_not_allD";
+ val not_exD = thm "meson_not_exD";
+ val imp_to_disjD = thm "meson_imp_to_disjD";
+ val not_impD = thm "meson_not_impD";
+ val iff_to_disjD = thm "meson_iff_to_disjD";
+ val not_iffD = thm "meson_not_iffD";
+ val conj_exD1 = thm "meson_conj_exD1";
+ val conj_exD2 = thm "meson_conj_exD2";
+ val disj_exD = thm "meson_disj_exD";
+ val disj_exD1 = thm "meson_disj_exD1";
+ val disj_exD2 = thm "meson_disj_exD2";
+ val disj_assoc = thm "meson_disj_assoc";
+ val disj_comm = thm "meson_disj_comm";
+ val disj_FalseD1 = thm "meson_disj_FalseD1";
+ val disj_FalseD2 = thm "meson_disj_FalseD2";
+
+
+ fun literals (Const("Trueprop",_) $ P) = literals P
+ | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q
+ | literals (Const("Not",_) $ P) = [(false,P)]
+ | literals P = [(true,P)];
+
+ (*number of literals in a term*)
+ val nliterals = length o literals;
+
+exception Not_in_list;
+
+
+(*Permute a rule's premises to move the i-th premise to the last position.*)
+fun make_last i th =
+ let val n = nprems_of th
+ in if 1 <= i andalso i <= n
+ then Thm.permute_prems (i-1) 1 th
+ else raise THM("make_last", i, [th])
+ end;
+
+(*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
+ double-negations.*)
+val negate_head = rewrite_rule [atomize_not, not_not RS eq_reflection];
+
+(*Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*)
+fun select_literal i cl = negate_head (make_last i cl);
+
+
+(* get a meta-clause for resolution with correct order of literals *)
+fun get_meta_cl (th,n) = let val lits = nliterals(prop_of th)
+ val contra = if lits = 1
+ then
+ th
+ else
+ rots (n,th)
+ in
+ if lits = 1
+ then
+
+ contra
+ else
+ rotate_prems (lits - n) contra
+ end
+
+
+
+
+
+
+
+fun zip xs [] = []
+| zip xs (y::ys) = (case xs of [] => [] | (z::zs) => ((z,y)::zip zs ys))
+
+
+fun unzip [] = ([],[])
+ | unzip((x,y)::pairs) =
+ let val (xs,ys) = unzip pairs
+ in (x::xs, y::ys) end;
+
+fun numlist 0 = []
+| numlist n = (numlist (n - 1))@[n]
+
+
+fun is_abs t = can dest_abs t;
+fun is_comb t = can dest_comb t;
+
+fun iscomb a = if is_Free a then
+ false
+ else if is_Var a then
+ false
+ else if is_conj a then
+ false
+ else if is_disj a then
+ false
+ else if is_forall a then
+ false
+ else if is_exists a then
+ false
+ else
+ true;
+
+
+
+
+fun last(x::xs) = if xs=[] then x else last xs
+fun butlast []= []
+| butlast(x::xs) = if xs=[] then [] else (x::(butlast xs))
+
+
+fun minus a b = b - a;
+
+
+
+
+(* gives meta clause with kth disj as concl (starting at 1) *)
+(*fun rots (0,th) = negate_nead (make_horn resolution_clause_rules th)
+ | rots (k,th) = rots(k-1, assoc_right (th RS disj_comm))*)
+
+
+(* get a meta-clause for resolution with correct order of literals *)
+fun get_meta_cl (th,n) = let val lits = nliterals(prop_of th)
+ val contra = if lits = 1
+ then
+ th
+ else
+ rots (n,th)
+ in
+ if lits = 1
+ then
+
+ contra
+ else
+ rotate_prems (lits - n) contra
+ end
+*)
+
+
+
+
+fun zip xs [] = []
+| zip xs (y::ys) = (case xs of [] => [] | (z::zs) => ((z,y)::zip zs ys))
+
+
+fun unzip [] = ([],[])
+ | unzip((x,y)::pairs) =
+ let val (xs,ys) = unzip pairs
+ in (x::xs, y::ys) end;
+
+fun numlist 0 = []
+| numlist n = (numlist (n - 1))@[n]
+
+
+fun is_abs t = can dest_abs t;
+fun is_comb t = can dest_comb t;
+
+fun iscomb a = if is_Free a then
+ false
+ else if is_Var a then
+ false
+ else if is_conj a then
+ false
+ else if is_disj a then
+ false
+ else if is_forall a then
+ false
+ else if is_exists a then
+ false
+ else
+ true;
+
+
+
+
+fun last(x::xs) = if xs=[] then x else last xs
+fun butlast []= []
+| butlast(x::xs) = if xs=[] then [] else (x::(butlast xs))
+
+
+fun minus a b = b - a;
+
+
+(* code to rearrange clauses so that they're the same as the parsed in SPASS version *)
+
+fun assoc3 a [] = raise Noassoc
+ | assoc3 a ((x, y, z)::t) = if a = x then z else assoc3 a t;
+
+
+fun third (a,b,c) = c;
+
+
+ fun takeUntil ch [] res = (res, [])
+ | takeUntil ch (x::xs) res = if x = ch
+ then
+ (res, xs)
+ else
+ takeUntil ch xs (res@[x])
+fun contains_eq str = inlist "=" str
+
+fun eq_not_neq str = let val uptoeq = fst(takeUntil "=" str [])
+ in
+ if ((last uptoeq) = "~")
+ then
+ false
+ else
+ true
+ end
+
+
+
+
+fun get_eq_strs str = if eq_not_neq str (*not an inequality *)
+ then
+ let val (left, right) = takeUntil "=" str []
+ in
+ ((butlast left), (drop 1 right))
+ end
+ else (* is an inequality *)
+ let val (left, right) = takeUntil "~" str []
+ in
+ ((butlast left), (drop 2 right))
+ end
+
+
+
+fun switch_equal a x = let val (a_lhs, a_rhs) = get_eq_strs a
+ val (x_lhs, x_rhs) = get_eq_strs x
+
+ in
+ (a_lhs = x_rhs) andalso (a_rhs = x_lhs)
+ end
+
+fun equal_pair (a,b) = equal a b
+
+fun is_var_pair (a,b) vars = (a mem vars) andalso (b mem vars)
+
+fun var_equiv vars (a,b) = (equal_pair (a,b)) orelse (is_var_pair (a,b) vars)
+
+fun all_true [] = false
+| all_true xs = let val falselist = List.filter (equal false ) xs
+ in
+ falselist = []
+ end
+
+
+
+fun var_pos_eq vars x y = let val xs = explode x
+ val ys = explode y
+ in
+ if not_equal (length xs) (length ys)
+ then
+ false
+ else
+ let val xsys = zip xs ys
+ val are_var_pairs = map (var_equiv vars) xsys
+ in
+ all_true are_var_pairs
+ end
+ end
+
+
+
+
+fun pos_in_list a [] allvars (pos_num, symlist, nsymlist) = raise Not_in_list
+ |pos_in_list a (x::[]) allvars (pos_num , symlist, nsymlist) =
+ let val y = explode x
+ val b = explode a
+ in
+ if b = y
+ then
+ (pos_num, symlist, nsymlist)
+ else
+ if (var_pos_eq allvars a x) (* Equal apart from meta-vars having different names *)
+ then
+ (pos_num, symlist, nsymlist)
+ else
+ if (contains_eq b) andalso (contains_eq y)
+ then
+ if (eq_not_neq b) andalso (eq_not_neq y) andalso (switch_equal b y ) (* both are equalities and equal under sym*)
+ then
+ (pos_num, (pos_num::symlist), nsymlist) (* add pos to symlist *) else
+ if not(eq_not_neq b) andalso not(eq_not_neq y) andalso (switch_equal b y ) (* if they're equal under not_sym *)
+ then
+ (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *)
+ else
+ raise Not_in_list
+ else
+ raise Not_in_list
+
+ end
+
+ | pos_in_list a (x::xs) allvars (pos_num, symlist, nsymlist) =
+ let val y = explode x
+ val b = explode a
+ in
+ if b = y
+ then
+ (pos_num, symlist, nsymlist)
+
+ else
+ if (var_pos_eq allvars a x) (* Equal apart from meta-vars having different names *)
+ then
+ (pos_num, symlist, nsymlist)
+ else
+ if (contains_eq b) andalso (contains_eq y)
+ then
+ if (eq_not_neq b) andalso (eq_not_neq y) andalso (switch_equal b y ) (* both are equalities and equal under sym*)
+ then
+ (pos_num, (pos_num::symlist), nsymlist) (* add pos to symlist *) else
+ if not(eq_not_neq b) andalso not(eq_not_neq y) andalso (switch_equal b y ) (* if they're equal under not_sym *)
+ then
+ (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *)
+ else
+ pos_in_list a xs allvars((pos_num + 1), symlist, nsymlist)
+ else
+ pos_in_list a xs allvars((pos_num + 1), symlist, nsymlist)
+
+ end
+
+
+
+
+
+
+
+ (* in
+ if b = y
+ then
+ (pos_num, symlist, nsymlist)
+ else if (contains_eq b) andalso (contains_eq y)
+ then if (eq_not_neq b) andalso (eq_not_neq y) (* both are equalities*)
+ then if (switch_equal b y ) (* if they're equal under sym *)
+ then
+ (pos_num, (pos_num::symlist), nsymlist) (* add pos to symlist *)
+ else
+ pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
+ else if not(eq_not_neq b) andalso not(eq_not_neq y) (* both are inequalities *)
+ then if (switch_equal b y ) (* if they're equal under not_sym *)
+ then
+ (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *)
+ else
+ pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
+ else
+ pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
+ else
+ pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
+ else
+ pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
+ end
+
+ *)
+
+
+
+
+
+
+
+
+
+
+(* checkorder Spass Isabelle [] *)
+
+fun checkorder [] strlist allvars (numlist, symlist, not_symlist)= (numlist,symlist, not_symlist)
+| checkorder (x::xs) strlist allvars (numlist, symlist, not_symlist) =
+ let val (posnum, symlist', not_symlist') = pos_in_list x strlist allvars (0, symlist, not_symlist)
+ in
+ checkorder xs strlist allvars ((numlist@[posnum]), symlist', not_symlist')
+ end
+
+fun is_digit ch =
+ ( ch >= "0" andalso ch <= "9")
+
+
+fun is_alpha ch =
+ (ch >= "A" andalso ch <= "Z") orelse
+ (ch >= "a" andalso ch <= "z")
+
+
+fun is_alpha_space_or_neg_or_eq ch = (ch = "~") orelse (is_alpha ch) orelse ( ch = " ")orelse ( ch = "=")
+
+fun lit_string t = let val termstr = (Sign.string_of_term Mainsign ) t
+ val exp_term = explode termstr
+ in
+ implode(List.filter is_alpha_space_or_neg_or_eq exp_term)
+ end
+
+fun get_meta_lits thm = map lit_string (prems_of thm)
+
+
+
+
+fun is_alpha_space_or_neg_or_eq_or_bracket ch = (ch = "~") orelse (is_alpha ch) orelse ( ch = " ")orelse ( ch = "=") orelse (ch= "(") orelse (ch = ")")
+
+fun lit_string_bracket t = let val termstr = (Sign.string_of_term Mainsign ) t
+ val exp_term = explode termstr
+ in
+ implode(List.filter is_alpha_space_or_neg_or_eq_or_bracket exp_term)
+ end
+
+fun get_meta_lits_bracket thm = map lit_string_bracket (prems_of thm)
+
+
+
+
+fun apply_rule rule [] thm = thm
+| apply_rule rule (x::xs) thm = let val thm' = rule RSN ((x+1),thm)
+ in
+ apply_rule rule xs thm'
+ end
+
+
+
+ (* resulting thm, clause-strs in spass order, vars *)
+
+fun rearrange_clause thm res_strlist allvars =
+ let val isa_strlist = get_meta_lits thm
+ val (posns, symlist, not_symlist) = checkorder res_strlist isa_strlist allvars([],[],[])
+ val symmed = apply_rule sym symlist thm
+ val not_symmed = apply_rule not_sym not_symlist symmed
+
+ in
+ ((rearrange_prems posns not_symmed), posns, symlist,not_symlist)
+ end