# HG changeset patch # User wenzelm # Date 1182433326 -7200 # Node ID bf46f5cbdd64b9781f0d764503bb3cd69aa9f050 # Parent 95b70054bb3a7c17fa572650f803c8864189496e Dense linear order witout endpoints and a quantifier elimination procedure in Ferrante and Rackoff style. diff -r 95b70054bb3a -r bf46f5cbdd64 src/HOL/Dense_Linear_Order.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Dense_Linear_Order.thy Thu Jun 21 15:42:06 2007 +0200 @@ -0,0 +1,424 @@ +(* + ID: $Id$ + Author: Amine Chaieb, TU Muenchen +*) + +header {* Dense linear order witout endpoints + and a quantifier elimination procedure in Ferrante and Rackoff style *} + +theory Dense_Linear_Order +imports Finite_Set +uses + "Tools/qelim.ML" + "Tools/Ferrante_Rackoff/ferrante_rackoff_data.ML" + ("Tools/Ferrante_Rackoff/ferrante_rackoff.ML") +begin + +setup Ferrante_Rackoff_Data.setup + +context Linorder +begin + +text{* Theorems for @{text "\z. \x. x \ z \ (P x \ P\<^bsub>-\\<^esub>)"}*} +lemma minf_lt: "\z . \x. x \ z \ (x \ t \ True)" by auto +lemma minf_gt: "\z . \x. x \ z \ (t \ x \ False)" + by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le) + +lemma minf_le: "\z. \x. x \ z \ (x \ t \ True)" by (auto simp add: less_le) +lemma minf_ge: "\z. \x. x \ z \ (t \ x \ False)" + by (auto simp add: less_le not_less not_le) +lemma minf_eq: "\z. \x. x \ z \ (x = t \ False)" by auto +lemma minf_neq: "\z. \x. x \ z \ (x \ t \ True)" by auto +lemma minf_P: "\z. \x. x \ z \ (P \ P)" by blast + +text{* Theorems for @{text "\z. \x. x \ z \ (P x \ P\<^bsub>+\\<^esub>)"}*} +lemma pinf_gt: "\z . \x. z \ x \ (t \ x \ True)" by auto +lemma pinf_lt: "\z . \x. z \ x \ (x \ t \ False)" + by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le) + +lemma pinf_ge: "\z. \x. z \ x \ (t \ x \ True)" by (auto simp add: less_le) +lemma pinf_le: "\z. \x. z \ x \ (x \ t \ False)" + by (auto simp add: less_le not_less not_le) +lemma pinf_eq: "\z. \x. z \ x \ (x = t \ False)" by auto +lemma pinf_neq: "\z. \x. z \ x \ (x \ t \ True)" by auto +lemma pinf_P: "\z. \x. z \ x \ (P \ P)" by blast + +lemma nmi_lt: "t \ U \ \x. \True \ x \ t \ (\ u\ U. u \ x)" by auto +lemma nmi_gt: "t \ U \ \x. \False \ t \ x \ (\ u\ U. u \ x)" + by (auto simp add: le_less) +lemma nmi_le: "t \ U \ \x. \True \ x\ t \ (\ u\ U. u \ x)" by auto +lemma nmi_ge: "t \ U \ \x. \False \ t\ x \ (\ u\ U. u \ x)" by auto +lemma nmi_eq: "t \ U \ \x. \False \ x = t \ (\ u\ U. u \ x)" by auto +lemma nmi_neq: "t \ U \\x. \True \ x \ t \ (\ u\ U. u \ x)" by auto +lemma nmi_P: "\ x. ~P \ P \ (\ u\ U. u \ x)" by auto +lemma nmi_conj: "\\x. \P1' \ P1 x \ (\ u\ U. u \ x) ; + \x. \P2' \ P2 x \ (\ u\ U. u \ x)\ \ + \x. \(P1' \ P2') \ (P1 x \ P2 x) \ (\ u\ U. u \ x)" by auto +lemma nmi_disj: "\\x. \P1' \ P1 x \ (\ u\ U. u \ x) ; + \x. \P2' \ P2 x \ (\ u\ U. u \ x)\ \ + \x. \(P1' \ P2') \ (P1 x \ P2 x) \ (\ u\ U. u \ x)" by auto + +lemma npi_lt: "t \ U \ \x. \False \ x \ t \ (\ u\ U. x \ u)" by (auto simp add: le_less) +lemma npi_gt: "t \ U \ \x. \True \ t \ x \ (\ u\ U. x \ u)" by auto +lemma npi_le: "t \ U \ \x. \False \ x \ t \ (\ u\ U. x \ u)" by auto +lemma npi_ge: "t \ U \ \x. \True \ t \ x \ (\ u\ U. x \ u)" by auto +lemma npi_eq: "t \ U \ \x. \False \ x = t \ (\ u\ U. x \ u)" by auto +lemma npi_neq: "t \ U \ \x. \True \ x \ t \ (\ u\ U. x \ u )" by auto +lemma npi_P: "\ x. ~P \ P \ (\ u\ U. x \ u)" by auto +lemma npi_conj: "\\x. \P1' \ P1 x \ (\ u\ U. x \ u) ; \x. \P2' \ P2 x \ (\ u\ U. x \ u)\ + \ \x. \(P1' \ P2') \ (P1 x \ P2 x) \ (\ u\ U. x \ u)" by auto +lemma npi_disj: "\\x. \P1' \ P1 x \ (\ u\ U. x \ u) ; \x. \P2' \ P2 x \ (\ u\ U. x \ u)\ + \ \x. \(P1' \ P2') \ (P1 x \ P2 x) \ (\ u\ U. x \ u)" by auto + +lemma lin_dense_lt: "t \ U \ \x l u. (\ t. l \ t \ t \ u \ t \ U) \ l\ x \ x \ u \ x \ t \ (\ y. l \ y \ y \ u \ y \ t)" +proof(clarsimp) + fix x l u y assume tU: "t \ U" and noU: "\t. l \ t \ t \ u \ t \ U" and lx: "l \ x" + and xu: "x\u" and px: "x \ t" and ly: "l\y" and yu:"y \ u" + from tU noU ly yu have tny: "t\y" by auto + {assume H: "t \ y" + from less_trans[OF lx px] less_trans[OF H yu] + have "l \ t \ t \ u" by simp + with tU noU have "False" by auto} + hence "\ t \ y" by auto hence "y \ t" by (simp add: not_less) + thus "y \ t" using tny by (simp add: less_le) +qed + +lemma lin_dense_gt: "t \ U \ \x l u. (\ t. l \ t \ t\ u \ t \ U) \ l \ x \ x \ u \ t \ x \ (\ y. l \ y \ y \ u \ t \ y)" +proof(clarsimp) + fix x l u y + assume tU: "t \ U" and noU: "\t. l \ t \ t \ u \ t \ U" and lx: "l \ x" and xu: "x\u" + and px: "t \ x" and ly: "l\y" and yu:"y \ u" + from tU noU ly yu have tny: "t\y" by auto + {assume H: "y\ t" + from less_trans[OF ly H] less_trans[OF px xu] have "l \ t \ t \ u" by simp + with tU noU have "False" by auto} + hence "\ y\t" by auto hence "t \ y" by (auto simp add: not_less) + thus "t \ y" using tny by (simp add:less_le) +qed + +lemma lin_dense_le: "t \ U \ \x l u. (\ t. l \ t \ t\ u \ t \ U) \ l\ x \ x \ u \ x \ t \ (\ y. l \ y \ y \ u \ y\ t)" +proof(clarsimp) + fix x l u y + assume tU: "t \ U" and noU: "\t. l \ t \ t \ u \ t \ U" and lx: "l \ x" and xu: "x\u" + and px: "x \ t" and ly: "l\y" and yu:"y \ u" + from tU noU ly yu have tny: "t\y" by auto + {assume H: "t \ y" + from less_le_trans[OF lx px] less_trans[OF H yu] + have "l \ t \ t \ u" by simp + with tU noU have "False" by auto} + hence "\ t \ y" by auto thus "y \ t" by (simp add: not_less) +qed + +lemma lin_dense_ge: "t \ U \ \x l u. (\ t. l \ t \ t\ u \ t \ U) \ l\ x \ x \ u \ t \ x \ (\ y. l \ y \ y \ u \ t \ y)" +proof(clarsimp) + fix x l u y + assume tU: "t \ U" and noU: "\t. l \ t \ t \ u \ t \ U" and lx: "l \ x" and xu: "x\u" + and px: "t \ x" and ly: "l\y" and yu:"y \ u" + from tU noU ly yu have tny: "t\y" by auto + {assume H: "y\ t" + from less_trans[OF ly H] le_less_trans[OF px xu] + have "l \ t \ t \ u" by simp + with tU noU have "False" by auto} + hence "\ y\t" by auto thus "t \ y" by (simp add: not_less) +qed +lemma lin_dense_eq: "t \ U \ \x l u. (\ t. l \ t \ t\ u \ t \ U) \ l\ x \ x \ u \ x = t \ (\ y. l \ y \ y \ u \ y= t)" by auto +lemma lin_dense_neq: "t \ U \ \x l u. (\ t. l \ t \ t\ u \ t \ U) \ l\ x \ x \ u \ x \ t \ (\ y. l \ y \ y \ u \ y\ t)" by auto +lemma lin_dense_P: "\x l u. (\ t. l \ t \ t\ u \ t \ U) \ l\ x \ x \ u \ P \ (\ y. l \ y \ y \ u \ P)" by auto + +lemma lin_dense_conj: + "\\x l u. (\ t. l \ t \ t\ u \ t \ U) \ l\ x \ x \ u \ P1 x + \ (\ y. l \ y \ y \ u \ P1 y) ; + \x l u. (\ t. l \ t \ t\ u \ t \ U) \ l\ x \ x \ u \ P2 x + \ (\ y. l \ y \ y \ u \ P2 y)\ \ + \x l u. (\ t. l \ t \ t\ u \ t \ U) \ l\ x \ x \ u \ (P1 x \ P2 x) + \ (\ y. l \ y \ y \ u \ (P1 y \ P2 y))" + by blast +lemma lin_dense_disj: + "\\x l u. (\ t. l \ t \ t\ u \ t \ U) \ l\ x \ x \ u \ P1 x + \ (\ y. l \ y \ y \ u \ P1 y) ; + \x l u. (\ t. l \ t \ t\ u \ t \ U) \ l\ x \ x \ u \ P2 x + \ (\ y. l \ y \ y \ u \ P2 y)\ \ + \x l u. (\ t. l \ t \ t\ u \ t \ U) \ l\ x \ x \ u \ (P1 x \ P2 x) + \ (\ y. l \ y \ y \ u \ (P1 y \ P2 y))" + by blast + +lemma npmibnd: "\\x. \ MP \ P x \ (\ u\ U. u \ x); \x. \PP \ P x \ (\ u\ U. x \ u)\ + \ \x. \ MP \ \PP \ P x \ (\ u\ U. \ u' \ U. u \ x \ x \ u')" +by auto + +lemma finite_set_intervals: + assumes px: "P x" and lx: "l \ x" and xu: "x \ u" and linS: "l\ S" + and uinS: "u \ S" and fS:"finite S" and lS: "\ x\ S. l \ x" and Su: "\ x\ S. x \ u" + shows "\ a \ S. \ b \ S. (\ y. a \ y \ y \ b \ y \ S) \ a \ x \ x \ b \ P x" +proof- + let ?Mx = "{y. y\ S \ y \ x}" + let ?xM = "{y. y\ S \ x \ y}" + let ?a = "Max ?Mx" + let ?b = "Min ?xM" + have MxS: "?Mx \ S" by blast + hence fMx: "finite ?Mx" using fS finite_subset by auto + from lx linS have linMx: "l \ ?Mx" by blast + hence Mxne: "?Mx \ {}" by blast + have xMS: "?xM \ S" by blast + hence fxM: "finite ?xM" using fS finite_subset by auto + from xu uinS have linxM: "u \ ?xM" by blast + hence xMne: "?xM \ {}" by blast + have ax:"?a \ x" using Mxne fMx by auto + have xb:"x \ ?b" using xMne fxM by auto + have "?a \ ?Mx" using Max_in[OF fMx Mxne] by simp hence ainS: "?a \ S" using MxS by blast + have "?b \ ?xM" using Min_in[OF fxM xMne] by simp hence binS: "?b \ S" using xMS by blast + have noy:"\ y. ?a \ y \ y \ ?b \ y \ S" + proof(clarsimp) + fix y assume ay: "?a \ y" and yb: "y \ ?b" and yS: "y \ S" + from yS have "y\ ?Mx \ y\ ?xM" by (auto simp add: linear) + moreover {assume "y \ ?Mx" hence "y \ ?a" using Mxne fMx by auto with ay have "False" by (simp add: not_le[symmetric])} + moreover {assume "y \ ?xM" hence "?b \ y" using xMne fxM by auto with yb have "False" by (simp add: not_le[symmetric])} + ultimately show "False" by blast + qed + from ainS binS noy ax xb px show ?thesis by blast +qed + + +lemma finite_set_intervals2: + assumes px: "P x" and lx: "l \ x" and xu: "x \ u" and linS: "l\ S" + and uinS: "u \ S" and fS:"finite S" and lS: "\ x\ S. l \ x" and Su: "\ x\ S. x \ u" + shows "(\ s\ S. P s) \ (\ a \ S. \ b \ S. (\ y. a \ y \ y \ b \ y \ S) \ a \ x \ x \ b \ P x)" +proof- + from finite_set_intervals[where P="P", OF px lx xu linS uinS fS lS Su] + obtain a and b where + as: "a\ S" and bs: "b\ S" and noS:"\y. a \ y \ y \ b \ y \ S" + and axb: "a \ x \ x \ b \ P x" by auto + from axb have "x= a \ x= b \ (a \ x \ x \ b)" by (auto simp add: le_less) + thus ?thesis using px as bs noS by blast +qed + +end + +text {* Linear order without upper bounds *} + +locale linorder_no_ub = Linorder + assumes gt_ex: "\x. \y. x \ y" +begin + +lemma ge_ex: "\x. \y. x \ y" using gt_ex by auto + +text {* Theorems for @{text "\z. \x. z \ x \ (P x \ P\<^bsub>+\\<^esub>)"} *} +lemma pinf_conj: + assumes ex1: "\z1. \x. z1 \ x \ (P1 x \ P1')" + and ex2: "\z2. \x. z2 \ x \ (P2 x \ P2')" + shows "\z. \x. z \ x \ ((P1 x \ P2 x) \ (P1' \ P2'))" +proof- + from ex1 ex2 obtain z1 and z2 where z1: "\x. z1 \ x \ (P1 x \ P1')" + and z2: "\x. z2 \ x \ (P2 x \ P2')" by blast + from gt_ex obtain z where z:"max z1 z2 \ z" by blast + from z have zz1: "z1 \ z" and zz2: "z2 \ z" by simp_all + {fix x assume H: "z \ x" + from less_trans[OF zz1 H] less_trans[OF zz2 H] + have "(P1 x \ P2 x) \ (P1' \ P2')" using z1 zz1 z2 zz2 by auto + } + thus ?thesis by blast +qed + +lemma pinf_disj: + assumes ex1: "\z1. \x. z1 \ x \ (P1 x \ P1')" + and ex2: "\z2. \x. z2 \ x \ (P2 x \ P2')" + shows "\z. \x. z \ x \ ((P1 x \ P2 x) \ (P1' \ P2'))" +proof- + from ex1 ex2 obtain z1 and z2 where z1: "\x. z1 \ x \ (P1 x \ P1')" + and z2: "\x. z2 \ x \ (P2 x \ P2')" by blast + from gt_ex obtain z where z:"max z1 z2 \ z" by blast + from z have zz1: "z1 \ z" and zz2: "z2 \ z" by simp_all + {fix x assume H: "z \ x" + from less_trans[OF zz1 H] less_trans[OF zz2 H] + have "(P1 x \ P2 x) \ (P1' \ P2')" using z1 zz1 z2 zz2 by auto + } + thus ?thesis by blast +qed + +lemma pinf_ex: assumes ex:"\z. \x. z \ x \ (P x \ P1)" and p1: P1 shows "\ x. P x" +proof- + from ex obtain z where z: "\x. z \ x \ (P x \ P1)" by blast + from gt_ex obtain x where x: "z \ x" by blast + from z x p1 show ?thesis by blast +qed + +end + +text {* Linear order without upper bounds *} + +locale linorder_no_lb = Linorder + assumes lt_ex: "\x. \y. y \ x" +begin + +lemma le_ex: "\x. \y. y \ x" using lt_ex by auto + + +text {* Theorems for @{text "\z. \x. x \ z \ (P x \ P\<^bsub>-\\<^esub>)"} *} +lemma minf_conj: + assumes ex1: "\z1. \x. x \ z1 \ (P1 x \ P1')" + and ex2: "\z2. \x. x \ z2 \ (P2 x \ P2')" + shows "\z. \x. x \ z \ ((P1 x \ P2 x) \ (P1' \ P2'))" +proof- + from ex1 ex2 obtain z1 and z2 where z1: "\x. x \ z1 \ (P1 x \ P1')"and z2: "\x. x \ z2 \ (P2 x \ P2')" by blast + from lt_ex obtain z where z:"z \ min z1 z2" by blast + from z have zz1: "z \ z1" and zz2: "z \ z2" by simp_all + {fix x assume H: "x \ z" + from less_trans[OF H zz1] less_trans[OF H zz2] + have "(P1 x \ P2 x) \ (P1' \ P2')" using z1 zz1 z2 zz2 by auto + } + thus ?thesis by blast +qed + +lemma minf_disj: + assumes ex1: "\z1. \x. x \ z1 \ (P1 x \ P1')" + and ex2: "\z2. \x. x \ z2 \ (P2 x \ P2')" + shows "\z. \x. x \ z \ ((P1 x \ P2 x) \ (P1' \ P2'))" +proof- + from ex1 ex2 obtain z1 and z2 where z1: "\x. x \ z1 \ (P1 x \ P1')"and z2: "\x. x \ z2 \ (P2 x \ P2')" by blast + from lt_ex obtain z where z:"z \ min z1 z2" by blast + from z have zz1: "z \ z1" and zz2: "z \ z2" by simp_all + {fix x assume H: "x \ z" + from less_trans[OF H zz1] less_trans[OF H zz2] + have "(P1 x \ P2 x) \ (P1' \ P2')" using z1 zz1 z2 zz2 by auto + } + thus ?thesis by blast +qed + +lemma minf_ex: assumes ex:"\z. \x. x \ z \ (P x \ P1)" and p1: P1 shows "\ x. P x" +proof- + from ex obtain z where z: "\x. x \ z \ (P x \ P1)" by blast + from lt_ex obtain x where x: "x \ z" by blast + from z x p1 show ?thesis by blast +qed + +end + +locale dense_linear_order = linorder_no_lb + linorder_no_ub + + fixes between + assumes between_less: "\x y. x \ y \ x \ between x y \ between x y \ y" + and between_same: "\x. between x x = x" +begin + +lemma rinf_U: + assumes fU: "finite U" + and lin_dense: "\x l u. (\ t. l \ t \ t\ u \ t \ U) \ l\ x \ x \ u \ P x + \ (\ y. l \ y \ y \ u \ P y )" + and nmpiU: "\x. \ MP \ \PP \ P x \ (\ u\ U. \ u' \ U. u \ x \ x \ u')" + and nmi: "\ MP" and npi: "\ PP" and ex: "\ x. P x" + shows "\ u\ U. \ u' \ U. P (between u u')" +proof- + from ex obtain x where px: "P x" by blast + from px nmi npi nmpiU have "\ u\ U. \ u' \ U. u \ x \ x \ u'" by auto + then obtain u and u' where uU:"u\ U" and uU': "u' \ U" and ux:"u \ x" and xu':"x \ u'" by auto + from uU have Une: "U \ {}" by auto + let ?l = "Min U" + let ?u = "Max U" + have linM: "?l \ U" using fU Une by simp + have uinM: "?u \ U" using fU Une by simp + have lM: "\ t\ U. ?l \ t" using Une fU by auto + have Mu: "\ t\ U. t \ ?u" using Une fU by auto + have th:"?l \ u" using uU Une lM by auto + from order_trans[OF th ux] have lx: "?l \ x" . + have th: "u' \ ?u" using uU' Une Mu by simp + from order_trans[OF xu' th] have xu: "x \ ?u" . + from finite_set_intervals2[where P="P",OF px lx xu linM uinM fU lM Mu] + have "(\ s\ U. P s) \ + (\ t1\ U. \ t2 \ U. (\ y. t1 \ y \ y \ t2 \ y \ U) \ t1 \ x \ x \ t2 \ P x)" . + moreover { fix u assume um: "u\U" and pu: "P u" + have "between u u = u" by (simp add: between_same) + with um pu have "P (between u u)" by simp + with um have ?thesis by blast} + moreover{ + assume "\ t1\ U. \ t2 \ U. (\ y. t1 \ y \ y \ t2 \ y \ U) \ t1 \ x \ x \ t2 \ P x" + then obtain t1 and t2 where t1M: "t1 \ U" and t2M: "t2\ U" + and noM: "\ y. t1 \ y \ y \ t2 \ y \ U" and t1x: "t1 \ x" and xt2: "x \ t2" and px: "P x" + by blast + from less_trans[OF t1x xt2] have t1t2: "t1 \ t2" . + let ?u = "between t1 t2" + from between_less t1t2 have t1lu: "t1 \ ?u" and ut2: "?u \ t2" by auto + from lin_dense[rule_format, OF] noM t1x xt2 px t1lu ut2 have "P ?u" by blast + with t1M t2M have ?thesis by blast} + ultimately show ?thesis by blast + qed + +theorem fr_eq: + assumes fU: "finite U" + and lin_dense: "\x l u. (\ t. l \ t \ t\ u \ t \ U) \ l\ x \ x \ u \ P x + \ (\ y. l \ y \ y \ u \ P y )" + and nmibnd: "\x. \ MP \ P x \ (\ u\ U. u \ x)" + and npibnd: "\x. \PP \ P x \ (\ u\ U. x \ u)" + and mi: "\z. \x. x \ z \ (P x = MP)" and pi: "\z. \x. z \ x \ (P x = PP)" + shows "(\ x. P x) \ (MP \ PP \ (\ u \ U. \ u'\ U. P (between u u')))" + (is "_ \ (_ \ _ \ ?F)" is "?E \ ?D") +proof- + { + assume px: "\ x. P x" + have "MP \ PP \ (\ MP \ \ PP)" by blast + moreover {assume "MP \ PP" hence "?D" by blast} + moreover {assume nmi: "\ MP" and npi: "\ PP" + from npmibnd[OF nmibnd npibnd] + have nmpiU: "\x. \ MP \ \PP \ P x \ (\ u\ U. \ u' \ U. u \ x \ x \ u')" . + from rinf_U[OF fU lin_dense nmpiU nmi npi px] have "?D" by blast} + ultimately have "?D" by blast} + moreover + { assume "?D" + moreover {assume m:"MP" from minf_ex[OF mi m] have "?E" .} + moreover {assume p: "PP" from pinf_ex[OF pi p] have "?E" . } + moreover {assume f:"?F" hence "?E" by blast} + ultimately have "?E" by blast} + ultimately have "?E = ?D" by blast thus "?E \ ?D" by simp +qed + +lemmas minf_thms = minf_conj minf_disj minf_eq minf_neq minf_lt minf_le minf_gt minf_ge minf_P +lemmas pinf_thms = pinf_conj pinf_disj pinf_eq pinf_neq pinf_lt pinf_le pinf_gt pinf_ge pinf_P + +lemmas nmi_thms = nmi_conj nmi_disj nmi_eq nmi_neq nmi_lt nmi_le nmi_gt nmi_ge nmi_P +lemmas npi_thms = npi_conj npi_disj npi_eq npi_neq npi_lt npi_le npi_gt npi_ge npi_P +lemmas lin_dense_thms = lin_dense_conj lin_dense_disj lin_dense_eq lin_dense_neq lin_dense_lt lin_dense_le lin_dense_gt lin_dense_ge lin_dense_P + +lemma ferrack_axiom: "dense_linear_order less_eq less between" by fact +lemma atoms: includes meta_term_syntax + shows "TERM (op \ :: 'a \ _)" and "TERM (op \)" and "TERM (op = :: 'a \ _)" . + +declare ferrack_axiom [dlo minf: minf_thms pinf: pinf_thms + nmi: nmi_thms npi: npi_thms lindense: + lin_dense_thms qe: fr_eq atoms: atoms] + +declaration {* +let +fun generic_whatis phi = + let + val [lt, le] = map (Morphism.term phi) + (ProofContext.read_term_pats @{typ "dummy"} @{context} ["op \", "op \"]) (* FIXME avoid read? *) + val le = Morphism.term phi @{term "op \"} + fun h x t = + case term_of t of + Const("op =", _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq + else Ferrante_Rackoff_Data.Nox + | @{term "Not"}$(Const("op =", _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq + else Ferrante_Rackoff_Data.Nox + | b$y$z => if Term.could_unify (b, lt) then + if term_of x aconv y then Ferrante_Rackoff_Data.Lt + else if term_of x aconv z then Ferrante_Rackoff_Data.Gt + else Ferrante_Rackoff_Data.Nox + else if Term.could_unify (b, le) then + if term_of x aconv y then Ferrante_Rackoff_Data.Le + else if term_of x aconv z then Ferrante_Rackoff_Data.Ge + else Ferrante_Rackoff_Data.Nox + else Ferrante_Rackoff_Data.Nox + | _ => Ferrante_Rackoff_Data.Nox + in h end + val ss = K (HOL_ss addsimps [@{thm "not_less"}, @{thm "not_le"}]) +in + Ferrante_Rackoff_Data.funs @{thm "ferrack_axiom"} + {isolate_conv = K (K (K Thm.reflexive)), whatis = generic_whatis, simpset = ss} +end +*} + +end + +use "Tools/Ferrante_Rackoff/ferrante_rackoff.ML" + +method_setup dlo = {* + Method.ctxt_args (Method.SIMPLE_METHOD' o FerranteRackoff.dlo_tac) +*} "Ferrante and Rackoff's algorithm for quantifier elimination in dense linear orders" + +end