src/HOL/ex/coopereif.ML
changeset 24423 ae9cd0e92423
parent 24000 467e77e4e276
child 24630 351a308ab58d
     1.1 --- a/src/HOL/ex/coopereif.ML	Fri Aug 24 14:14:18 2007 +0200
     1.2 +++ b/src/HOL/ex/coopereif.ML	Fri Aug 24 14:14:20 2007 +0200
     1.3 @@ -37,11 +37,11 @@
     1.4        | Const(@{const_name "Divides.dvd"},_)$t1$t2 => 
     1.5            (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => error "qf_of_term: unsupported dvd")
     1.6        | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
     1.7 -      | @{term "op = :: bool => _ "}$t1$t2 => Iffa(qf_of_term ps vs t1,qf_of_term ps vs t2)
     1.8 +      | @{term "op = :: bool => _ "}$t1$t2 => Iff(qf_of_term ps vs t1,qf_of_term ps vs t2)
     1.9        | Const("op &",_)$t1$t2 => And(qf_of_term ps vs t1,qf_of_term ps vs t2)
    1.10        | Const("op |",_)$t1$t2 => Or(qf_of_term ps vs t1,qf_of_term ps vs t2)
    1.11 -      | Const("op -->",_)$t1$t2 => Impa(qf_of_term ps vs t1,qf_of_term ps vs t2)
    1.12 -      | Const("Not",_)$t' => Nota(qf_of_term ps vs t')
    1.13 +      | Const("op -->",_)$t1$t2 => Imp(qf_of_term ps vs t1,qf_of_term ps vs t2)
    1.14 +      | Const("Not",_)$t' => Not(qf_of_term ps vs t')
    1.15        | Const("Ex",_)$Abs(xn,xT,p) => 
    1.16           let val (xn',p') = variant_abs (xn,xT,p)
    1.17               val vs' = (Free (xn',xT), nat 0) :: (map (fn(v,n) => (v,1 + n)) vs)
    1.18 @@ -102,17 +102,17 @@
    1.19    | Gt t' => @{term "op < :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
    1.20    | Ge t' => @{term "op <= :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
    1.21    | Eq t' => @{term "op = :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
    1.22 -  | NEq t' => term_of_qf ps vs (Nota(Eq t'))
    1.23 +  | NEq t' => term_of_qf ps vs (Not(Eq t'))
    1.24    | Dvd(i,t') => @{term "op dvd :: int => _ "}$ 
    1.25        (HOLogic.mk_number HOLogic.intT i)$(term_of_i vs t')
    1.26 -  | NDvd(i,t')=> term_of_qf ps vs (Nota(Dvd(i,t')))
    1.27 -  | Nota t' => HOLogic.Not$(term_of_qf ps vs t')
    1.28 +  | NDvd(i,t')=> term_of_qf ps vs (Not(Dvd(i,t')))
    1.29 +  | Not t' => HOLogic.Not$(term_of_qf ps vs t')
    1.30    | And(t1,t2) => HOLogic.conj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
    1.31    | Or(t1,t2) => HOLogic.disj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
    1.32 -  | Impa(t1,t2) => HOLogic.imp$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
    1.33 -  | Iffa(t1,t2) => HOLogic.eq_const HOLogic.boolT $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
    1.34 +  | Imp(t1,t2) => HOLogic.imp$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
    1.35 +  | Iff(t1,t2) => HOLogic.eq_const HOLogic.boolT $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
    1.36    | Closed n => (fst o the) (find_first (fn (_, m) => m = n) ps)
    1.37 -  | NClosed n => term_of_qf ps vs (Nota (Closed n))
    1.38 +  | NClosed n => term_of_qf ps vs (Not (Closed n))
    1.39    | _ => error "If this is raised, Isabelle/HOL or generate_code is inconsistent!";
    1.40  
    1.41  (* The oracle *)