--- a/src/ZF/ex/TF.ML Fri Oct 22 13:44:27 1993 +0100
+++ b/src/ZF/ex/TF.ML Fri Oct 22 17:39:12 1993 +0100
@@ -17,9 +17,9 @@
val rec_styp = "i=>i";
val ext = None
val sintrs =
- ["[| a:A; tf: forest(A) |] ==> Tcons(a,tf) : tree(A)",
+ ["[| a:A; f: forest(A) |] ==> Tcons(a,f) : tree(A)",
"Fnil : forest(A)",
- "[| t: tree(A); tf: forest(A) |] ==> Fcons(t,tf) : forest(A)"];
+ "[| t: tree(A); f: forest(A) |] ==> Fcons(t,f) : forest(A)"];
val monos = [];
val type_intrs = datatype_intrs
val type_elims = datatype_elims);
--- a/src/ZF/ex/TF_Fn.ML Fri Oct 22 13:44:27 1993 +0100
+++ b/src/ZF/ex/TF_Fn.ML Fri Oct 22 17:39:12 1993 +0100
@@ -18,7 +18,7 @@
(** conversion rules **)
-goal TF_Fn.thy "TF_rec(Tcons(a,tf), b, c, d) = b(a, tf, TF_rec(tf,b,c,d))";
+goal TF_Fn.thy "TF_rec(Tcons(a,f), b, c, d) = b(a, f, TF_rec(f,b,c,d))";
by (rtac (TF_rec_def RS def_Vrec RS trans) 1);
by (rewrite_goals_tac TF.con_defs);
by (simp_tac rank_ss 1);
@@ -30,8 +30,8 @@
by (simp_tac rank_ss 1);
val TF_rec_Fnil = result();
-goal TF_Fn.thy "TF_rec(Fcons(t,tf), b, c, d) = \
-\ d(t, tf, TF_rec(t, b, c, d), TF_rec(tf, b, c, d))";
+goal TF_Fn.thy "TF_rec(Fcons(t,f), b, c, d) = \
+\ d(t, f, TF_rec(t, b, c, d), TF_rec(f, b, c, d))";
by (rtac (TF_rec_def RS def_Vrec RS trans) 1);
by (rewrite_goals_tac TF.con_defs);
by (simp_tac rank_ss 1);
@@ -45,11 +45,11 @@
val major::prems = goal TF_Fn.thy
"[| z: tree_forest(A); \
-\ !!x tf r. [| x: A; tf: forest(A); r: C(tf) \
-\ |] ==> b(x,tf,r): C(Tcons(x,tf)); \
+\ !!x f r. [| x: A; f: forest(A); r: C(f) \
+\ |] ==> b(x,f,r): C(Tcons(x,f)); \
\ c : C(Fnil); \
-\ !!t tf r1 r2. [| t: tree(A); tf: forest(A); r1: C(t); r2: C(tf) \
-\ |] ==> d(t,tf,r1,r2): C(Fcons(t,tf)) \
+\ !!t f r1 r2. [| t: tree(A); f: forest(A); r1: C(t); r2: C(f) \
+\ |] ==> d(t,f,r1,r2): C(Fcons(t,f)) \
\ |] ==> TF_rec(z,b,c,d) : C(z)";
by (rtac (major RS TF.induct) 1);
by (ALLGOALS (asm_simp_tac (TF_rec_ss addsimps prems)));
@@ -57,13 +57,13 @@
(*Mutually recursive version*)
val prems = goal TF_Fn.thy
- "[| !!x tf r. [| x: A; tf: forest(A); r: D(tf) \
-\ |] ==> b(x,tf,r): C(Tcons(x,tf)); \
+ "[| !!x f r. [| x: A; f: forest(A); r: D(f) \
+\ |] ==> b(x,f,r): C(Tcons(x,f)); \
\ c : D(Fnil); \
-\ !!t tf r1 r2. [| t: tree(A); tf: forest(A); r1: C(t); r2: D(tf) \
-\ |] ==> d(t,tf,r1,r2): D(Fcons(t,tf)) \
+\ !!t f r1 r2. [| t: tree(A); f: forest(A); r1: C(t); r2: D(f) \
+\ |] ==> d(t,f,r1,r2): D(Fcons(t,f)) \
\ |] ==> (ALL t:tree(A). TF_rec(t,b,c,d) : C(t)) & \
-\ (ALL tf: forest(A). TF_rec(tf,b,c,d) : D(tf))";
+\ (ALL f: forest(A). TF_rec(f,b,c,d) : D(f))";
by (rewtac Ball_def);
by (rtac TF.mutual_induct 1);
by (ALLGOALS (asm_simp_tac (TF_rec_ss addsimps prems)));
@@ -73,7 +73,7 @@
(** Versions for use with definitions **)
val [rew] = goal TF_Fn.thy
- "[| !!z. j(z)==TF_rec(z,b,c,d) |] ==> j(Tcons(a,tf)) = b(a,tf,j(tf))";
+ "[| !!z. j(z)==TF_rec(z,b,c,d) |] ==> j(Tcons(a,f)) = b(a,f,j(f))";
by (rewtac rew);
by (rtac TF_rec_Tcons 1);
val def_TF_rec_Tcons = result();
@@ -85,7 +85,7 @@
val def_TF_rec_Fnil = result();
val [rew] = goal TF_Fn.thy
- "[| !!z. j(z)==TF_rec(z,b,c,d) |] ==> j(Fcons(t,tf)) = d(t,tf,j(t),j(tf))";
+ "[| !!z. j(z)==TF_rec(z,b,c,d) |] ==> j(Fcons(t,f)) = d(t,f,j(t),j(f))";
by (rewtac rew);
by (rtac TF_rec_Fcons 1);
val def_TF_rec_Fcons = result();
@@ -119,7 +119,7 @@
val prems = goalw TF_Fn.thy [TF_map_def]
"[| !!x. x: A ==> h(x): B |] ==> \
\ (ALL t:tree(A). TF_map(h,t) : tree(B)) & \
-\ (ALL tf: forest(A). TF_map(h,tf) : forest(B))";
+\ (ALL f: forest(A). TF_map(h,f) : forest(B))";
by (REPEAT
(ares_tac ([tree_forest_rec_type, TconsI, FnilI, FconsI] @ prems) 1));
val TF_map_type = result();
@@ -170,15 +170,15 @@
(*essentially the same as list induction*)
val major::prems = goal TF_Fn.thy
- "[| tf: forest(A); \
+ "[| f: forest(A); \
\ R(Fnil); \
-\ !!t tf. [| t: tree(A); tf: forest(A); R(tf) |] ==> R(Fcons(t,tf)) \
-\ |] ==> R(tf)";
+\ !!t f. [| t: tree(A); f: forest(A); R(f) |] ==> R(Fcons(t,f)) \
+\ |] ==> R(f)";
by (rtac (major RS (TF.mutual_induct RS conjunct2 RS spec RSN (2,rev_mp))) 1);
by (REPEAT (ares_tac (TrueI::prems) 1));
val forest_induct = result();
-goal TF_Fn.thy "!!tf A. tf: forest(A) ==> TF_of_list(list_of_TF(tf)) = tf";
+goal TF_Fn.thy "!!f A. f: forest(A) ==> TF_of_list(list_of_TF(f)) = f";
by (etac forest_induct 1);
by (ALLGOALS (asm_simp_tac TF_ss));
val forest_iso = result();
--- a/src/ZF/ex/TF_Fn.thy Fri Oct 22 13:44:27 1993 +0100
+++ b/src/ZF/ex/TF_Fn.thy Fri Oct 22 17:39:12 1993 +0100
@@ -18,25 +18,25 @@
rules
TF_rec_def
"TF_rec(z,b,c,d) == Vrec(z, \
-\ %z r. tree_forest_case(%x tf. b(x, tf, r`tf), \
+\ %z r. tree_forest_case(%x f. b(x, f, r`f), \
\ c, \
-\ %t tf. d(t, tf, r`t, r`tf), z))"
+\ %t f. d(t, f, r`t, r`f), z))"
list_of_TF_def
- "list_of_TF(z) == TF_rec(z, %x tf r. [Tcons(x,tf)], [], \
-\ %t tf r1 r2. Cons(t, r2))"
+ "list_of_TF(z) == TF_rec(z, %x f r. [Tcons(x,f)], [], \
+\ %t f r1 r2. Cons(t, r2))"
TF_of_list_def
- "TF_of_list(tf) == list_rec(tf, Fnil, %t tf r. Fcons(t,r))"
+ "TF_of_list(f) == list_rec(f, Fnil, %t f r. Fcons(t,r))"
TF_map_def
- "TF_map(h,z) == TF_rec(z, %x tf r.Tcons(h(x),r), Fnil, \
-\ %t tf r1 r2. Fcons(r1,r2))"
+ "TF_map(h,z) == TF_rec(z, %x f r.Tcons(h(x),r), Fnil, \
+\ %t f r1 r2. Fcons(r1,r2))"
TF_size_def
- "TF_size(z) == TF_rec(z, %x tf r.succ(r), 0, %t tf r1 r2. r1#+r2)"
+ "TF_size(z) == TF_rec(z, %x f r.succ(r), 0, %t f r1 r2. r1#+r2)"
TF_preorder_def
- "TF_preorder(z) == TF_rec(z, %x tf r.Cons(x,r), Nil, %t tf r1 r2. r1@r2)"
+ "TF_preorder(z) == TF_rec(z, %x f r.Cons(x,r), Nil, %t f r1 r2. r1@r2)"
end
--- a/src/ZF/ex/tf.ML Fri Oct 22 13:44:27 1993 +0100
+++ b/src/ZF/ex/tf.ML Fri Oct 22 17:39:12 1993 +0100
@@ -17,9 +17,9 @@
val rec_styp = "i=>i";
val ext = None
val sintrs =
- ["[| a:A; tf: forest(A) |] ==> Tcons(a,tf) : tree(A)",
+ ["[| a:A; f: forest(A) |] ==> Tcons(a,f) : tree(A)",
"Fnil : forest(A)",
- "[| t: tree(A); tf: forest(A) |] ==> Fcons(t,tf) : forest(A)"];
+ "[| t: tree(A); f: forest(A) |] ==> Fcons(t,f) : forest(A)"];
val monos = [];
val type_intrs = datatype_intrs
val type_elims = datatype_elims);
--- a/src/ZF/ex/tf_fn.ML Fri Oct 22 13:44:27 1993 +0100
+++ b/src/ZF/ex/tf_fn.ML Fri Oct 22 17:39:12 1993 +0100
@@ -18,7 +18,7 @@
(** conversion rules **)
-goal TF_Fn.thy "TF_rec(Tcons(a,tf), b, c, d) = b(a, tf, TF_rec(tf,b,c,d))";
+goal TF_Fn.thy "TF_rec(Tcons(a,f), b, c, d) = b(a, f, TF_rec(f,b,c,d))";
by (rtac (TF_rec_def RS def_Vrec RS trans) 1);
by (rewrite_goals_tac TF.con_defs);
by (simp_tac rank_ss 1);
@@ -30,8 +30,8 @@
by (simp_tac rank_ss 1);
val TF_rec_Fnil = result();
-goal TF_Fn.thy "TF_rec(Fcons(t,tf), b, c, d) = \
-\ d(t, tf, TF_rec(t, b, c, d), TF_rec(tf, b, c, d))";
+goal TF_Fn.thy "TF_rec(Fcons(t,f), b, c, d) = \
+\ d(t, f, TF_rec(t, b, c, d), TF_rec(f, b, c, d))";
by (rtac (TF_rec_def RS def_Vrec RS trans) 1);
by (rewrite_goals_tac TF.con_defs);
by (simp_tac rank_ss 1);
@@ -45,11 +45,11 @@
val major::prems = goal TF_Fn.thy
"[| z: tree_forest(A); \
-\ !!x tf r. [| x: A; tf: forest(A); r: C(tf) \
-\ |] ==> b(x,tf,r): C(Tcons(x,tf)); \
+\ !!x f r. [| x: A; f: forest(A); r: C(f) \
+\ |] ==> b(x,f,r): C(Tcons(x,f)); \
\ c : C(Fnil); \
-\ !!t tf r1 r2. [| t: tree(A); tf: forest(A); r1: C(t); r2: C(tf) \
-\ |] ==> d(t,tf,r1,r2): C(Fcons(t,tf)) \
+\ !!t f r1 r2. [| t: tree(A); f: forest(A); r1: C(t); r2: C(f) \
+\ |] ==> d(t,f,r1,r2): C(Fcons(t,f)) \
\ |] ==> TF_rec(z,b,c,d) : C(z)";
by (rtac (major RS TF.induct) 1);
by (ALLGOALS (asm_simp_tac (TF_rec_ss addsimps prems)));
@@ -57,13 +57,13 @@
(*Mutually recursive version*)
val prems = goal TF_Fn.thy
- "[| !!x tf r. [| x: A; tf: forest(A); r: D(tf) \
-\ |] ==> b(x,tf,r): C(Tcons(x,tf)); \
+ "[| !!x f r. [| x: A; f: forest(A); r: D(f) \
+\ |] ==> b(x,f,r): C(Tcons(x,f)); \
\ c : D(Fnil); \
-\ !!t tf r1 r2. [| t: tree(A); tf: forest(A); r1: C(t); r2: D(tf) \
-\ |] ==> d(t,tf,r1,r2): D(Fcons(t,tf)) \
+\ !!t f r1 r2. [| t: tree(A); f: forest(A); r1: C(t); r2: D(f) \
+\ |] ==> d(t,f,r1,r2): D(Fcons(t,f)) \
\ |] ==> (ALL t:tree(A). TF_rec(t,b,c,d) : C(t)) & \
-\ (ALL tf: forest(A). TF_rec(tf,b,c,d) : D(tf))";
+\ (ALL f: forest(A). TF_rec(f,b,c,d) : D(f))";
by (rewtac Ball_def);
by (rtac TF.mutual_induct 1);
by (ALLGOALS (asm_simp_tac (TF_rec_ss addsimps prems)));
@@ -73,7 +73,7 @@
(** Versions for use with definitions **)
val [rew] = goal TF_Fn.thy
- "[| !!z. j(z)==TF_rec(z,b,c,d) |] ==> j(Tcons(a,tf)) = b(a,tf,j(tf))";
+ "[| !!z. j(z)==TF_rec(z,b,c,d) |] ==> j(Tcons(a,f)) = b(a,f,j(f))";
by (rewtac rew);
by (rtac TF_rec_Tcons 1);
val def_TF_rec_Tcons = result();
@@ -85,7 +85,7 @@
val def_TF_rec_Fnil = result();
val [rew] = goal TF_Fn.thy
- "[| !!z. j(z)==TF_rec(z,b,c,d) |] ==> j(Fcons(t,tf)) = d(t,tf,j(t),j(tf))";
+ "[| !!z. j(z)==TF_rec(z,b,c,d) |] ==> j(Fcons(t,f)) = d(t,f,j(t),j(f))";
by (rewtac rew);
by (rtac TF_rec_Fcons 1);
val def_TF_rec_Fcons = result();
@@ -119,7 +119,7 @@
val prems = goalw TF_Fn.thy [TF_map_def]
"[| !!x. x: A ==> h(x): B |] ==> \
\ (ALL t:tree(A). TF_map(h,t) : tree(B)) & \
-\ (ALL tf: forest(A). TF_map(h,tf) : forest(B))";
+\ (ALL f: forest(A). TF_map(h,f) : forest(B))";
by (REPEAT
(ares_tac ([tree_forest_rec_type, TconsI, FnilI, FconsI] @ prems) 1));
val TF_map_type = result();
@@ -170,15 +170,15 @@
(*essentially the same as list induction*)
val major::prems = goal TF_Fn.thy
- "[| tf: forest(A); \
+ "[| f: forest(A); \
\ R(Fnil); \
-\ !!t tf. [| t: tree(A); tf: forest(A); R(tf) |] ==> R(Fcons(t,tf)) \
-\ |] ==> R(tf)";
+\ !!t f. [| t: tree(A); f: forest(A); R(f) |] ==> R(Fcons(t,f)) \
+\ |] ==> R(f)";
by (rtac (major RS (TF.mutual_induct RS conjunct2 RS spec RSN (2,rev_mp))) 1);
by (REPEAT (ares_tac (TrueI::prems) 1));
val forest_induct = result();
-goal TF_Fn.thy "!!tf A. tf: forest(A) ==> TF_of_list(list_of_TF(tf)) = tf";
+goal TF_Fn.thy "!!f A. f: forest(A) ==> TF_of_list(list_of_TF(f)) = f";
by (etac forest_induct 1);
by (ALLGOALS (asm_simp_tac TF_ss));
val forest_iso = result();
--- a/src/ZF/ex/tf_fn.thy Fri Oct 22 13:44:27 1993 +0100
+++ b/src/ZF/ex/tf_fn.thy Fri Oct 22 17:39:12 1993 +0100
@@ -18,25 +18,25 @@
rules
TF_rec_def
"TF_rec(z,b,c,d) == Vrec(z, \
-\ %z r. tree_forest_case(%x tf. b(x, tf, r`tf), \
+\ %z r. tree_forest_case(%x f. b(x, f, r`f), \
\ c, \
-\ %t tf. d(t, tf, r`t, r`tf), z))"
+\ %t f. d(t, f, r`t, r`f), z))"
list_of_TF_def
- "list_of_TF(z) == TF_rec(z, %x tf r. [Tcons(x,tf)], [], \
-\ %t tf r1 r2. Cons(t, r2))"
+ "list_of_TF(z) == TF_rec(z, %x f r. [Tcons(x,f)], [], \
+\ %t f r1 r2. Cons(t, r2))"
TF_of_list_def
- "TF_of_list(tf) == list_rec(tf, Fnil, %t tf r. Fcons(t,r))"
+ "TF_of_list(f) == list_rec(f, Fnil, %t f r. Fcons(t,r))"
TF_map_def
- "TF_map(h,z) == TF_rec(z, %x tf r.Tcons(h(x),r), Fnil, \
-\ %t tf r1 r2. Fcons(r1,r2))"
+ "TF_map(h,z) == TF_rec(z, %x f r.Tcons(h(x),r), Fnil, \
+\ %t f r1 r2. Fcons(r1,r2))"
TF_size_def
- "TF_size(z) == TF_rec(z, %x tf r.succ(r), 0, %t tf r1 r2. r1#+r2)"
+ "TF_size(z) == TF_rec(z, %x f r.succ(r), 0, %t f r1 r2. r1#+r2)"
TF_preorder_def
- "TF_preorder(z) == TF_rec(z, %x tf r.Cons(x,r), Nil, %t tf r1 r2. r1@r2)"
+ "TF_preorder(z) == TF_rec(z, %x f r.Cons(x,r), Nil, %t f r1 r2. r1@r2)"
end