dropped toy example Code_Antiq
authorhaftmann
Fri Mar 27 10:05:13 2009 +0100 (2009-03-27)
changeset 307402d3ae5a7edb2
parent 30739 8a854c90f7e6
child 30741 9e23e3ea7edd
dropped toy example Code_Antiq
NEWS
src/HOL/ex/Code_Antiq.thy
src/HOL/ex/ROOT.ML
     1.1 --- a/NEWS	Fri Mar 27 10:05:12 2009 +0100
     1.2 +++ b/NEWS	Fri Mar 27 10:05:13 2009 +0100
     1.3 @@ -498,10 +498,9 @@
     1.4  resulting ML value/function/datatype constructor binding in place.
     1.5  All occurrences of @{code} with a single ML block are generated
     1.6  simultaneously.  Provides a generic and safe interface for
     1.7 -instrumentalizing code generation.  See HOL/ex/Code_Antiq for a toy
     1.8 -example, or HOL/Complex/ex/ReflectedFerrack for a more ambitious
     1.9 -application.  In future you ought refrain from ad-hoc compiling
    1.10 -generated SML code on the ML toplevel.  Note that (for technical
    1.11 +instrumentalizing code generation.  See HOL/Decision_Procs/Ferrack for
    1.12 +a more ambitious application.  In future you ought refrain from ad-hoc
    1.13 +compiling generated SML code on the ML toplevel.  Note that (for technical
    1.14  reasons) @{code} cannot refer to constants for which user-defined
    1.15  serializations are set.  Refer to the corresponding ML counterpart
    1.16  directly in that cases.
     2.1 --- a/src/HOL/ex/Code_Antiq.thy	Fri Mar 27 10:05:12 2009 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,84 +0,0 @@
     2.4 -(*  Title:      HOL/ex/Code_Antiq.thy
     2.5 -    ID:         $Id$
     2.6 -    Author:     Florian Haftmann
     2.7 -*)
     2.8 -
     2.9 -header {* A simple certificate check as toy example for the code antiquotation *}
    2.10 -
    2.11 -theory Code_Antiq
    2.12 -imports Plain
    2.13 -begin
    2.14 -
    2.15 -lemma div_cert1:
    2.16 -  fixes n m q r :: nat
    2.17 -  assumes "r < m"
    2.18 -    and "0 < m"
    2.19 -    and "n = m * q + r"
    2.20 -  shows "n div m = q"
    2.21 -using assms by (simp add: div_mult_self2 add_commute)
    2.22 -
    2.23 -lemma div_cert2:
    2.24 -  fixes n :: nat
    2.25 -  shows "n div 0 = 0"
    2.26 -by simp
    2.27 -
    2.28 -ML {*
    2.29 -local
    2.30 -
    2.31 -fun code_of_val k = if k <= 0 then @{code "0::nat"}
    2.32 -  else @{code Suc} (code_of_val (k - 1));
    2.33 -
    2.34 -fun val_of_code @{code "0::nat"} = 0
    2.35 -  | val_of_code (@{code Suc} n) = val_of_code n + 1;
    2.36 -
    2.37 -val term_of_code = HOLogic.mk_nat o val_of_code;
    2.38 -
    2.39 -infix 9 &$;
    2.40 -val op &$ = uncurry Thm.capply;
    2.41 -
    2.42 -val simpset = HOL_ss addsimps
    2.43 -  @{thms plus_nat.simps add_0_right add_Suc_right times_nat.simps mult_0_right mult_Suc_right  less_nat_zero_code le_simps(2) less_eq_nat.simps(1) le_simps(3)}
    2.44 -
    2.45 -fun prove prop = Goal.prove_internal [] (@{cterm Trueprop} &$ prop)
    2.46 -  (K (ALLGOALS (Simplifier.simp_tac simpset))); (*FIXME*)
    2.47 -
    2.48 -in
    2.49 -
    2.50 -fun simp_div ctxt ct_n ct_m =
    2.51 -  let
    2.52 -    val m = HOLogic.dest_nat (Thm.term_of ct_m);
    2.53 -  in if m = 0 then Drule.instantiate'[] [SOME ct_n] @{thm div_cert2} else
    2.54 -    let
    2.55 -      val thy = ProofContext.theory_of ctxt;
    2.56 -      val n = HOLogic.dest_nat (Thm.term_of ct_n);
    2.57 -      val c_n = code_of_val n;
    2.58 -      val c_m = code_of_val m;
    2.59 -      val (c_q, c_r) = @{code divmod} c_n c_m;
    2.60 -      val t_q = term_of_code c_q;
    2.61 -      val t_r = term_of_code c_r;
    2.62 -      val ct_q = Thm.cterm_of thy t_q;
    2.63 -      val ct_r = Thm.cterm_of thy t_r;
    2.64 -      val thm_r = prove (@{cterm "op < \<Colon> nat \<Rightarrow> _"} &$ ct_r &$ ct_m);
    2.65 -      val thm_m = prove (@{cterm "(op < \<Colon> nat \<Rightarrow> _) 0"} &$ ct_m);
    2.66 -      val thm_n = prove (@{cterm "(op = \<Colon> nat \<Rightarrow> _)"} &$ ct_n
    2.67 -        &$ (@{cterm "(op + \<Colon> nat \<Rightarrow> _)"}
    2.68 -          &$ (@{cterm "(op * \<Colon> nat \<Rightarrow> _)"} &$ ct_m &$ ct_q) &$ ct_r));
    2.69 -    in @{thm div_cert1} OF [thm_r, thm_m, thm_n] end
    2.70 -  end;
    2.71 -
    2.72 -end;
    2.73 -*}
    2.74 -
    2.75 -ML_val {*
    2.76 -  simp_div @{context}
    2.77 -    @{cterm "Suc (Suc (Suc (Suc (Suc 0))))"}
    2.78 -    @{cterm "(Suc (Suc 0))"}
    2.79 -*}
    2.80 -
    2.81 -ML_val {*
    2.82 -  simp_div @{context}
    2.83 -    (Thm.cterm_of @{theory} (HOLogic.mk_nat 170))
    2.84 -    (Thm.cterm_of @{theory} (HOLogic.mk_nat 42))
    2.85 -*}
    2.86 -
    2.87 -end
    2.88 \ No newline at end of file
     3.1 --- a/src/HOL/ex/ROOT.ML	Fri Mar 27 10:05:12 2009 +0100
     3.2 +++ b/src/HOL/ex/ROOT.ML	Fri Mar 27 10:05:13 2009 +0100
     3.3 @@ -56,7 +56,6 @@
     3.4    "Classical",
     3.5    "set",
     3.6    "Meson_Test",
     3.7 -  "Code_Antiq",
     3.8    "Termination",
     3.9    "Coherent",
    3.10    "PresburgerEx",