src/HOL/Decision_Procs/Ferrack.thy
changeset 35416 d8d7d1b785af
parent 33639 603320b93668
child 36853 c8e4102b08aa
     1.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -169,26 +169,26 @@
     1.4  lemma not[simp]: "Ifm bs (not p) = Ifm bs (NOT p)"
     1.5  by (cases p) auto
     1.6  
     1.7 -constdefs conj :: "fm \<Rightarrow> fm \<Rightarrow> fm"
     1.8 +definition conj :: "fm \<Rightarrow> fm \<Rightarrow> fm" where
     1.9    "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.10     if p = q then p else And p q)"
    1.11  lemma conj[simp]: "Ifm bs (conj p q) = Ifm bs (And p q)"
    1.12  by (cases "p=F \<or> q=F",simp_all add: conj_def) (cases p,simp_all)
    1.13  
    1.14 -constdefs disj :: "fm \<Rightarrow> fm \<Rightarrow> fm"
    1.15 +definition disj :: "fm \<Rightarrow> fm \<Rightarrow> fm" where
    1.16    "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.17         else if p=q then p else Or p q)"
    1.18  
    1.19  lemma disj[simp]: "Ifm bs (disj p q) = Ifm bs (Or p q)"
    1.20  by (cases "p=T \<or> q=T",simp_all add: disj_def) (cases p,simp_all)
    1.21  
    1.22 -constdefs  imp :: "fm \<Rightarrow> fm \<Rightarrow> fm"
    1.23 +definition imp :: "fm \<Rightarrow> fm \<Rightarrow> fm" where
    1.24    "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.25      else Imp p q)"
    1.26  lemma imp[simp]: "Ifm bs (imp p q) = Ifm bs (Imp p q)"
    1.27  by (cases "p=F \<or> q=T",simp_all add: imp_def) 
    1.28  
    1.29 -constdefs   iff :: "fm \<Rightarrow> fm \<Rightarrow> fm"
    1.30 +definition iff :: "fm \<Rightarrow> fm \<Rightarrow> fm" where
    1.31    "iff p q \<equiv> (if (p = q) then T else if (p = NOT q \<or> NOT p = q) then F else 
    1.32         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.33    Iff p q)"
    1.34 @@ -369,10 +369,10 @@
    1.35  lemma bound0_qf: "bound0 p \<Longrightarrow> qfree p"
    1.36  by (induct p, simp_all)
    1.37  
    1.38 -constdefs djf:: "('a \<Rightarrow> fm) \<Rightarrow> 'a \<Rightarrow> fm \<Rightarrow> fm"
    1.39 +definition djf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a \<Rightarrow> fm \<Rightarrow> fm" where
    1.40    "djf f p q \<equiv> (if q=T then T else if q=F then f p else 
    1.41    (let fp = f p in case fp of T \<Rightarrow> T | F \<Rightarrow> q | _ \<Rightarrow> Or (f p) q))"
    1.42 -constdefs evaldjf:: "('a \<Rightarrow> fm) \<Rightarrow> 'a list \<Rightarrow> fm"
    1.43 +definition evaldjf :: "('a \<Rightarrow> fm) \<Rightarrow> 'a list \<Rightarrow> fm" where
    1.44    "evaldjf f ps \<equiv> foldr (djf f) ps F"
    1.45  
    1.46  lemma djf_Or: "Ifm bs (djf f p q) = Ifm bs (Or (f p) q)"
    1.47 @@ -423,7 +423,7 @@
    1.48    thus ?thesis by (simp only: list_all_iff)
    1.49  qed
    1.50  
    1.51 -constdefs DJ :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm"
    1.52 +definition DJ :: "(fm \<Rightarrow> fm) \<Rightarrow> fm \<Rightarrow> fm" where
    1.53    "DJ f p \<equiv> evaldjf f (disjuncts p)"
    1.54  
    1.55  lemma DJ: assumes fdj: "\<forall> p q. Ifm bs (f (Or p q)) = Ifm bs (Or (f p) (f q))"
    1.56 @@ -653,10 +653,10 @@
    1.57  lemma nummul_nb[simp]: "\<And> i. numbound0 t \<Longrightarrow> numbound0 (nummul t i)"
    1.58  by (induct t rule: nummul.induct, auto )
    1.59  
    1.60 -constdefs numneg :: "num \<Rightarrow> num"
    1.61 +definition numneg :: "num \<Rightarrow> num" where
    1.62    "numneg t \<equiv> nummul t (- 1)"
    1.63  
    1.64 -constdefs numsub :: "num \<Rightarrow> num \<Rightarrow> num"
    1.65 +definition numsub :: "num \<Rightarrow> num \<Rightarrow> num" where
    1.66    "numsub s t \<equiv> (if s = t then C 0 else numadd (s,numneg t))"
    1.67  
    1.68  lemma numneg[simp]: "Inum bs (numneg t) = Inum bs (Neg t)"
    1.69 @@ -724,7 +724,7 @@
    1.70    from maxcoeff_nz[OF nz th] show ?thesis .
    1.71  qed
    1.72  
    1.73 -constdefs simp_num_pair:: "(num \<times> int) \<Rightarrow> num \<times> int"
    1.74 +definition simp_num_pair :: "(num \<times> int) \<Rightarrow> num \<times> int" where
    1.75    "simp_num_pair \<equiv> (\<lambda> (t,n). (if n = 0 then (C 0, 0) else
    1.76     (let t' = simpnum t ; g = numgcd t' in 
    1.77        if g > 1 then (let g' = gcd n g in 
    1.78 @@ -1779,7 +1779,7 @@
    1.79  
    1.80  
    1.81      (* Implement the right hand side of Ferrante and Rackoff's Theorem. *)
    1.82 -constdefs ferrack:: "fm \<Rightarrow> fm"
    1.83 +definition ferrack :: "fm \<Rightarrow> fm" where
    1.84    "ferrack p \<equiv> (let p' = rlfm (simpfm p); mp = minusinf p'; pp = plusinf p'
    1.85                  in if (mp = T \<or> pp = T) then T else 
    1.86                     (let U = remdps(map simp_num_pair