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