src/HOL/ex/coopereif.ML
changeset 24423 ae9cd0e92423
parent 24000 467e77e4e276
child 24630 351a308ab58d
equal deleted inserted replaced
24422:c0b5ff9e9e4d 24423:ae9cd0e92423
    35       | Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
    35       | Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
    36       | Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
    36       | Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
    37       | Const(@{const_name "Divides.dvd"},_)$t1$t2 => 
    37       | Const(@{const_name "Divides.dvd"},_)$t1$t2 => 
    38           (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => error "qf_of_term: unsupported dvd")
    38           (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => error "qf_of_term: unsupported dvd")
    39       | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
    39       | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
    40       | @{term "op = :: bool => _ "}$t1$t2 => Iffa(qf_of_term ps vs t1,qf_of_term ps vs t2)
    40       | @{term "op = :: bool => _ "}$t1$t2 => Iff(qf_of_term ps vs t1,qf_of_term ps vs t2)
    41       | Const("op &",_)$t1$t2 => And(qf_of_term ps vs t1,qf_of_term ps vs t2)
    41       | Const("op &",_)$t1$t2 => And(qf_of_term ps vs t1,qf_of_term ps vs t2)
    42       | Const("op |",_)$t1$t2 => Or(qf_of_term ps vs t1,qf_of_term ps vs t2)
    42       | Const("op |",_)$t1$t2 => Or(qf_of_term ps vs t1,qf_of_term ps vs t2)
    43       | Const("op -->",_)$t1$t2 => Impa(qf_of_term ps vs t1,qf_of_term ps vs t2)
    43       | Const("op -->",_)$t1$t2 => Imp(qf_of_term ps vs t1,qf_of_term ps vs t2)
    44       | Const("Not",_)$t' => Nota(qf_of_term ps vs t')
    44       | Const("Not",_)$t' => Not(qf_of_term ps vs t')
    45       | Const("Ex",_)$Abs(xn,xT,p) => 
    45       | Const("Ex",_)$Abs(xn,xT,p) => 
    46          let val (xn',p') = variant_abs (xn,xT,p)
    46          let val (xn',p') = variant_abs (xn,xT,p)
    47              val vs' = (Free (xn',xT), nat 0) :: (map (fn(v,n) => (v,1 + n)) vs)
    47              val vs' = (Free (xn',xT), nat 0) :: (map (fn(v,n) => (v,1 + n)) vs)
    48          in E (qf_of_term ps vs' p')
    48          in E (qf_of_term ps vs' p')
    49          end
    49          end
   100   | Lt t' => @{term "op < :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
   100   | Lt t' => @{term "op < :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
   101   | Le t' => @{term "op <= :: int => _ "}$ term_of_i vs t' $ @{term "0::int"}
   101   | Le t' => @{term "op <= :: int => _ "}$ term_of_i vs t' $ @{term "0::int"}
   102   | Gt t' => @{term "op < :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
   102   | Gt t' => @{term "op < :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
   103   | Ge t' => @{term "op <= :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
   103   | Ge t' => @{term "op <= :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
   104   | Eq t' => @{term "op = :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
   104   | Eq t' => @{term "op = :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
   105   | NEq t' => term_of_qf ps vs (Nota(Eq t'))
   105   | NEq t' => term_of_qf ps vs (Not(Eq t'))
   106   | Dvd(i,t') => @{term "op dvd :: int => _ "}$ 
   106   | Dvd(i,t') => @{term "op dvd :: int => _ "}$ 
   107       (HOLogic.mk_number HOLogic.intT i)$(term_of_i vs t')
   107       (HOLogic.mk_number HOLogic.intT i)$(term_of_i vs t')
   108   | NDvd(i,t')=> term_of_qf ps vs (Nota(Dvd(i,t')))
   108   | NDvd(i,t')=> term_of_qf ps vs (Not(Dvd(i,t')))
   109   | Nota t' => HOLogic.Not$(term_of_qf ps vs t')
   109   | Not t' => HOLogic.Not$(term_of_qf ps vs t')
   110   | And(t1,t2) => HOLogic.conj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
   110   | And(t1,t2) => HOLogic.conj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
   111   | Or(t1,t2) => HOLogic.disj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
   111   | Or(t1,t2) => HOLogic.disj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
   112   | Impa(t1,t2) => HOLogic.imp$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
   112   | Imp(t1,t2) => HOLogic.imp$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
   113   | Iffa(t1,t2) => HOLogic.eq_const HOLogic.boolT $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
   113   | Iff(t1,t2) => HOLogic.eq_const HOLogic.boolT $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
   114   | Closed n => (fst o the) (find_first (fn (_, m) => m = n) ps)
   114   | Closed n => (fst o the) (find_first (fn (_, m) => m = n) ps)
   115   | NClosed n => term_of_qf ps vs (Nota (Closed n))
   115   | NClosed n => term_of_qf ps vs (Not (Closed n))
   116   | _ => error "If this is raised, Isabelle/HOL or generate_code is inconsistent!";
   116   | _ => error "If this is raised, Isabelle/HOL or generate_code is inconsistent!";
   117 
   117 
   118 (* The oracle *)
   118 (* The oracle *)
   119 fun cooper_oracle thy t = 
   119 fun cooper_oracle thy t = 
   120   let
   120   let