1 (* Title: HOLCF/Dnat2.ML |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 Lemmas for theory Dnat2.thy |
|
7 *) |
|
8 |
|
9 open Dnat2; |
|
10 |
|
11 |
|
12 (* ------------------------------------------------------------------------- *) |
|
13 (* expand fixed point properties *) |
|
14 (* ------------------------------------------------------------------------- *) |
|
15 |
|
16 val iterator_def2 = fix_prover2 Dnat2.thy iterator_def |
|
17 "iterator = (LAM n f x. dnat_when`x`(LAM m.f`(iterator`m`f`x)) `n)"; |
|
18 |
|
19 (* ------------------------------------------------------------------------- *) |
|
20 (* recursive properties *) |
|
21 (* ------------------------------------------------------------------------- *) |
|
22 |
|
23 qed_goal "iterator1" Dnat2.thy "iterator`UU`f`x = UU" |
|
24 (fn prems => |
|
25 [ |
|
26 (stac iterator_def2 1), |
|
27 (simp_tac (!simpset addsimps dnat_when) 1) |
|
28 ]); |
|
29 |
|
30 qed_goal "iterator2" Dnat2.thy "iterator`dzero`f`x = x" |
|
31 (fn prems => |
|
32 [ |
|
33 (stac iterator_def2 1), |
|
34 (simp_tac (!simpset addsimps dnat_when) 1) |
|
35 ]); |
|
36 |
|
37 qed_goal "iterator3" Dnat2.thy |
|
38 "n~=UU ==> iterator`(dsucc`n)`f`x = f`(iterator`n`f`x)" |
|
39 (fn prems => |
|
40 [ |
|
41 (cut_facts_tac prems 1), |
|
42 (rtac trans 1), |
|
43 (stac iterator_def2 1), |
|
44 (asm_simp_tac (!simpset addsimps dnat_rews) 1), |
|
45 (rtac refl 1) |
|
46 ]); |
|
47 |
|
48 val dnat2_rews = |
|
49 [iterator1, iterator2, iterator3]; |
|
50 |
|
51 |
|
52 |
|