--- a/src/ZF/Coind/ECR.ML Mon Dec 28 16:53:24 1998 +0100
+++ b/src/ZF/Coind/ECR.ML Mon Dec 28 16:54:01 1998 +0100
@@ -45,25 +45,15 @@
(* Properties of the pointwise extension to environments *)
+bind_thm ("HasTyRel_non_zero",
+ HasTyRel.dom_subset RS subsetD RS SigmaD1 RS ValNEE);
+
Goalw [hastyenv_def]
"[| ve:ValEnv; te:TyEnv; hastyenv(ve,te); <v,t>:HasTyRel |] ==> \
\ hastyenv(ve_owr(ve,x,v),te_owr(te,x,t))";
-by Safe_tac;
-by (stac ve_dom_owr 1);
-by (assume_tac 1);
-by (etac (HasTyRel.dom_subset RS subsetD RS SigmaD1 RS ValNEE) 1);
-by (stac te_dom_owr 1);
-by (Asm_simp_tac 1);
-by (rtac (excluded_middle RS disjE) 1);
-by (stac ve_app_owr2 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (stac te_app_owr2 1);
-by (assume_tac 1);
-by (dtac (ve_dom_owr RS subst) 1);
-by (etac (HasTyRel.dom_subset RS subsetD RS SigmaD1 RS ValNEE) 1);
-by ((Fast_tac 1) THEN (Fast_tac 1));
-by (asm_simp_tac (simpset() addsimps [ve_app_owr1,te_app_owr1]) 1);
+by (asm_full_simp_tac
+ (simpset() addsimps [ve_app_owr, HasTyRel_non_zero, ve_dom_owr]) 1);
+by Auto_tac;
qed "hastyenv_owr";
Goalw [isofenv_def,hastyenv_def]
--- a/src/ZF/Coind/MT.ML Mon Dec 28 16:53:24 1998 +0100
+++ b/src/ZF/Coind/MT.ML Mon Dec 28 16:54:01 1998 +0100
@@ -4,9 +4,6 @@
Copyright 1995 University of Cambridge
*)
-open MT;
-
-
(* ############################################################ *)
(* The Consistency theorem *)
(* ############################################################ *)
@@ -28,13 +25,13 @@
"[| ve:ValEnv; x:ExVar; e:Exp; hastyenv(ve,te); \
\ <te,e_fn(x,e),t>:ElabRel \
\ |] ==> <v_clos(x, e, ve), t> : HasTyRel";
-by (Best_tac 1);
+by (Blast_tac 1);
qed "consistency_fn";
AddIs (Ty.intrs@TyEnv.intrs@Val_ValEnv.intrs);
AddDs [te_owrE,(ElabRel.dom_subset RS subsetD)];
-Addsimps [ve_dom_owr, te_dom_owr, ve_app_owr1, ve_app_owr2,
+Addsimps [ve_dom_owr, ve_app_owr1, ve_app_owr2,
te_app_owr1, te_app_owr2];
val clean_tac =
@@ -43,12 +40,11 @@
(match_tac (Ty.intrs@TyEnv.intrs@Val_ValEnv.intrs) i) ORELSE
(ematch_tac [te_owrE] i));
-val prems = goalw MT.thy [hastyenv_def]
+Goalw [hastyenv_def]
"[| ve:ValEnv; x:ExVar; e:Exp; f:ExVar; cl:Val; \
\ v_clos(x,e,ve_owr(ve,f,cl)) = cl; \
\ hastyenv(ve,te); <te,e_fix(f,x,e),t>:ElabRel |] ==> \
\ <cl,t>:HasTyRel";
-by (cut_facts_tac prems 1);
by (etac elab_fixE 1);
by Safe_tac;
by (EVERY [forward_tac [subst] 1,atac 2,rtac htr_closCI 1]);
@@ -82,8 +78,8 @@
qed "consistency_fix";
-val prems = goal MT.thy
- " [| ve:ValEnv; e1:Exp; e2:Exp; c1:Const; c2:Const; \
+Goal
+ "[| ve:ValEnv; e1:Exp; e2:Exp; c1:Const; c2:Const; \
\ <ve,e1,v_const(c1)>:EvalRel; \
\ ALL t te. \
\ hastyenv(ve,te) --> <te,e1,t>:ElabRel --> <v_const(c1),t>:HasTyRel; \
@@ -93,13 +89,12 @@
\ hastyenv(ve, te); \
\ <te,e_app(e1,e2),t>:ElabRel |] ==> \
\ <v_const(c_app(c1, c2)),t>:HasTyRel";
-by (cut_facts_tac prems 1);
by (etac elab_appE 1);
by (fast_tac ((mk_htr_cs ZF_cs) addSIs [c_appI] addIs [isof_app]) 1);
qed "consistency_app1";
-val prems = goal MT.thy
- " [| ve:ValEnv; vem:ValEnv; e1:Exp; e2:Exp; em:Exp; xm:ExVar; v:Val; \
+Goal
+ "[| ve:ValEnv; vem:ValEnv; e1:Exp; e2:Exp; em:Exp; xm:ExVar; v:Val; \
\ <ve,e1,v_clos(xm,em,vem)>:EvalRel; \
\ ALL t te. \
\ hastyenv(ve,te) --> \
@@ -117,7 +112,6 @@
\ <v,t>:HasTyRel; \
\ hastyenv(ve,te); <te,e_app(e1,e2),t>:ElabRel |] ==> \
\ <v,t>:HasTyRel ";
-by (cut_facts_tac prems 1);
by (etac elab_appE 1);
by (dtac (spec RS spec RS mp RS mp) 1);
by (assume_tac 1);
@@ -136,7 +130,7 @@
by (assume_tac 1);
by (assume_tac 1);
by (assume_tac 2);
-by (rewrite_tac [hastyenv_def]);
+by (simp_tac (simpset() addsimps [hastyenv_def]) 1);
by (Fast_tac 1);
qed "consistency_app2";
@@ -155,20 +149,15 @@
qed "consistency";
-val prems = goal MT.thy
+Goal
"[| ve:ValEnv; te:TyEnv; \
\ isofenv(ve,te); \
\ <ve,e,v_const(c)>:EvalRel; \
\ <te,e,t>:ElabRel \
\ |] ==> \
\ isof(c,t)";
-by (cut_facts_tac prems 1);
by (rtac (htr_constE) 1);
by (dtac consistency 1);
by (fast_tac (claset() addSIs [basic_consistency_lem]) 1);
by (assume_tac 1);
qed "basic_consistency";
-
-
-
-
--- a/src/ZF/Coind/Map.ML Mon Dec 28 16:53:24 1998 +0100
+++ b/src/ZF/Coind/Map.ML Mon Dec 28 16:54:01 1998 +0100
@@ -33,6 +33,10 @@
(* Lemmas *)
(* ############################################################ *)
+Goal "Sigma(A,B)``{a} = if (a:A, B(a), 0)";
+by Auto_tac;
+qed "qbeta_if";
+
Goal "a:A ==> Sigma(A,B)``{a} = B(a)";
by (Fast_tac 1);
qed "qbeta";
@@ -190,59 +194,15 @@
(** Application **)
Goalw [map_app_def,map_owr_def]
- "map_app(map_owr(f,a,b),a) = b";
-by (stac qbeta 1);
+ "map_app(map_owr(f,a,b),c) = if (c=a, b, map_app(f,c))";
+by (asm_simp_tac (simpset() addsimps [qbeta_if]) 1);
by (Fast_tac 1);
-by (Simp_tac 1);
+qed "map_app_owr";
+
+Goal "map_app(map_owr(f,a,b),a) = b";
+by (asm_simp_tac (simpset() addsimps [map_app_owr]) 1);
qed "map_app_owr1";
-Goalw [map_app_def,map_owr_def]
- "c ~= a ==> map_app(map_owr(f,a,b),c)= map_app(f,c)";
-by (rtac (excluded_middle RS disjE) 1);
-by (stac qbeta_emp 1);
-by (assume_tac 1);
-by (Fast_tac 1);
-by (etac (qbeta RS ssubst) 1);
-by (Asm_simp_tac 1);
+Goal "c ~= a ==> map_app(map_owr(f,a,b),c)= map_app(f,c)";
+by (asm_simp_tac (simpset() addsimps [map_app_owr]) 1);
qed "map_app_owr2";
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
--- a/src/ZF/Coind/Types.ML Mon Dec 28 16:53:24 1998 +0100
+++ b/src/ZF/Coind/Types.ML Mon Dec 28 16:54:01 1998 +0100
@@ -9,36 +9,12 @@
val te_owrE =
TyEnv.mk_cases TyEnv.con_defs "te_owr(te,f,t):TyEnv";
-Goalw TyEnv.con_defs "rank(te) < rank(te_owr(te,x,t))";
-by (simp_tac rank_ss 1);
-qed "rank_te_owr1";
-
-Goal "te_rec(te_emp,c_te_emp,f_te_owr) = c_te_emp";
-by (rtac (te_rec_def RS def_Vrec RS trans) 1);
-by (simp_tac (simpset() addsimps rank_te_owr1::TyEnv.case_eqns) 1);
-qed "te_rec_emp";
-
-Goal " te_rec(te_owr(te,x,t),c_te_emp,f_te_owr) = \
-\ f_te_owr(te,x,t,te_rec(te,c_te_emp,f_te_owr))";
-by (rtac (te_rec_def RS def_Vrec RS trans) 1);
-by (simp_tac (rank_ss addsimps rank_te_owr1::TyEnv.case_eqns) 1);
-qed "te_rec_owr";
-
-Goalw [te_dom_def] "te_dom(te_emp) = 0";
-by (simp_tac (simpset() addsimps [te_rec_emp]) 1);
-qed "te_dom_emp";
-
-Goalw [te_dom_def] "te_dom(te_owr(te,x,v)) = te_dom(te) Un {x}";
-by (simp_tac (simpset() addsimps [te_rec_owr]) 1);
-qed "te_dom_owr";
-
-Goalw [te_app_def] "te_app(te_owr(te,x,t),x) = t";
-by (simp_tac (simpset() addsimps [te_rec_owr]) 1);
+Goal "te_app(te_owr(te,x,t),x) = t";
+by (Simp_tac 1);
qed "te_app_owr1";
-Goalw [te_app_def]
- "x ~= y ==> te_app(te_owr(te,x,t),y) = te_app(te,y)";
-by (asm_simp_tac (simpset() addsimps [te_rec_owr,(not_sym RS if_not_P)]) 1);
+Goal "x ~= y ==> te_app(te_owr(te,x,t),y) = te_app(te,y)";
+by Auto_tac;
qed "te_app_owr2";
Goal "[| te:TyEnv; x:ExVar; x:te_dom(te) |] ==> te_app(te,x):Ty";
@@ -46,14 +22,9 @@
by (assume_tac 2);
by (assume_tac 2);
by (etac TyEnv.induct 1);
-by (simp_tac (simpset() addsimps [te_dom_emp]) 1);
-by (rtac impI 1);
-by (rtac (excluded_middle RS disjE) 1);
-by (stac te_app_owr2 1);
-by (assume_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [te_dom_owr]) 1);
-by (Fast_tac 1);
-by (asm_simp_tac (simpset() addsimps [te_app_owr1]) 1);
+by (Simp_tac 1);
+by (case_tac "xa = x" 1);
+by Auto_tac;
qed "te_appI";
--- a/src/ZF/Coind/Types.thy Mon Dec 28 16:53:24 1998 +0100
+++ b/src/ZF/Coind/Types.thy Mon Dec 28 16:54:01 1998 +0100
@@ -23,19 +23,17 @@
| te_owr("te:TyEnv","x:ExVar","t:Ty")
consts
- te_rec :: [i,i,[i,i,i,i]=>i] => i
-defs
- te_rec_def
- "te_rec(te,c,h) ==
- Vrec(te,%te g. TyEnv_case(c,%tem x t. h(tem,x,t,g`tem),te))"
-
-consts
te_dom :: i => i
te_app :: [i,i] => i
-defs
- te_dom_def "te_dom(te) == te_rec(te,0,% te x t r. r Un {x})"
- te_app_def "te_app(te,x) == te_rec(te,0, % te y t r. if(x=y,t,r))"
-
+
+
+primrec (*domain of the type environment*)
+ "te_dom (te_emp) = 0"
+ "te_dom(te_owr(te,x,v)) = te_dom(te) Un {x}"
+
+primrec (*lookup up identifiers in the type environment*)
+ "te_app (te_emp,x) = 0"
+ "te_app (te_owr(te,y,t),x) = if(x=y, t, te_app(te,x))"
end
--- a/src/ZF/Coind/Values.ML Mon Dec 28 16:53:24 1998 +0100
+++ b/src/ZF/Coind/Values.ML Mon Dec 28 16:54:01 1998 +0100
@@ -84,48 +84,47 @@
(* Equalities for value environments *)
-val prems = goalw Values.thy [ve_dom_def,ve_owr_def]
- "[| ve:ValEnv; v ~=0 |] ==> ve_dom(ve_owr(ve,x,v)) = ve_dom(ve) Un {x}";
-by (cut_facts_tac prems 1);
+Goal "[| ve:ValEnv; v ~=0 |] ==> ve_dom(ve_owr(ve,x,v)) = ve_dom(ve) Un {x}";
by (etac ValEnvE 1);
-by (asm_full_simp_tac (simpset() addsimps Val_ValEnv.case_eqns) 1);
+by (Asm_full_simp_tac 1);
by (stac map_domain_owr 1);
by (assume_tac 1);
by (rtac Un_commute 1);
qed "ve_dom_owr";
-Goalw [ve_app_def,ve_owr_def]
-"ve:ValEnv ==> ve_app(ve_owr(ve,x,v),x) = v";
+Goal "ve:ValEnv ==> ve_app(ve_owr(ve,y,v),x) = if(x=y, v, ve_app(ve,x))";
by (etac ValEnvE 1);
-by (asm_full_simp_tac (simpset() addsimps Val_ValEnv.case_eqns) 1);
+by (asm_simp_tac (simpset() addsimps [map_app_owr]) 1);
+qed "ve_app_owr";
+
+Goal "ve:ValEnv ==> ve_app(ve_owr(ve,x,v),x) = v";
+by (etac ValEnvE 1);
+by (Asm_full_simp_tac 1);
by (rtac map_app_owr1 1);
qed "ve_app_owr1";
-Goalw [ve_app_def,ve_owr_def]
- "ve:ValEnv ==> x ~= y ==> ve_app(ve_owr(ve,x,v),y) = ve_app(ve,y)";
+Goal "ve:ValEnv ==> x ~= y ==> ve_app(ve_owr(ve,x,v),y) = ve_app(ve,y)";
by (etac ValEnvE 1);
-by (asm_full_simp_tac (simpset() addsimps Val_ValEnv.case_eqns) 1);
+by (Asm_full_simp_tac 1);
by (rtac map_app_owr2 1);
by (Fast_tac 1);
qed "ve_app_owr2";
(* Introduction rules for operators on value environments *)
-Goalw [ve_app_def,ve_owr_def,ve_dom_def]
- "[| ve:ValEnv; x:ve_dom(ve) |] ==> ve_app(ve,x):Val";
+Goal "[| ve:ValEnv; x:ve_dom(ve) |] ==> ve_app(ve,x):Val";
by (etac ValEnvE 1);
by (hyp_subst_tac 1);
-by (asm_full_simp_tac (simpset() addsimps Val_ValEnv.case_eqns) 1);
+by (Asm_full_simp_tac 1);
by (rtac pmap_appI 1);
by (assume_tac 1);
by (assume_tac 1);
qed "ve_appI";
-Goalw [ve_dom_def]
- "[| ve:ValEnv; x:ve_dom(ve) |] ==> x:ExVar";
+Goal "[| ve:ValEnv; x:ve_dom(ve) |] ==> x:ExVar";
by (etac ValEnvE 1);
by (hyp_subst_tac 1);
-by (asm_full_simp_tac (simpset() addsimps Val_ValEnv.case_eqns) 1);
+by (Asm_full_simp_tac 1);
by (rtac pmap_domainD 1);
by (assume_tac 1);
by (assume_tac 1);
@@ -136,10 +135,10 @@
by (rtac pmap_empI 1);
qed "ve_empI";
-Goalw [ve_owr_def] "[|ve:ValEnv; x:ExVar; v:Val |] ==> ve_owr(ve,x,v):ValEnv";
+Goal "[|ve:ValEnv; x:ExVar; v:Val |] ==> ve_owr(ve,x,v):ValEnv";
by (etac ValEnvE 1);
by (hyp_subst_tac 1);
-by (asm_full_simp_tac (simpset() addsimps Val_ValEnv.case_eqns) 1);
+by (Asm_full_simp_tac 1);
by (rtac Val_ValEnv.ve_mk_I 1);
by (etac pmap_owrI 1);
by (assume_tac 1);
--- a/src/ZF/Coind/Values.thy Mon Dec 28 16:53:24 1998 +0100
+++ b/src/ZF/Coind/Values.thy Mon Dec 28 16:54:01 1998 +0100
@@ -19,19 +19,20 @@
type_intrs "[A_into_univ, mapQU]"
consts
- ve_emp :: i
ve_owr :: [i,i,i] => i
ve_dom :: i=>i
ve_app :: [i,i] => i
-defs
- ve_emp_def "ve_emp == ve_mk(map_emp)"
- ve_owr_def
- "ve_owr(ve,x,v) ==
- ve_mk(Val_ValEnv_case(%x.0,%x y z.0,%m. map_owr(m,x,v),ve))"
- ve_dom_def
- "ve_dom(ve) == Val_ValEnv_case(%x.0,%x y z.0,%m. domain(m),ve)"
- ve_app_def
- "ve_app(ve,a) == Val_ValEnv_case(%x.0,%x y z.0,%m. map_app(m,a),ve)"
+
+
+primrec "ve_owr(ve_mk(m), x, v) = ve_mk(map_owr(m,x,v))"
+
+primrec "ve_dom(ve_mk(m)) = domain(m)"
+
+primrec "ve_app(ve_mk(m), a) = map_app(m,a)"
+
+constdefs
+ ve_emp :: i
+ "ve_emp == ve_mk(map_emp)"
end
--- a/src/ZF/Integ/Bin.ML Mon Dec 28 16:53:24 1998 +0100
+++ b/src/ZF/Integ/Bin.ML Mon Dec 28 16:54:01 1998 +0100
@@ -6,7 +6,9 @@
Arithmetic on binary integers.
*)
-Addsimps bin.case_eqns;
+
+Addsimps bin.intrs;
+Addsimps int_typechecks;
(*Perform induction on l, then prove the major premise using prems. *)
fun bin_ind_tac a prems i =
@@ -15,148 +17,91 @@
ares_tac prems i];
-(** bin_rec -- by Vset recursion **)
-
-Goal "bin_rec(Pls,a,b,h) = a";
-by (rtac (bin_rec_def RS def_Vrec RS trans) 1);
-by (rewrite_goals_tac bin.con_defs);
-by (simp_tac rank_ss 1);
-qed "bin_rec_Pls";
-
-Goal "bin_rec(Min,a,b,h) = b";
-by (rtac (bin_rec_def RS def_Vrec RS trans) 1);
-by (rewrite_goals_tac bin.con_defs);
-by (simp_tac rank_ss 1);
-qed "bin_rec_Min";
-
-Goal "bin_rec(Cons(w,x),a,b,h) = h(w, x, bin_rec(w,a,b,h))";
-by (rtac (bin_rec_def RS def_Vrec RS trans) 1);
-by (rewrite_goals_tac bin.con_defs);
-by (simp_tac rank_ss 1);
-qed "bin_rec_Cons";
-
-(*Type checking*)
-val prems = goal Bin.thy
- "[| w: bin; \
-\ a: C(Pls); b: C(Min); \
-\ !!w x r. [| w: bin; x: bool; r: C(w) |] ==> h(w,x,r): C(Cons(w,x)) \
-\ |] ==> bin_rec(w,a,b,h) : C(w)";
-by (bin_ind_tac "w" prems 1);
-by (ALLGOALS
- (asm_simp_tac (simpset() addsimps prems @ [bin_rec_Pls, bin_rec_Min,
- bin_rec_Cons])));
-qed "bin_rec_type";
-
-(** Versions for use with definitions **)
-
-val [rew] = goal Bin.thy
- "[| !!w. j(w)==bin_rec(w,a,b,h) |] ==> j(Pls) = a";
-by (rewtac rew);
-by (rtac bin_rec_Pls 1);
-qed "def_bin_rec_Pls";
-
-val [rew] = goal Bin.thy
- "[| !!w. j(w)==bin_rec(w,a,b,h) |] ==> j(Min) = b";
-by (rewtac rew);
-by (rtac bin_rec_Min 1);
-qed "def_bin_rec_Min";
-
-val [rew] = goal Bin.thy
- "[| !!w. j(w)==bin_rec(w,a,b,h) |] ==> j(Cons(w,x)) = h(w,x,j(w))";
-by (rewtac rew);
-by (rtac bin_rec_Cons 1);
-qed "def_bin_rec_Cons";
-
-fun bin_recs def = map standard
- ([def] RL [def_bin_rec_Pls, def_bin_rec_Min, def_bin_rec_Cons]);
-
-Goalw [NCons_def] "NCons(Pls,0) = Pls";
+Goal "NCons(Pls,0) = Pls";
by (Asm_simp_tac 1);
qed "NCons_Pls_0";
-Goalw [NCons_def] "NCons(Pls,1) = Cons(Pls,1)";
+Goal "NCons(Pls,1) = Cons(Pls,1)";
by (Asm_simp_tac 1);
qed "NCons_Pls_1";
-Goalw [NCons_def] "NCons(Min,0) = Cons(Min,0)";
+Goal "NCons(Min,0) = Cons(Min,0)";
by (Asm_simp_tac 1);
qed "NCons_Min_0";
-Goalw [NCons_def] "NCons(Min,1) = Min";
+Goal "NCons(Min,1) = Min";
by (Asm_simp_tac 1);
qed "NCons_Min_1";
-Goalw [NCons_def]
- "NCons(Cons(w,x),b) = Cons(Cons(w,x),b)";
+Goal "NCons(Cons(w,x),b) = Cons(Cons(w,x),b)";
by (asm_simp_tac (simpset() addsimps bin.case_eqns) 1);
qed "NCons_Cons";
val NCons_simps = [NCons_Pls_0, NCons_Pls_1,
NCons_Min_0, NCons_Min_1,
NCons_Cons];
+Addsimps NCons_simps;
+
(** Type checking **)
-val bin_typechecks0 = bin_rec_type :: bin.intrs;
+Addsimps [bool_into_nat];
-Goalw [integ_of_def] "w: bin ==> integ_of(w) : int";
-by (typechk_tac (bin_typechecks0@int_typechecks@
- nat_typechecks@[bool_into_nat]));
+Goal "w: bin ==> integ_of(w) : int";
+by (bin_ind_tac "w" [] 1);
+by (ALLGOALS (Asm_simp_tac));
qed "integ_of_type";
+Addsimps [integ_of_type];
-Goalw [NCons_def] "[| w: bin; b: bool |] ==> NCons(w,b) : bin";
-by (etac bin.elim 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps bin.case_eqns)));
-by (typechk_tac (bin_typechecks0@bool_typechecks));
+Goal "[| w: bin; b: bool |] ==> NCons(w,b) : bin";
+by (bin_ind_tac "w" [] 1);
+by Auto_tac;
qed "NCons_type";
+Addsimps [NCons_type];
-Goalw [bin_succ_def] "w: bin ==> bin_succ(w) : bin";
-by (typechk_tac ([NCons_type]@bin_typechecks0@bool_typechecks));
+Goal "w: bin ==> bin_succ(w) : bin";
+by (bin_ind_tac "w" [] 1);
+by Auto_tac;
qed "bin_succ_type";
-
-Goalw [bin_pred_def] "w: bin ==> bin_pred(w) : bin";
-by (typechk_tac ([NCons_type]@bin_typechecks0@bool_typechecks));
-qed "bin_pred_type";
+Addsimps [bin_succ_type];
-Goalw [bin_minus_def] "w: bin ==> bin_minus(w) : bin";
-by (typechk_tac ([NCons_type,bin_pred_type]@
- bin_typechecks0@bool_typechecks));
-qed "bin_minus_type";
+Goal "w: bin ==> bin_pred(w) : bin";
+by (bin_ind_tac "w" [] 1);
+by Auto_tac;
+qed "bin_pred_type";
+Addsimps [bin_pred_type];
-Goalw [bin_add_def]
- "[| v: bin; w: bin |] ==> bin_add(v,w) : bin";
-by (typechk_tac ([NCons_type, bin_succ_type, bin_pred_type]@
- bin_typechecks0@ bool_typechecks@ZF_typechecks));
-qed "bin_add_type";
+Goal "w: bin ==> bin_minus(w) : bin";
+by (bin_ind_tac "w" [] 1);
+by Auto_tac;
+qed "bin_minus_type";
+Addsimps [bin_minus_type];
-Goalw [bin_mult_def]
- "[| v: bin; w: bin |] ==> bin_mult(v,w) : bin";
-by (typechk_tac ([NCons_type, bin_minus_type, bin_add_type]@
- bin_typechecks0@ bool_typechecks));
-qed "bin_mult_type";
+(*This proof is complicated by the mutual recursion*)
+Goal "v: bin ==> ALL w: bin. bin_add(v,w) : bin";
+by (bin_ind_tac "v" [] 1);
+by (rtac ballI 3);
+by (bin_ind_tac "w" [] 3);
+by Auto_tac;
+bind_thm ("bin_add_type", result() RS bspec);
+Addsimps [bin_add_type];
-val bin_typechecks = bin_typechecks0 @
- [integ_of_type, NCons_type, bin_succ_type, bin_pred_type,
- bin_minus_type, bin_add_type, bin_mult_type];
+Goal "[| v: bin; w: bin |] ==> bin_mult(v,w) : bin";
+by (bin_ind_tac "v" [] 1);
+by Auto_tac;
+qed "bin_mult_type";
+Addsimps [bin_mult_type];
-Addsimps ([bool_1I, bool_0I,
- bin_rec_Pls, bin_rec_Min, bin_rec_Cons] @
- bin_recs integ_of_def @ bin_typechecks);
-
-val typechecks = bin_typechecks @ int_typechecks @ nat_typechecks @
- [bool_subset_nat RS subsetD];
(**** The carry/borrow functions, bin_succ and bin_pred ****)
-Addsimps (bin_recs bin_succ_def @ bin_recs bin_pred_def);
-
(*NCons preserves the integer value of its argument*)
Goal "[| w: bin; b: bool |] ==> \
\ integ_of(NCons(w,b)) = integ_of(Cons(w,b))";
by (etac bin.elim 1);
-by (asm_simp_tac (simpset() addsimps NCons_simps) 3);
+by (Asm_simp_tac 3);
by (ALLGOALS (etac boolE));
-by (ALLGOALS (asm_simp_tac (simpset() addsimps NCons_simps)));
+by (ALLGOALS Asm_simp_tac);
qed "integ_of_NCons";
Addsimps [integ_of_NCons];
@@ -177,13 +122,11 @@
by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac)));
qed "integ_of_pred";
-(*These two results replace the definitions of bin_succ and bin_pred*)
+Addsimps [integ_of_succ, integ_of_pred];
(*** bin_minus: (unary!) negation of binary integers ***)
-Addsimps (bin_recs bin_minus_def @ [integ_of_succ, integ_of_pred]);
-
Goal "w: bin ==> integ_of(bin_minus(w)) = $~ integ_of(w)";
by (etac bin.induct 1);
by (Simp_tac 1);
@@ -193,29 +136,30 @@
(asm_simp_tac (simpset() addsimps zadd_ac@[zminus_zadd_distrib])));
qed "integ_of_minus";
+Addsimps [integ_of_minus];
+
(*** bin_add: binary addition ***)
-Goalw [bin_add_def] "w: bin ==> bin_add(Pls,w) = w";
+Goal "w: bin ==> bin_add(Pls,w) = w";
by (Asm_simp_tac 1);
qed "bin_add_Pls";
-Goalw [bin_add_def] "w: bin ==> bin_add(Min,w) = bin_pred(w)";
+Goal "w: bin ==> bin_add(Min,w) = bin_pred(w)";
by (Asm_simp_tac 1);
qed "bin_add_Min";
-Goalw [bin_add_def] "bin_add(Cons(v,x),Pls) = Cons(v,x)";
+Goal "bin_add(Cons(v,x),Pls) = Cons(v,x)";
by (Simp_tac 1);
qed "bin_add_Cons_Pls";
-Goalw [bin_add_def] "bin_add(Cons(v,x),Min) = bin_pred(Cons(v,x))";
+Goal "bin_add(Cons(v,x),Min) = bin_pred(Cons(v,x))";
by (Simp_tac 1);
qed "bin_add_Cons_Min";
-Goalw [bin_add_def]
- "[| w: bin; y: bool |] ==> \
-\ bin_add(Cons(v,x), Cons(w,y)) = \
-\ NCons(bin_add(v, cond(x and y, bin_succ(w), w)), x xor y)";
+Goal "[| w: bin; y: bool |] \
+\ ==> bin_add(Cons(v,x), Cons(w,y)) = \
+\ NCons(bin_add(v, cond(x and y, bin_succ(w), w)), x xor y)";
by (Asm_simp_tac 1);
qed "bin_add_Cons_Cons";
@@ -223,48 +167,36 @@
bin_add_Cons_Min, bin_add_Cons_Cons,
integ_of_succ, integ_of_pred];
-Addsimps [bool_subset_nat RS subsetD];
-
Goal "v: bin ==> \
-\ ALL w: bin. integ_of(bin_add(v,w)) = \
-\ integ_of(v) $+ integ_of(w)";
+\ ALL w: bin. integ_of(bin_add(v,w)) = integ_of(v) $+ integ_of(w)";
by (etac bin.induct 1);
by (Simp_tac 1);
by (Simp_tac 1);
by (rtac ballI 1);
by (bin_ind_tac "wa" [] 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac setloop (etac boolE))));
-val integ_of_add_lemma = result();
+bind_thm("integ_of_add", result() RS bspec);
-bind_thm("integ_of_add", integ_of_add_lemma RS bspec);
+Addsimps [integ_of_add];
(*** bin_add: binary multiplication ***)
-Addsimps (bin_recs bin_mult_def @
- [integ_of_minus, integ_of_add]);
-
-val major::prems = goal Bin.thy
- "[| v: bin; w: bin |] ==> \
-\ integ_of(bin_mult(v,w)) = \
-\ integ_of(v) $* integ_of(w)";
-by (cut_facts_tac prems 1);
+Goal "[| v: bin; w: bin |] \
+\ ==> integ_of(bin_mult(v,w)) = integ_of(v) $* integ_of(w)";
by (bin_ind_tac "v" [major] 1);
by (Asm_simp_tac 1);
by (Asm_simp_tac 1);
by (etac boolE 1);
by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib]) 2);
by (asm_simp_tac
- (simpset() addsimps [zadd_zmult_distrib, zmult_1] @ zadd_ac) 1);
+ (simpset() addsimps [zadd_zmult_distrib] @ zadd_ac) 1);
qed "integ_of_mult";
(**** Computations ****)
(** extra rules for bin_succ, bin_pred **)
-val [bin_succ_Pls, bin_succ_Min, _] = bin_recs bin_succ_def;
-val [bin_pred_Pls, bin_pred_Min, _] = bin_recs bin_pred_def;
-
Goal "bin_succ(Cons(w,1)) = Cons(bin_succ(w), 0)";
by (Simp_tac 1);
qed "bin_succ_Cons1";
@@ -283,8 +215,6 @@
(** extra rules for bin_minus **)
-val [bin_minus_Pls, bin_minus_Min, _] = bin_recs bin_minus_def;
-
Goal "bin_minus(Cons(w,1)) = bin_pred(NCons(bin_minus(w), 0))";
by (Simp_tac 1);
qed "bin_minus_Cons1";
@@ -312,8 +242,6 @@
(** extra rules for bin_mult **)
-val [bin_mult_Pls, bin_mult_Min, _] = bin_recs bin_mult_def;
-
Goal "bin_mult(Cons(v,1), w) = bin_add(NCons(bin_mult(v,w),0), w)";
by (Simp_tac 1);
qed "bin_mult_Cons1";
@@ -342,4 +270,4 @@
bin_mult_Pls, bin_mult_Min,
bin_mult_Cons1, bin_mult_Cons0]
@ NCons_simps
- setSolver (type_auto_tac ([bool_1I, bool_0I] @ bin_typechecks0));
+ setSolver (type_auto_tac ([bool_1I, bool_0I] @ bin.intrs));
--- a/src/ZF/Integ/Bin.thy Mon Dec 28 16:53:24 1998 +0100
+++ b/src/ZF/Integ/Bin.thy Mon Dec 28 16:54:01 1998 +0100
@@ -21,13 +21,13 @@
Bin = Int + Datatype +
consts
- bin_rec :: [i, i, i, [i,i,i]=>i] => i
integ_of :: i=>i
NCons :: [i,i]=>i
bin_succ :: i=>i
bin_pred :: i=>i
bin_minus :: i=>i
bin_add :: [i,i]=>i
+ adding :: [i,i,i]=>i
bin_mult :: [i,i]=>i
bin :: i
@@ -42,52 +42,62 @@
type_intrs "[bool_into_univ]"
-defs
-
- bin_rec_def
- "bin_rec(z,a,b,h) ==
- Vrec(z, %z g. bin_case(a, b, %w x. h(w, x, g`w), z))"
-
- integ_of_def
- "integ_of(w) == bin_rec(w, $#0, $~($#1), %w x r. $#x $+ r $+ r)"
+primrec
+ "integ_of (Pls) = $# 0"
+ "integ_of (Min) = $~($#1)"
+ "integ_of (Cons(w,b)) = $#b $+ integ_of(w) $+ integ_of(w)"
(** recall that cond(1,b,c)=b and cond(0,b,c)=0 **)
- (*NCons adds a bit, suppressing leading 0s and 1s*)
- NCons_def
- "NCons(w,b) ==
- bin_case(cond(b,Cons(w,b),w), cond(b,w,Cons(w,b)),
- %w' x'. Cons(w,b), w)"
+primrec (*NCons adds a bit, suppressing leading 0s and 1s*)
+ "NCons (Pls,b) = cond(b,Cons(Pls,b),Pls)"
+ "NCons (Min,b) = cond(b,Min,Cons(Min,b))"
+ "NCons (Cons(w,c),b) = Cons(Cons(w,c),b)"
- bin_succ_def
- "bin_succ(w0) ==
- bin_rec(w0, Cons(Pls,1), Pls,
- %w x r. cond(x, Cons(r,0), NCons(w,1)))"
+primrec (*successor. If a Cons, can change a 0 to a 1 without recursion.*)
+ bin_succ_Pls
+ "bin_succ (Pls) = Cons(Pls,1)"
+ bin_succ_Min
+ "bin_succ (Min) = Pls"
+ "bin_succ (Cons(w,b)) = cond(b, Cons(bin_succ(w), 0),
+ NCons(w,1))"
- bin_pred_def
- "bin_pred(w0) ==
- bin_rec(w0, Min, Cons(Min,0),
- %w x r. cond(x, NCons(w,0), Cons(r,1)))"
+primrec (*predecessor*)
+ bin_pred_Pls
+ "bin_pred (Pls) = Min"
+ bin_pred_Min
+ "bin_pred (Min) = Cons(Min,0)"
+ "bin_pred (Cons(w,b)) = cond(b, NCons(w,0),
+ Cons(bin_pred(w), 1))"
- bin_minus_def
- "bin_minus(w0) ==
- bin_rec(w0, Pls, Cons(Pls,1),
- %w x r. cond(x, bin_pred(NCons(r,0)), Cons(r,0)))"
+primrec (*unary negation*)
+ bin_minus_Pls
+ "bin_minus (Pls) = Pls"
+ bin_minus_Min
+ "bin_minus (Min) = Cons(Pls,1)"
+ "bin_minus (Cons(w,b)) = cond(b, bin_pred(NCons(bin_minus(w),0)),
+ Cons(bin_minus(w),0))"
+
+(*Mutual recursion is not always sound, but it is for primitive recursion.*)
+primrec (*sum*)
+ "bin_add (Pls,w) = w"
+ "bin_add (Min,w) = bin_pred(w)"
+ "bin_add (Cons(v,x),w) = adding(v,x,w)"
- bin_add_def
- "bin_add(v0,w0) ==
- bin_rec(v0,
- lam w:bin. w,
- lam w:bin. bin_pred(w),
- %v x r. lam w1:bin.
- bin_rec(w1, Cons(v,x), bin_pred(Cons(v,x)),
- %w y s. NCons(r`cond(x and y, bin_succ(w), w),
- x xor y))) ` w0"
+primrec (*auxilliary function for sum*)
+ "adding (v,x,Pls) = Cons(v,x)"
+ "adding (v,x,Min) = bin_pred(Cons(v,x))"
+ "adding (v,x,Cons(w,y)) = NCons(bin_add (v, cond(x and y, bin_succ(w), w)),
+ x xor y)"
- bin_mult_def
- "bin_mult(v0,w) ==
- bin_rec(v0, Pls, bin_minus(w),
- %v x r. cond(x, bin_add(NCons(r,0),w), NCons(r,0)))"
+primrec
+ bin_mult_Pls
+ "bin_mult (Pls,w) = Pls"
+ bin_mult_Min
+ "bin_mult (Min,w) = bin_minus(w)"
+ "bin_mult (Cons(v,b),w) = cond(b, bin_add(NCons(bin_mult(v,w),0),w),
+ NCons(bin_mult(v,w),0))"
+
end
--- a/src/ZF/Resid/Cube.ML Mon Dec 28 16:53:24 1998 +0100
+++ b/src/ZF/Resid/Cube.ML Mon Dec 28 16:54:01 1998 +0100
@@ -5,8 +5,6 @@
Logic Image: ZF
*)
-open Cube;
-
Addsimps [commutation, residuals_preserve_comp, sub_preserve_reg,
residuals_preserve_reg, sub_comp, sub_comp RS comp_sym];
--- a/src/ZF/Resid/Redex.ML Mon Dec 28 16:53:24 1998 +0100
+++ b/src/ZF/Resid/Redex.ML Mon Dec 28 16:54:01 1998 +0100
@@ -5,31 +5,109 @@
Logic Image: ZF
*)
-open Redex;
+Addsimps redexes.intrs;
+
+fun rotate n i = EVERY(replicate n (etac revcut_rl i));
+(* ------------------------------------------------------------------------- *)
+(* Specialisation of comp-rules *)
+(* ------------------------------------------------------------------------- *)
+
+val compD1 =Scomp.dom_subset RS subsetD RS SigmaD1;
+val compD2 =Scomp.dom_subset RS subsetD RS SigmaD2;
+
+val regD =Sreg.dom_subset RS subsetD;
(* ------------------------------------------------------------------------- *)
-(* redex_rec conversions *)
+(* Equality rules for union *)
(* ------------------------------------------------------------------------- *)
-Goal "redex_rec(Var(n),b,c,d) = b(n)";
-by (rtac (redex_rec_def RS def_Vrec RS trans) 1);
-by (simp_tac (rank_ss addsimps redexes.con_defs) 1);
-qed "redex_rec_Var";
+Goal "n:nat==>Var(n) un Var(n)=Var(n)";
+by (asm_simp_tac (simpset() addsimps [union_def]) 1);
+qed "union_Var";
+
+Goal "[|u:redexes; v:redexes|]==>Fun(u) un Fun(v)=Fun(u un v)";
+by (asm_simp_tac (simpset() addsimps [union_def]) 1);
+qed "union_Fun";
+
+Goal
+ "[|b1:bool; b2:bool; u1:redexes; v1:redexes; u2:redexes; v2:redexes|]==> \
+\ App(b1,u1,v1) un App(b2,u2,v2)=App(b1 or b2,u1 un u2,v1 un v2)";
+by (asm_simp_tac (simpset() addsimps [union_def]) 1);
+qed "union_App";
-Goal "redex_rec(Fun(t),b,c,d) = c(t,redex_rec(t,b,c,d))";
-by (rtac (redex_rec_def RS def_Vrec RS trans) 1);
-by (simp_tac (rank_ss addsimps redexes.con_defs) 1);
-qed "redex_rec_Fun";
+Addsimps (Ssub.intrs@bool_typechecks@
+ Sreg.intrs@Scomp.intrs@
+ [or_1 RSN (3,or_commute RS trans),
+ or_0 RSN (3,or_commute RS trans),
+ union_App,union_Fun,union_Var,compD2,compD1,regD]);
-Goal "redex_rec(App(m,f,a),b,c,d) = \
-\ d(m,f,a,redex_rec(f,b,c,d),redex_rec(a,b,c,d))";
-by (rtac (redex_rec_def RS def_Vrec RS trans) 1);
-by (simp_tac (rank_ss addsimps redexes.con_defs) 1);
-qed "redex_rec_App";
-
-Addsimps ([redex_rec_App,redex_rec_Fun,redex_rec_Var]@redexes.intrs);
+AddIs Scomp.intrs;
+AddSEs [Sreg.mk_cases redexes.con_defs "regular(App(b,f,a))",
+ Sreg.mk_cases redexes.con_defs "regular(Fun(b))",
+ Sreg.mk_cases redexes.con_defs "regular(Var(b))",
+ Scomp.mk_cases redexes.con_defs "Fun(u) ~ Fun(t)",
+ Scomp.mk_cases redexes.con_defs "u ~ Fun(t)",
+ Scomp.mk_cases redexes.con_defs "u ~ Var(n)",
+ Scomp.mk_cases redexes.con_defs "u ~ App(b,t,a)",
+ Scomp.mk_cases redexes.con_defs "Fun(t) ~ v",
+ Scomp.mk_cases redexes.con_defs "App(b,f,a) ~ v",
+ Scomp.mk_cases redexes.con_defs "Var(n) ~ u"
+ ];
+(* ------------------------------------------------------------------------- *)
+(* comp proofs *)
+(* ------------------------------------------------------------------------- *)
+
+Goal "u:redexes ==> u ~ u";
+by (etac redexes.induct 1);
+by (ALLGOALS Fast_tac);
+qed "comp_refl";
+
+Goal "u ~ v ==> v ~ u";
+by (etac Scomp.induct 1);
+by (ALLGOALS Fast_tac);
+qed "comp_sym";
+
+Goal "u ~ v <-> v ~ u";
+by (fast_tac (claset() addIs [comp_sym]) 1);
+qed "comp_sym_iff";
+Goal "u ~ v ==> ALL w. v ~ w-->u ~ w";
+by (etac Scomp.induct 1);
+by (ALLGOALS Fast_tac);
+qed_spec_mp "comp_trans";
+
+(* ------------------------------------------------------------------------- *)
+(* union proofs *)
+(* ------------------------------------------------------------------------- *)
+
+Goal "u ~ v ==> u <== (u un v)";
+by (etac Scomp.induct 1);
+by (etac boolE 3);
+by (ALLGOALS Asm_simp_tac);
+qed "union_l";
+
+Goal "u ~ v ==> v <== (u un v)";
+by (etac Scomp.induct 1);
+by (eres_inst_tac [("c","b2")] boolE 3);
+by (ALLGOALS Asm_simp_tac);
+qed "union_r";
+
+Goal "u ~ v ==> u un v = v un u";
+by (etac Scomp.induct 1);
+by (ALLGOALS(asm_simp_tac (simpset() addsimps [or_commute])));
+qed "union_sym";
+
+(* ------------------------------------------------------------------------- *)
+(* regular proofs *)
+(* ------------------------------------------------------------------------- *)
+
+Goal "u ~ v ==> regular(u)-->regular(v)-->regular(u un v)";
+by (etac Scomp.induct 1);
+by Auto_tac;
+by (dres_inst_tac [("psi", "regular(Fun(?u) un ?v)")] asm_rl 1);
+by (Asm_full_simp_tac 1);
+qed_spec_mp "union_preserve_regular";
--- a/src/ZF/Resid/Redex.thy Mon Dec 28 16:53:24 1998 +0100
+++ b/src/ZF/Resid/Redex.thy Mon Dec 28 16:54:01 1998 +0100
@@ -16,13 +16,67 @@
type_intrs "[bool_into_univ]"
+
consts
- redex_rec :: [i, i=>i, [i,i]=>i, [i,i,i,i,i]=>i]=>i
-
+ Ssub,Scomp,Sreg :: i
+ "<==","~" :: [i,i]=>o (infixl 70)
+ un :: [i,i]=>i (infixl 70)
+ union_aux :: i=>i
+ regular :: i=>o
+
+primrec (*explicit lambda is required because both arguments of "un" vary*)
+ "union_aux(Var(n)) =
+ (lam t:redexes. redexes_case(%j. Var(n), %x. 0, %b x y.0, t))"
+
+ "union_aux(Fun(u)) =
+ (lam t:redexes. redexes_case(%j. 0, %y. Fun(u un y),
+ %b y z. 0, t))"
+
+ "union_aux(App(b,f,a)) =
+ (lam t:redexes.
+ redexes_case(%j. 0, %y. 0,
+ %c z u. App(b or c, f un z, a un u), t))"
+
defs
- redex_rec_def
- "redex_rec(p,b,c,d) ==
- Vrec(p, %p g. redexes_case(b, %x. c(x,g`x),
- %n x y. d(n, x, y, g`x, g`y), p))"
+ union_def "u un v == union_aux(u)`v"
+
+
+translations
+ "a<==b" == "<a,b>:Ssub"
+ "a ~ b" == "<a,b>:Scomp"
+ "regular(a)" == "a:Sreg"
+
+inductive
+ domains "Ssub" <= "redexes*redexes"
+ intrs
+ Sub_Var "n:nat ==> Var(n)<== Var(n)"
+ Sub_Fun "[|u<== v|]==> Fun(u)<== Fun(v)"
+ Sub_App1 "[|u1<== v1; u2<== v2; b:bool|]==>
+ App(0,u1,u2)<== App(b,v1,v2)"
+ Sub_App2 "[|u1<== v1; u2<== v2|]==>
+ App(1,u1,u2)<== App(1,v1,v2)"
+ type_intrs "redexes.intrs@bool_typechecks"
+
+inductive
+ domains "Scomp" <= "redexes*redexes"
+ intrs
+ Comp_Var "n:nat ==> Var(n) ~ Var(n)"
+ Comp_Fun "[|u ~ v|]==> Fun(u) ~ Fun(v)"
+ Comp_App "[|u1 ~ v1; u2 ~ v2; b1:bool; b2:bool|]==>
+ App(b1,u1,u2) ~ App(b2,v1,v2)"
+ type_intrs "redexes.intrs@bool_typechecks"
+
+inductive
+ domains "Sreg" <= "redexes"
+ intrs
+ Reg_Var "n:nat ==> regular(Var(n))"
+ Reg_Fun "[|regular(u)|]==> regular(Fun(u))"
+ Reg_App1 "[|regular(Fun(u)); regular(v)
+ |]==>regular(App(1,Fun(u),v))"
+ Reg_App2 "[|regular(u); regular(v)
+ |]==>regular(App(0,u,v))"
+ type_intrs "redexes.intrs@bool_typechecks"
+
+
end
--- a/src/ZF/Resid/Residuals.ML Mon Dec 28 16:53:24 1998 +0100
+++ b/src/ZF/Resid/Residuals.ML Mon Dec 28 16:54:01 1998 +0100
@@ -50,43 +50,38 @@
by (ALLGOALS Fast_tac);
qed "residuals_intro";
-val prems =
-Goal "[| u~v; residuals(u,v,THE w. residuals(u, v, w))==> R; \
-\ regular(v) |] ==> R";
-by (cut_facts_tac prems 1);
-by (resolve_tac prems 1);
+Goal "[| u~v; regular(v) |] ==> residuals(u,v,THE w. residuals(u, v, w))";
by (resolve_tac [residuals_intro RS mp RS exE] 1);
by (stac the_equality 3);
by (ALLGOALS (blast_tac (claset() addIs [residuals_function])));
-qed "comp_resfuncE";
+qed "comp_resfuncD";
(* ------------------------------------------------------------------------- *)
(* Residual function *)
(* ------------------------------------------------------------------------- *)
-Goalw [res_func_def]
- "n:nat ==> Var(n) |> Var(n) = Var(n)";
+Goalw [res_func_def] "n:nat ==> Var(n) |> Var(n) = Var(n)";
by (Blast_tac 1);
qed "res_Var";
Goalw [res_func_def]
"[|s~t; regular(t)|]==> Fun(s) |> Fun(t) = Fun(s |> t)";
-by (blast_tac (claset() addSEs [comp_resfuncE]
+by (blast_tac (claset() addSDs [comp_resfuncD]
addIs [residuals_function]) 1);
qed "res_Fun";
Goalw [res_func_def]
"[|s~u; regular(u); t~v; regular(v); b:bool|]==> \
\ App(b,s,t) |> App(0,u,v) = App(b, s |> u, t |> v)";
-by (blast_tac (claset() addSEs [comp_resfuncE]
+by (blast_tac (claset() addSDs [comp_resfuncD]
addIs [residuals_function]) 1);
qed "res_App";
Goalw [res_func_def]
"[|s~u; regular(u); t~v; regular(v); b:bool|]==> \
\ App(b,Fun(s),t) |> App(1,Fun(u),v) = (t |> v)/ (s |> u)";
-by (blast_tac (claset() addSEs [comp_resfuncE]
+by (blast_tac (claset() addSDs [comp_resfuncD]
addIs [residuals_function]) 1);
qed "res_redex";
@@ -99,10 +94,11 @@
simpset() addsimps [res_Fun]));
qed "resfunc_type";
-Addsimps ([res_Var, res_Fun, res_App, res_redex, lift_rec_preserve_comp,
+Addsimps [res_Var, res_Fun, res_App, res_redex, lift_rec_preserve_comp,
lift_rec_preserve_reg, subst_rec_preserve_comp, resfunc_type,
- subst_rec_preserve_reg] @
- redexes.free_iffs);
+ subst_rec_preserve_reg];
+
+Addsimps redexes.free_iffs;
(* ------------------------------------------------------------------------- *)
@@ -124,7 +120,7 @@
by (etac Scomp.induct 1);
by Safe_tac;
by (ALLGOALS
- (asm_simp_tac
+ (asm_full_simp_tac
(simpset() addsimps [lift_rec_Var,subst_Var,lift_subst])));
by (rotate_tac ~2 1);
by (Asm_full_simp_tac 1);
--- a/src/ZF/Resid/SubUnion.ML Mon Dec 28 16:53:24 1998 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,118 +0,0 @@
-(* Title: SubUnion.ML
- ID: $Id$
- Author: Ole Rasmussen
- Copyright 1995 University of Cambridge
- Logic Image: ZF
-*)
-
-open SubUnion;
-
-fun rotate n i = EVERY(replicate n (etac revcut_rl i));
-(* ------------------------------------------------------------------------- *)
-(* Specialisation of comp-rules *)
-(* ------------------------------------------------------------------------- *)
-
-val compD1 =Scomp.dom_subset RS subsetD RS SigmaD1;
-val compD2 =Scomp.dom_subset RS subsetD RS SigmaD2;
-
-val regD =Sreg.dom_subset RS subsetD;
-
-(* ------------------------------------------------------------------------- *)
-(* Equality rules for union *)
-(* ------------------------------------------------------------------------- *)
-
-Goalw [union_def]
- "n:nat==>Var(n) un Var(n)=Var(n)";
-by (Asm_simp_tac 1);
-by (simp_tac (rank_ss addsimps redexes.con_defs) 1);
-qed "union_Var";
-
-Goalw [union_def]
- "[|u:redexes; v:redexes|]==>Fun(u) un Fun(v)=Fun(u un v)";
-by (Asm_simp_tac 1);
-by (simp_tac (rank_ss addsimps redexes.con_defs) 1);
-qed "union_Fun";
-
-Goalw [union_def]
- "[|b1:bool; b2:bool; u1:redexes; v1:redexes; u2:redexes; v2:redexes|]==> \
-\ App(b1,u1,v1) un App(b2,u2,v2)=App(b1 or b2,u1 un u2,v1 un v2)";
-by (Asm_simp_tac 1);
-by (simp_tac (rank_ss addsimps redexes.con_defs) 1);
-qed "union_App";
-
-Addsimps (Ssub.intrs@bool_typechecks@
- Sreg.intrs@Scomp.intrs@
- [or_1 RSN (3,or_commute RS trans),
- or_0 RSN (3,or_commute RS trans),
- union_App,union_Fun,union_Var,compD2,compD1,regD]);
-
-AddIs Scomp.intrs;
-AddSEs [Sreg.mk_cases redexes.con_defs "regular(App(b,f,a))",
- Sreg.mk_cases redexes.con_defs "regular(Fun(b))",
- Sreg.mk_cases redexes.con_defs "regular(Var(b))",
- Scomp.mk_cases redexes.con_defs "Fun(u) ~ Fun(t)",
- Scomp.mk_cases redexes.con_defs "u ~ Fun(t)",
- Scomp.mk_cases redexes.con_defs "u ~ Var(n)",
- Scomp.mk_cases redexes.con_defs "u ~ App(b,t,a)",
- Scomp.mk_cases redexes.con_defs "Fun(t) ~ v",
- Scomp.mk_cases redexes.con_defs "App(b,f,a) ~ v",
- Scomp.mk_cases redexes.con_defs "Var(n) ~ u"
- ];
-
-
-
-(* ------------------------------------------------------------------------- *)
-(* comp proofs *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "u:redexes ==> u ~ u";
-by (etac redexes.induct 1);
-by (ALLGOALS Fast_tac);
-qed "comp_refl";
-
-Goal "u ~ v ==> v ~ u";
-by (etac Scomp.induct 1);
-by (ALLGOALS Fast_tac);
-qed "comp_sym";
-
-Goal "u ~ v <-> v ~ u";
-by (fast_tac (claset() addIs [comp_sym]) 1);
-qed "comp_sym_iff";
-
-
-Goal "u ~ v ==> ALL w. v ~ w-->u ~ w";
-by (etac Scomp.induct 1);
-by (ALLGOALS Fast_tac);
-qed_spec_mp "comp_trans";
-
-(* ------------------------------------------------------------------------- *)
-(* union proofs *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "u ~ v ==> u <== (u un v)";
-by (etac Scomp.induct 1);
-by (etac boolE 3);
-by (ALLGOALS Asm_simp_tac);
-qed "union_l";
-
-Goal "u ~ v ==> v <== (u un v)";
-by (etac Scomp.induct 1);
-by (eres_inst_tac [("c","b2")] boolE 3);
-by (ALLGOALS Asm_simp_tac);
-qed "union_r";
-
-Goal "u ~ v ==> u un v = v un u";
-by (etac Scomp.induct 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps [or_commute])));
-qed "union_sym";
-
-(* ------------------------------------------------------------------------- *)
-(* regular proofs *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "u ~ v ==> regular(u)-->regular(v)-->regular(u un v)";
-by (etac Scomp.induct 1);
-by Auto_tac;
-by (dres_inst_tac [("psi", "regular(Fun(?u) un ?v)")] asm_rl 1);
-by (Asm_full_simp_tac 1);
-qed_spec_mp "union_preserve_regular";
--- a/src/ZF/Resid/SubUnion.thy Mon Dec 28 16:53:24 1998 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,58 +0,0 @@
-(* Title: SubUnion.thy
- ID: $Id$
- Author: Ole Rasmussen
- Copyright 1995 University of Cambridge
- Logic Image: ZF
-*)
-
-SubUnion = Redex +
-
-consts
- Ssub,Scomp,Sreg :: i
- "<==","~" :: [i,i]=>o (infixl 70)
- un :: [i,i]=>i (infixl 70)
- regular :: i=>o
-
-translations
- "a<==b" == "<a,b>:Ssub"
- "a ~ b" == "<a,b>:Scomp"
- "regular(a)" == "a:Sreg"
-
-inductive
- domains "Ssub" <= "redexes*redexes"
- intrs
- Sub_Var "n:nat ==> Var(n)<== Var(n)"
- Sub_Fun "[|u<== v|]==> Fun(u)<== Fun(v)"
- Sub_App1 "[|u1<== v1; u2<== v2; b:bool|]==>
- App(0,u1,u2)<== App(b,v1,v2)"
- Sub_App2 "[|u1<== v1; u2<== v2|]==>
- App(1,u1,u2)<== App(1,v1,v2)"
- type_intrs "redexes.intrs@bool_typechecks"
-
-inductive
- domains "Scomp" <= "redexes*redexes"
- intrs
- Comp_Var "n:nat ==> Var(n) ~ Var(n)"
- Comp_Fun "[|u ~ v|]==> Fun(u) ~ Fun(v)"
- Comp_App "[|u1 ~ v1; u2 ~ v2; b1:bool; b2:bool|]==>
- App(b1,u1,u2) ~ App(b2,v1,v2)"
- type_intrs "redexes.intrs@bool_typechecks"
-
-inductive
- domains "Sreg" <= "redexes"
- intrs
- Reg_Var "n:nat ==> regular(Var(n))"
- Reg_Fun "[|regular(u)|]==> regular(Fun(u))"
- Reg_App1 "[|regular(Fun(u)); regular(v)
- |]==>regular(App(1,Fun(u),v))"
- Reg_App2 "[|regular(u); regular(v)
- |]==>regular(App(0,u,v))"
- type_intrs "redexes.intrs@bool_typechecks"
-
-defs
- union_def "u un v == redex_rec(u,
- %i. lam t:redexes. redexes_case(%j. Var(i), %x.0, %b x y.0, t),
- %x m. lam t:redexes. redexes_case(%j.0, %y. Fun(m`y), %b y z.0, t),
-%b x y m p. lam t:redexes. redexes_case(%j.0, %y.0,
- %c z u. App(b or c, m`z, p`u), t))`v"
-end
--- a/src/ZF/Resid/Substitution.ML Mon Dec 28 16:53:24 1998 +0100
+++ b/src/ZF/Resid/Substitution.ML Mon Dec 28 16:54:01 1998 +0100
@@ -5,8 +5,6 @@
Logic Image: ZF
*)
-open Substitution;
-
(* ------------------------------------------------------------------------- *)
(* Arithmetic extensions *)
(* ------------------------------------------------------------------------- *)
@@ -42,88 +40,78 @@
(* ------------------------------------------------------------------------- *)
(* lift_rec equality rules *)
(* ------------------------------------------------------------------------- *)
-Goalw [lift_rec_def]
- "[|n:nat; i:nat|]==> lift_rec(Var(i),n) =if(i<n,Var(i),Var(succ(i)))";
-by (Asm_simp_tac 1);
+Goal "[|n:nat; i:nat|]==> lift_rec(Var(i),n) =if(i<n,Var(i),Var(succ(i)))";
+by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
qed "lift_rec_Var";
-Goalw [lift_rec_def]
- "[|n:nat; i:nat; k:nat; k le i|]==> lift_rec(Var(i),k) = Var(succ(i))";
-by (Asm_simp_tac 1);
+Goal "[|n:nat; i:nat; k:nat; k le i|]==> lift_rec(Var(i),k) = Var(succ(i))";
+by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
qed "lift_rec_le";
-Goalw [lift_rec_def]
- "[|i:nat; k:nat; i<k |]==> lift_rec(Var(i),k) = Var(i)";
-by (Asm_simp_tac 1);
+Goal "[|i:nat; k:nat; i<k |]==> lift_rec(Var(i),k) = Var(i)";
+by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
qed "lift_rec_gt";
-Goalw [lift_rec_def]
- "[|n:nat; k:nat|]==> \
+Goal "[|n:nat; k:nat|]==> \
\ lift_rec(Fun(t),k) = Fun(lift_rec(t,succ(k)))";
-by (Asm_simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
qed "lift_rec_Fun";
-Goalw [lift_rec_def]
- "[|n:nat; k:nat|]==> \
+Goal "[|n:nat; k:nat|]==> \
\ lift_rec(App(b,f,a),k) = App(b,lift_rec(f,k),lift_rec(a,k))";
-by (Asm_simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
qed "lift_rec_App";
+
(* ------------------------------------------------------------------------- *)
(* substitution quality rules *)
(* ------------------------------------------------------------------------- *)
-Goalw [subst_rec_def]
- "[|i:nat; k:nat; u:redexes|]==> \
-\ subst_rec(u,Var(i),k) = if(k<i,Var(i #- 1),if(k=i,u,Var(i)))";
-by (asm_simp_tac (simpset() addsimps [gt_not_eq,leI]) 1);
+Goal "[|i:nat; k:nat; u:redexes|]==> \
+\ subst_rec(u,Var(i),k) = if(k<i,Var(i #- 1),if(k=i,u,Var(i)))";
+by (asm_simp_tac (simpset() addsimps [subst_rec_def, gt_not_eq, leI]) 1);
qed "subst_Var";
-Goalw [subst_rec_def]
- "[|n:nat; u:redexes|]==> subst_rec(u,Var(n),n) = u";
-by (Asm_simp_tac 1);
+Goal "[|n:nat; u:redexes|]==> subst_rec(u,Var(n),n) = u";
+by (asm_simp_tac (simpset() addsimps [subst_rec_def]) 1);
qed "subst_eq";
-Goalw [subst_rec_def]
- "[|n:nat; u:redexes; p:nat; p<n|]==> \
-\ subst_rec(u,Var(n),p) = Var(n #- 1)";
-by (Asm_simp_tac 1);
+Goal "[|n:nat; u:redexes; p:nat; p<n|]==> \
+\ subst_rec(u,Var(n),p) = Var(n #- 1)";
+by (asm_simp_tac (simpset() addsimps [subst_rec_def]) 1);
qed "subst_gt";
-Goalw [subst_rec_def]
- "[|n:nat; u:redexes; p:nat; n<p|]==> \
-\ subst_rec(u,Var(n),p) = Var(n)";
-by (asm_simp_tac (simpset() addsimps [gt_not_eq,leI]) 1);
+Goal "[|n:nat; u:redexes; p:nat; n<p|]==> \
+\ subst_rec(u,Var(n),p) = Var(n)";
+by (asm_simp_tac (simpset() addsimps [subst_rec_def, gt_not_eq, leI]) 1);
qed "subst_lt";
-Goalw [subst_rec_def]
- "[|p:nat; u:redexes|]==> \
-\ subst_rec(u,Fun(t),p) = Fun(subst_rec(lift(u),t,succ(p))) ";
-by (Asm_simp_tac 1);
+Goal "[|p:nat; u:redexes|]==> \
+\ subst_rec(u,Fun(t),p) = Fun(subst_rec(lift(u),t,succ(p))) ";
+by (asm_simp_tac (simpset() addsimps [subst_rec_def]) 1);
qed "subst_Fun";
-Goalw [subst_rec_def]
- "[|p:nat; u:redexes|]==> \
-\ subst_rec(u,App(b,f,a),p) = App(b,subst_rec(u,f,p),subst_rec(u,a,p))";
-by (Asm_simp_tac 1);
+Goal "[|p:nat; u:redexes|]==> \
+\ subst_rec(u,App(b,f,a),p) = App(b,subst_rec(u,f,p),subst_rec(u,a,p))";
+by (asm_simp_tac (simpset() addsimps [subst_rec_def]) 1);
qed "subst_App";
+(*But not lift_rec_Var, subst_Var: too many case splits*)
Addsimps [subst_Fun, subst_App];
+
Goal "u:redexes ==> ALL k:nat. lift_rec(u,k):redexes";
by (etac redexes.induct 1);
by (ALLGOALS
(asm_simp_tac (simpset() addsimps [lift_rec_Var,
- lift_rec_Fun, lift_rec_App])));
-qed "lift_rec_type_a";
-val lift_rec_type = lift_rec_type_a RS bspec;
+ lift_rec_Fun, lift_rec_App])));
+bind_thm ("lift_rec_type", result() RS bspec);
Goal "v:redexes ==> ALL n:nat. ALL u:redexes. subst_rec(u,v,n):redexes";
by (etac redexes.induct 1);
by (ALLGOALS(asm_simp_tac
(simpset() addsimps [subst_Var, lift_rec_type])));
-qed "subst_type_a";
-val subst_type = subst_type_a RS bspec RS bspec;
+bind_thm ("subst_type", result() RS bspec RS bspec);
Addsimps [subst_eq, subst_gt, subst_lt, subst_type,
@@ -137,14 +125,14 @@
Goal "u:redexes ==> ALL n:nat. ALL i:nat. i le n --> \
\ (lift_rec(lift_rec(u,i),succ(n)) = lift_rec(lift_rec(u,n),i))";
-by ((etac redexes.induct 1) THEN (ALLGOALS Asm_simp_tac));
+by (etac redexes.induct 1);
+by (ALLGOALS Asm_simp_tac);
by Safe_tac;
by (case_tac "n < xa" 1);
by ((forward_tac [lt_trans2] 1) THEN (assume_tac 1));
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [lift_rec_Var, leI])));
qed "lift_lift_rec";
-
Goal "[|u:redexes; n:nat|]==> \
\ lift_rec(lift(u),succ(n)) = lift(lift_rec(u,n))";
by (asm_simp_tac (simpset() addsimps [lift_lift_rec]) 1);
--- a/src/ZF/Resid/Substitution.thy Mon Dec 28 16:53:24 1998 +0100
+++ b/src/ZF/Resid/Substitution.thy Mon Dec 28 16:54:01 1998 +0100
@@ -5,41 +5,55 @@
Logic Image: ZF
*)
-Substitution = SubUnion +
+Substitution = Redex +
consts
+ lift_aux :: i=> i
+ lift :: i=> i
+ subst_aux :: i=> i
+ "'/" :: [i,i]=>i (infixl 70) (*subst*)
+
+constdefs
lift_rec :: [i,i]=> i
- lift :: i=>i
+ "lift_rec(r,k) == lift_aux(r)`k"
+
subst_rec :: [i,i,i]=> i
- "'/" :: [i,i]=>i (infixl 70) (*subst*)
+ "subst_rec(u,r,k) == subst_aux(r)`u`k"
+
translations
"lift(r)" == "lift_rec(r,0)"
- "u/v" == "subst_rec(u,v,0)"
+ "u/v" == "subst_rec(u,v,0)"
-defs
- lift_rec_def "lift_rec(r,kg) ==
- redex_rec(r,%i.(lam k:nat. if(i<k,Var(i),Var(succ(i)))),
- %x m.(lam k:nat. Fun(m`(succ(k)))),
- %b x y m p. lam k:nat. App(b,m`k,p`k))`kg"
+
+(** The clumsy _aux functions are required because other arguments vary
+ in the recursive calls ***)
+
+primrec
+ "lift_aux(Var(i)) = (lam k:nat. if(i<k, Var(i), Var(succ(i))))"
+
+ "lift_aux(Fun(t)) = (lam k:nat. Fun(lift_aux(t) ` succ(k)))"
+
+ "lift_aux(App(b,f,a)) = (lam k:nat. App(b, lift_aux(f)`k, lift_aux(a)`k))"
+
-(* subst_rec(u,Var(i),k) = if k<i then Var(i-1)
+primrec
+(* subst_aux(u,Var(i),k) = if k<i then Var(i-1)
else if k=i then u
else Var(i)
- subst_rec(u,Fun(t),k) = Fun(subst_rec(lift(u),t,succ(k)))
- subst_rec(u,App(b,f,a),k) = App(b,subst_rec(u,f,p),subst_rec(u,a,p))
+ subst_aux(u,Fun(t),k) = Fun(subst_aux(lift(u),t,succ(k)))
+ subst_aux(u,App(b,f,a),k) = App(b,subst_aux(u,f,p),subst_aux(u,a,p))
*)
- subst_rec_def "subst_rec(u,t,kg) ==
- redex_rec(t,
- %i.(lam r:redexes. lam k:nat.
- if(k<i,Var(i #- 1),
- if(k=i,r,Var(i)))),
- %x m.(lam r:redexes. lam k:nat.
- Fun(m`(lift(r))`(succ(k)))),
- %b x y m p. lam r:redexes. lam k:nat.
- App(b,m`r`k,p`r`k))`u`kg"
+ "subst_aux(Var(i)) =
+ (lam r:redexes. lam k:nat. if(k<i, Var(i #- 1),
+ if(k=i, r, Var(i))))"
+ "subst_aux(Fun(t)) =
+ (lam r:redexes. lam k:nat. Fun(subst_rec(lift(r), t, succ(k))))"
+
+ "subst_aux(App(b,f,a)) =
+ (lam r:redexes. lam k:nat. App(b, subst_rec(r,f,k), subst_rec(r,a,k)))"
end
--- a/src/ZF/Resid/Terms.ML Mon Dec 28 16:53:24 1998 +0100
+++ b/src/ZF/Resid/Terms.ML Mon Dec 28 16:54:01 1998 +0100
@@ -5,41 +5,14 @@
Logic Image: ZF
*)
-open Terms;
-
-(* ------------------------------------------------------------------------- *)
-(* unmark simplifications *)
-(* ------------------------------------------------------------------------- *)
-
-Goalw [unmark_def] "unmark(Var(n)) = Var(n)";
-by (Asm_simp_tac 1);
-qed "unmark_Var";
-
-Goalw [unmark_def] "unmark(Fun(t)) = Fun(unmark(t))";
-by (Asm_simp_tac 1);
-qed "unmark_Fun";
-
-Goalw [unmark_def] "unmark(App(b,n,m)) = App(0,unmark(n),unmark(m))";
-by (Asm_simp_tac 1);
-qed "unmark_App";
-
-
-(* ------------------------------------------------------------------------- *)
-(* term simplification set *)
-(* ------------------------------------------------------------------------- *)
-
-
-Addsimps ([unmark_App, unmark_Fun, unmark_Var,
- lambda.dom_subset RS subsetD] @
- lambda.intrs);
+Addsimps ([lambda.dom_subset RS subsetD] @ lambda.intrs);
(* ------------------------------------------------------------------------- *)
(* unmark lemmas *)
(* ------------------------------------------------------------------------- *)
-Goalw [unmark_def]
- "u:redexes ==> unmark(u):lambda";
+Goal "u:redexes ==> unmark(u):lambda";
by (etac redexes.induct 1);
by (ALLGOALS Asm_simp_tac);
qed "unmark_type";
@@ -57,14 +30,13 @@
Goal "v:lambda ==> ALL k:nat. lift_rec(v,k):lambda";
by (etac lambda.induct 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [lift_rec_Var])));
-qed "liftL_typea";
-val liftL_type =liftL_typea RS bspec ;
+bind_thm ("liftL_type", result() RS bspec);
Goal "v:lambda ==> ALL n:nat. ALL u:lambda. subst_rec(u,v,n):lambda";
by (etac lambda.induct 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [liftL_type,subst_Var])));
qed "substL_typea";
-val substL_type = substL_typea RS bspec RS bspec ;
+bind_thm ("substL_type", result() RS bspec RS bspec);
(* ------------------------------------------------------------------------- *)
--- a/src/ZF/Resid/Terms.thy Mon Dec 28 16:53:24 1998 +0100
+++ b/src/ZF/Resid/Terms.thy Mon Dec 28 16:54:01 1998 +0100
@@ -23,10 +23,11 @@
Lambda_App "[|u:lambda; v:lambda|]==> Apl(u,v):lambda"
type_intrs "redexes.intrs@bool_typechecks"
-defs
- unmark_def "unmark(u) == redex_rec(u,%i. Var(i),
- %x m. Fun(m),
- %b x y m p. Apl(m,p))"
+primrec
+ "unmark(Var(n)) = Var(n)"
+ "unmark(Fun(u)) = Fun(unmark(u))"
+ "unmark(App(b,f,a)) = Apl(unmark(f), unmark(a))"
+
end
--- a/src/ZF/ex/BT.ML Mon Dec 28 16:53:24 1998 +0100
+++ b/src/ZF/ex/BT.ML Mon Dec 28 16:54:01 1998 +0100
@@ -6,10 +6,6 @@
Datatype definition of binary trees
*)
-open BT;
-
-Addsimps bt.case_eqns;
-
(*Perform induction on l, then prove the major premise using prems. *)
fun bt_ind_tac a prems i =
EVERY [res_inst_tac [("x",a)] bt.induct i,
@@ -17,6 +13,8 @@
ares_tac prems i];
+Addsimps bt.intrs;
+
(** Lemmas to justify using "bt" in other recursive type definitions **)
Goalw bt.defs "A<=B ==> bt(A) <= bt(B)";
@@ -32,30 +30,8 @@
Pair_in_univ]) 1);
qed "bt_univ";
-bind_thm ("bt_subset_univ", ([bt_mono, bt_univ] MRS subset_trans));
-
-
-(** bt_rec -- by Vset recursion **)
-
-Goalw bt.con_defs "rank(l) < rank(Br(a,l,r))";
-by (simp_tac rank_ss 1);
-qed "rank_Br1";
+bind_thm ("bt_subset_univ", [bt_mono, bt_univ] MRS subset_trans);
-Goalw bt.con_defs "rank(r) < rank(Br(a,l,r))";
-by (simp_tac rank_ss 1);
-qed "rank_Br2";
-
-Goal "bt_rec(Lf,c,h) = c";
-by (rtac (bt_rec_def RS def_Vrec RS trans) 1);
-by (Simp_tac 1);
-qed "bt_rec_Lf";
-
-Goal "bt_rec(Br(a,l,r), c, h) = h(a, l, r, bt_rec(l,c,h), bt_rec(r,c,h))";
-by (rtac (bt_rec_def RS def_Vrec RS trans) 1);
-by (simp_tac (rank_ss addsimps bt.case_eqns @ [rank_Br1, rank_Br2]) 1);
-qed "bt_rec_Br";
-
-Addsimps [bt_rec_Lf, bt_rec_Br];
(*Type checking -- proved by induction, as usual*)
val prems = goal BT.thy
@@ -63,53 +39,31 @@
\ c: C(Lf); \
\ !!x y z r s. [| x:A; y:bt(A); z:bt(A); r:C(y); s:C(z) |] ==> \
\ h(x,y,z,r,s): C(Br(x,y,z)) \
-\ |] ==> bt_rec(t,c,h) : C(t)";
+\ |] ==> bt_rec(c,h,t) : C(t)";
by (bt_ind_tac "t" prems 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
qed "bt_rec_type";
-(** Versions for use with definitions **)
-
-val [rew] = goal BT.thy "[| !!t. j(t)==bt_rec(t, c, h) |] ==> j(Lf) = c";
-by (rewtac rew);
-by (rtac bt_rec_Lf 1);
-qed "def_bt_rec_Lf";
-
-val [rew] = goal BT.thy
- "[| !!t. j(t)==bt_rec(t, c, h) |] ==> j(Br(a,l,r)) = h(a,l,r,j(l),j(r))";
-by (rewtac rew);
-by (rtac bt_rec_Br 1);
-qed "def_bt_rec_Br";
-
-fun bt_recs def = map standard ([def] RL [def_bt_rec_Lf, def_bt_rec_Br]);
-
(** n_nodes **)
-val [n_nodes_Lf,n_nodes_Br] = bt_recs n_nodes_def;
-Addsimps [n_nodes_Lf, n_nodes_Br];
-
-val prems = goalw BT.thy [n_nodes_def]
- "xs: bt(A) ==> n_nodes(xs) : nat";
-by (REPEAT (ares_tac (prems @ [bt_rec_type, nat_0I, nat_succI, add_type]) 1));
+Goal "t: bt(A) ==> n_nodes(t) : nat";
+by (bt_ind_tac "t" [] 1);
+by Auto_tac;
qed "n_nodes_type";
(** n_leaves **)
-val [n_leaves_Lf,n_leaves_Br] = bt_recs n_leaves_def;
-Addsimps [n_leaves_Lf, n_leaves_Br];
-
-val prems = goalw BT.thy [n_leaves_def]
- "xs: bt(A) ==> n_leaves(xs) : nat";
-by (REPEAT (ares_tac (prems @ [bt_rec_type, nat_0I, nat_succI, add_type]) 1));
+Goal "t: bt(A) ==> n_leaves(t) : nat";
+by (bt_ind_tac "t" [] 1);
+by Auto_tac;
qed "n_leaves_type";
(** bt_reflect **)
-val [bt_reflect_Lf, bt_reflect_Br] = bt_recs bt_reflect_def;
-Addsimps [bt_reflect_Lf, bt_reflect_Br];
-
-Goalw [bt_reflect_def] "xs: bt(A) ==> bt_reflect(xs) : bt(A)";
+Goal "t: bt(A) ==> bt_reflect(t) : bt(A)";
+by (bt_ind_tac "t" [] 1);
+by Auto_tac;
by (REPEAT (ares_tac (bt.intrs @ [bt_rec_type]) 1));
qed "bt_reflect_type";
@@ -117,10 +71,7 @@
(** BT simplification **)
-val bt_typechecks =
- bt.intrs @ [bt_rec_type, n_nodes_type, n_leaves_type, bt_reflect_type];
-
-Addsimps bt_typechecks;
+Addsimps [bt_rec_type, n_nodes_type, n_leaves_type, bt_reflect_type];
(*** theorems about n_leaves ***)
--- a/src/ZF/ex/BT.thy Mon Dec 28 16:53:24 1998 +0100
+++ b/src/ZF/ex/BT.thy Mon Dec 28 16:54:01 1998 +0100
@@ -8,7 +8,6 @@
BT = Datatype +
consts
- bt_rec :: [i, i, [i,i,i,i,i]=>i] => i
n_nodes :: i=>i
n_leaves :: i=>i
bt_reflect :: i=>i
@@ -18,12 +17,17 @@
datatype
"bt(A)" = Lf | Br ("a: A", "t1: bt(A)", "t2: bt(A)")
-defs
- bt_rec_def
- "bt_rec(t,c,h) == Vrec(t, %t g. bt_case(c, %x y z. h(x,y,z,g`y,g`z), t))"
+
+primrec
+ "n_nodes(Lf) = 0"
+ "n_nodes(Br(a,l,r)) = succ(n_nodes(l) #+ n_nodes(r))"
- n_nodes_def "n_nodes(t) == bt_rec(t, 0, %x y z r s. succ(r#+s))"
- n_leaves_def "n_leaves(t) == bt_rec(t, succ(0), %x y z r s. r#+s)"
- bt_reflect_def "bt_reflect(t) == bt_rec(t, Lf, %x y z r s. Br(x,s,r))"
+primrec
+ "n_leaves(Lf) = 1"
+ "n_leaves(Br(a,l,r)) = n_leaves(l) #+ n_leaves(r)"
+
+primrec
+ "bt_reflect(Lf) = Lf"
+ "bt_reflect(Br(a,l,r)) = Br(a, bt_reflect(r), bt_reflect(l))"
end
--- a/src/ZF/ex/Limit.ML Mon Dec 28 16:53:24 1998 +0100
+++ b/src/ZF/ex/Limit.ML Mon Dec 28 16:54:01 1998 +0100
@@ -312,8 +312,7 @@
val Yub = rewrite_rule[islub_def]Ylub RS conjunct1;
val Xub_y = Yub RS (dom RS dominate_isub);
val lem = Xub_y RS (rewrite_rule[islub_def]Xlub RS conjunct2 RS spec RS mp);
-val thm = Y RS (X RS (cpo RS lem));
-by (rtac thm 1);
+by (rtac (Y RS (X RS (cpo RS lem))) 1);
qed "dominate_islub";
val prems = Goalw [subchain_def] (* subchainE *)
--- a/src/ZF/ex/ListN.ML Mon Dec 28 16:53:24 1998 +0100
+++ b/src/ZF/ex/ListN.ML Mon Dec 28 16:54:01 1998 +0100
@@ -19,9 +19,9 @@
Goal "<n,l> : listn(A) <-> l:list(A) & length(l)=n";
by (rtac iffI 1);
+by (blast_tac (claset() addIs [list_into_listn]) 2);
by (etac listn.induct 1);
-by (safe_tac (claset() addSIs list_typechecks @
- [length_Nil, length_Cons, list_into_listn]));
+by (ALLGOALS Asm_simp_tac);
qed "listn_iff";
Goal "listn(A)``{n} = {l:list(A). length(l)=n}";
--- a/src/ZF/ex/PropLog.ML Mon Dec 28 16:53:24 1998 +0100
+++ b/src/ZF/ex/PropLog.ML Mon Dec 28 16:54:01 1998 +0100
@@ -9,29 +9,7 @@
Prove: If H|=p then G|=p where G:Fin(H)
*)
-open PropLog;
-
-(*** prop_rec -- by Vset recursion ***)
-
-(** conversion rules **)
-
-Goal "prop_rec(Fls,b,c,d) = b";
-by (rtac (prop_rec_def RS def_Vrec RS trans) 1);
-by (simp_tac (simpset() addsimps prop.con_defs) 1);
-qed "prop_rec_Fls";
-
-Goal "prop_rec(#v,b,c,d) = c(v)";
-by (rtac (prop_rec_def RS def_Vrec RS trans) 1);
-by (simp_tac (simpset() addsimps prop.con_defs) 1);
-qed "prop_rec_Var";
-
-Goal "prop_rec(p=>q,b,c,d) = \
-\ d(p, q, prop_rec(p,b,c,d), prop_rec(q,b,c,d))";
-by (rtac (prop_rec_def RS def_Vrec RS trans) 1);
-by (simp_tac (rank_ss addsimps prop.con_defs) 1);
-qed "prop_rec_Imp";
-
-Addsimps [prop_rec_Fls, prop_rec_Var, prop_rec_Imp];
+Addsimps prop.intrs;
(*** Semantics of propositional logic ***)
@@ -49,23 +27,8 @@
by (Simp_tac 1);
qed "is_true_Imp";
-(** The function hyps **)
-
-Goalw [hyps_def] "hyps(Fls,t) = 0";
-by (Simp_tac 1);
-qed "hyps_Fls";
+Addsimps [is_true_Fls, is_true_Var, is_true_Imp];
-Goalw [hyps_def] "hyps(#v,t) = {if(v:t, #v, #v=>Fls)}";
-by (Simp_tac 1);
-qed "hyps_Var";
-
-Goalw [hyps_def] "hyps(p=>q,t) = hyps(p,t) Un hyps(q,t)";
-by (Simp_tac 1);
-qed "hyps_Imp";
-
-Addsimps prop.intrs;
-Addsimps [is_true_Fls, is_true_Var, is_true_Imp,
- hyps_Fls, hyps_Var, hyps_Imp];
(*** Proof theory of propositional logic ***)
@@ -138,8 +101,7 @@
(*Soundness of the rules wrt truth-table semantics*)
Goalw [logcon_def] "H |- p ==> H |= p";
by (etac thms.induct 1);
-by (fast_tac (claset() addSDs [is_true_Imp RS iffD1 RS mp]) 5);
-by (ALLGOALS Asm_simp_tac);
+by Auto_tac;
qed "soundness";
(*** Towards the completeness proof ***)
@@ -165,7 +127,7 @@
(*Typical example of strengthening the induction formula*)
Goal "p: prop ==> hyps(p,t) |- if(is_true(p,t), p, p=>Fls)";
-by (rtac (split_if RS iffD2) 1);
+by (Simp_tac 1);
by (etac prop.induct 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [thms_I, thms.H])));
by (safe_tac (claset() addSEs [Fls_Imp RS weaken_left_Un1,
--- a/src/ZF/ex/PropLog.thy Mon Dec 28 16:53:24 1998 +0100
+++ b/src/ZF/ex/PropLog.thy Mon Dec 28 16:54:01 1998 +0100
@@ -21,6 +21,8 @@
(** The proof system **)
consts
thms :: i => i
+
+syntax
"|-" :: [i,i] => o (infixl 50)
translations
@@ -39,29 +41,27 @@
(** The semantics **)
consts
- prop_rec :: [i, i, i=>i, [i,i,i,i]=>i] => i
- is_true :: [i,i] => o
- "|=" :: [i,i] => o (infixl 50)
- hyps :: [i,i] => i
+ "|=" :: [i,i] => o (infixl 50)
+ hyps :: [i,i] => i
+ is_true_fun :: [i,i] => i
+
+constdefs (*this definitionis necessary since predicates can't be recursive*)
+ is_true :: [i,i] => o
+ "is_true(p,t) == is_true_fun(p,t)=1"
defs
-
- prop_rec_def
- "prop_rec(p,b,c,h) ==
- Vrec(p, %p g. prop_case(b, c, %x y. h(x, y, g`x, g`y), p))"
-
- (** Semantics of propositional logic **)
- is_true_def
- "is_true(p,t) == prop_rec(p, 0, %v. if(v:t, 1, 0),
- %p q tp tq. if(tp=1,tq,1)) = 1"
-
(*Logical consequence: for every valuation, if all elements of H are true
then so is p*)
logcon_def "H |= p == ALL t. (ALL q:H. is_true(q,t)) --> is_true(p,t)"
- (** A finite set of hypotheses from t and the Vars in p **)
- hyps_def
- "hyps(p,t) == prop_rec(p, 0, %v. {if(v:t, #v, #v=>Fls)},
- %p q Hp Hq. Hp Un Hq)"
+primrec (** A finite set of hypotheses from t and the Vars in p **)
+ "hyps(Fls, t) = 0"
+ "hyps(Var(v), t) = if(v:t, {#v}, {#v=>Fls})"
+ "hyps(p=>q, t) = hyps(p,t) Un hyps(q,t)"
+
+primrec (** Semantics of propositional logic **)
+ "is_true_fun(Fls, t) = 0"
+ "is_true_fun(Var(v), t) = if(v:t, 1, 0)"
+ "is_true_fun(p=>q, t) = if(is_true_fun(p,t)=1, is_true_fun(q,t), 1)"
end
--- a/src/ZF/ex/TF.ML Mon Dec 28 16:53:24 1998 +0100
+++ b/src/ZF/ex/TF.ML Mon Dec 28 16:54:01 1998 +0100
@@ -4,16 +4,9 @@
Copyright 1993 University of Cambridge
Trees & forests, a mutually recursive type definition.
-
-Still needs
-
-"TF_reflect == (%z. TF_rec(z, %x ts r. Tcons(x,r), 0,
- %t ts r1 r2. TF_of_list(list_of_TF(r2) @ <r1,0>)))"
*)
-open TF;
-
-val [TconsI, FnilI, FconsI] = tree_forest.intrs;
+Addsimps tree_forest.intrs;
(** tree_forest(A) as the union of tree(A) and forest(A) **)
@@ -58,32 +51,7 @@
qed "forest_unfold";
-(*** TF_rec -- by Vset recursion ***)
-
-(** conversion rules **)
-
-Goal "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 tree_forest.con_defs);
-by (simp_tac rank_ss 1);
-qed "TF_rec_Tcons";
-
-Goal "TF_rec(Fnil, b, c, d) = c";
-by (rtac (TF_rec_def RS def_Vrec RS trans) 1);
-by (rewrite_goals_tac tree_forest.con_defs);
-by (Simp_tac 1);
-qed "TF_rec_Fnil";
-
-Goal "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 tree_forest.con_defs);
-by (simp_tac rank_ss 1);
-qed "TF_rec_Fcons";
-
-Addsimps [TF_rec_Tcons, TF_rec_Fnil, TF_rec_Fcons, TconsI, FnilI, FconsI];
-
-(** Type checking **)
+(** Type checking for recursor: Not needed; possibly interesting (??) **)
val major::prems = goal TF.thy
"[| z: tree_forest(A); \
@@ -92,7 +60,7 @@
\ c : C(Fnil); \
\ !!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)";
+\ |] ==> tree_forest_rec(b,c,d,z) : C(z)";
by (rtac (major RS tree_forest.induct) 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
qed "TF_rec_type";
@@ -104,93 +72,53 @@
\ c : D(Fnil); \
\ !!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 f: forest(A). TF_rec(f,b,c,d) : D(f))";
+\ |] ==> (ALL t:tree(A). tree_forest_rec(b,c,d,t) : C(t)) & \
+\ (ALL f: forest(A). tree_forest_rec(b,c,d,f) : D(f))";
by (rewtac Ball_def);
by (rtac tree_forest.mutual_induct 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
qed "tree_forest_rec_type";
-(** Versions for use with definitions **)
-
-val [rew] = goal TF.thy
- "[| !!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);
-qed "def_TF_rec_Tcons";
-
-val [rew] = goal TF.thy
- "[| !!z. j(z)==TF_rec(z,b,c,d) |] ==> j(Fnil) = c";
-by (rewtac rew);
-by (rtac TF_rec_Fnil 1);
-qed "def_TF_rec_Fnil";
+(** list_of_TF and of_list **)
-val [rew] = goal TF.thy
- "[| !!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);
-qed "def_TF_rec_Fcons";
-
-fun TF_recs def = map standard
- ([def] RL [def_TF_rec_Tcons, def_TF_rec_Fnil, def_TF_rec_Fcons]);
-
-
-(** list_of_TF and TF_of_list **)
-
-val [list_of_TF_Tcons, list_of_TF_Fnil, list_of_TF_Fcons] =
- TF_recs list_of_TF_def;
-Addsimps [list_of_TF_Tcons, list_of_TF_Fnil, list_of_TF_Fcons];
-
-Goalw [list_of_TF_def]
- "z: tree_forest(A) ==> list_of_TF(z) : list(tree(A))";
-by (REPEAT (ares_tac ([TF_rec_type,TconsI] @ list_typechecks) 1));
+Goal "z: tree_forest(A) ==> list_of_TF(z) : list(tree(A))";
+by (etac tree_forest.induct 1);
+by (ALLGOALS Asm_simp_tac);
qed "list_of_TF_type";
-val [TF_of_list_Nil,TF_of_list_Cons] = list_recs TF_of_list_def;
-Addsimps [TF_of_list_Nil,TF_of_list_Cons];
-
-Goalw [TF_of_list_def]
- "l: list(tree(A)) ==> TF_of_list(l) : forest(A)";
-by (REPEAT (ares_tac [list_rec_type, FnilI, FconsI] 1));
-qed "TF_of_list_type";
+Goal "l: list(tree(A)) ==> of_list(l) : forest(A)";
+by (etac list.induct 1);
+by (ALLGOALS Asm_simp_tac);
+qed "of_list_type";
-(** TF_map **)
-
-val [TF_map_Tcons, TF_map_Fnil, TF_map_Fcons] = TF_recs TF_map_def;
-Addsimps [TF_map_Tcons, TF_map_Fnil, TF_map_Fcons];
+(** map **)
-val prems = goalw TF.thy [TF_map_def]
+val prems = Goal
"[| !!x. x: A ==> h(x): B |] ==> \
-\ (ALL t:tree(A). TF_map(h,t) : tree(B)) & \
-\ (ALL f: forest(A). TF_map(h,f) : forest(B))";
-by (REPEAT
- (ares_tac ([tree_forest_rec_type, TconsI, FnilI, FconsI] @ prems) 1));
-qed "TF_map_type";
+\ (ALL t:tree(A). map(h,t) : tree(B)) & \
+\ (ALL f: forest(A). map(h,f) : forest(B))";
+by (rewtac Ball_def);
+by (rtac tree_forest.mutual_induct 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
+qed "map_type";
-(** TF_size **)
-
-val [TF_size_Tcons, TF_size_Fnil, TF_size_Fcons] = TF_recs TF_size_def;
-Addsimps [TF_size_Tcons, TF_size_Fnil, TF_size_Fcons];
+(** size **)
-Goalw [TF_size_def]
- "z: tree_forest(A) ==> TF_size(z) : nat";
-by (REPEAT (ares_tac [TF_rec_type, add_type, nat_0I, nat_succI] 1));
-qed "TF_size_type";
+Goal "z: tree_forest(A) ==> size(z) : nat";
+by (etac tree_forest.induct 1);
+by (ALLGOALS Asm_simp_tac);
+qed "size_type";
-(** TF_preorder **)
+(** preorder **)
-val [TF_preorder_Tcons, TF_preorder_Fnil, TF_preorder_Fcons] =
- TF_recs TF_preorder_def;
-Addsimps [TF_preorder_Tcons, TF_preorder_Fnil, TF_preorder_Fcons];
-
-Goalw [TF_preorder_def]
- "z: tree_forest(A) ==> TF_preorder(z) : list(A)";
-by (REPEAT (ares_tac ([TF_rec_type, app_type] @ list.intrs) 1));
-qed "TF_preorder_type";
+Goal "z: tree_forest(A) ==> preorder(z) : list(A)";
+by (etac tree_forest.induct 1);
+by (ALLGOALS Asm_simp_tac);
+qed "preorder_type";
(** Term simplification **)
@@ -198,16 +126,16 @@
val treeI = tree_subset_TF RS subsetD
and forestI = forest_subset_TF RS subsetD;
-val TF_typechecks =
- [TconsI, FnilI, FconsI, treeI, forestI,
- list_of_TF_type, TF_map_type, TF_size_type, TF_preorder_type];
+val typechecks =
+ [treeI, forestI,
+ list_of_TF_type, map_type, size_type, preorder_type];
-simpset_ref() := simpset() setSolver type_auto_tac (list_typechecks@TF_typechecks);
+Addsimps typechecks;
-(** theorems about list_of_TF and TF_of_list **)
+(** theorems about list_of_TF and of_list **)
(*essentially the same as list induction*)
-val major::prems = goal TF.thy
+val major::prems = Goal
"[| f: forest(A); \
\ R(Fnil); \
\ !!t f. [| t: tree(A); f: forest(A); R(f) |] ==> R(Fcons(t,f)) \
@@ -216,44 +144,47 @@
by (REPEAT (ares_tac (TrueI::prems) 1));
qed "forest_induct";
-Goal "f: forest(A) ==> TF_of_list(list_of_TF(f)) = f";
+Goal "f: forest(A) ==> of_list(list_of_TF(f)) = f";
by (etac forest_induct 1);
by (ALLGOALS Asm_simp_tac);
qed "forest_iso";
-Goal "ts: list(tree(A)) ==> list_of_TF(TF_of_list(ts)) = ts";
+Goal "ts: list(tree(A)) ==> list_of_TF(of_list(ts)) = ts";
by (etac list.induct 1);
by (ALLGOALS Asm_simp_tac);
qed "tree_list_iso";
-(** theorems about TF_map **)
+(** theorems about map **)
-Goal "z: tree_forest(A) ==> TF_map(%u. u, z) = z";
+Goal "z: tree_forest(A) ==> map(%u. u, z) = z";
by (etac tree_forest.induct 1);
by (ALLGOALS Asm_simp_tac);
-qed "TF_map_ident";
+qed "map_ident";
-Goal "z: tree_forest(A) ==> TF_map(h, TF_map(j,z)) = TF_map(%u. h(j(u)), z)";
+Goal "z: tree_forest(A) ==> map(h, map(j,z)) = map(%u. h(j(u)), z)";
+by (etac tree_forest.induct 1);
+by (ALLGOALS Asm_simp_tac);
+qed "map_compose";
+
+(** theorems about size **)
+
+Goal "z: tree_forest(A) ==> size(map(h,z)) = size(z)";
by (etac tree_forest.induct 1);
by (ALLGOALS Asm_simp_tac);
-qed "TF_map_compose";
-
-(** theorems about TF_size **)
+qed "size_map";
-Goal "z: tree_forest(A) ==> TF_size(TF_map(h,z)) = TF_size(z)";
-by (etac tree_forest.induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "TF_size_TF_map";
-
-Goal "z: tree_forest(A) ==> TF_size(z) = length(TF_preorder(z))";
+Goal "z: tree_forest(A) ==> size(z) = length(preorder(z))";
by (etac tree_forest.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app])));
-qed "TF_size_length";
+by (ALLGOALS (*TYPECHECKING: why so explicit?*)
+ (asm_simp_tac
+ (simpset() addsimps [treeI RS preorder_type RS length_app])));
+qed "size_length";
-(** theorems about TF_preorder **)
+(** theorems about preorder **)
-Goal "z: tree_forest(A) ==> \
-\ TF_preorder(TF_map(h,z)) = map(h, TF_preorder(z))";
+Goal "z: tree_forest(A) ==> preorder(TF.map(h,z)) = List.map(h, preorder(z))";
by (etac tree_forest.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [map_app_distrib])));
-qed "TF_preorder_TF_map";
+by (ALLGOALS (*TYPECHECKING: why so explicit?*)
+ (asm_simp_tac
+ (simpset() addsimps [treeI RS preorder_type RS map_app_distrib])));
+qed "preorder_map";
--- a/src/ZF/ex/TF.thy Mon Dec 28 16:53:24 1998 +0100
+++ b/src/ZF/ex/TF.thy Mon Dec 28 16:54:01 1998 +0100
@@ -8,12 +8,12 @@
TF = List +
consts
- TF_rec :: [i, [i,i,i]=>i, i, [i,i,i,i]=>i] => i
- TF_map :: [i=>i, i] => i
- TF_size :: i=>i
- TF_preorder :: i=>i
+ map :: [i=>i, i] => i
+ size :: i=>i
+ preorder :: i=>i
list_of_TF :: i=>i
- TF_of_list :: i=>i
+ of_list :: i=>i
+ reflect :: i=>i
tree, forest, tree_forest :: i=>i
@@ -22,28 +22,35 @@
and
"forest(A)" = Fnil | Fcons ("t: tree(A)", "f: forest(A)")
-defs
- TF_rec_def
- "TF_rec(z,b,c,d) == Vrec(z,
- %z r. tree_forest_case(%x f. b(x, f, r`f),
- c,
- %t f. d(t, f, r`t, r`f), z))"
+primrec
+ "list_of_TF (Tcons(x,f)) = [Tcons(x,f)]"
+ "list_of_TF (Fnil) = []"
+ "list_of_TF (Fcons(t,tf)) = Cons (t, list_of_TF(tf))"
- list_of_TF_def
- "list_of_TF(z) == TF_rec(z, %x f r. [Tcons(x,f)], [],
- %t f r1 r2. Cons(t, r2))"
+primrec
+ "of_list([]) = Fnil"
+ "of_list(Cons(t,l)) = Fcons(t, of_list(l))"
+
+primrec
+ "map (h, Tcons(x,f)) = Tcons(h(x), map(h,f))"
+ "map (h, Fnil) = Fnil"
+ "map (h, Fcons(t,tf)) = Fcons (map(h, t), map(h, tf))"
- TF_of_list_def
- "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 f r. Tcons(h(x),r), Fnil,
- %t f r1 r2. Fcons(r1,r2))"
-
- TF_size_def
- "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 f r. Cons(x,r), Nil, %t f r1 r2. r1@r2)"
+primrec
+ "size (Tcons(x,f)) = succ(size(f))"
+ "size (Fnil) = 0"
+ "size (Fcons(t,tf)) = size(t) #+ size(tf)"
+
+primrec
+ "preorder (Tcons(x,f)) = Cons(x, preorder(f))"
+ "preorder (Fnil) = Nil"
+ "preorder (Fcons(t,tf)) = preorder(t) @ preorder(tf)"
+
+primrec
+ "reflect (Tcons(x,f)) = Tcons(x, reflect(f))"
+ "reflect (Fnil) = Fnil"
+ "reflect (Fcons(t,tf)) = of_list
+ (list_of_TF (reflect(tf)) @
+ Cons(reflect(t), Nil))"
end
--- a/src/ZF/ex/Term.ML Mon Dec 28 16:53:24 1998 +0100
+++ b/src/ZF/ex/Term.ML Mon Dec 28 16:54:01 1998 +0100
@@ -16,7 +16,7 @@
qed "term_unfold";
(*Induction on term(A) followed by induction on List *)
-val major::prems = goal Term.thy
+val major::prems = Goal
"[| t: term(A); \
\ !!x. [| x: A |] ==> P(Apply(x,Nil)); \
\ !!x z zs. [| x: A; z: term(A); zs: list(term(A)); P(Apply(x,zs)) \
@@ -29,7 +29,7 @@
qed "term_induct2";
(*Induction on term(A) to prove an equation*)
-val major::prems = goal Term.thy
+val major::prems = Goal
"[| t: term(A); \
\ !!x zs. [| x: A; zs: list(term(A)); map(f,zs) = map(g,zs) |] ==> \
\ f(Apply(x,zs)) = g(Apply(x,zs)) \
@@ -66,28 +66,27 @@
(*** term_rec -- by Vset recursion ***)
(*Lemma: map works correctly on the underlying list of terms*)
-val [major,ordi] = goal list.thy
- "[| l: list(A); Ord(i) |] ==> \
-\ rank(l)<i --> map(%z. (lam x:Vset(i).h(x)) ` z, l) = map(h,l)";
-by (rtac (major RS list.induct) 1);
+Goal "[| l: list(A); Ord(i) |] ==> \
+\ rank(l)<i --> map(%z. (lam x:Vset(i).h(x)) ` z, l) = map(h,l)";
+by (etac list.induct 1);
by (Simp_tac 1);
by (rtac impI 1);
-by (forward_tac [rank_Cons1 RS lt_trans] 1);
-by (dtac (rank_Cons2 RS lt_trans) 1);
-by (asm_simp_tac (simpset() addsimps [ordi, VsetI]) 1);
+by (subgoal_tac "rank(a)<i & rank(l) < i" 1);
+by (asm_simp_tac (simpset() addsimps [VsetI]) 1);
+by (full_simp_tac (simpset() addsimps list.con_defs) 1);
+by (blast_tac (claset() addDs (rank_rls RL [lt_trans])) 1);
qed "map_lemma";
(*Typing premise is necessary to invoke map_lemma*)
-val [prem] = goal Term.thy
- "ts: list(A) ==> \
-\ term_rec(Apply(a,ts), d) = d(a, ts, map (%z. term_rec(z,d), ts))";
+Goal "ts: list(A) ==> \
+\ term_rec(Apply(a,ts), d) = d(a, ts, map (%z. term_rec(z,d), ts))";
by (rtac (term_rec_def RS def_Vrec RS trans) 1);
by (rewrite_goals_tac term.con_defs);
-by (simp_tac (simpset() addsimps [Ord_rank, rank_pair2, prem RS map_lemma]) 1);;
+by (asm_simp_tac (simpset() addsimps [Ord_rank, rank_pair2, map_lemma]) 1);;
qed "term_rec";
(*Slightly odd typing condition on r in the second premise!*)
-val major::prems = goal Term.thy
+val major::prems = Goal
"[| t: term(A); \
\ !!x zs r. [| x: A; zs: list(term(A)); \
\ r: list(UN t:term(A). C(t)) |] \
@@ -103,14 +102,14 @@
by (REPEAT (ares_tac [list.Cons_I, UN_I] 1));
qed "term_rec_type";
-val [rew,tslist] = goal Term.thy
+val [rew,tslist] = Goal
"[| !!t. j(t)==term_rec(t,d); ts: list(A) |] ==> \
\ j(Apply(a,ts)) = d(a, ts, map(%Z. j(Z), ts))";
by (rewtac rew);
by (rtac (tslist RS term_rec) 1);
qed "def_term_rec";
-val prems = goal Term.thy
+val prems = Goal
"[| t: term(A); \
\ !!x zs r. [| x: A; zs: list(term(A)); r: list(C) |] \
\ ==> d(x, zs, r): C \
@@ -124,14 +123,13 @@
bind_thm ("term_map", (term_map_def RS def_term_rec));
-val prems = goalw Term.thy [term_map_def]
+val prems = Goalw [term_map_def]
"[| t: term(A); !!x. x: A ==> f(x): B |] ==> term_map(f,t) : term(B)";
by (REPEAT (ares_tac ([term_rec_simple_type, term.Apply_I] @ prems) 1));
qed "term_map_type";
-val [major] = goal Term.thy
- "t: term(A) ==> term_map(f,t) : term({f(u). u:A})";
-by (rtac (major RS term_map_type) 1);
+Goal "t: term(A) ==> term_map(f,t) : term({f(u). u:A})";
+by (etac term_map_type 1);
by (etac RepFunI 1);
qed "term_map_type2";