# HG changeset patch
# User haftmann
# Date 1486502107 -3600
# Node ID f8f76a501d2530511410f67d07acace5d059cffc
# Parent  d51478d6aae44fc1ef63c3adc78bc60656d2e90c
elaborated examples for computations

diff -r d51478d6aae4 -r f8f76a501d25 src/HOL/Decision_Procs/Commutative_Ring.thy
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Tue Feb 07 22:15:06 2017 +0100
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Tue Feb 07 22:15:07 2017 +0100
@@ -655,22 +655,37 @@
 lemma in_carrier_trivial: "cring_class.in_carrier l"
   by (induct l) (simp_all add: cring_class.in_carrier_def carrier_class)
 
-code_reflect Ring_Code
-  datatypes pol = Pc | Pinj | PX
-  and polex = Var | Const | Add | Sub | Mul | Pow | Neg
-  and nat and int
-  functions norm pnsubstl mk_monpol_list
-    Nat.zero_nat_inst.zero_nat Nat.one_nat_inst.one_nat
-    Nat.minus_nat_inst.minus_nat Nat.times_nat_inst.times_nat nat_of_integer integer_of_nat
-    Int.zero_int_inst.zero_int Int.one_int_inst.one_int
-    Int.uminus_int_inst.uminus_int
-    int_of_integer
-    term_of_pol_inst.term_of_pol
-    term_of_polex_inst.term_of_polex
-    equal_pol_inst.equal_pol
+ML \<open>
+val term_of_nat = HOLogic.mk_number @{typ nat} o @{code integer_of_nat};
+
+val term_of_int = HOLogic.mk_number @{typ int} o @{code integer_of_int};
+
+fun term_of_pol (@{code Pc} k) = @{term Pc} $ term_of_int k
+  | term_of_pol (@{code Pinj} (n, p)) = @{term Pinj} $ term_of_nat n $ term_of_pol p
+  | term_of_pol (@{code PX} (p, n, q)) = @{term PX} $ term_of_pol p $ term_of_nat n $ term_of_pol q;
+
+local
+
+fun pol (ctxt, ct, t) = Thm.mk_binop @{cterm "Pure.eq :: pol \<Rightarrow> pol \<Rightarrow> prop"}
+  ct (Thm.cterm_of ctxt t);
 
-definition ring_codegen_aux :: "pol itself" where
-  "ring_codegen_aux = (Code_Evaluation.TERM_OF_EQUAL::pol itself)"
+val (_, raw_pol_oracle) = Context.>>> (Context.map_theory_result
+  (Thm.add_oracle (@{binding pnsubstl}, pol)));
+
+fun pol_oracle ctxt ct t = raw_pol_oracle (ctxt, ct, t);
+
+in
+
+val cv = @{computation_conv pol
+  terms: pnsubstl mk_monpol_list norm
+    nat_of_integer Code_Target_Nat.natural
+      "0::nat" "1::nat" "2::nat" "3::nat"
+      "0::int" "1::int" "2::int" "3::int" "-1::int"
+  datatypes: polex "(polex * polex) list" int integer num}
+  (fn p => fn ct => pol_oracle @{context} ct (term_of_pol p))
+
+end
+\<close>
 
 ML \<open>
 signature RING_TAC =
@@ -906,14 +921,6 @@
 val iterations = @{cterm "1000::nat"};
 val Trueprop_cong = Thm.combination (Thm.reflexive @{cterm Trueprop});
 
-val cv = Code_Evaluation.static_conv
-  {ctxt = @{context},
-   consts =
-     [@{const_name pnsubstl},
-      @{const_name norm},
-      @{const_name mk_monpol_list},
-      @{const_name ring_codegen_aux}]};
-
 fun commutative_ring_conv ctxt prems eqs ct =
   let
     val cT = Thm.ctyp_of_cterm ct;
diff -r d51478d6aae4 -r f8f76a501d25 src/HOL/Decision_Procs/Reflective_Field.thy
--- a/src/HOL/Decision_Procs/Reflective_Field.thy	Tue Feb 07 22:15:06 2017 +0100
+++ b/src/HOL/Decision_Procs/Reflective_Field.thy	Tue Feb 07 22:15:07 2017 +0100
@@ -5,7 +5,7 @@
 *)
 
 theory Reflective_Field
