src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
changeset 51143 0a2371e7ced3
parent 50282 fe4d4bb9f4c2
child 53374 a14d2a854c02
     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Feb 15 08:31:30 2013 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Feb 15 08:31:31 2013 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  theory Parametric_Ferrante_Rackoff
     1.6  imports Reflected_Multivariate_Polynomial Dense_Linear_Order DP_Library
     1.7 -  "~~/src/HOL/Library/Efficient_Nat" "~~/src/HOL/Library/Old_Recdef"
     1.8 +  "~~/src/HOL/Library/Code_Target_Numeral" "~~/src/HOL/Library/Old_Recdef"
     1.9  begin
    1.10  
    1.11  subsection {* Terms *}
    1.12 @@ -2795,6 +2795,10 @@
    1.13  fun binopT T = T --> T --> T;
    1.14  fun relT T = T --> T --> @{typ bool};
    1.15  
    1.16 +val mk_C = @{code C} o pairself @{code int_of_integer};
    1.17 +val mk_poly_Bound = @{code poly.Bound} o @{code nat_of_integer};
    1.18 +val mk_Bound = @{code Bound} o @{code nat_of_integer};
    1.19 +
    1.20  val dest_num = snd o HOLogic.dest_number;
    1.21  
    1.22  fun try_dest_num t = SOME ((snd o HOLogic.dest_number) t)
    1.23 @@ -2812,19 +2816,19 @@
    1.24    | num_of_term ps (Const (@{const_name Groups.plus}, _) $ a $ b) = @{code poly.Add} (num_of_term ps a, num_of_term ps b)
    1.25    | num_of_term ps (Const (@{const_name Groups.minus}, _) $ a $ b) = @{code poly.Sub} (num_of_term ps a, num_of_term ps b)
    1.26    | num_of_term ps (Const (@{const_name Groups.times}, _) $ a $ b) = @{code poly.Mul} (num_of_term ps a, num_of_term ps b)
    1.27 -  | num_of_term ps (Const (@{const_name Power.power}, _) $ a $ n) = @{code poly.Pw} (num_of_term ps a, dest_nat n)
    1.28 -  | num_of_term ps (Const (@{const_name Fields.divide}, _) $ a $ b) = @{code poly.C} (dest_num a, dest_num b)
    1.29 +  | num_of_term ps (Const (@{const_name Power.power}, _) $ a $ n) = @{code poly.Pw} (num_of_term ps a, @{code nat_of_integer} (dest_nat n))
    1.30 +  | num_of_term ps (Const (@{const_name Fields.divide}, _) $ a $ b) = mk_C (dest_num a, dest_num b)
    1.31    | num_of_term ps t = (case try_dest_num t
    1.32 -     of SOME k => @{code poly.C} (k, 1)
    1.33 -      | NONE => @{code poly.Bound} (the_index ps t));
    1.34 +     of SOME k => mk_C (k, 1)
    1.35 +      | NONE => mk_poly_Bound (the_index ps t));
    1.36  
    1.37  fun tm_of_term fs ps (Const(@{const_name Groups.uminus}, _) $ t) = @{code Neg} (tm_of_term fs ps t)
    1.38    | tm_of_term fs ps (Const(@{const_name Groups.plus}, _) $ a $ b) = @{code Add} (tm_of_term fs ps a, tm_of_term fs ps b)
    1.39    | tm_of_term fs ps (Const(@{const_name Groups.minus}, _) $ a $ b) = @{code Sub} (tm_of_term fs ps a, tm_of_term fs ps b)
    1.40    | tm_of_term fs ps (Const(@{const_name Groups.times}, _) $ a $ b) = @{code Mul} (num_of_term ps a, tm_of_term fs ps b)
    1.41    | tm_of_term fs ps t = (@{code CP} (num_of_term ps t) 
    1.42 -      handle TERM _ => @{code Bound} (the_index fs t)
    1.43 -           | General.Subscript => @{code Bound} (the_index fs t));
    1.44 +      handle TERM _ => mk_Bound (the_index fs t)
    1.45 +           | General.Subscript => mk_Bound (the_index fs t));
    1.46  
    1.47  fun fm_of_term fs ps @{term True} = @{code T}
    1.48    | fm_of_term fs ps @{term False} = @{code F}
    1.49 @@ -2850,21 +2854,25 @@
    1.50    | fm_of_term fs ps _ = error "fm_of_term";
    1.51  
    1.52  fun term_of_num T ps (@{code poly.C} (a, b)) = 
    1.53 -    (if b = 1 then HOLogic.mk_number T a
    1.54 -     else if b = 0 then Const (@{const_name Groups.zero}, T)
    1.55 -     else Const (@{const_name Fields.divide}, binopT T) $ HOLogic.mk_number T a $ HOLogic.mk_number T b)
    1.56 -  | term_of_num T ps (@{code poly.Bound} i) = nth ps i
    1.57 +      let
    1.58 +        val (c, d) = pairself (@{code integer_of_int}) (a, b)
    1.59 +      in
    1.60 +        (if d = 1 then HOLogic.mk_number T c
    1.61 +        else if d = 0 then Const (@{const_name Groups.zero}, T)
    1.62 +        else Const (@{const_name Fields.divide}, binopT T) $ HOLogic.mk_number T c $ HOLogic.mk_number T d)
    1.63 +      end
    1.64 +  | term_of_num T ps (@{code poly.Bound} i) = nth ps (@{code integer_of_nat} i)
    1.65    | term_of_num T ps (@{code poly.Add} (a, b)) = Const (@{const_name Groups.plus}, binopT T) $ term_of_num T ps a $ term_of_num T ps b
    1.66    | term_of_num T ps (@{code poly.Mul} (a, b)) = Const (@{const_name Groups.times}, binopT T) $ term_of_num T ps a $ term_of_num T ps b
    1.67    | term_of_num T ps (@{code poly.Sub} (a, b)) = Const (@{const_name Groups.minus}, binopT T) $ term_of_num T ps a $ term_of_num T ps b
    1.68    | term_of_num T ps (@{code poly.Neg} a) = Const (@{const_name Groups.uminus}, T --> T) $ term_of_num T ps a
    1.69 -  | term_of_num T ps (@{code poly.Pw} (a, n)) =
    1.70 -      Const (@{const_name Power.power}, T --> @{typ nat} --> T) $ term_of_num T ps a $ HOLogic.mk_number HOLogic.natT n
    1.71 +  | term_of_num T ps (@{code poly.Pw} (a, n)) = Const (@{const_name Power.power},
    1.72 +      T --> @{typ nat} --> T) $ term_of_num T ps a $ HOLogic.mk_number HOLogic.natT (@{code integer_of_nat} n)
    1.73    | term_of_num T ps (@{code poly.CN} (c, n, p)) =
    1.74        term_of_num T ps (@{code poly.Add} (c, @{code poly.Mul} (@{code poly.Bound} n, p)));
    1.75  
    1.76  fun term_of_tm T fs ps (@{code CP} p) = term_of_num T ps p
    1.77 -  | term_of_tm T fs ps (@{code Bound} i) = nth fs i
    1.78 +  | term_of_tm T fs ps (@{code Bound} i) = nth fs (@{code integer_of_nat} i)
    1.79    | term_of_tm T fs ps (@{code Add} (a, b)) = Const (@{const_name Groups.plus}, binopT T) $ term_of_tm T fs ps a $ term_of_tm T fs ps b
    1.80    | term_of_tm T fs ps (@{code Mul} (a, b)) = Const (@{const_name Groups.times}, binopT T) $ term_of_num T ps a $ term_of_tm T fs ps b
    1.81    | term_of_tm T fs ps (@{code Sub} (a, b)) = Const (@{const_name Groups.minus}, binopT T) $ term_of_tm T fs ps a $ term_of_tm T fs ps b
    1.82 @@ -2993,3 +3001,4 @@
    1.83  *)
    1.84  end
    1.85  
    1.86 +