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 +
```