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)"