# HG changeset patch # User paulson # Date 914860441 -3600 # Node ID 2c8a8be36c94d99946b744741a458606a0de7580 # Parent 6a9dc67d48f57f66afa4cccc2b646917ab71a5a7 converted to use new primrec section diff -r 6a9dc67d48f5 -r 2c8a8be36c94 src/ZF/Coind/ECR.ML --- 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); :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] diff -r 6a9dc67d48f5 -r 2c8a8be36c94 src/ZF/Coind/MT.ML --- 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); \ \ :ElabRel \ \ |] ==> : 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); :ElabRel |] ==> \ \ :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; \ \ :EvalRel; \ \ ALL t te. \ \ hastyenv(ve,te) --> :ElabRel --> :HasTyRel; \ @@ -93,13 +89,12 @@ \ hastyenv(ve, te); \ \ :ElabRel |] ==> \ \ :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; \ \ :EvalRel; \ \ ALL t te. \ \ hastyenv(ve,te) --> \ @@ -117,7 +112,6 @@ \ :HasTyRel; \ \ hastyenv(ve,te); :ElabRel |] ==> \ \ :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); \ \ :EvalRel; \ \ :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"; - - - - diff -r 6a9dc67d48f5 -r 2c8a8be36c94 src/ZF/Coind/Map.ML --- 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"; - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff -r 6a9dc67d48f5 -r 2c8a8be36c94 src/ZF/Coind/Types.ML --- 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"; diff -r 6a9dc67d48f5 -r 2c8a8be36c94 src/ZF/Coind/Types.thy --- 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 diff -r 6a9dc67d48f5 -r 2c8a8be36c94 src/ZF/Coind/Values.ML --- 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); diff -r 6a9dc67d48f5 -r 2c8a8be36c94 src/ZF/Coind/Values.thy --- 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 diff -r 6a9dc67d48f5 -r 2c8a8be36c94 src/ZF/Integ/Bin.ML --- 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)); diff -r 6a9dc67d48f5 -r 2c8a8be36c94 src/ZF/Integ/Bin.thy --- 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 diff -r 6a9dc67d48f5 -r 2c8a8be36c94 src/ZF/Resid/Cube.ML --- 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]; diff -r 6a9dc67d48f5 -r 2c8a8be36c94 src/ZF/Resid/Redex.ML --- 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"; diff -r 6a9dc67d48f5 -r 2c8a8be36c94 src/ZF/Resid/Redex.thy --- 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" == ":Ssub" + "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 diff -r 6a9dc67d48f5 -r 2c8a8be36c94 src/ZF/Resid/Residuals.ML --- 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); diff -r 6a9dc67d48f5 -r 2c8a8be36c94 src/ZF/Resid/SubUnion.ML --- 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"; diff -r 6a9dc67d48f5 -r 2c8a8be36c94 src/ZF/Resid/SubUnion.thy --- 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" == ":Ssub" - "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 diff -r 6a9dc67d48f5 -r 2c8a8be36c94 src/ZF/Resid/Substitution.ML --- 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 lift_rec(Var(i),n) =if(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 lift_rec(Var(i),k) = Var(i)"; -by (Asm_simp_tac 1); +Goal "[|i:nat; k:nat; i 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 \ +\ subst_rec(u,Var(i),k) = if(k 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 \ -\ subst_rec(u,Var(n),p) = Var(n #- 1)"; -by (Asm_simp_tac 1); +Goal "[|n:nat; u:redexes; p:nat; p \ +\ 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 \ -\ 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 \ +\ 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); diff -r 6a9dc67d48f5 -r 2c8a8be36c94 src/ZF/Resid/Substitution.thy --- 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 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); (* ------------------------------------------------------------------------- *) diff -r 6a9dc67d48f5 -r 2c8a8be36c94 src/ZF/Resid/Terms.thy --- 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 diff -r 6a9dc67d48f5 -r 2c8a8be36c94 src/ZF/ex/BT.ML --- 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 ***) diff -r 6a9dc67d48f5 -r 2c8a8be36c94 src/ZF/ex/BT.thy --- 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 diff -r 6a9dc67d48f5 -r 2c8a8be36c94 src/ZF/ex/Limit.ML --- 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 *) diff -r 6a9dc67d48f5 -r 2c8a8be36c94 src/ZF/ex/ListN.ML --- 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 " : 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}"; diff -r 6a9dc67d48f5 -r 2c8a8be36c94 src/ZF/ex/PropLog.ML --- 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, diff -r 6a9dc67d48f5 -r 2c8a8be36c94 src/ZF/ex/PropLog.thy --- 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 diff -r 6a9dc67d48f5 -r 2c8a8be36c94 src/ZF/ex/TF.ML --- 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) @ )))" *) -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"; diff -r 6a9dc67d48f5 -r 2c8a8be36c94 src/ZF/ex/TF.thy --- 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 diff -r 6a9dc67d48f5 -r 2c8a8be36c94 src/ZF/ex/Term.ML --- 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) 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) 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) \ -\ 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";