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.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.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.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.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.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.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.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.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.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.60 -constdefs numneg :: "num \<Rightarrow> num"
1.61 +definition numneg :: "num \<Rightarrow> num" where
1.62    "numneg t \<equiv> nummul t (- 1)"
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.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.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.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