1461
|
1 |
(* Title: Redex.ML
|
1048
|
2 |
ID: $Id$
|
1461
|
3 |
Author: Ole Rasmussen
|
1048
|
4 |
Copyright 1995 University of Cambridge
|
|
5 |
Logic Image: ZF
|
|
6 |
*)
|
|
7 |
|
|
8 |
open Redex;
|
|
9 |
|
|
10 |
(* ------------------------------------------------------------------------- *)
|
|
11 |
(* redex_rec conversions *)
|
|
12 |
(* ------------------------------------------------------------------------- *)
|
|
13 |
|
|
14 |
goal Redex.thy "redex_rec(Var(n),b,c,d) = b(n)";
|
|
15 |
by (rtac (redex_rec_def RS def_Vrec RS trans) 1);
|
|
16 |
by (simp_tac (rank_ss addsimps redexes.con_defs) 1);
|
|
17 |
val redex_rec_Var = result();
|
|
18 |
|
|
19 |
goal Redex.thy "redex_rec(Fun(t),b,c,d) = c(t,redex_rec(t,b,c,d))";
|
|
20 |
by (rtac (redex_rec_def RS def_Vrec RS trans) 1);
|
|
21 |
by (simp_tac (rank_ss addsimps redexes.con_defs) 1);
|
|
22 |
val redex_rec_Fun = result();
|
|
23 |
|
|
24 |
goal Redex.thy "redex_rec(App(m,f,a),b,c,d) = \
|
|
25 |
\ d(m,f,a,redex_rec(f,b,c,d),redex_rec(a,b,c,d))";
|
|
26 |
by (rtac (redex_rec_def RS def_Vrec RS trans) 1);
|
|
27 |
by (simp_tac (rank_ss addsimps redexes.con_defs) 1);
|
|
28 |
val redex_rec_App = result();
|
|
29 |
|
|
30 |
val redexes_ss = (arith_ss addsimps
|
1461
|
31 |
([redex_rec_App,redex_rec_Fun,redex_rec_Var]@redexes.intrs));
|
1048
|
32 |
|
|
33 |
|
|
34 |
|
|
35 |
|
|
36 |
|