|
27436
|
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 |