author | blanchet |
Wed, 12 Feb 2014 08:35:57 +0100 | |
changeset 55415 | 05f5fdb8d093 |
parent 51113 | 222fb6cb2c3e |
child 55757 | 9fc71814b8c1 |
permissions | -rw-r--r-- |
51113
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
1 |
(* Title: HOL/Library/Code_Abstract_Nat.thy |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
2 |
Author: Stefan Berghofer, Florian Haftmann, TU Muenchen |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
3 |
*) |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
4 |
|
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
5 |
header {* Avoidance of pattern matching on natural numbers *} |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
6 |
|
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
7 |
theory Code_Abstract_Nat |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
8 |
imports Main |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
9 |
begin |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
10 |
|
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
11 |
text {* |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
12 |
When natural numbers are implemented in another than the |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
13 |
conventional inductive @{term "0::nat"}/@{term Suc} representation, |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
14 |
it is necessary to avoid all pattern matching on natural numbers |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
15 |
altogether. This is accomplished by this theory (up to a certain |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
16 |
extent). |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
17 |
*} |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
18 |
|
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
19 |
subsection {* Case analysis *} |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
20 |
|
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
21 |
text {* |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
22 |
Case analysis on natural numbers is rephrased using a conditional |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
23 |
expression: |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
24 |
*} |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
25 |
|
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
26 |
lemma [code, code_unfold]: |
55415 | 27 |
"case_nat = (\<lambda>f g n. if n = 0 then f else g (n - 1))" |
51113
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
28 |
by (auto simp add: fun_eq_iff dest!: gr0_implies_Suc) |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
29 |
|
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
30 |
|
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
31 |
subsection {* Preprocessors *} |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
32 |
|
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
33 |
text {* |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
34 |
The term @{term "Suc n"} is no longer a valid pattern. Therefore, |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
35 |
all occurrences of this term in a position where a pattern is |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
36 |
expected (i.e.~on the left-hand side of a code equation) must be |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
37 |
eliminated. This can be accomplished – as far as possible – by |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
38 |
applying the following transformation rule: |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
39 |
*} |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
40 |
|
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
41 |
lemma Suc_if_eq: "(\<And>n. f (Suc n) \<equiv> h n) \<Longrightarrow> f 0 \<equiv> g \<Longrightarrow> |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
42 |
f n \<equiv> if n = 0 then g else h (n - 1)" |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
43 |
by (rule eq_reflection) (cases n, simp_all) |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
44 |
|
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
45 |
text {* |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
46 |
The rule above is built into a preprocessor that is plugged into |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
47 |
the code generator. |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
48 |
*} |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
49 |
|
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
50 |
setup {* |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
51 |
let |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
52 |
|
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
53 |
fun remove_suc thy thms = |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
54 |
let |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
55 |
val vname = singleton (Name.variant_list (map fst |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
56 |
(fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n"; |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
57 |
val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT)); |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
58 |
fun lhs_of th = snd (Thm.dest_comb |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
59 |
(fst (Thm.dest_comb (cprop_of th)))); |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
60 |
fun rhs_of th = snd (Thm.dest_comb (cprop_of th)); |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
61 |
fun find_vars ct = (case term_of ct of |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
62 |
(Const (@{const_name Suc}, _) $ Var _) => [(cv, snd (Thm.dest_comb ct))] |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
63 |
| _ $ _ => |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
64 |
let val (ct1, ct2) = Thm.dest_comb ct |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
65 |
in |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
66 |
map (apfst (fn ct => Thm.apply ct ct2)) (find_vars ct1) @ |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
67 |
map (apfst (Thm.apply ct1)) (find_vars ct2) |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
68 |
end |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
69 |
| _ => []); |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
70 |
val eqs = maps |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
71 |
(fn th => map (pair th) (find_vars (lhs_of th))) thms; |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
72 |
fun mk_thms (th, (ct, cv')) = |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
73 |
let |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
74 |
val th' = |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
75 |
Thm.implies_elim |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
76 |
(Conv.fconv_rule (Thm.beta_conversion true) |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
77 |
(Drule.instantiate' |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
78 |
[SOME (ctyp_of_term ct)] [SOME (Thm.lambda cv ct), |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
79 |
SOME (Thm.lambda cv' (rhs_of th)), NONE, SOME cv'] |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
80 |
@{thm Suc_if_eq})) (Thm.forall_intr cv' th) |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
81 |
in |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
82 |
case map_filter (fn th'' => |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
83 |
SOME (th'', singleton |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
84 |
(Variable.trade (K (fn [th'''] => [th''' RS th'])) |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
85 |
(Variable.global_thm_context th'')) th'') |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
86 |
handle THM _ => NONE) thms of |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
87 |
[] => NONE |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
88 |
| thps => |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
89 |
let val (ths1, ths2) = split_list thps |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
90 |
in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
91 |
end |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
92 |
in get_first mk_thms eqs end; |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
93 |
|
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
94 |
fun eqn_suc_base_preproc thy thms = |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
95 |
let |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
96 |
val dest = fst o Logic.dest_equals o prop_of; |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
97 |
val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc}); |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
98 |
in |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
99 |
if forall (can dest) thms andalso exists (contains_suc o dest) thms |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
100 |
then thms |> perhaps_loop (remove_suc thy) |> (Option.map o map) Drule.zero_var_indexes |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
101 |
else NONE |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
102 |
end; |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
103 |
|
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
104 |
val eqn_suc_preproc = Code_Preproc.simple_functrans eqn_suc_base_preproc; |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
105 |
|
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
106 |
in |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
107 |
|
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
108 |
Code_Preproc.add_functrans ("eqn_Suc", eqn_suc_preproc) |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
109 |
|
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
110 |
end; |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
111 |
*} |
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
112 |
|
222fb6cb2c3e
factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
haftmann
parents:
diff
changeset
|
113 |
end |