src/HOL/Complex/ex/mireif.ML
changeset 24423 ae9cd0e92423
parent 23881 851c74f1bb69
child 25919 8b1c0d434824
     1.1 --- a/src/HOL/Complex/ex/mireif.ML	Fri Aug 24 14:14:18 2007 +0200
     1.2 +++ b/src/HOL/Complex/ex/mireif.ML	Fri Aug 24 14:14:20 2007 +0200
     1.3 @@ -42,18 +42,18 @@
     1.4      case t of 
     1.5          Const("True",_) => T
     1.6        | Const("False",_) => F
     1.7 -      | Const(@{const_name HOL.less},_)$t1$t2 => Lta (Sub (num_of_term vs t1,num_of_term vs t2))
     1.8 -      | Const(@{const_name HOL.less_eq},_)$t1$t2 => Lea (Sub (num_of_term vs t1,num_of_term vs t2))
     1.9 +      | Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (num_of_term vs t1,num_of_term vs t2))
    1.10 +      | Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub (num_of_term vs t1,num_of_term vs t2))
    1.11        | Const (@{const_name "MIR.rdvd"},_ )$ (Const("RealDef.real",_) $ (Const(@{const_name "Numeral.number_of"},_)$t1))$t2 => 
    1.12 -        Dvda (HOLogic.dest_numeral t1, num_of_term vs t2)
    1.13 +        Dvd (HOLogic.dest_numeral t1, num_of_term vs t2)
    1.14        | Const("op =",eqT)$t1$t2 => 
    1.15          if (domain_type eqT = @{typ real})
    1.16 -        then Eqa (Sub (num_of_term vs t1, num_of_term vs t2)) 
    1.17 -        else Iffa (fm_of_term vs t1, fm_of_term vs t2)
    1.18 +        then Eq (Sub (num_of_term vs t1, num_of_term vs t2)) 
    1.19 +        else Iff (fm_of_term vs t1, fm_of_term vs t2)
    1.20        | Const("op &",_)$t1$t2 => And (fm_of_term vs t1, fm_of_term vs t2)
    1.21        | Const("op |",_)$t1$t2 => Or (fm_of_term vs t1, fm_of_term vs t2)
    1.22 -      | Const("op -->",_)$t1$t2 => Impa (fm_of_term vs t1, fm_of_term vs t2)
    1.23 -      | Const("Not",_)$t' => Nota (fm_of_term vs t')
    1.24 +      | Const("op -->",_)$t1$t2 => Imp (fm_of_term vs t1, fm_of_term vs t2)
    1.25 +      | Const("Not",_)$t' => Not (fm_of_term vs t')
    1.26        | Const("Ex",_)$Abs(xn,xT,p) => 
    1.27          E (fm_of_term (map (fn (v, n) => (v, Suc n)) vs) p)
    1.28        | Const("All",_)$Abs(xn,xT,p) => 
    1.29 @@ -93,19 +93,19 @@
    1.30      case t of 
    1.31          T => HOLogic.true_const 
    1.32        | F => HOLogic.false_const
    1.33 -      | Lta t => @{term "op <:: real => _"} $ term_of_num vs t $ rzero
    1.34 -      | Lea t => @{term "op <=:: real => _"} $ term_of_num vs t $ rzero
    1.35 -      | Gta t => @{term "op <:: real => _"}$ rzero $ term_of_num vs t
    1.36 -      | Gea t => @{term "op <=:: real => _"} $ rzero $ term_of_num vs t
    1.37 -      | Eqa t => @{term "op = :: real => _"}$ term_of_num vs t $ rzero
    1.38 -      | NEq t => term_of_fm vs (Nota (Eqa t))
    1.39 -      | NDvd (i,t) => term_of_fm vs (Nota (Dvda (i,t)))
    1.40 -      | Dvda (i,t) => @{term "op rdvd"} $ term_of_num vs (C i) $ term_of_num vs t
    1.41 -      | Nota t' => HOLogic.Not$(term_of_fm vs t')
    1.42 +      | Lt t => @{term "op <:: real => _"} $ term_of_num vs t $ rzero
    1.43 +      | Le t => @{term "op <=:: real => _"} $ term_of_num vs t $ rzero
    1.44 +      | Gt t => @{term "op <:: real => _"}$ rzero $ term_of_num vs t
    1.45 +      | Ge t => @{term "op <=:: real => _"} $ rzero $ term_of_num vs t
    1.46 +      | Eq t => @{term "op = :: real => _"}$ term_of_num vs t $ rzero
    1.47 +      | NEq t => term_of_fm vs (Not (Eq t))
    1.48 +      | NDvd (i,t) => term_of_fm vs (Not (Dvd (i,t)))
    1.49 +      | Dvd (i,t) => @{term "op rdvd"} $ term_of_num vs (C i) $ term_of_num vs t
    1.50 +      | Not t' => HOLogic.Not$(term_of_fm vs t')
    1.51        | And(t1,t2) => HOLogic.conj $ term_of_fm vs t1 $ term_of_fm vs t2
    1.52        | Or(t1,t2) => HOLogic.disj $ term_of_fm vs t1 $ term_of_fm vs t2
    1.53 -      | Impa(t1,t2) => HOLogic.imp $ term_of_fm vs t1 $ term_of_fm vs t2
    1.54 -      | Iffa(t1,t2) => HOLogic.mk_eq (term_of_fm vs t1, term_of_fm vs t2)
    1.55 +      | Imp(t1,t2) => HOLogic.imp $ term_of_fm vs t1 $ term_of_fm vs t2
    1.56 +      | Iff(t1,t2) => HOLogic.mk_eq (term_of_fm vs t1, term_of_fm vs t2)
    1.57        | _ => error "If this is raised, Isabelle/HOL or generate_code is inconsistent!";
    1.58  
    1.59  (* The oracle *)