src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
 changeset 35416 d8d7d1b785af parent 35267 8dfd816713c6 child 35625 9c818cab0dd0
```     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Feb 24 11:55:52 2010 +0100
1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Mar 01 13:40:23 2010 +0100
1.3 @@ -273,10 +273,10 @@
1.4    assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero, field})"
1.5    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)
1.6
1.7 -constdefs tmneg :: "tm \<Rightarrow> tm"
1.8 +definition tmneg :: "tm \<Rightarrow> tm" where
1.9    "tmneg t \<equiv> tmmul t (C (- 1,1))"
1.10
1.11 -constdefs tmsub :: "tm \<Rightarrow> tm \<Rightarrow> tm"
1.12 +definition tmsub :: "tm \<Rightarrow> tm \<Rightarrow> tm" where
1.13    "tmsub s t \<equiv> (if s = t then CP 0\<^sub>p else tmadd (s,tmneg t))"
1.14
1.15  lemma tmneg[simp]: "Itm vs bs (tmneg t) = Itm vs bs (Neg t)"
1.16 @@ -477,26 +477,26 @@
1.17  lemma not[simp]: "Ifm vs bs (not p) = Ifm vs bs (NOT p)"
1.18  by (induct p rule: not.induct) auto
1.19
1.20 -constdefs conj :: "fm \<Rightarrow> fm \<Rightarrow> fm"
1.21 +definition conj :: "fm \<Rightarrow> fm \<Rightarrow> fm" where
1.22    "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
1.23     if p = q then p else And p q)"
1.24  lemma conj[simp]: "Ifm vs bs (conj p q) = Ifm vs bs (And p q)"
1.25  by (cases "p=F \<or> q=F",simp_all add: conj_def) (cases p,simp_all)
1.26
1.27 -constdefs disj :: "fm \<Rightarrow> fm \<Rightarrow> fm"
1.28 +definition disj :: "fm \<Rightarrow> fm \<Rightarrow> fm" where
1.29    "disj p q \<equiv> (if (p = T \<or> q=T) then T else if p=F then q else if q=F then p
1.30         else if p=q then p else Or p q)"
1.31
1.32  lemma disj[simp]: "Ifm vs bs (disj p q) = Ifm vs bs (Or p q)"
1.33  by (cases "p=T \<or> q=T",simp_all add: disj_def) (cases p,simp_all)
1.34
1.35 -constdefs  imp :: "fm \<Rightarrow> fm \<Rightarrow> fm"
1.36 +definition imp :: "fm \<Rightarrow> fm \<Rightarrow> fm" where
1.37    "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
1.38      else Imp p q)"
1.39  lemma imp[simp]: "Ifm vs bs (imp p q) = Ifm vs bs (Imp p q)"
1.40  by (cases "p=F \<or> q=T",simp_all add: imp_def)
1.41
1.42 -constdefs   iff :: "fm \<Rightarrow> fm \<Rightarrow> fm"
1.43 +definition iff :: "fm \<Rightarrow> fm \<Rightarrow> fm" where
1.44    "iff p q \<equiv> (if (p = q) then T else if (p = NOT q \<or> NOT p = q) then F else
1.45         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
1.46    Iff p q)"
1.47 @@ -776,10 +776,10 @@
1.48  lemma bound0_qf: "bound0 p \<Longrightarrow> qfree p"
1.49  by (induct p, simp_all)
1.50
1.51 -constdefs djf:: "('a \<Rightarrow> fm) \<Rightarrow> 'a \<Rightarrow> fm \<Rightarrow> fm"
1.52 +definition djf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a \<Rightarrow> fm \<Rightarrow> fm" where
1.53    "djf f p q \<equiv> (if q=T then T else if q=F then f p else
1.54    (let fp = f p in case fp of T \<Rightarrow> T | F \<Rightarrow> q | _ \<Rightarrow> Or (f p) q))"
1.55 -constdefs evaldjf:: "('a \<Rightarrow> fm) \<Rightarrow> 'a list \<Rightarrow> fm"
1.56 +definition evaldjf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a list \<Rightarrow> fm" where
1.57    "evaldjf f ps \<equiv> foldr (djf f) ps F"
1.58
1.59  lemma djf_Or: "Ifm vs bs (djf f p q) = Ifm vs bs (Or (f p) q)"
1.60 @@ -823,7 +823,7 @@
1.61    thus ?thesis by (simp only: list_all_iff)
1.62  qed
1.63
1.64 -constdefs DJ :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm"
1.65 +definition DJ :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm" where
1.66    "DJ f p \<equiv> evaldjf f (disjuncts p)"
1.67
1.68  lemma DJ: assumes fdj: "\<forall> p q. Ifm vs bs (f (Or p q)) = Ifm vs bs (Or (f p) (f q))"
1.69 @@ -869,10 +869,10 @@
1.70    "conjuncts T = []"
1.71    "conjuncts p = [p]"
1.72
1.73 -constdefs list_conj :: "fm list \<Rightarrow> fm"
1.74 +definition list_conj :: "fm list \<Rightarrow> fm" where
1.75    "list_conj ps \<equiv> foldr conj ps T"
1.76
1.77 -constdefs CJNB:: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm"
1.78 +definition CJNB :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm" where
1.79    "CJNB f p \<equiv> (let cjs = conjuncts p ; (yes,no) = partition bound0 cjs
1.80                     in conj (decr0 (list_conj yes)) (f (list_conj no)))"
1.81
1.82 @@ -1158,7 +1158,7 @@
1.83    "conjs p = [p]"
1.84  lemma conjs_ci: "(\<forall> q \<in> set (conjs p). Ifm vs bs q) = Ifm vs bs p"
1.85  by (induct p rule: conjs.induct, auto)
1.86 -constdefs list_disj :: "fm list \<Rightarrow> fm"
1.87 +definition list_disj :: "fm list \<Rightarrow> fm" where
1.88    "list_disj ps \<equiv> foldr disj ps F"
1.89
1.90  lemma list_conj: "Ifm vs bs (list_conj ps) = (\<forall>p\<in> set ps. Ifm vs bs p)"
```