271 |
271 |
272 lemma tmmul_allpolys_npoly[simp]: |
272 lemma tmmul_allpolys_npoly[simp]: |
273 assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero, field})" |
273 assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero, field})" |
274 shows "allpolys isnpoly t \<Longrightarrow> isnpoly c \<Longrightarrow> allpolys isnpoly (tmmul t c)" by (induct t rule: tmmul.induct, simp_all add: Let_def polymul_norm) |
274 shows "allpolys isnpoly t \<Longrightarrow> isnpoly c \<Longrightarrow> allpolys isnpoly (tmmul t c)" by (induct t rule: tmmul.induct, simp_all add: Let_def polymul_norm) |
275 |
275 |
276 constdefs tmneg :: "tm \<Rightarrow> tm" |
276 definition tmneg :: "tm \<Rightarrow> tm" where |
277 "tmneg t \<equiv> tmmul t (C (- 1,1))" |
277 "tmneg t \<equiv> tmmul t (C (- 1,1))" |
278 |
278 |
279 constdefs tmsub :: "tm \<Rightarrow> tm \<Rightarrow> tm" |
279 definition tmsub :: "tm \<Rightarrow> tm \<Rightarrow> tm" where |
280 "tmsub s t \<equiv> (if s = t then CP 0\<^sub>p else tmadd (s,tmneg t))" |
280 "tmsub s t \<equiv> (if s = t then CP 0\<^sub>p else tmadd (s,tmneg t))" |
281 |
281 |
282 lemma tmneg[simp]: "Itm vs bs (tmneg t) = Itm vs bs (Neg t)" |
282 lemma tmneg[simp]: "Itm vs bs (tmneg t) = Itm vs bs (Neg t)" |
283 using tmneg_def[of t] |
283 using tmneg_def[of t] |
284 apply simp |
284 apply simp |
475 "not (NEq t) = Eq t" |
475 "not (NEq t) = Eq t" |
476 "not p = NOT p" |
476 "not p = NOT p" |
477 lemma not[simp]: "Ifm vs bs (not p) = Ifm vs bs (NOT p)" |
477 lemma not[simp]: "Ifm vs bs (not p) = Ifm vs bs (NOT p)" |
478 by (induct p rule: not.induct) auto |
478 by (induct p rule: not.induct) auto |
479 |
479 |
480 constdefs conj :: "fm \<Rightarrow> fm \<Rightarrow> fm" |
480 definition conj :: "fm \<Rightarrow> fm \<Rightarrow> fm" where |
481 "conj p q \<equiv> (if (p = F \<or> q=F) then F else if p=T then q else if q=T then p else |
481 "conj p q \<equiv> (if (p = F \<or> q=F) then F else if p=T then q else if q=T then p else |
482 if p = q then p else And p q)" |
482 if p = q then p else And p q)" |
483 lemma conj[simp]: "Ifm vs bs (conj p q) = Ifm vs bs (And p q)" |
483 lemma conj[simp]: "Ifm vs bs (conj p q) = Ifm vs bs (And p q)" |
484 by (cases "p=F \<or> q=F",simp_all add: conj_def) (cases p,simp_all) |
484 by (cases "p=F \<or> q=F",simp_all add: conj_def) (cases p,simp_all) |
485 |
485 |
486 constdefs disj :: "fm \<Rightarrow> fm \<Rightarrow> fm" |
486 definition disj :: "fm \<Rightarrow> fm \<Rightarrow> fm" where |
487 "disj p q \<equiv> (if (p = T \<or> q=T) then T else if p=F then q else if q=F then p |
487 "disj p q \<equiv> (if (p = T \<or> q=T) then T else if p=F then q else if q=F then p |
488 else if p=q then p else Or p q)" |
488 else if p=q then p else Or p q)" |
489 |
489 |
490 lemma disj[simp]: "Ifm vs bs (disj p q) = Ifm vs bs (Or p q)" |
490 lemma disj[simp]: "Ifm vs bs (disj p q) = Ifm vs bs (Or p q)" |
491 by (cases "p=T \<or> q=T",simp_all add: disj_def) (cases p,simp_all) |
491 by (cases "p=T \<or> q=T",simp_all add: disj_def) (cases p,simp_all) |
492 |
492 |
493 constdefs imp :: "fm \<Rightarrow> fm \<Rightarrow> fm" |
493 definition imp :: "fm \<Rightarrow> fm \<Rightarrow> fm" where |
494 "imp p q \<equiv> (if (p = F \<or> q=T \<or> p=q) then T else if p=T then q else if q=F then not p |
494 "imp p q \<equiv> (if (p = F \<or> q=T \<or> p=q) then T else if p=T then q else if q=F then not p |
495 else Imp p q)" |
495 else Imp p q)" |
496 lemma imp[simp]: "Ifm vs bs (imp p q) = Ifm vs bs (Imp p q)" |
496 lemma imp[simp]: "Ifm vs bs (imp p q) = Ifm vs bs (Imp p q)" |
497 by (cases "p=F \<or> q=T",simp_all add: imp_def) |
497 by (cases "p=F \<or> q=T",simp_all add: imp_def) |
498 |
498 |
499 constdefs iff :: "fm \<Rightarrow> fm \<Rightarrow> fm" |
499 definition iff :: "fm \<Rightarrow> fm \<Rightarrow> fm" where |
500 "iff p q \<equiv> (if (p = q) then T else if (p = NOT q \<or> NOT p = q) then F else |
500 "iff p q \<equiv> (if (p = q) then T else if (p = NOT q \<or> NOT p = q) then F else |
501 if p=F then not q else if q=F then not p else if p=T then q else if q=T then p else |
501 if p=F then not q else if q=F then not p else if p=T then q else if q=T then p else |
502 Iff p q)" |
502 Iff p q)" |
503 lemma iff[simp]: "Ifm vs bs (iff p q) = Ifm vs bs (Iff p q)" |
503 lemma iff[simp]: "Ifm vs bs (iff p q) = Ifm vs bs (Iff p q)" |
504 by (unfold iff_def,cases "p=q", simp,cases "p=NOT q", simp) (cases "NOT p= q", auto) |
504 by (unfold iff_def,cases "p=q", simp,cases "p=NOT q", simp) (cases "NOT p= q", auto) |
774 "isatom p = False" |
774 "isatom p = False" |
775 |
775 |
776 lemma bound0_qf: "bound0 p \<Longrightarrow> qfree p" |
776 lemma bound0_qf: "bound0 p \<Longrightarrow> qfree p" |
777 by (induct p, simp_all) |
777 by (induct p, simp_all) |
778 |
778 |
779 constdefs djf:: "('a \<Rightarrow> fm) \<Rightarrow> 'a \<Rightarrow> fm \<Rightarrow> fm" |
779 definition djf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a \<Rightarrow> fm \<Rightarrow> fm" where |
780 "djf f p q \<equiv> (if q=T then T else if q=F then f p else |
780 "djf f p q \<equiv> (if q=T then T else if q=F then f p else |
781 (let fp = f p in case fp of T \<Rightarrow> T | F \<Rightarrow> q | _ \<Rightarrow> Or (f p) q))" |
781 (let fp = f p in case fp of T \<Rightarrow> T | F \<Rightarrow> q | _ \<Rightarrow> Or (f p) q))" |
782 constdefs evaldjf:: "('a \<Rightarrow> fm) \<Rightarrow> 'a list \<Rightarrow> fm" |
782 definition evaldjf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a list \<Rightarrow> fm" where |
783 "evaldjf f ps \<equiv> foldr (djf f) ps F" |
783 "evaldjf f ps \<equiv> foldr (djf f) ps F" |
784 |
784 |
785 lemma djf_Or: "Ifm vs bs (djf f p q) = Ifm vs bs (Or (f p) q)" |
785 lemma djf_Or: "Ifm vs bs (djf f p q) = Ifm vs bs (Or (f p) q)" |
786 by (cases "q=T", simp add: djf_def,cases "q=F",simp add: djf_def) |
786 by (cases "q=T", simp add: djf_def,cases "q=F",simp add: djf_def) |
787 (cases "f p", simp_all add: Let_def djf_def) |
787 (cases "f p", simp_all add: Let_def djf_def) |
821 hence "list_all qfree (disjuncts p)" |
821 hence "list_all qfree (disjuncts p)" |
822 by (induct p rule: disjuncts.induct, auto) |
822 by (induct p rule: disjuncts.induct, auto) |
823 thus ?thesis by (simp only: list_all_iff) |
823 thus ?thesis by (simp only: list_all_iff) |
824 qed |
824 qed |
825 |
825 |
826 constdefs DJ :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm" |
826 definition DJ :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm" where |
827 "DJ f p \<equiv> evaldjf f (disjuncts p)" |
827 "DJ f p \<equiv> evaldjf f (disjuncts p)" |
828 |
828 |
829 lemma DJ: assumes fdj: "\<forall> p q. Ifm vs bs (f (Or p q)) = Ifm vs bs (Or (f p) (f q))" |
829 lemma DJ: assumes fdj: "\<forall> p q. Ifm vs bs (f (Or p q)) = Ifm vs bs (Or (f p) (f q))" |
830 and fF: "f F = F" |
830 and fF: "f F = F" |
831 shows "Ifm vs bs (DJ f p) = Ifm vs bs (f p)" |
831 shows "Ifm vs bs (DJ f p) = Ifm vs bs (f p)" |
867 recdef conjuncts "measure size" |
867 recdef conjuncts "measure size" |
868 "conjuncts (And p q) = (conjuncts p) @ (conjuncts q)" |
868 "conjuncts (And p q) = (conjuncts p) @ (conjuncts q)" |
869 "conjuncts T = []" |
869 "conjuncts T = []" |
870 "conjuncts p = [p]" |
870 "conjuncts p = [p]" |
871 |
871 |
872 constdefs list_conj :: "fm list \<Rightarrow> fm" |
872 definition list_conj :: "fm list \<Rightarrow> fm" where |
873 "list_conj ps \<equiv> foldr conj ps T" |
873 "list_conj ps \<equiv> foldr conj ps T" |
874 |
874 |
875 constdefs CJNB:: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm" |
875 definition CJNB :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm" where |
876 "CJNB f p \<equiv> (let cjs = conjuncts p ; (yes,no) = partition bound0 cjs |
876 "CJNB f p \<equiv> (let cjs = conjuncts p ; (yes,no) = partition bound0 cjs |
877 in conj (decr0 (list_conj yes)) (f (list_conj no)))" |
877 in conj (decr0 (list_conj yes)) (f (list_conj no)))" |
878 |
878 |
879 lemma conjuncts_qf: "qfree p \<Longrightarrow> \<forall> q\<in> set (conjuncts p). qfree q" |
879 lemma conjuncts_qf: "qfree p \<Longrightarrow> \<forall> q\<in> set (conjuncts p). qfree q" |
880 proof- |
880 proof- |
1156 "conjs (And p q) = (conjs p)@(conjs q)" |
1156 "conjs (And p q) = (conjs p)@(conjs q)" |
1157 "conjs T = []" |
1157 "conjs T = []" |
1158 "conjs p = [p]" |
1158 "conjs p = [p]" |
1159 lemma conjs_ci: "(\<forall> q \<in> set (conjs p). Ifm vs bs q) = Ifm vs bs p" |
1159 lemma conjs_ci: "(\<forall> q \<in> set (conjs p). Ifm vs bs q) = Ifm vs bs p" |
1160 by (induct p rule: conjs.induct, auto) |
1160 by (induct p rule: conjs.induct, auto) |
1161 constdefs list_disj :: "fm list \<Rightarrow> fm" |
1161 definition list_disj :: "fm list \<Rightarrow> fm" where |
1162 "list_disj ps \<equiv> foldr disj ps F" |
1162 "list_disj ps \<equiv> foldr disj ps F" |
1163 |
1163 |
1164 lemma list_conj: "Ifm vs bs (list_conj ps) = (\<forall>p\<in> set ps. Ifm vs bs p)" |
1164 lemma list_conj: "Ifm vs bs (list_conj ps) = (\<forall>p\<in> set ps. Ifm vs bs p)" |
1165 by (induct ps, auto simp add: list_conj_def) |
1165 by (induct ps, auto simp add: list_conj_def) |
1166 lemma list_conj_qf: " \<forall>p\<in> set ps. qfree p \<Longrightarrow> qfree (list_conj ps)" |
1166 lemma list_conj_qf: " \<forall>p\<in> set ps. qfree p \<Longrightarrow> qfree (list_conj ps)" |