src/HOL/ex/Code_Antiq.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 27436 9581777503e9
permissions -rw-r--r--
added lemmas
     1 (*  Title:      HOL/ex/Code_Antiq.thy
     2     ID:         $Id$
     3     Author:     Florian Haftmann
     4 *)
     5 
     6 header {* A simple certificate check as toy example for the code antiquotation *}
     7 
     8 theory Code_Antiq
     9 imports Plain
    10 begin
    11 
    12 lemma div_cert1:
    13   fixes n m q r :: nat
    14   assumes "r < m"
    15     and "0 < m"
    16     and "n = m * q + r"
    17   shows "n div m = q"
    18 using assms by (simp add: div_mult_self2 add_commute)
    19 
    20 lemma div_cert2:
    21   fixes n :: nat
    22   shows "n div 0 = 0"
    23 by simp
    24 
    25 ML {*
    26 local
    27 
    28 fun code_of_val k = if k <= 0 then @{code "0::nat"}
    29   else @{code Suc} (code_of_val (k - 1));
    30 
    31 fun val_of_code @{code "0::nat"} = 0
    32   | val_of_code (@{code Suc} n) = val_of_code n + 1;
    33 
    34 val term_of_code = HOLogic.mk_nat o val_of_code;
    35 
    36 infix 9 &$;
    37 val op &$ = uncurry Thm.capply;
    38 
    39 val simpset = HOL_ss addsimps
    40   @{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)}
    41 
    42 fun prove prop = Goal.prove_internal [] (@{cterm Trueprop} &$ prop)
    43   (K (ALLGOALS (Simplifier.simp_tac simpset))); (*FIXME*)
    44 
    45 in
    46 
    47 fun simp_div ctxt ct_n ct_m =
    48   let
    49     val m = HOLogic.dest_nat (Thm.term_of ct_m);
    50   in if m = 0 then Drule.instantiate'[] [SOME ct_n] @{thm div_cert2} else
    51     let
    52       val thy = ProofContext.theory_of ctxt;
    53       val n = HOLogic.dest_nat (Thm.term_of ct_n);
    54       val c_n = code_of_val n;
    55       val c_m = code_of_val m;
    56       val (c_q, c_r) = @{code divmod} c_n c_m;
    57       val t_q = term_of_code c_q;
    58       val t_r = term_of_code c_r;
    59       val ct_q = Thm.cterm_of thy t_q;
    60       val ct_r = Thm.cterm_of thy t_r;
    61       val thm_r = prove (@{cterm "op < \<Colon> nat \<Rightarrow> _"} &$ ct_r &$ ct_m);
    62       val thm_m = prove (@{cterm "(op < \<Colon> nat \<Rightarrow> _) 0"} &$ ct_m);
    63       val thm_n = prove (@{cterm "(op = \<Colon> nat \<Rightarrow> _)"} &$ ct_n
    64         &$ (@{cterm "(op + \<Colon> nat \<Rightarrow> _)"}
    65           &$ (@{cterm "(op * \<Colon> nat \<Rightarrow> _)"} &$ ct_m &$ ct_q) &$ ct_r));
    66     in @{thm div_cert1} OF [thm_r, thm_m, thm_n] end
    67   end;
    68 
    69 end;
    70 *}
    71 
    72 ML_val {*
    73   simp_div @{context}
    74     @{cterm "Suc (Suc (Suc (Suc (Suc 0))))"}
    75     @{cterm "(Suc (Suc 0))"}
    76 *}
    77 
    78 ML_val {*
    79   simp_div @{context}
    80     (Thm.cterm_of @{theory} (HOLogic.mk_nat 170))
    81     (Thm.cterm_of @{theory} (HOLogic.mk_nat 42))
    82 *}
    83 
    84 end