-imports Commutative_Ring
+imports "~~/src/HOL/Decision_Procs/Commutative_Ring"
 begin
 
 datatype fexpr =
@@ -639,18 +639,46 @@
   qed
 qed
 
-code_reflect Field_Code
-  datatypes fexpr = FCnst | FVar | FAdd | FSub | FMul | FNeg | FDiv | FPow
-  and pexpr = PExpr1 | PExpr2
-  and pexpr1 = PCnst | PVar | PAdd | PSub | PNeg
-  and pexpr2 = PMul | PPow
-  functions fnorm
-    term_of_fexpr_inst.term_of_fexpr
-    term_of_pexpr_inst.term_of_pexpr
-    equal_pexpr_inst.equal_pexpr
+ML \<open>
+val term_of_nat = HOLogic.mk_number @{typ nat} o @{code integer_of_nat};
+
+val term_of_int = HOLogic.mk_number @{typ int} o @{code integer_of_int};
+
+fun term_of_pexpr (@{code PExpr1} x) = @{term PExpr1} $ term_of_pexpr1 x
+  | term_of_pexpr (@{code PExpr2} x) = @{term PExpr2} $ term_of_pexpr2 x
+and term_of_pexpr1 (@{code PCnst} k) = @{term PCnst} $ term_of_int k
+  | term_of_pexpr1 (@{code PVar} n) = @{term PVar} $ term_of_nat n
+  | term_of_pexpr1 (@{code PAdd} (x, y)) = @{term PAdd} $ term_of_pexpr x $ term_of_pexpr y
+  | term_of_pexpr1 (@{code PSub} (x, y)) = @{term PSub} $ term_of_pexpr x $ term_of_pexpr y
+  | term_of_pexpr1 (@{code PNeg} x) = @{term PNeg} $ term_of_pexpr x
+and term_of_pexpr2 (@{code PMul} (x, y)) = @{term PMul} $ term_of_pexpr x $ term_of_pexpr y
+  | term_of_pexpr2 (@{code PPow} (x, n)) = @{term PPow} $ term_of_pexpr x $ term_of_nat n
+
+fun term_of_result (x, (y, zs)) =
+  HOLogic.mk_prod (term_of_pexpr x, HOLogic.mk_prod
+    (term_of_pexpr y, HOLogic.mk_list @{typ pexpr} (map term_of_pexpr zs)));
 
-definition field_codegen_aux :: "(pexpr \<times> pexpr list) itself" where
-  "field_codegen_aux = (Code_Evaluation.TERM_OF_EQUAL::(pexpr \<times> pexpr list) itself)"
+local
+
+fun fnorm (ctxt, ct, t) = Thm.mk_binop @{cterm "Pure.eq :: pexpr \<times> pexpr \<times> pexpr list \<Rightarrow> pexpr \<times> pexpr \<times> pexpr list \<Rightarrow> prop"}
+  ct (Thm.cterm_of ctxt t);
+
+val (_, raw_fnorm_oracle) = Context.>>> (Context.map_theory_result
+  (Thm.add_oracle (@{binding fnorm}, fnorm)));
+
+fun fnorm_oracle ctxt ct t = raw_fnorm_oracle (ctxt, ct, t);
+
+in
+
+val cv = @{computation_conv "pexpr \<times> pexpr \<times> pexpr list"
+  terms: fnorm nat_of_integer Code_Target_Nat.natural
+    "0::nat" "1::nat" "2::nat" "3::nat"
+    "0::int" "1::int" "2::int" "3::int" "-1::int"
+  datatypes: fexpr int integer num}
+  (fn result => fn ct => fnorm_oracle @{context} ct (term_of_result result))
+
+end
+\<close>
 
 ML \<open>
 signature FIELD_TAC =
@@ -861,12 +889,6 @@
               (cong2 (cong1 (cong2 (args2 peval_conv') Thm.reflexive)) (args2 conv))))
   in conv end;
 
-val cv = Code_Evaluation.static_conv
-  {ctxt = @{context},
-   consts =
-     [@{const_name nat_of_integer},
-      @{const_name fnorm}, @{const_name field_codegen_aux}]};
-
 fun field_tac in_prem ctxt =
   SUBGOAL (fn (g, i) =>
     let