author | huffman |
Thu, 26 May 2005 02:23:27 +0200 | |
changeset 16081 | 81a4b4a245b0 |
parent 16056 | 32c3b7188c28 |
child 16214 | e3816a7db016 |
permissions | -rw-r--r-- |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
1 |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
2 |
(* legacy ML bindings *) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
3 |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
4 |
val iterate_0 = thm "iterate_0"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
5 |
val iterate_Suc = thm "iterate_Suc"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
6 |
val Ifix_def = thm "Ifix_def"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
7 |
val fix_def = thm "fix_def"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
8 |
val admw_def = thm "admw_def"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
9 |
val iterate_Suc2 = thm "iterate_Suc2"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
10 |
val chain_iterate2 = thm "chain_iterate2"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
11 |
val chain_iterate = thm "chain_iterate"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
12 |
val Ifix_eq = thm "Ifix_eq"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
13 |
val Ifix_least = thm "Ifix_least"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
14 |
val monofun_iterate = thm "monofun_iterate"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
15 |
val contlub_iterate = thm "contlub_iterate"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
16 |
val cont_iterate = thm "cont_iterate"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
17 |
val monofun_iterate2 = thm "monofun_iterate2"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
18 |
val contlub_iterate2 = thm "contlub_iterate2"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
19 |
val cont_iterate2 = thm "cont_iterate2"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
20 |
val monofun_Ifix = thm "monofun_Ifix"; |
16005 | 21 |
(*val chain_iterate_lub = thm "chain_iterate_lub";*) |
22 |
(*val contlub_Ifix_lemma1 = thm "contlub_Ifix_lemma1";*) |
|
23 |
(*val ex_lub_iterate = thm "ex_lub_iterate";*) |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
24 |
val contlub_Ifix = thm "contlub_Ifix"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
25 |
val cont_Ifix = thm "cont_Ifix"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
26 |
val fix_eq = thm "fix_eq"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
27 |
val fix_least = thm "fix_least"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
28 |
val fix_eqI = thm "fix_eqI"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
29 |
val fix_eq2 = thm "fix_eq2"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
30 |
val fix_eq3 = thm "fix_eq3"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
31 |
val fix_eq4 = thm "fix_eq4"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
32 |
val fix_eq5 = thm "fix_eq5"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
33 |
val Ifix_def2 = thm "Ifix_def2"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
34 |
val fix_def2 = thm "fix_def2"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
35 |
val admw_def2 = thm "admw_def2"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
36 |
val def_fix_ind = thm "def_fix_ind"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
37 |
val adm_impl_admw = thm "adm_impl_admw"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
38 |
val fix_ind = thm "fix_ind"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
39 |
val def_fix_ind = thm "def_fix_ind"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
40 |
val wfix_ind = thm "wfix_ind"; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
41 |
val def_wfix_ind = thm "def_wfix_ind"; |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
42 |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
43 |
structure Fix = |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
44 |
struct |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
45 |
val thy = the_context (); |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
46 |
val Ifix_def = Ifix_def; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
47 |
val fix_def = fix_def; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
48 |
val adm_def = adm_def; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
49 |
val admw_def = admw_def; |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
50 |
end; |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
51 |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
52 |
fun fix_tac3 thm i = ((rtac trans i) THEN (rtac (thm RS fix_eq3) i)); |
1274 | 53 |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
54 |
fun fix_tac5 thm i = ((rtac trans i) THEN (rtac (thm RS fix_eq5) i)); |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
55 |
|
10834 | 56 |
(* proves the unfolding theorem for function equations f = fix$... *) |
3652 | 57 |
fun fix_prover thy fixeq s = prove_goal thy s (fn prems => [ |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
58 |
(rtac trans 1), |
3652 | 59 |
(rtac (fixeq RS fix_eq4) 1), |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
60 |
(rtac trans 1), |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
61 |
(rtac beta_cfun 1), |
2566 | 62 |
(Simp_tac 1) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
63 |
]); |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
64 |
|
10834 | 65 |
(* proves the unfolding theorem for function definitions f == fix$... *) |
3652 | 66 |
fun fix_prover2 thy fixdef s = prove_goal thy s (fn prems => [ |
1461 | 67 |
(rtac trans 1), |
68 |
(rtac (fix_eq2) 1), |
|
69 |
(rtac fixdef 1), |
|
70 |
(rtac beta_cfun 1), |
|
2566 | 71 |
(Simp_tac 1) |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
72 |
]); |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
73 |
|
3652 | 74 |
(* proves an application case for a function from its unfolding thm *) |
75 |
fun case_prover thy unfold s = prove_goal thy s (fn prems => [ |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
76 |
(cut_facts_tac prems 1), |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
77 |
(rtac trans 1), |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
78 |
(stac unfold 1), |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
79 |
Auto_tac |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
14981
diff
changeset
|
80 |
]); |