src/HOL/Tools/Qelim/cooper.ML
changeset 36832 e6078ef937df
parent 36831 3037d6810fca
child 36833 9628f969d843
     1.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Tue May 11 18:31:36 2010 +0200
     1.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Tue May 11 18:46:03 2010 +0200
     1.3 @@ -582,81 +582,96 @@
     1.4      | _ => if skip orelse is_op t then I else insert (op aconv) t
     1.5    end;
     1.6  
     1.7 +fun descend vs (abs as (_, xT, _)) =
     1.8 +  let
     1.9 +    val (xn', p') = variant_abs abs;
    1.10 +    val vs' = ((xn', xT), 0) :: (map o apsnd) (fn n => n + 1) vs;
    1.11 +  in (vs', p') end;
    1.12 +
    1.13  local structure Proc = Cooper_Procedure in
    1.14  
    1.15 -fun i_of_term vs (Free vT) = Proc.Bound (the (AList.lookup (op =) vs vT))
    1.16 -  | i_of_term vs (Term.Bound i) = Proc.Bound i
    1.17 -  | i_of_term vs @{term "0::int"} = Proc.C 0
    1.18 -  | i_of_term vs @{term "1::int"} = Proc.C 1
    1.19 -  | i_of_term vs (t as Const (@{const_name number_of}, _) $ _) = Proc.C (dest_number t)
    1.20 -  | i_of_term vs (Const (@{const_name Groups.uminus}, _) $ t') = Proc.Neg (i_of_term vs t')
    1.21 -  | i_of_term vs (Const (@{const_name Groups.plus}, _) $ t1 $ t2) = Proc.Add (i_of_term vs t1, i_of_term vs t2)
    1.22 -  | i_of_term vs (Const (@{const_name Groups.minus}, _) $ t1 $ t2) = Proc.Sub (i_of_term vs t1, i_of_term vs t2)
    1.23 -  | i_of_term vs (Const (@{const_name Groups.times}, _) $ t1 $ t2) = (case perhaps_number t1
    1.24 -     of SOME n => Proc.Mul (n, i_of_term vs t2)
    1.25 -      | NONE => (case perhaps_number t2
    1.26 -         of SOME n => Proc.Mul (n, i_of_term vs t1)
    1.27 -          | NONE => raise COOPER "reification: unsupported kind of multiplication"))
    1.28 -  | i_of_term _ _ = raise COOPER "reification: unknown term";
    1.29 +fun num_of_term vs (Free vT) = Proc.Bound (the (AList.lookup (op =) vs vT))
    1.30 +  | num_of_term vs (Term.Bound i) = Proc.Bound i
    1.31 +  | num_of_term vs @{term "0::int"} = Proc.C 0
    1.32 +  | num_of_term vs @{term "1::int"} = Proc.C 1
    1.33 +  | num_of_term vs (t as Const (@{const_name number_of}, _) $ _) =
    1.34 +      Proc.C (dest_number t)
    1.35 +  | num_of_term vs (Const (@{const_name Groups.uminus}, _) $ t') =
    1.36 +      Proc.Neg (num_of_term vs t')
    1.37 +  | num_of_term vs (Const (@{const_name Groups.plus}, _) $ t1 $ t2) =
    1.38 +      Proc.Add (num_of_term vs t1, num_of_term vs t2)
    1.39 +  | num_of_term vs (Const (@{const_name Groups.minus}, _) $ t1 $ t2) =
    1.40 +      Proc.Sub (num_of_term vs t1, num_of_term vs t2)
    1.41 +  | num_of_term vs (Const (@{const_name Groups.times}, _) $ t1 $ t2) =
    1.42 +     (case perhaps_number t1
    1.43 +       of SOME n => Proc.Mul (n, num_of_term vs t2)
    1.44 +        | NONE => (case perhaps_number t2
    1.45 +           of SOME n => Proc.Mul (n, num_of_term vs t1)
    1.46 +            | NONE => raise COOPER "reification: unsupported kind of multiplication"))
    1.47 +  | num_of_term _ _ = raise COOPER "reification: bad term";
    1.48  
    1.49 -fun qf_of_term ps vs t = case t
    1.50 - of Const (@{const_name True}, _) => Proc.T
    1.51 -  | Const (@{const_name False}, _) => Proc.F
    1.52 -  | Const (@{const_name Orderings.less}, _) $ t1 $ t2 => Proc.Lt (Proc.Sub (i_of_term vs t1, i_of_term vs t2))
    1.53 -  | Const (@{const_name Orderings.less_eq}, _) $ t1 $ t2 => Proc.Le (Proc.Sub(i_of_term vs t1, i_of_term vs t2))
    1.54 -  | Const (@{const_name Rings.dvd}, _) $ t1 $ t2 =>
    1.55 -      (Proc.Dvd (dest_number t1, i_of_term vs t2)
    1.56 -        handle TERM _ => raise COOPER "reification: unsupported dvd")
    1.57 -  | @{term "op = :: int => _"} $ t1 $ t2 => Proc.Eq (Proc.Sub (i_of_term vs t1, i_of_term vs t2))
    1.58 -  | @{term "op = :: bool => _ "} $ t1 $ t2 => Proc.Iff (qf_of_term ps vs t1, qf_of_term ps vs t2)
    1.59 -  | Const ("op &", _) $ t1 $t2 => Proc.And (qf_of_term ps vs t1, qf_of_term ps vs t2)
    1.60 -  | Const ("op |", _) $ t1 $ t2 => Proc.Or (qf_of_term ps vs t1, qf_of_term ps vs t2)
    1.61 -  | Const ("op -->", _) $ t1 $t2 => Proc.Imp (qf_of_term ps vs t1, qf_of_term ps vs t2)
    1.62 -  | Const (@{const_name Not}, _) $ t' => Proc.Not (qf_of_term ps vs t')
    1.63 -  | Const ("Ex", _) $ Abs (xn, xT, p) =>
    1.64 -     let val (xn',p') = variant_abs (xn,xT,p)
    1.65 -         val vs' = ((xn',xT), 0) :: (map (fn(v,n) => (v,1+ n)) vs)
    1.66 -     in Proc.E (qf_of_term ps vs' p')
    1.67 -     end
    1.68 -  | Const("All", _) $ Abs (xn, xT, p) =>
    1.69 -     let val (xn',p') = variant_abs (xn,xT,p)
    1.70 -         val vs' = ((xn',xT), 0) :: (map (fn(v,n) => (v,1+ n)) vs)
    1.71 -     in Proc.A (qf_of_term ps vs' p')
    1.72 -     end
    1.73 -  | _ =>(case AList.lookup (op aconv) ps t of
    1.74 -           NONE => raise COOPER "reification: unknown term"
    1.75 -         | SOME n => Proc.Closed n);
    1.76 +fun fm_of_term ps vs (Const (@{const_name True}, _)) = Proc.T
    1.77 +  | fm_of_term ps vs (Const (@{const_name False}, _)) = Proc.F
    1.78 +  | fm_of_term ps vs (Const ("op &", _) $ t1 $ t2) =
    1.79 +      Proc.And (fm_of_term ps vs t1, fm_of_term ps vs t2)
    1.80 +  | fm_of_term ps vs (Const ("op |", _) $ t1 $ t2) =
    1.81 +      Proc.Or (fm_of_term ps vs t1, fm_of_term ps vs t2)
    1.82 +  | fm_of_term ps vs (Const ("op -->", _) $ t1 $ t2) =
    1.83 +      Proc.Imp (fm_of_term ps vs t1, fm_of_term ps vs t2)
    1.84 +  | fm_of_term ps vs (@{term "op = :: bool => _ "} $ t1 $ t2) =
    1.85 +      Proc.Iff (fm_of_term ps vs t1, fm_of_term ps vs t2)
    1.86 +  | fm_of_term ps vs (Const (@{const_name Not}, _) $ t') =
    1.87 +      Proc.Not (fm_of_term ps vs t')
    1.88 +  | fm_of_term ps vs (Const ("Ex", _) $ Abs abs) =
    1.89 +      Proc.E (uncurry (fm_of_term ps) (descend vs abs))
    1.90 +  | fm_of_term ps vs (Const ("All", _) $ Abs abs) =
    1.91 +      Proc.A (uncurry (fm_of_term ps) (descend vs abs))
    1.92 +  | fm_of_term ps vs (@{term "op = :: int => _"} $ t1 $ t2) =
    1.93 +      Proc.Eq (Proc.Sub (num_of_term vs t1, num_of_term vs t2))
    1.94 +  | fm_of_term ps vs (Const (@{const_name Orderings.less_eq}, _) $ t1 $ t2) =
    1.95 +      Proc.Le (Proc.Sub (num_of_term vs t1, num_of_term vs t2))
    1.96 +  | fm_of_term ps vs (Const (@{const_name Orderings.less}, _) $ t1 $ t2) =
    1.97 +      Proc.Lt (Proc.Sub (num_of_term vs t1, num_of_term vs t2))
    1.98 +  | fm_of_term ps vs (Const (@{const_name Rings.dvd}, _) $ t1 $ t2) =
    1.99 +     (case perhaps_number t1
   1.100 +       of SOME n => Proc.Dvd (n, num_of_term vs t2)
   1.101 +        | NONE => raise COOPER "reification: unsupported dvd")
   1.102 +  | fm_of_term ps vs t =
   1.103 +     (case AList.lookup (op aconv) ps t
   1.104 +       of SOME n => Proc.Closed n
   1.105 +        | NONE => raise COOPER "reification: unknown term");
   1.106  
   1.107 -fun term_of_i vs t = case t
   1.108 - of Proc.C i => HOLogic.mk_number HOLogic.intT i
   1.109 -  | Proc.Bound n => Free (the (AList.lookup (op =) vs n))
   1.110 -  | Proc.Neg t' => @{term "uminus :: int => _"} $ term_of_i vs t'
   1.111 -  | Proc.Add (t1, t2) => @{term "op + :: int => _"} $ term_of_i vs t1 $ term_of_i vs t2
   1.112 -  | Proc.Sub (t1, t2) => @{term "op - :: int => _"} $ term_of_i vs t1 $ term_of_i vs t2
   1.113 -  | Proc.Mul (i, t2) => @{term "op * :: int => _"} $
   1.114 -      HOLogic.mk_number HOLogic.intT i $ term_of_i vs t2
   1.115 -  | Proc.Cn (n, i, t') => term_of_i vs (Proc.Add (Proc.Mul (i, Proc.Bound n), t'));
   1.116 +fun term_of_num vs (Proc.C i) = HOLogic.mk_number HOLogic.intT i
   1.117 +  | term_of_num vs (Proc.Bound n) = Free (the (AList.lookup (op =) vs n))
   1.118 +  | term_of_num vs (Proc.Neg t') =
   1.119 +      @{term "uminus :: int => _"} $ term_of_num vs t'
   1.120 +  | term_of_num vs (Proc.Add (t1, t2)) =
   1.121 +      @{term "op + :: int => _"} $ term_of_num vs t1 $ term_of_num vs t2
   1.122 +  | term_of_num vs (Proc.Sub (t1, t2)) =
   1.123 +      @{term "op - :: int => _"} $ term_of_num vs t1 $ term_of_num vs t2
   1.124 +  | term_of_num vs (Proc.Mul (i, t2)) =
   1.125 +      @{term "op * :: int => _"} $ HOLogic.mk_number HOLogic.intT i $ term_of_num vs t2
   1.126 +  | term_of_num vs (Proc.Cn (n, i, t')) =
   1.127 +      term_of_num vs (Proc.Add (Proc.Mul (i, Proc.Bound n), t'));
   1.128  
   1.129 -fun term_of_qf ps vs t =
   1.130 - case t of
   1.131 -   Proc.T => HOLogic.true_const
   1.132 - | Proc.F => HOLogic.false_const
   1.133 - | Proc.Lt t' => @{term "op < :: int => _ "} $ term_of_i vs t' $ @{term "0::int"}
   1.134 - | Proc.Le t' => @{term "op <= :: int => _ "} $ term_of_i vs t' $ @{term "0::int"}
   1.135 - | Proc.Gt t' => @{term "op < :: int => _ "} $ @{term "0::int"} $ term_of_i vs t'
   1.136 - | Proc.Ge t' => @{term "op <= :: int => _ "} $ @{term "0::int"} $ term_of_i vs t'
   1.137 - | Proc.Eq t' => @{term "op = :: int => _ "} $ term_of_i vs t'$ @{term "0::int"}
   1.138 - | Proc.NEq t' => term_of_qf ps vs (Proc.Not (Proc.Eq t'))
   1.139 - | Proc.Dvd (i, t') => @{term "op dvd :: int => _ "} $
   1.140 -    HOLogic.mk_number HOLogic.intT i $ term_of_i vs t'
   1.141 - | Proc.NDvd (i, t')=> term_of_qf ps vs (Proc.Not (Proc.Dvd (i, t')))
   1.142 - | Proc.Not t' => HOLogic.Not $ term_of_qf ps vs t'
   1.143 - | Proc.And (t1, t2) => HOLogic.conj $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
   1.144 - | Proc.Or (t1, t2) => HOLogic.disj $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
   1.145 - | Proc.Imp (t1, t2) => HOLogic.imp $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
   1.146 - | Proc.Iff (t1, t2) => @{term "op = :: bool => _"} $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
   1.147 - | Proc.Closed n => the (AList.lookup (op =) ps n)
   1.148 - | Proc.NClosed n => term_of_qf ps vs (Proc.Not (Proc.Closed n));
   1.149 +fun term_of_fm ps vs Proc.T = HOLogic.true_const
   1.150 +  | term_of_fm ps vs Proc.F = HOLogic.false_const
   1.151 +  | term_of_fm ps vs (Proc.And (t1, t2)) = HOLogic.conj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
   1.152 +  | term_of_fm ps vs (Proc.Or (t1, t2)) = HOLogic.disj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
   1.153 +  | term_of_fm ps vs (Proc.Imp (t1, t2)) = HOLogic.imp $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
   1.154 +  | term_of_fm ps vs (Proc.Iff (t1, t2)) = @{term "op = :: bool => _"} $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
   1.155 +  | term_of_fm ps vs (Proc.Not t') = HOLogic.Not $ term_of_fm ps vs t'
   1.156 +  | term_of_fm ps vs (Proc.Eq t') = @{term "op = :: int => _ "} $ term_of_num vs t'$ @{term "0::int"}
   1.157 +  | term_of_fm ps vs (Proc.NEq t') = term_of_fm ps vs (Proc.Not (Proc.Eq t'))
   1.158 +  | term_of_fm ps vs (Proc.Lt t') = @{term "op < :: int => _ "} $ term_of_num vs t' $ @{term "0::int"}
   1.159 +  | term_of_fm ps vs (Proc.Le t') = @{term "op <= :: int => _ "} $ term_of_num vs t' $ @{term "0::int"}
   1.160 +  | term_of_fm ps vs (Proc.Gt t') = @{term "op < :: int => _ "} $ @{term "0::int"} $ term_of_num vs t'
   1.161 +  | term_of_fm ps vs (Proc.Ge t') = @{term "op <= :: int => _ "} $ @{term "0::int"} $ term_of_num vs t'
   1.162 +  | term_of_fm ps vs (Proc.Dvd (i, t')) = @{term "op dvd :: int => _ "} $
   1.163 +      HOLogic.mk_number HOLogic.intT i $ term_of_num vs t'
   1.164 +  | term_of_fm ps vs (Proc.NDvd (i, t')) = term_of_fm ps vs (Proc.Not (Proc.Dvd (i, t')))
   1.165 +  | term_of_fm ps vs (Proc.Closed n) = the (AList.lookup (op =) ps n)
   1.166 +  | term_of_fm ps vs (Proc.NClosed n) = term_of_fm ps vs (Proc.Not (Proc.Closed n));
   1.167  
   1.168  fun invoke t =
   1.169    let
   1.170 @@ -664,7 +679,7 @@
   1.171      val ps = map_index swap (add_bools t []);
   1.172    in
   1.173      Logic.mk_equals (HOLogic.mk_Trueprop t,
   1.174 -      HOLogic.mk_Trueprop (term_of_qf (map swap ps) (map swap vs) (Proc.pa (qf_of_term ps vs t))))
   1.175 +      HOLogic.mk_Trueprop (term_of_fm (map swap ps) (map swap vs) (Proc.pa (fm_of_term ps vs t))))
   1.176    end;
   1.177  
   1.178  end;