# HG changeset patch # User clasohm # Date 823011876 -3600 # Node ID 5d7a7e439cec5b4cad10d1f56101377fbce9faaa # Parent a608f83e3421f447d0f2a3c6427200211cb2dcdf expanded tabs diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Arith.ML --- a/src/HOL/Arith.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Arith.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/Arith.ML +(* Title: HOL/Arith.ML ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge Proofs about elementary arithmetic: addition, multiplication, etc. @@ -227,7 +227,7 @@ by (case_tac "k i m <= n+k"; -by (eresolve_tac [le_trans] 1); -by (resolve_tac [le_add1] 1); +by (etac le_trans 1); +by (rtac le_add1 1); qed "le_imp_add_le"; goal Arith.thy "!!k::nat. m < n ==> m < n+k"; -by (eresolve_tac [less_le_trans] 1); -by (resolve_tac [le_add1] 1); +by (etac less_le_trans 1); +by (rtac le_add1 1); qed "less_imp_add_less"; goal Arith.thy "m+k<=n --> m<=(n::nat)"; @@ -350,7 +350,7 @@ by (asm_full_simp_tac (!simpset delsimps [add_Suc_right] addsimps ([add_Suc_right RS sym, add_left_cancel] @add_ac)) 1); -by (eresolve_tac [subst] 1); +by (etac subst 1); by (simp_tac (!simpset addsimps [less_add_Suc1]) 1); qed "less_add_eq_less"; @@ -375,8 +375,8 @@ (*A [clumsy] way of lifting < monotonicity to <= monotonicity *) val [lt_mono,le] = goal Arith.thy - "[| !!i j::nat. i f(i) < f(j); \ -\ i <= j \ + "[| !!i j::nat. i f(i) < f(j); \ +\ i <= j \ \ |] ==> f(i) <= (f(j)::nat)"; by (cut_facts_tac [le] 1); by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1); @@ -386,7 +386,7 @@ (*non-strict, in 1st argument*) goal Arith.thy "!!i j k::nat. i<=j ==> i + k <= j + k"; by (res_inst_tac [("f", "%j.j+k")] less_mono_imp_le_mono 1); -by (eresolve_tac [add_less_mono1] 1); +by (etac add_less_mono1 1); by (assume_tac 1); qed "add_le_mono1"; @@ -395,5 +395,5 @@ by (etac (add_le_mono1 RS le_trans) 1); by (simp_tac (!simpset addsimps [add_commute]) 1); (*j moves to the end because it is free while k, l are bound*) -by (eresolve_tac [add_le_mono1] 1); +by (etac add_le_mono1 1); qed "add_le_mono"; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/AxClasses/Group/Group.ML --- a/src/HOL/AxClasses/Group/Group.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/AxClasses/Group/Group.ML Tue Jan 30 15:24:36 1996 +0100 @@ -12,121 +12,121 @@ goal thy "x * inv x = (1::'a::group)"; -br (sub left_unit) 1; +by (rtac (sub left_unit) 1); back(); -br (sub assoc) 1; -br (sub left_inv) 1; +by (rtac (sub assoc) 1); +by (rtac (sub left_inv) 1); back(); back(); -br (ssub assoc) 1; +by (rtac (ssub assoc) 1); back(); -br (ssub left_inv) 1; -br (ssub assoc) 1; -br (ssub left_unit) 1; -br (ssub left_inv) 1; -br refl 1; +by (rtac (ssub left_inv) 1); +by (rtac (ssub assoc) 1); +by (rtac (ssub left_unit) 1); +by (rtac (ssub left_inv) 1); +by (rtac refl 1); qed "right_inv"; goal thy "x * 1 = (x::'a::group)"; -br (sub left_inv) 1; -br (sub assoc) 1; -br (ssub right_inv) 1; -br (ssub left_unit) 1; -br refl 1; +by (rtac (sub left_inv) 1); +by (rtac (sub assoc) 1); +by (rtac (ssub right_inv) 1); +by (rtac (ssub left_unit) 1); +by (rtac refl 1); qed "right_unit"; goal thy "e * x = x --> e = (1::'a::group)"; -br impI 1; -br (sub right_unit) 1; +by (rtac impI 1); +by (rtac (sub right_unit) 1); back(); by (res_inst_tac [("x", "x")] (sub right_inv) 1); -br (sub assoc) 1; -br arg_cong 1; +by (rtac (sub assoc) 1); +by (rtac arg_cong 1); back(); -ba 1; +by (assume_tac 1); qed "strong_one_unit"; goal thy "EX! e. ALL x. e * x = (x::'a::group)"; -br ex1I 1; -br allI 1; -br left_unit 1; -br mp 1; -br strong_one_unit 1; -be allE 1; -ba 1; +by (rtac ex1I 1); +by (rtac allI 1); +by (rtac left_unit 1); +by (rtac mp 1); +by (rtac strong_one_unit 1); +by (etac allE 1); +by (assume_tac 1); qed "ex1_unit"; goal thy "ALL x. EX! e. e * x = (x::'a::group)"; -br allI 1; -br ex1I 1; -br left_unit 1; -br (strong_one_unit RS mp) 1; -ba 1; +by (rtac allI 1); +by (rtac ex1I 1); +by (rtac left_unit 1); +by (rtac (strong_one_unit RS mp) 1); +by (assume_tac 1); qed "ex1_unit'"; goal thy "inj (op * (x::'a::group))"; -br injI 1; -br (sub left_unit) 1; +by (rtac injI 1); +by (rtac (sub left_unit) 1); back(); -br (sub left_unit) 1; +by (rtac (sub left_unit) 1); by (res_inst_tac [("x", "x")] (sub left_inv) 1); -br (ssub assoc) 1; +by (rtac (ssub assoc) 1); back(); -br (ssub assoc) 1; -br arg_cong 1; +by (rtac (ssub assoc) 1); +by (rtac arg_cong 1); back(); -ba 1; +by (assume_tac 1); qed "inj_times"; goal thy "y * x = 1 --> y = inv (x::'a::group)"; -br impI 1; -br (sub right_unit) 1; +by (rtac impI 1); +by (rtac (sub right_unit) 1); back(); back(); -br (sub right_unit) 1; +by (rtac (sub right_unit) 1); by (res_inst_tac [("x", "x")] (sub right_inv) 1); -br (sub assoc) 1; -br (sub assoc) 1; -br arg_cong 1; +by (rtac (sub assoc) 1); +by (rtac (sub assoc) 1); +by (rtac arg_cong 1); back(); -br (ssub left_inv) 1; -ba 1; +by (rtac (ssub left_inv) 1); +by (assume_tac 1); qed "one_inv"; goal thy "ALL x. EX! y. y * x = (1::'a::group)"; -br allI 1; -br ex1I 1; -br left_inv 1; -br mp 1; -br one_inv 1; -ba 1; +by (rtac allI 1); +by (rtac ex1I 1); +by (rtac left_inv 1); +by (rtac mp 1); +by (rtac one_inv 1); +by (assume_tac 1); qed "ex1_inv"; goal thy "inv (x * y) = inv y * inv (x::'a::group)"; -br sym 1; -br mp 1; -br one_inv 1; -br (ssub assoc) 1; -br (sub assoc) 1; +by (rtac sym 1); +by (rtac mp 1); +by (rtac one_inv 1); +by (rtac (ssub assoc) 1); +by (rtac (sub assoc) 1); back(); -br (ssub left_inv) 1; -br (ssub left_unit) 1; -br (ssub left_inv) 1; -br refl 1; +by (rtac (ssub left_inv) 1); +by (rtac (ssub left_unit) 1); +by (rtac (ssub left_inv) 1); +by (rtac refl 1); qed "inv_times"; goal thy "inv (inv x) = (x::'a::group)"; -br sym 1; -br (one_inv RS mp) 1; -br (ssub right_inv) 1; -br refl 1; +by (rtac sym 1); +by (rtac (one_inv RS mp) 1); +by (rtac (ssub right_inv) 1); +by (rtac refl 1); qed "inv_inv"; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/AxClasses/Group/GroupDefs.ML --- a/src/HOL/AxClasses/Group/GroupDefs.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/AxClasses/Group/GroupDefs.ML Tue Jan 30 15:24:36 1996 +0100 @@ -37,12 +37,12 @@ goalw thy [times_prod_def, one_prod_def] "1 * x = (x::'a::monoid*'b::monoid)"; by (simp_tac (prod_ss addsimps [Monoid.left_unit]) 1); -br (surjective_pairing RS sym) 1; +by (rtac (surjective_pairing RS sym) 1); qed "prod_left_unit"; goalw thy [times_prod_def, one_prod_def] "x * 1 = (x::'a::monoid*'b::monoid)"; by (simp_tac (prod_ss addsimps [Monoid.right_unit]) 1); -br (surjective_pairing RS sym) 1; +by (rtac (surjective_pairing RS sym) 1); qed "prod_right_unit"; goalw thy [times_prod_def, inv_prod_def, one_prod_def] "inv x * x = (1::'a::group*'b::group)"; @@ -58,30 +58,30 @@ goalw thy [times_fun_def] "(x * y) * z = x * (y * (z::'a => 'b::semigroup))"; by (stac expand_fun_eq 1); -br allI 1; -br assoc 1; +by (rtac allI 1); +by (rtac assoc 1); qed "fun_assoc"; goalw thy [times_fun_def, one_fun_def] "1 * x = (x::'a => 'b::monoid)"; by (stac expand_fun_eq 1); -br allI 1; -br Monoid.left_unit 1; +by (rtac allI 1); +by (rtac Monoid.left_unit 1); qed "fun_left_unit"; goalw thy [times_fun_def, one_fun_def] "x * 1 = (x::'a => 'b::monoid)"; by (stac expand_fun_eq 1); -br allI 1; -br Monoid.right_unit 1; +by (rtac allI 1); +by (rtac Monoid.right_unit 1); qed "fun_right_unit"; goalw thy [times_fun_def, inv_fun_def, one_fun_def] "inv x * x = (1::'a => 'b::group)"; by (stac expand_fun_eq 1); -br allI 1; -br left_inv 1; +by (rtac allI 1); +by (rtac left_inv 1); qed "fun_left_inv"; goalw thy [times_fun_def] "x * y = y * (x::'a => 'b::agroup)"; by (stac expand_fun_eq 1); -br allI 1; -br commut 1; +by (rtac allI 1); +by (rtac commut 1); qed "fun_commut"; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/AxClasses/Lattice/CLattice.ML --- a/src/HOL/AxClasses/Lattice/CLattice.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/AxClasses/Lattice/CLattice.ML Tue Jan 30 15:24:36 1996 +0100 @@ -56,14 +56,14 @@ by (cut_facts_tac prems 1); br selectI2 1; br Inf_is_Inf 1; - by (rewrite_goals_tac [is_Inf_def]); + by (rewtac is_Inf_def); by (fast_tac set_cs 1); qed "Inf_lb"; val [prem] = goalw thy [Inf_def] "(!!x. x:A ==> z [= x) ==> z [= Inf A"; br selectI2 1; br Inf_is_Inf 1; - by (rewrite_goals_tac [is_Inf_def]); + by (rewtac is_Inf_def); by (step_tac HOL_cs 1); by (step_tac HOL_cs 1); be mp 1; @@ -76,14 +76,14 @@ by (cut_facts_tac prems 1); br selectI2 1; br Sup_is_Sup 1; - by (rewrite_goals_tac [is_Sup_def]); + by (rewtac is_Sup_def); by (fast_tac set_cs 1); qed "Sup_ub"; val [prem] = goalw thy [Sup_def] "(!!x. x:A ==> x [= z) ==> Sup A [= z"; br selectI2 1; br Sup_is_Sup 1; - by (rewrite_goals_tac [is_Sup_def]); + by (rewtac is_Sup_def); by (step_tac HOL_cs 1); by (step_tac HOL_cs 1); be mp 1; @@ -126,7 +126,7 @@ goal thy "A <= B --> Inf B [= Inf A"; br impI 1; by (stac le_Inf_eq 1); - by (rewrite_goals_tac [Ball_def]); + by (rewtac Ball_def); by (safe_tac set_cs); bd subsetD 1; ba 1; @@ -136,7 +136,7 @@ goal thy "A <= B --> Sup A [= Sup B"; br impI 1; by (stac ge_Sup_eq 1); - by (rewrite_goals_tac [Ball_def]); + by (rewtac Ball_def); by (safe_tac set_cs); bd subsetD 1; ba 1; @@ -148,7 +148,7 @@ goal thy "Inf {x} = x"; br (Inf_uniq RS mp) 1; - by (rewrite_goals_tac [is_Inf_def]); + by (rewtac is_Inf_def); by (safe_tac set_cs); br le_refl 1; by (fast_tac set_cs 1); @@ -156,7 +156,7 @@ goal thy "Sup {x} = x"; br (Sup_uniq RS mp) 1; - by (rewrite_goals_tac [is_Sup_def]); + by (rewtac is_Sup_def); by (safe_tac set_cs); br le_refl 1; by (fast_tac set_cs 1); @@ -165,7 +165,7 @@ goal thy "Inf {} = Sup {x. True}"; br (Inf_uniq RS mp) 1; - by (rewrite_goals_tac [is_Inf_def]); + by (rewtac is_Inf_def); by (safe_tac set_cs); br (sing_Sup_eq RS subst) 1; back(); @@ -175,7 +175,7 @@ goal thy "Sup {} = Inf {x. True}"; br (Sup_uniq RS mp) 1; - by (rewrite_goals_tac [is_Sup_def]); + by (rewtac is_Sup_def); by (safe_tac set_cs); br (sing_Inf_eq RS subst) 1; br (Inf_subset_antimon RS mp) 1; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/AxClasses/Lattice/LatInsts.ML --- a/src/HOL/AxClasses/Lattice/LatInsts.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/AxClasses/Lattice/LatInsts.ML Tue Jan 30 15:24:36 1996 +0100 @@ -20,7 +20,7 @@ goal thy "Inf (A Un B) = Inf A && Inf B"; br (Inf_uniq RS mp) 1; - by (rewrite_goals_tac [is_Inf_def]); + by (rewtac is_Inf_def); by (safe_tac set_cs); br (conjI RS (le_trans RS mp)) 1; @@ -41,7 +41,7 @@ goal thy "Inf (UN i:A. B i) = Inf {Inf (B i) |i. i:A}"; br (Inf_uniq RS mp) 1; - by (rewrite_goals_tac [is_Inf_def]); + by (rewtac is_Inf_def); by (safe_tac set_cs); (*level 3*) br (conjI RS (le_trans RS mp)) 1; @@ -60,7 +60,7 @@ goal thy "Sup (A Un B) = Sup A || Sup B"; br (Sup_uniq RS mp) 1; - by (rewrite_goals_tac [is_Sup_def]); + by (rewtac is_Sup_def); by (safe_tac set_cs); br (conjI RS (le_trans RS mp)) 1; @@ -81,7 +81,7 @@ goal thy "Sup (UN i:A. B i) = Sup {Sup (B i) |i. i:A}"; br (Sup_uniq RS mp) 1; - by (rewrite_goals_tac [is_Sup_def]); + by (rewtac is_Sup_def); by (safe_tac set_cs); (*level 3*) br (conjI RS (le_trans RS mp)) 1; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/AxClasses/Lattice/Lattice.ML --- a/src/HOL/AxClasses/Lattice/Lattice.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/AxClasses/Lattice/Lattice.ML Tue Jan 30 15:24:36 1996 +0100 @@ -102,7 +102,7 @@ br inf_lb2 1; (*<==*) br (inf_uniq RS mp) 1; - by (rewrite_goals_tac [is_inf_def]); + by (rewtac is_inf_def); by (REPEAT_FIRST (rtac conjI)); br le_refl 1; ba 1; @@ -116,7 +116,7 @@ br sup_ub1 1; (*<==*) br (sup_uniq RS mp) 1; - by (rewrite_goals_tac [is_sup_def]); + by (rewtac is_sup_def); by (REPEAT_FIRST (rtac conjI)); ba 1; br le_refl 1; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/AxClasses/Lattice/OrdDefs.ML --- a/src/HOL/AxClasses/Lattice/OrdDefs.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/AxClasses/Lattice/OrdDefs.ML Tue Jan 30 15:24:36 1996 +0100 @@ -58,7 +58,7 @@ (*"'a dual" is even an isotype*) goal thy "Rep_dual (Abs_dual y) = y"; br Abs_dual_inverse 1; - by (rewrite_goals_tac [dual_def]); + by (rewtac dual_def); by (fast_tac set_cs 1); qed "Abs_dual_inverse'"; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/AxClasses/Tutorial/Group.ML --- a/src/HOL/AxClasses/Tutorial/Group.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/AxClasses/Tutorial/Group.ML Tue Jan 30 15:24:36 1996 +0100 @@ -12,107 +12,107 @@ goal Group.thy "x <*> inv x = (1::'a::group)"; -br (sub left_unit) 1; +by (rtac (sub left_unit) 1); back(); -br (sub assoc) 1; -br (sub left_inv) 1; +by (rtac (sub assoc) 1); +by (rtac (sub left_inv) 1); back(); back(); -br (ssub assoc) 1; +by (rtac (ssub assoc) 1); back(); -br (ssub left_inv) 1; -br (ssub assoc) 1; -br (ssub left_unit) 1; -br (ssub left_inv) 1; -br refl 1; +by (rtac (ssub left_inv) 1); +by (rtac (ssub assoc) 1); +by (rtac (ssub left_unit) 1); +by (rtac (ssub left_inv) 1); +by (rtac refl 1); qed "right_inv"; goal Group.thy "x <*> 1 = (x::'a::group)"; -br (sub left_inv) 1; -br (sub assoc) 1; -br (ssub right_inv) 1; -br (ssub left_unit) 1; -br refl 1; +by (rtac (sub left_inv) 1); +by (rtac (sub assoc) 1); +by (rtac (ssub right_inv) 1); +by (rtac (ssub left_unit) 1); +by (rtac refl 1); qed "right_unit"; goal Group.thy "e <*> x = x --> e = (1::'a::group)"; -br impI 1; -br (sub right_unit) 1; +by (rtac impI 1); +by (rtac (sub right_unit) 1); back(); by (res_inst_tac [("x", "x")] (sub right_inv) 1); -br (sub assoc) 1; -br arg_cong 1; +by (rtac (sub assoc) 1); +by (rtac arg_cong 1); back(); -ba 1; +by (assume_tac 1); qed "strong_one_unit"; goal Group.thy "EX! e. ALL x. e <*> x = (x::'a::group)"; -br ex1I 1; -br allI 1; -br left_unit 1; -br mp 1; -br strong_one_unit 1; -be allE 1; -ba 1; +by (rtac ex1I 1); +by (rtac allI 1); +by (rtac left_unit 1); +by (rtac mp 1); +by (rtac strong_one_unit 1); +by (etac allE 1); +by (assume_tac 1); qed "ex1_unit"; goal Group.thy "ALL x. EX! e. e <*> x = (x::'a::group)"; -br allI 1; -br ex1I 1; -br left_unit 1; -br (strong_one_unit RS mp) 1; -ba 1; +by (rtac allI 1); +by (rtac ex1I 1); +by (rtac left_unit 1); +by (rtac (strong_one_unit RS mp) 1); +by (assume_tac 1); qed "ex1_unit'"; goal Group.thy "y <*> x = 1 --> y = inv (x::'a::group)"; -br impI 1; -br (sub right_unit) 1; +by (rtac impI 1); +by (rtac (sub right_unit) 1); back(); back(); -br (sub right_unit) 1; +by (rtac (sub right_unit) 1); by (res_inst_tac [("x", "x")] (sub right_inv) 1); -br (sub assoc) 1; -br (sub assoc) 1; -br arg_cong 1; +by (rtac (sub assoc) 1); +by (rtac (sub assoc) 1); +by (rtac arg_cong 1); back(); -br (ssub left_inv) 1; -ba 1; +by (rtac (ssub left_inv) 1); +by (assume_tac 1); qed "one_inv"; goal Group.thy "ALL x. EX! y. y <*> x = (1::'a::group)"; -br allI 1; -br ex1I 1; -br left_inv 1; -br mp 1; -br one_inv 1; -ba 1; +by (rtac allI 1); +by (rtac ex1I 1); +by (rtac left_inv 1); +by (rtac mp 1); +by (rtac one_inv 1); +by (assume_tac 1); qed "ex1_inv"; goal Group.thy "inv (x <*> y) = inv y <*> inv (x::'a::group)"; -br sym 1; -br mp 1; -br one_inv 1; -br (ssub assoc) 1; -br (sub assoc) 1; +by (rtac sym 1); +by (rtac mp 1); +by (rtac one_inv 1); +by (rtac (ssub assoc) 1); +by (rtac (sub assoc) 1); back(); -br (ssub left_inv) 1; -br (ssub left_unit) 1; -br (ssub left_inv) 1; -br refl 1; +by (rtac (ssub left_inv) 1); +by (rtac (ssub left_unit) 1); +by (rtac (ssub left_inv) 1); +by (rtac refl 1); qed "inv_product"; goal Group.thy "inv (inv x) = (x::'a::group)"; -br sym 1; -br (one_inv RS mp) 1; -br (ssub right_inv) 1; -br refl 1; +by (rtac sym 1); +by (rtac (one_inv RS mp) 1); +by (rtac (ssub right_inv) 1); +by (rtac refl 1); qed "inv_inv"; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Finite.ML --- a/src/HOL/Finite.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Finite.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/Finite.thy +(* Title: HOL/Finite.thy ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge Finite powerset operator @@ -9,7 +9,7 @@ open Finite; goalw Finite.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)"; -br lfp_mono 1; +by (rtac lfp_mono 1); by (REPEAT (ares_tac basic_monos 1)); qed "Fin_mono"; @@ -23,7 +23,7 @@ (*Discharging ~ x:y entails extra work*) val major::prems = goal Finite.thy "[| F:Fin(A); P({}); \ -\ !!F x. [| x:A; F:Fin(A); x~:F; P(F) |] ==> P(insert x F) \ +\ !!F x. [| x:A; F:Fin(A); x~:F; P(F) |] ==> P(insert x F) \ \ |] ==> P(F)"; by (rtac (major RS Fin.induct) 1); by (excluded_middle_tac "a:b" 2); @@ -45,8 +45,8 @@ (*Every subset of a finite set is finite*) val [subs,fin] = goal Finite.thy "[| A<=B; B: Fin(M) |] ==> A: Fin(M)"; by (EVERY1 [subgoal_tac "ALL C. C<=B --> C: Fin(M)", - rtac mp, etac spec, - rtac subs]); + rtac mp, etac spec, + rtac subs]); by (rtac (fin RS Fin_induct) 1); by (simp_tac (!simpset addsimps [subset_Un_eq]) 1); by (safe_tac (set_cs addSDs [subset_insert_iff RS iffD1])); @@ -64,8 +64,8 @@ qed "Fin_imageI"; val major::prems = goal Finite.thy - "[| c: Fin(A); b: Fin(A); \ -\ P(b); \ + "[| c: Fin(A); b: Fin(A); \ +\ P(b); \ \ !!(x::'a) y. [| x:A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) \ \ |] ==> c<=b --> P(b-c)"; by (rtac (major RS Fin_induct) 1); @@ -75,8 +75,8 @@ qed "Fin_empty_induct_lemma"; val prems = goal Finite.thy - "[| b: Fin(A); \ -\ P(b); \ + "[| b: Fin(A); \ +\ P(b); \ \ !!x y. [| x:A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) \ \ |] ==> P({})"; by (rtac (Diff_cancel RS subst) 1); diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Fun.ML --- a/src/HOL/Fun.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Fun.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/Fun +(* Title: HOL/Fun ID: $Id$ - Author: Tobias Nipkow, Cambridge University Computer Laboratory + Author: Tobias Nipkow, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge Lemmas about functions. @@ -166,7 +166,7 @@ "[| inj(f); A<=range(f) |] ==> inj_onto (Inv f) A"; by (cut_facts_tac prems 1); by (fast_tac (HOL_cs addIs [inj_ontoI] - addEs [Inv_injective,injD,subsetD]) 1); + addEs [Inv_injective,injD,subsetD]) 1); qed "inj_onto_Inv"; @@ -174,12 +174,12 @@ val set_cs = HOL_cs addSIs [ballI, PowI, subsetI, InterI, INT_I, INT1_I, CollectI, - ComplI, IntI, DiffI, UnCI, insertCI] + ComplI, IntI, DiffI, UnCI, insertCI] addIs [bexI, UnionI, UN_I, UN1_I, imageI, rangeI] addSEs [bexE, make_elim PowD, UnionE, UN_E, UN1_E, DiffE, - CollectE, ComplE, IntE, UnE, insertE, imageE, rangeE, emptyE] + CollectE, ComplE, IntE, UnE, insertE, imageE, rangeE, emptyE] addEs [ballE, InterD, InterE, INT_D, INT_E, make_elim INT1_D, - subsetD, subsetCE]; + subsetD, subsetCE]; fun cfast_tac prems = cut_facts_tac prems THEN' fast_tac set_cs; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Gfp.ML --- a/src/HOL/Gfp.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Gfp.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/gfp +(* Title: HOL/gfp ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge For gfp.thy. The Knaster-Tarski Theorem for greatest fixed points. @@ -25,12 +25,12 @@ val [mono] = goal Gfp.thy "mono(f) ==> gfp(f) <= f(gfp(f))"; by (EVERY1 [rtac gfp_least, rtac subset_trans, atac, - rtac (mono RS monoD), rtac gfp_upperbound, atac]); + rtac (mono RS monoD), rtac gfp_upperbound, atac]); qed "gfp_lemma2"; val [mono] = goal Gfp.thy "mono(f) ==> f(gfp(f)) <= gfp(f)"; by (EVERY1 [rtac gfp_upperbound, rtac (mono RS monoD), - rtac gfp_lemma2, rtac mono]); + rtac gfp_lemma2, rtac mono]); qed "gfp_lemma3"; val [mono] = goal Gfp.thy "mono(f) ==> gfp(f) = f(gfp(f))"; @@ -64,8 +64,8 @@ val [mono,prem] = goal Gfp.thy "[| mono(f); a: gfp(f) |] ==> a: f(X Un gfp(f))"; -br (mono RS mono_Un RS subsetD) 1; -br (mono RS gfp_lemma2 RS subsetD RS UnI2) 1; +by (rtac (mono RS mono_Un RS subsetD) 1); +by (rtac (mono RS gfp_lemma2 RS subsetD RS UnI2) 1); by (rtac prem 1); qed "gfp_fun_UnI2"; @@ -140,6 +140,6 @@ (*Monotonicity of gfp!*) val [prem] = goal Gfp.thy "[| !!Z. f(Z)<=g(Z) |] ==> gfp(f) <= gfp(g)"; -br (gfp_upperbound RS gfp_least) 1; -be (prem RSN (2,subset_trans)) 1; +by (rtac (gfp_upperbound RS gfp_least) 1); +by (etac (prem RSN (2,subset_trans)) 1); qed "gfp_mono"; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/HOL.ML --- a/src/HOL/HOL.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/HOL.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,9 +1,9 @@ -(* Title: HOL/HOL.ML +(* Title: HOL/HOL.ML ID: $Id$ - Author: Tobias Nipkow + Author: Tobias Nipkow Copyright 1991 University of Cambridge -For hol.thy +For HOL.thy Derived rules from Appendix of Mike Gordons HOL Report, Cambridge TR 68 *) @@ -20,12 +20,12 @@ qed_goal "trans" HOL.thy "[| r=s; s=t |] ==> r=t" (fn prems => - [rtac subst 1, resolve_tac prems 1, resolve_tac prems 1]); + [rtac subst 1, resolve_tac prems 1, resolve_tac prems 1]); (*Useful with eresolve_tac for proving equalties from known equalities. - a = b - | | - c = d *) + a = b + | | + c = d *) qed_goal "box_equals" HOL.thy "[| a=b; a=c; b=d |] ==> c=d" (fn prems=> @@ -57,7 +57,7 @@ qed_goal "iffD2" HOL.thy "[| P=Q; Q |] ==> P" (fn prems => - [rtac ssubst 1, resolve_tac prems 1, resolve_tac prems 1]); + [rtac ssubst 1, resolve_tac prems 1, resolve_tac prems 1]); val iffD1 = sym RS iffD2; @@ -160,8 +160,8 @@ qed_goal "conjE" HOL.thy "[| P&Q; [| P; Q |] ==> R |] ==> R" (fn prems => - [cut_facts_tac prems 1, resolve_tac prems 1, - etac conjunct1 1, etac conjunct2 1]); + [cut_facts_tac prems 1, resolve_tac prems 1, + etac conjunct1 1, etac conjunct2 1]); (** Disjunction *) @@ -173,8 +173,8 @@ qed_goalw "disjE" HOL.thy [or_def] "[| P | Q; P ==> R; Q ==> R |] ==> R" (fn [a1,a2,a3] => - [rtac (mp RS mp) 1, rtac spec 1, rtac a1 1, - rtac (a2 RS impI) 1, assume_tac 1, rtac (a3 RS impI) 1, assume_tac 1]); + [rtac (mp RS mp) 1, rtac spec 1, rtac a1 1, + rtac (a2 RS impI) 1, assume_tac 1, rtac (a3 RS impI) 1, assume_tac 1]); (** CCONTR -- classical logic **) @@ -211,13 +211,13 @@ qed_goal "selectI2" HOL.thy "[| P(a); !!x. P(x) ==> Q(x) |] ==> Q(@x.P(x))" (fn prems => [ resolve_tac prems 1, - rtac selectI 1, - resolve_tac prems 1 ]); + rtac selectI 1, + resolve_tac prems 1 ]); qed_goal "select_equality" HOL.thy "[| P(a); !!x. P(x) ==> x=a |] ==> (@x.P(x)) = a" (fn prems => [ rtac selectI2 1, - REPEAT (ares_tac prems 1) ]); + REPEAT (ares_tac prems 1) ]); (** Classical intro rules for disjunction and existential quantifiers *) @@ -247,7 +247,7 @@ (fn major::prems => [ (rtac (major RS iffE) 1), (REPEAT (DEPTH_SOLVE_1 - (eresolve_tac ([asm_rl,impCE,notE]@prems) 1))) ]); + (eresolve_tac ([asm_rl,impCE,notE]@prems) 1))) ]); qed_goal "exCI" HOL.thy "(! x. ~P(x) ==> P(a)) ==> ? x.P(x)" (fn prems=> @@ -292,10 +292,10 @@ (*** Applying ClassicalFun to create a classical prover ***) structure Classical_Data = struct - val sizef = size_of_thm - val mp = mp - val not_elim = notE - val classical = classical + val sizef = size_of_thm + val mp = mp + val not_elim = notE + val classical = classical val hyp_subst_tacs=[hyp_subst_tac] end; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Hoare/Arith2.ML --- a/src/HOL/Hoare/Arith2.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Hoare/Arith2.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/Hoare/Arith2.ML +(* Title: HOL/Hoare/Arith2.ML ID: $Id$ - Author: Norbert Galm + Author: Norbert Galm Copyright 1995 TUM More arithmetic lemmas. @@ -30,16 +30,16 @@ \ !!x y z. [| P x y z |] ==> P (Suc x) (Suc y) (Suc z) \ \ |] ==> P m n k"; by (res_inst_tac [("x","m")] spec 1); -br diff_induct 1; -br allI 1; -br allI 2; +by (rtac diff_induct 1); +by (rtac allI 1); +by (rtac allI 2); by (res_inst_tac [("m","xa"),("n","x")] diff_induct 1); by (res_inst_tac [("m","x"),("n","Suc y")] diff_induct 4); -br allI 7; +by (rtac allI 7); by (nat_ind_tac "xa" 7); by (ALLGOALS (resolve_tac prems)); -ba 1; -ba 1; +by (assume_tac 1); +by (assume_tac 1); by (fast_tac HOL_cs 1); by (fast_tac HOL_cs 1); qed "diff_induct3"; @@ -48,33 +48,33 @@ val prems=goal Arith.thy "~m (m - n) - k = m - ((n + k)::nat)"; by (cut_facts_tac prems 1); -br mp 1; -ba 2; +by (rtac mp 1); +by (assume_tac 2); by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); by (ALLGOALS Asm_simp_tac); qed "diff_not_assoc"; val prems=goal Arith.thy "[|~m (m - n) + k = m - ((n - k)::nat)"; by (cut_facts_tac prems 1); -bd conjI 1; -ba 1; +by (dtac conjI 1); +by (assume_tac 1); by (res_inst_tac [("P","~m (m + n) - k = m + ((n - k)::nat)"; by (cut_facts_tac prems 1); -br mp 1; -ba 2; +by (rtac mp 1); +by (assume_tac 2); by (res_inst_tac [("m","n"),("n","k")] diff_induct 1); by (ALLGOALS Asm_simp_tac); qed "add_diff_assoc"; @@ -82,12 +82,12 @@ (*** more ***) val prems = goal Arith.thy "m~=(n::nat) = (m n-m~=0"; @@ -115,7 +115,7 @@ by (res_inst_tac [("n","k")] natE 1); by (ALLGOALS Asm_full_simp_tac); by (nat_ind_tac "x" 1); -be add_less_mono 2; +by (etac add_less_mono 2); by (ALLGOALS Asm_full_simp_tac); qed "mult_less_mono_r"; @@ -124,8 +124,8 @@ by (nat_ind_tac "k" 1); by (ALLGOALS Simp_tac); by (fold_goals_tac [le_def]); -be add_le_mono 1; -ba 1; +by (etac add_le_mono 1); +by (assume_tac 1); qed "mult_not_less_mono_r"; val prems = goal Arith.thy "m=(n::nat) ==> m*k=n*k"; @@ -137,10 +137,10 @@ val prems = goal Arith.thy "[|0 m*k~=n*k"; by (cut_facts_tac prems 1); by (res_inst_tac [("P","m n mod n = 0"; by (cut_facts_tac prems 1); -br (mod_def RS wf_less_trans) 1; +by (rtac (mod_def RS wf_less_trans) 1); by (asm_full_simp_tac ((simpset_of "Arith") addsimps [diff_self_eq_0,cut_def,less_eq]) 1); -be mod_less 1; +by (etac mod_less 1); qed "mod_nn_is_0"; val prems=goal thy "0 m mod n = (m+n) mod n"; by (cut_facts_tac prems 1); by (res_inst_tac [("s","n+m"),("t","m+n")] subst 1); -br add_commute 1; +by (rtac add_commute 1); by (res_inst_tac [("s","n+m-n"),("P","%x.x mod n = (n + m) mod n")] subst 1); -br diff_add_inverse 1; -br sym 1; -be mod_geq 1; +by (rtac diff_add_inverse 1); +by (rtac sym 1); +by (etac mod_geq 1); by (res_inst_tac [("s","n<=n+m"),("t","~n+m m*n mod n = 0"; by (cut_facts_tac prems 1); by (nat_ind_tac "m" 1); by (Simp_tac 1); -be mod_less 1; +by (etac mod_less 1); by (dres_inst_tac [("n","n"),("m","m1*n")] mod_eq_add 1); by (asm_full_simp_tac ((simpset_of "Arith") addsimps [add_commute]) 1); qed "mod_prod_nn_is_0"; @@ -208,25 +208,25 @@ val prems=goal thy "[|0 (m+n) mod x = 0"; by (cut_facts_tac prems 1); by (res_inst_tac [("s","m div x * x + m mod x"),("t","m")] subst 1); -be mod_div_equality 1; +by (etac mod_div_equality 1); by (res_inst_tac [("s","n div x * x + n mod x"),("t","n")] subst 1); -be mod_div_equality 1; +by (etac mod_div_equality 1); by (Asm_simp_tac 1); by (res_inst_tac [("s","(m div x + n div x) * x"),("t","m div x * x + n div x * x")] subst 1); -br add_mult_distrib 1; -be mod_prod_nn_is_0 1; +by (rtac add_mult_distrib 1); +by (etac mod_prod_nn_is_0 1); qed "mod0_sum"; val prems=goal thy "[|0 (m-n) mod x = 0"; by (cut_facts_tac prems 1); by (res_inst_tac [("s","m div x * x + m mod x"),("t","m")] subst 1); -be mod_div_equality 1; +by (etac mod_div_equality 1); by (res_inst_tac [("s","n div x * x + n mod x"),("t","n")] subst 1); -be mod_div_equality 1; +by (etac mod_div_equality 1); by (Asm_simp_tac 1); by (res_inst_tac [("s","(m div x - n div x) * x"),("t","m div x * x - n div x * x")] subst 1); -br diff_mult_distrib_r 1; -be mod_prod_nn_is_0 1; +by (rtac diff_mult_distrib_r 1); +by (etac mod_prod_nn_is_0 1); qed "mod0_diff"; @@ -234,11 +234,11 @@ val prems = goal thy "0 m*n div n = m"; by (cut_facts_tac prems 1); -br (mult_not_eq_mono_r RS not_imp_swap) 1; -ba 1; -ba 1; +by (rtac (mult_not_eq_mono_r RS not_imp_swap) 1); +by (assume_tac 1); +by (assume_tac 1); by (res_inst_tac [("P","%x.m*n div n * n = x")] (mod_div_equality RS subst) 1); -ba 1; +by (assume_tac 1); by (dres_inst_tac [("m","m")] mod_prod_nn_is_0 1); by (Asm_simp_tac 1); qed "div_prod_nn_is_m"; @@ -254,32 +254,32 @@ val prems=goalw thy [divides_def] "x divides n ==> x<=n"; by (cut_facts_tac prems 1); -br ((mod_less COMP rev_contrapos) RS (le_def RS meta_eq_to_obj_eq RS iffD2)) 1; +by (rtac ((mod_less COMP rev_contrapos) RS (le_def RS meta_eq_to_obj_eq RS iffD2)) 1); by (Asm_simp_tac 1); -br (less_not_refl2 RS not_sym) 1; +by (rtac (less_not_refl2 RS not_sym) 1); by (Asm_simp_tac 1); qed "divides_le"; val prems=goalw thy [divides_def] "[|x divides m; x divides n|] ==> x divides (m+n)"; by (cut_facts_tac prems 1); by (REPEAT ((dtac conjE 1) THEN (atac 2))); -br conjI 1; +by (rtac conjI 1); by (dres_inst_tac [("m","0"),("n","m")] less_imp_add_less 1); -ba 1; -be conjI 1; -br mod0_sum 1; +by (assume_tac 1); +by (etac conjI 1); +by (rtac mod0_sum 1); by (ALLGOALS atac); qed "divides_sum"; val prems=goalw thy [divides_def] "[|x divides m; x divides n; n x divides (m-n)"; by (cut_facts_tac prems 1); by (REPEAT ((dtac conjE 1) THEN (atac 2))); -br conjI 1; -be less_imp_diff_positive 1; -be conjI 1; -br mod0_diff 1; +by (rtac conjI 1); +by (etac less_imp_diff_positive 1); +by (etac conjI 1); +by (rtac mod0_diff 1); by (ALLGOALS (asm_simp_tac ((simpset_of "Arith") addsimps [le_def]))); -be less_not_sym 1; +by (etac less_not_sym 1); qed "divides_diff"; @@ -288,16 +288,16 @@ val prems=goalw thy [cd_def] "0 cd n n n"; by (cut_facts_tac prems 1); -bd divides_nn 1; +by (dtac divides_nn 1); by (Asm_simp_tac 1); qed "cd_nnn"; val prems=goalw thy [cd_def] "cd x m n ==> x<=m & x<=n"; by (cut_facts_tac prems 1); -bd conjE 1; -ba 2; -bd divides_le 1; -bd divides_le 1; +by (dtac conjE 1); +by (assume_tac 2); +by (dtac divides_le 1); +by (dtac divides_le 1); by (Asm_simp_tac 1); qed "cd_le"; @@ -307,32 +307,32 @@ val prems=goalw thy [cd_def] "n cd x m n = cd x (m-n) n"; by (cut_facts_tac prems 1); -br iffI 1; -bd conjE 1; -ba 2; -br conjI 1; -br divides_diff 1; -bd conjE 5; -ba 6; -br conjI 5; -bd less_not_sym 5; -bd add_diff_inverse 5; +by (rtac iffI 1); +by (dtac conjE 1); +by (assume_tac 2); +by (rtac conjI 1); +by (rtac divides_diff 1); +by (dtac conjE 5); +by (assume_tac 6); +by (rtac conjI 5); +by (dtac less_not_sym 5); +by (dtac add_diff_inverse 5); by (dres_inst_tac [("m","n"),("n","m-n")] divides_sum 5); by (ALLGOALS Asm_full_simp_tac); qed "cd_diff_l"; val prems=goalw thy [cd_def] "m cd x m n = cd x m (n-m)"; by (cut_facts_tac prems 1); -br iffI 1; -bd conjE 1; -ba 2; -br conjI 1; -br divides_diff 2; -bd conjE 5; -ba 6; -br conjI 5; -bd less_not_sym 6; -bd add_diff_inverse 6; +by (rtac iffI 1); +by (dtac conjE 1); +by (assume_tac 2); +by (rtac conjI 1); +by (rtac divides_diff 2); +by (dtac conjE 5); +by (assume_tac 6); +by (rtac conjI 5); +by (dtac less_not_sym 6); +by (dtac add_diff_inverse 6); by (dres_inst_tac [("n","n-m")] divides_sum 6); by (ALLGOALS Asm_full_simp_tac); qed "cd_diff_r"; @@ -342,15 +342,15 @@ val prems = goalw thy [gcd_def] "0 n = gcd n n"; by (cut_facts_tac prems 1); -bd cd_nnn 1; -br (select_equality RS sym) 1; -be conjI 1; -br allI 1; -br impI 1; -bd cd_le 1; -bd conjE 2; -ba 3; -br le_anti_sym 2; +by (dtac cd_nnn 1); +by (rtac (select_equality RS sym) 1); +by (etac conjI 1); +by (rtac allI 1); +by (rtac impI 1); +by (dtac cd_le 1); +by (dtac conjE 2); +by (assume_tac 3); +by (rtac le_anti_sym 2); by (dres_inst_tac [("x","x")] cd_le 2); by (dres_inst_tac [("x","n")] spec 3); by (ALLGOALS Asm_full_simp_tac); @@ -364,16 +364,16 @@ by (cut_facts_tac prems 1); by (subgoal_tac "n !x.cd x m n = cd x (m-n) n" 1); by (Asm_simp_tac 1); -br allI 1; -be cd_diff_l 1; +by (rtac allI 1); +by (etac cd_diff_l 1); qed "gcd_diff_l"; val prems=goalw thy [gcd_def] "m gcd m n = gcd m (n-m)"; by (cut_facts_tac prems 1); by (subgoal_tac "m !x.cd x m n = cd x m (n-m)" 1); by (Asm_simp_tac 1); -br allI 1; -be cd_diff_r 1; +by (rtac allI 1); +by (etac cd_diff_r 1); qed "gcd_diff_r"; @@ -392,7 +392,7 @@ by (nat_ind_tac "k" 1); by (ALLGOALS Asm_simp_tac); by (fold_goals_tac [pow_def]); -br (pow_add_reduce RS sym) 1; +by (rtac (pow_add_reduce RS sym) 1); qed "pow_pow_reduce"; (*** fac ***) diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Hoare/Examples.ML --- a/src/HOL/Hoare/Examples.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Hoare/Examples.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/Hoare/Examples.thy +(* Title: HOL/Hoare/Examples.thy ID: $Id$ - Author: Norbert Galm + Author: Norbert Galm Copyright 1995 TUM Various arithmetic examples. @@ -38,15 +38,15 @@ by (safe_tac HOL_cs); -be less_imp_diff_positive 1; -be gcd_diff_r 1; +by (etac less_imp_diff_positive 1); +by (etac gcd_diff_r 1); by (cut_facts_tac [less_linear] 1); by (cut_facts_tac [less_linear] 2); -br less_imp_diff_positive 1; -br gcd_diff_l 2; +by (rtac less_imp_diff_positive 1); +by (rtac gcd_diff_l 2); -bd gcd_nnn 3; +by (dtac gcd_nnn 3); by (ALLGOALS (fast_tac HOL_cs)); @@ -78,7 +78,7 @@ by (subgoal_tac "a*a=a pow 2" 1); by (Asm_simp_tac 1); -br (pow_pow_reduce RS ssubst) 1; +by (rtac (pow_pow_reduce RS ssubst) 1); by (subgoal_tac "(b div 2)*2=b" 1); by (subgoal_tac "0<2" 2); @@ -89,10 +89,10 @@ by (subgoal_tac "b~=0" 1); by (res_inst_tac [("n","b")] natE 1); by (res_inst_tac [("Q","b mod 2 ~= 0")] not_imp_swap 3); -ba 4; +by (assume_tac 4); by (ALLGOALS (asm_full_simp_tac ((simpset_of "Arith") addsimps [pow_0,pow_Suc,mult_assoc]))); -br mod_less 1; +by (rtac mod_less 1); by (Simp_tac 1); qed "power_by_mult"; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Hoare/Hoare.ML --- a/src/HOL/Hoare/Hoare.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Hoare/Hoare.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/Hoare/Hoare.ML +(* Title: HOL/Hoare/Hoare.ML ID: $Id$ - Author: Norbert Galm & Tobias Nipkow + Author: Norbert Galm & Tobias Nipkow Copyright 1995 TUM The verification condition generation tactics. @@ -29,14 +29,14 @@ (fn [prem1,prem2,prem3] => [REPEAT (rtac allI 1), REPEAT (rtac impI 1), - dresolve_tac [prem1] 1, + dtac prem1 1, cut_facts_tac [prem2,prem3] 1, fast_tac (HOL_cs addIs [prem1]) 1]); val strenthen_pre = prove_goalw thy [SpecDef] "[| !!s. p s ==> p' s; Spec p' c q |] ==> Spec p c q" (fn [prem1,prem2] =>[cut_facts_tac [prem2] 1, - fast_tac (HOL_cs addIs [prem1]) 1]); + fast_tac (HOL_cs addIs [prem1]) 1]); val [iter_0,iter_Suc] = nat_recs IterDef; @@ -70,31 +70,31 @@ (* rename_abs:term (von:string,nach:string,trm:term) benennt in trm alle Lambda-Abstraktionen mit Namen von in nach um *) -fun rename_abs (von,nach,Abs (s,t,trm)) =if von=s - then Abs (nach,t,rename_abs (von,nach,trm)) - else Abs (s,t,rename_abs (von,nach,trm)) - | rename_abs (von,nach,trm1 $ trm2) =rename_abs (von,nach,trm1) $ rename_abs (von,nach,trm2) - | rename_abs (_,_,trm) =trm; +fun rename_abs (von,nach,Abs (s,t,trm)) =if von=s + then Abs (nach,t,rename_abs (von,nach,trm)) + else Abs (s,t,rename_abs (von,nach,trm)) + | rename_abs (von,nach,trm1 $ trm2) =rename_abs (von,nach,trm1) $ rename_abs (von,nach,trm2) + | rename_abs (_,_,trm) =trm; (* ren_abs_thm:thm (von:string,nach:string,theorem:thm) benennt in theorem alle Lambda-Abstraktionen mit Namen von in nach um. Vorgehen: - - Term t zu thoerem bestimmen - - Term t' zu t durch Umbenennen der Namen generieren - - Certified Term ct' zu t' erstellen - - Thoerem ct'==ct' anlegen - - Nach der Regel "[|P==Q; P|] ==> Q" wird aus "ct'==ct'" und theorem das Theorem zu ct' - abgeleitet (ist moeglich, da t' mit t unifiziert werden kann, da nur Umnbenennungen) *) + - Term t zu thoerem bestimmen + - Term t' zu t durch Umbenennen der Namen generieren + - Certified Term ct' zu t' erstellen + - Thoerem ct'==ct' anlegen + - Nach der Regel "[|P==Q; P|] ==> Q" wird aus "ct'==ct'" und theorem das Theorem zu ct' + abgeleitet (ist moeglich, da t' mit t unifiziert werden kann, da nur Umnbenennungen) *) -fun ren_abs_thm (von,nach,theorem) = - equal_elim - ( - reflexive ( - cterm_of - (#sign (rep_thm theorem)) - (rename_abs (von,nach,#prop (rep_thm theorem))) - ) - ) - theorem; +fun ren_abs_thm (von,nach,theorem) = + equal_elim + ( + reflexive ( + cterm_of + (#sign (rep_thm theorem)) + (rename_abs (von,nach,#prop (rep_thm theorem))) + ) + ) + theorem; (**************************************************************************************************) @@ -107,15 +107,15 @@ (* - rens:(string*string) list, d.h. es koennen verschiedene Lambda-Abstraktionen umbenannt werden - insts:(cterm*cterm) list, d.h. es koennen verschiedene Variablen instanziiert werden *) -fun comp_inst_ren_tac rens insts theorem i = - let - fun compose_inst_ren_tac [] insts theorem i = - compose_tac (false,cterm_instantiate insts theorem,nprems_of theorem) i - | compose_inst_ren_tac ((von,nach)::rl) insts theorem i = - compose_inst_ren_tac rl insts (ren_abs_thm (von,nach,theorem)) i - in - compose_inst_ren_tac rens insts theorem i - end; +fun comp_inst_ren_tac rens insts theorem i = + let + fun compose_inst_ren_tac [] insts theorem i = + compose_tac (false,cterm_instantiate insts theorem,nprems_of theorem) i + | compose_inst_ren_tac ((von,nach)::rl) insts theorem i = + compose_inst_ren_tac rl insts (ren_abs_thm (von,nach,theorem)) i + in + compose_inst_ren_tac rens insts theorem i + end; (**************************************************************************************************) @@ -125,100 +125,100 @@ (* pvars_of_term:term list (name:string,trm:term) gibt die Liste aller Programm-Variablen aus trm zurueck. name gibt dabei den Namen der Zustandsvariablen an. - Bsp.: bei name="s" und dem Term "s(Suc(Suc(0)))=s(0)" (entspricht "c=a") - wird [0,Suc(Suc(0))] geliefert (Liste ist i.A. unsortiert) *) + Bsp.: bei name="s" und dem Term "s(Suc(Suc(0)))=s(0)" (entspricht "c=a") + wird [0,Suc(Suc(0))] geliefert (Liste ist i.A. unsortiert) *) -fun pvars_of_term (name,trm) = - let - fun add_vars (name,Free (s,t) $ trm,vl) =if name=s - then if trm mem vl - then vl - else trm::vl - else add_vars (name,trm,vl) - | add_vars (name,Abs (s,t,trm),vl) =add_vars (name,trm,vl) - | add_vars (name,trm1 $ trm2,vl) =add_vars (name,trm2,add_vars (name,trm1,vl)) - | add_vars (_,_,vl) =vl - in - add_vars (name,trm,[]) - end; +fun pvars_of_term (name,trm) = + let + fun add_vars (name,Free (s,t) $ trm,vl) =if name=s + then if trm mem vl + then vl + else trm::vl + else add_vars (name,trm,vl) + | add_vars (name,Abs (s,t,trm),vl) =add_vars (name,trm,vl) + | add_vars (name,trm1 $ trm2,vl) =add_vars (name,trm2,add_vars (name,trm1,vl)) + | add_vars (_,_,vl) =vl + in + add_vars (name,trm,[]) + end; (* VarsElimTac: Taktik zum Eliminieren von bestimmten Programmvariablen aus dem Subgoal i - - v::vl:(term) list Liste der zu eliminierenden Programmvariablen - - meta_spec:thm Theorem, welches zur Entfernung der Variablen benutzt wird - z.B.: "(!!s x.PROP P(s,x)) ==> (!!s.PROP P(s,x(s)))" - - namexAll:string Name von ^ (hier "x") - - varx:term Term zu ^ (hier Var(("x",0),...)) - - varP:term Term zu ^ (hier Var(("P",0),...)) - - type_pvar:typ Typ der Programmvariablen (d.h. 'a bei 'a prog, z.B.: nat, bool, ...) + - v::vl:(term) list Liste der zu eliminierenden Programmvariablen + - meta_spec:thm Theorem, welches zur Entfernung der Variablen benutzt wird + z.B.: "(!!s x.PROP P(s,x)) ==> (!!s.PROP P(s,x(s)))" + - namexAll:string Name von ^ (hier "x") + - varx:term Term zu ^ (hier Var(("x",0),...)) + - varP:term Term zu ^ (hier Var(("P",0),...)) + - type_pvar:typ Typ der Programmvariablen (d.h. 'a bei 'a prog, z.B.: nat, bool, ...) Vorgehen: - - eliminiere jede pvar durch Anwendung von comp_inst_ren_tac. Dazu: - - Unbenennung in meta_spec: namexAll wird in den Namen der Prog.-Var. umbenannt - z.B.: fuer die Prog.-Var. mit Namen "a" ergibt sich - meta_spec zu "(!! s a.PROP P(s,a)) ==> (!! s.PROP P(s,x(s)))" - - Instanziierungen in meta_spec: - varx wird mit "%s:(type_pvar) state.s(pvar)" instanziiert - varP wird entsprechend instanziiert. Beispiel fuer Prog.-Var. "a": - - zu Subgoal "!!s.s(Suc(0)) = s(0) ==> s(0) = 1" bestimme Term ohne "!!s.": - trm0 = "s(Suc(0)) = s(0) ==> s(0) = 1" (s ist hier freie Variable) - - substituiere alle Vorkommen von s(pvar) durch eine freie Var. xs: - trm1 = "s(Suc(0)) = xs ==> xs = 1" - - abstrahiere ueber xs: - trm2 = "%xs.s(Suc(0)) = xs ==> xs = 1" - - abstrahiere ueber restliche Vorkommen von s: - trm3 = "%s xs.s(Suc(0)) = xs ==> xs = 1" - - instanziiere varP mit trm3 + - eliminiere jede pvar durch Anwendung von comp_inst_ren_tac. Dazu: + - Unbenennung in meta_spec: namexAll wird in den Namen der Prog.-Var. umbenannt + z.B.: fuer die Prog.-Var. mit Namen "a" ergibt sich + meta_spec zu "(!! s a.PROP P(s,a)) ==> (!! s.PROP P(s,x(s)))" + - Instanziierungen in meta_spec: + varx wird mit "%s:(type_pvar) state.s(pvar)" instanziiert + varP wird entsprechend instanziiert. Beispiel fuer Prog.-Var. "a": + - zu Subgoal "!!s.s(Suc(0)) = s(0) ==> s(0) = 1" bestimme Term ohne "!!s.": + trm0 = "s(Suc(0)) = s(0) ==> s(0) = 1" (s ist hier freie Variable) + - substituiere alle Vorkommen von s(pvar) durch eine freie Var. xs: + trm1 = "s(Suc(0)) = xs ==> xs = 1" + - abstrahiere ueber xs: + trm2 = "%xs.s(Suc(0)) = xs ==> xs = 1" + - abstrahiere ueber restliche Vorkommen von s: + trm3 = "%s xs.s(Suc(0)) = xs ==> xs = 1" + - instanziiere varP mit trm3 *) -fun VarsElimTac ([],_,_,_,_,_) i =all_tac - | VarsElimTac (v::vl,meta_spec,namexAll,varx,varP,type_pvar) i = - STATE ( - fn state => - comp_inst_ren_tac - [(namexAll,pvar2pvarID v)] - [( - cterm_of (#sign (rep_thm state)) varx, - cterm_of (#sign (rep_thm state)) ( - Abs ("s",Type ("nat",[]) --> type_pvar,Bound 0 $ v) - ) - ),( - cterm_of (#sign (rep_thm state)) varP, - cterm_of (#sign (rep_thm state)) ( - let - val (_,_,_ $ Abs (_,_,trm),_) = dest_state (state,i); - val (sname,trm0) = variant_abs ("s",dummyT,trm); - val xsname = variant_name ("xs",trm0); - val trm1 = subst_term (Free (sname,dummyT) $ v,Syntax.free xsname,trm0) - val trm2 = Abs ("xs",type_pvar,abstract_over (Syntax.free xsname,trm1)) - in - Abs ("s",Type ("nat",[]) --> type_pvar,abstract_over (Free (sname,dummyT),trm2)) - end - ) - )] - meta_spec i - ) - THEN - (VarsElimTac (vl,meta_spec,namexAll,varx,varP,type_pvar) i); +fun VarsElimTac ([],_,_,_,_,_) i =all_tac + | VarsElimTac (v::vl,meta_spec,namexAll,varx,varP,type_pvar) i = + STATE ( + fn state => + comp_inst_ren_tac + [(namexAll,pvar2pvarID v)] + [( + cterm_of (#sign (rep_thm state)) varx, + cterm_of (#sign (rep_thm state)) ( + Abs ("s",Type ("nat",[]) --> type_pvar,Bound 0 $ v) + ) + ),( + cterm_of (#sign (rep_thm state)) varP, + cterm_of (#sign (rep_thm state)) ( + let + val (_,_,_ $ Abs (_,_,trm),_) = dest_state (state,i); + val (sname,trm0) = variant_abs ("s",dummyT,trm); + val xsname = variant_name ("xs",trm0); + val trm1 = subst_term (Free (sname,dummyT) $ v,Syntax.free xsname,trm0) + val trm2 = Abs ("xs",type_pvar,abstract_over (Syntax.free xsname,trm1)) + in + Abs ("s",Type ("nat",[]) --> type_pvar,abstract_over (Free (sname,dummyT),trm2)) + end + ) + )] + meta_spec i + ) + THEN + (VarsElimTac (vl,meta_spec,namexAll,varx,varP,type_pvar) i); (* StateElimTac: Taktik zum Eliminieren aller Programmvariablen aus dem Subgoal i zur Erinnerung: - - das Subgoal hat vor Anwendung dieser Taktik die Form "!!s:('a) state.P(s)", - d.h. den Term Const("all",_) $ Abs ("s",pvar --> 'a,_) + - das Subgoal hat vor Anwendung dieser Taktik die Form "!!s:('a) state.P(s)", + d.h. den Term Const("all",_) $ Abs ("s",pvar --> 'a,_) - meta_spec hat die Form "(!!s x.PROP P(s,x)) ==> (!!s.PROP P(s,x(s)))" *) -fun StateElimTac i = - STATE ( - fn state => - let - val (_,_,_ $ Abs (_,Type ("fun",[_,type_pvar]),trm),_) = dest_state (state,i); - val _ $ (_ $ Abs (_,_,_ $ Abs (namexAll,_,_))) $ - (_ $ Abs (_,_,varP $ _ $ (varx $ _))) = #prop (rep_thm meta_spec) - in - VarsElimTac (pvars_of_term (variant_abs ("s",dummyT,trm)),meta_spec,namexAll,varx,varP,type_pvar) i - end - ); +fun StateElimTac i = + STATE ( + fn state => + let + val (_,_,_ $ Abs (_,Type ("fun",[_,type_pvar]),trm),_) = dest_state (state,i); + val _ $ (_ $ Abs (_,_,_ $ Abs (namexAll,_,_))) $ + (_ $ Abs (_,_,varP $ _ $ (varx $ _))) = #prop (rep_thm meta_spec) + in + VarsElimTac (pvars_of_term (variant_abs ("s",dummyT,trm)),meta_spec,namexAll,varx,varP,type_pvar) i + end + ); @@ -232,20 +232,20 @@ fun WlpTac i = (rtac SeqRule i) THEN (HoareRuleTac (i+1) false) and HoareRuleTac i pre_cond = STATE(fn state => - ((WlpTac i) THEN (HoareRuleTac i pre_cond)) + ((WlpTac i) THEN (HoareRuleTac i pre_cond)) ORELSE - (FIRST[rtac SkipRule i, - rtac AssignRule i, - EVERY[rtac IfRule i, + (FIRST[rtac SkipRule i, + rtac AssignRule i, + EVERY[rtac IfRule i, HoareRuleTac (i+2) false, HoareRuleTac (i+1) false], - EVERY[rtac WhileRule i, + EVERY[rtac WhileRule i, Asm_full_simp_tac (i+2), HoareRuleTac (i+1) true]] - THEN + THEN (if pre_cond then (Asm_full_simp_tac i) else (atac i)) - ) - ); + ) + ); val HoareTac1 = EVERY[HoareRuleTac 1 true, ALLGOALS StateElimTac, prune_params_tac]; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Hoare/ROOT.ML --- a/src/HOL/Hoare/ROOT.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Hoare/ROOT.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,10 +1,10 @@ -(* Title: HOL/IMP/ROOT.ML +(* Title: HOL/IMP/ROOT.ML ID: $Id$ - Author: Tobias Nipkow + Author: Tobias Nipkow Copyright 1995 TUM *) -HOL_build_completed; (*Make examples fail if HOL did*) +HOL_build_completed; (*Make examples fail if HOL did*) use_thy "Examples"; use_thy "List_Examples"; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/IMP/Com.ML --- a/src/HOL/IMP/Com.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/IMP/Com.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/IMP/Com.ML +(* Title: HOL/IMP/Com.ML ID: $Id$ - Author: Heiko Loetzbeyer & Robert Sandner, TUM + Author: Heiko Loetzbeyer & Robert Sandner, TUM Copyright 1994 TUM *) diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/IMP/Denotation.ML --- a/src/HOL/IMP/Denotation.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/IMP/Denotation.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/IMP/Denotation.ML +(* Title: HOL/IMP/Denotation.ML ID: $Id$ - Author: Heiko Loetzbeyer & Robert Sandner, TUM + Author: Heiko Loetzbeyer & Robert Sandner, TUM Copyright 1994 TUM *) @@ -17,5 +17,5 @@ (**** mono (Gamma(b,c)) ****) qed_goalw "Gamma_mono" Denotation.thy [mono_def,Gamma_def] - "mono (Gamma b c)" + "mono (Gamma b c)" (fn _ => [(best_tac comp_cs 1)]); diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/IMP/Equiv.ML --- a/src/HOL/IMP/Equiv.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/IMP/Equiv.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,12 +1,12 @@ -(* Title: HOL/IMP/Equiv.ML +(* Title: HOL/IMP/Equiv.ML ID: $Id$ - Author: Heiko Loetzbeyer & Robert Sandner, TUM + Author: Heiko Loetzbeyer & Robert Sandner, TUM Copyright 1994 TUM *) goal Equiv.thy "!n. ( -a-> n) = (n = A a s)"; -by (aexp.induct_tac "a" 1); (* struct. ind. *) -by (ALLGOALS Simp_tac); (* rewr. Den. *) +by (aexp.induct_tac "a" 1); (* struct. ind. *) +by (ALLGOALS Simp_tac); (* rewr. Den. *) by (TRYALL (fast_tac (set_cs addSIs (evala.intrs@prems) addSEs evala_elim_cases))); bind_thm("aexp_iff", result() RS spec); @@ -23,7 +23,7 @@ goal Equiv.thy "!!c. -c-> t ==> (s,t) : C(c)"; (* start with rule induction *) -be (evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1; +by (etac (evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1); by (rewrite_tac (Gamma_def::C_simps)); (* simplification with HOL_ss again too agressive *) (* skip *) @@ -52,7 +52,7 @@ (* while *) by (strip_tac 1); by (etac (Gamma_mono RSN (2,induct)) 1); -by (rewrite_goals_tac [Gamma_def]); +by (rewtac Gamma_def); by (fast_tac equiv_cs 1); bind_thm("com2", result() RS spec RS spec RS mp); diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/IMP/Hoare.ML --- a/src/HOL/IMP/Hoare.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/IMP/Hoare.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/IMP/Hoare.ML +(* Title: HOL/IMP/Hoare.ML ID: $Id$ - Author: Tobias Nipkow + Author: Tobias Nipkow Copyright 1995 TUM Soundness of Hoare rules wrt denotational semantics @@ -9,16 +9,16 @@ open Hoare; goalw Hoare.thy [spec_def] "!P c Q. ({{P}}c{{Q}}) --> spec P c Q"; -br hoare.mutual_induct 1; +by (rtac hoare.mutual_induct 1); by(ALLGOALS Asm_simp_tac); by(fast_tac rel_cs 1); by(fast_tac HOL_cs 1); -br allI 1; -br allI 1; -br impI 1; -be induct2 1; +by (rtac allI 1); +by (rtac allI 1); +by (rtac impI 1); +by (etac induct2 1); br Gamma_mono 1; -by (rewrite_goals_tac [Gamma_def]); +by (rewtac Gamma_def); by(eres_inst_tac [("x","a")] allE 1); by (safe_tac comp_cs); by(ALLGOALS Asm_full_simp_tac); diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/IMP/Properties.ML --- a/src/HOL/IMP/Properties.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/IMP/Properties.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/IMP/Properties.ML +(* Title: HOL/IMP/Properties.ML ID: $Id$ - Author: Tobias Nipkow, TUM + Author: Tobias Nipkow, TUM Copyright 1994 TUM IMP is deterministic. @@ -27,7 +27,7 @@ (* evaluation of com is deterministic *) goal Com.thy "!!c. -c-> t ==> !u. -c-> u --> u=t"; (* start with rule induction *) -be (evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1; +by (etac (evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1); by(fast_tac (set_cs addSEs evalc_elim_cases) 1); by(fast_tac (set_cs addSEs evalc_elim_cases addDs [aexp_detD]) 1); by(fast_tac (set_cs addSEs evalc_elim_cases) 1); diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/IMP/ROOT.ML --- a/src/HOL/IMP/ROOT.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/IMP/ROOT.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,10 +1,10 @@ -(* Title: HOL/IMP/ROOT.ML +(* Title: HOL/IMP/ROOT.ML ID: $Id$ - Author: Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow + Author: Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow Copyright 1995 TUM *) -HOL_build_completed; (*Make examples fail if HOL did*) +HOL_build_completed; (*Make examples fail if HOL did*) writeln"Root file for HOL/IMP"; proof_timing := true; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/IMP/VC.ML --- a/src/HOL/IMP/VC.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/IMP/VC.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/IMP/VC.ML +(* Title: HOL/IMP/VC.ML ID: $Id$ - Author: Tobias Nipkow + Author: Tobias Nipkow Copyright 1996 TUM Soundness and completeness of vc @@ -30,7 +30,7 @@ by(fast_tac HOL_cs 1); (* while *) by(safe_tac HOL_cs); -brs hoare.intrs 1; +by (resolve_tac hoare.intrs 1); br lemma 1; brs hoare.intrs 1; brs hoare.intrs 1; @@ -57,7 +57,7 @@ goal VC.thy "!P c Q. ({{P}}c{{Q}}) --> \ \ (? ac. astrip ac = c & (!s. P s --> wp ac Q s) & (!s. vc ac Q s))"; -br hoare.mutual_induct 1; +by (rtac hoare.mutual_induct 1); by(res_inst_tac [("x","Askip")] exI 1); by(Simp_tac 1); by(res_inst_tac [("x","Aass x a")] exI 1); diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/IOA/ABP/Check.ML --- a/src/HOL/IOA/ABP/Check.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/IOA/ABP/Check.ML Tue Jan 30 15:24:36 1996 +0100 @@ -167,4 +167,4 @@ fun nexts s A = [(s+1) mod 5]; -*) \ No newline at end of file +*) diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/IOA/ABP/Correctness.ML --- a/src/HOL/IOA/ABP/Correctness.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/IOA/ABP/Correctness.ML Tue Jan 30 15:24:36 1996 +0100 @@ -184,7 +184,7 @@ by (rtac conjI 1); (* -------------- start states ----------------- *) by (Simp_tac 1); -br ballI 1; +by (rtac ballI 1); by (Asm_full_simp_tac 1); (* ---------------- main-part ------------------- *) by (REPEAT (rtac allI 1)); @@ -229,7 +229,7 @@ by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1); by (rtac conjI 1); (* start states *) -br ballI 1; +by (rtac ballI 1); by (Simp_tac 1); (* main-part *) by (REPEAT (rtac allI 1)); @@ -245,7 +245,7 @@ by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1); by (rtac conjI 1); (* start states *) -br ballI 1; +by (rtac ballI 1); by (Simp_tac 1); (* main-part *) by (REPEAT (rtac allI 1)); @@ -260,7 +260,7 @@ by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1); by (rtac conjI 1); (* start states *) -br ballI 1; +by (rtac ballI 1); by (Simp_tac 1); (* main-part *) by (REPEAT (rtac allI 1)); diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/IOA/ABP/Lemmas.ML --- a/src/HOL/IOA/ABP/Lemmas.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/IOA/ABP/Lemmas.ML Tue Jan 30 15:24:36 1996 +0100 @@ -54,4 +54,4 @@ by (List.list.induct_tac "l" 1); by (simp_tac list_ss 1); by (fast_tac HOL_cs 1); -qed"cons_not_nil"; \ No newline at end of file +qed"cons_not_nil"; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/IOA/NTP/Correctness.ML --- a/src/HOL/IOA/NTP/Correctness.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/IOA/NTP/Correctness.ML Tue Jan 30 15:24:36 1996 +0100 @@ -70,13 +70,13 @@ by(simp_tac (!simpset addsimps [Correctness.hom_def, cancel_restrict,externals_lemma]) 1); -br conjI 1; +by (rtac conjI 1); by(simp_tac ss' 1); -br ballI 1; -bd CollectD 1; +by (rtac ballI 1); +by (dtac CollectD 1); by(asm_simp_tac (!simpset addsimps sels) 1); by(REPEAT(rtac allI 1)); -br imp_conj_lemma 1; (* from lemmas.ML *) +by (rtac imp_conj_lemma 1); (* from lemmas.ML *) by(Action.action.induct_tac "a" 1); by(asm_simp_tac (ss' setloop (split_tac [expand_if])) 1); @@ -94,13 +94,13 @@ by(asm_simp_tac ss' 1); by(forward_tac [inv4] 1); by(forward_tac [inv2] 1); -be disjE 1; +by (etac disjE 1); by(Asm_simp_tac 1); by(asm_full_simp_tac (!simpset addsimps [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1); by(asm_simp_tac ss' 1); by(forward_tac [inv2] 1); -be disjE 1; +by (etac disjE 1); by(forward_tac [inv3] 1); by(case_tac "sq(sen(s))=[]" 1); diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/IOA/NTP/Impl.ML --- a/src/HOL/IOA/NTP/Impl.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/IOA/NTP/Impl.ML Tue Jan 30 15:24:36 1996 +0100 @@ -71,7 +71,7 @@ (* INVARIANT 1 *) goalw Impl.thy impl_ioas "invariant impl_ioa inv1"; -br invariantI 1; +by (rtac invariantI 1); by(asm_full_simp_tac (!simpset addsimps [inv1_def, hdr_sum_def, Sender.srcvd_def, Sender.ssent_def, Receiver.rsent_def,Receiver.rrcvd_def]) 1); @@ -84,7 +84,7 @@ (* First half *) by(asm_full_simp_tac (!simpset addsimps [Impl.inv1_def]) 1); -br Action.action.induct 1; +by (rtac Action.action.induct 1); by (EVERY1[tac, tac, tac, tac]); by (tac 1); @@ -101,7 +101,7 @@ (* Now the other half *) by(asm_full_simp_tac (!simpset addsimps [Impl.inv1_def]) 1); -br Action.action.induct 1; +by (rtac Action.action.induct 1); by(EVERY1[tac, tac]); (* detour 1 *) @@ -132,7 +132,7 @@ by (rtac (pred_suc RS mp RS sym RS iffD2) 1); by (dtac less_le_trans 1); by (cut_facts_tac [rewrite_rule[Packet.hdr_def] - eq_packet_imp_eq_hdr RS countm_props] 1);; + eq_packet_imp_eq_hdr RS countm_props] 1);; by (assume_tac 1); by (assume_tac 1); diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/IOA/NTP/Lemmas.ML --- a/src/HOL/IOA/NTP/Lemmas.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/IOA/NTP/Lemmas.ML Tue Jan 30 15:24:36 1996 +0100 @@ -211,5 +211,4 @@ qed "not_hd_append"; - -Addsimps ([append_cons,not_hd_append,Suc_pred_lemma] @ set_lemmas); \ No newline at end of file +Addsimps ([append_cons,not_hd_append,Suc_pred_lemma] @ set_lemmas); diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/IOA/NTP/Multiset.ML --- a/src/HOL/IOA/NTP/Multiset.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/IOA/NTP/Multiset.ML Tue Jan 30 15:24:36 1996 +0100 @@ -84,4 +84,4 @@ Addsimps [count_addm_simp, count_delm_simp, Multiset.countm_empty_def, Multiset.delm_empty_def, - count_empty]; \ No newline at end of file + count_empty]; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/IOA/meta_theory/Asig.ML --- a/src/HOL/IOA/meta_theory/Asig.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/IOA/meta_theory/Asig.ML Tue Jan 30 15:24:36 1996 +0100 @@ -16,4 +16,4 @@ goal Asig.thy "!!a.[|a:externals(S)|] ==> a:actions(S)"; by (asm_full_simp_tac (!simpset addsimps [externals_def,actions_def]) 1); -qed"ext_is_act"; \ No newline at end of file +qed"ext_is_act"; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Inductive.ML --- a/src/HOL/Inductive.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Inductive.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/inductive.ML +(* Title: HOL/inductive.ML ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge (Co)Inductive Definitions for HOL @@ -18,16 +18,16 @@ structure Lfp_items = struct - val oper = gen_fp_oper "lfp" - val Tarski = def_lfp_Tarski - val induct = def_induct + val oper = gen_fp_oper "lfp" + val Tarski = def_lfp_Tarski + val induct = def_induct end; structure Gfp_items = struct - val oper = gen_fp_oper "gfp" - val Tarski = def_gfp_Tarski - val induct = def_Collect_coinduct + val oper = gen_fp_oper "gfp" + val Tarski = def_gfp_Tarski + val induct = def_Collect_coinduct end; @@ -35,18 +35,18 @@ : sig include INTR_ELIM INDRULE end = let structure Intr_elim = Intr_elim_Fun(structure Inductive=Inductive and - Fp=Lfp_items); + Fp=Lfp_items); structure Indrule = Indrule_Fun (structure Inductive=Inductive and Intr_elim=Intr_elim); in struct - val thy = Intr_elim.thy - val defs = Intr_elim.defs - val mono = Intr_elim.mono - val intrs = Intr_elim.intrs - val elim = Intr_elim.elim - val mk_cases = Intr_elim.mk_cases + val thy = Intr_elim.thy + val defs = Intr_elim.defs + val mono = Intr_elim.mono + val intrs = Intr_elim.intrs + val elim = Intr_elim.elim + val mk_cases = Intr_elim.mk_cases open Indrule end end; @@ -57,9 +57,9 @@ signature INDUCTIVE_STRING = sig - val thy_name : string (*name of the new theory*) - val srec_tms : string list (*recursion terms*) - val sintrs : string list (*desired introduction rules*) + val thy_name : string (*name of the new theory*) + val srec_tms : string list (*recursion terms*) + val sintrs : string list (*desired introduction rules*) end; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Integ/Equiv.ML --- a/src/HOL/Integ/Equiv.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Integ/Equiv.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,7 +1,7 @@ -(* Title: Equiv.ML +(* Title: Equiv.ML ID: $Id$ - Authors: Riccardo Mattolini, Dip. Sistemi e Informatica - Lawrence C Paulson, Cambridge University Computer Laboratory + Authors: Riccardo Mattolini, Dip. Sistemi e Informatica + Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 Universita' di Firenze Copyright 1993 University of Cambridge @@ -118,7 +118,7 @@ qed "quotientI"; val [major,minor] = goalw Equiv.thy [quotient_def] - "[| X:(A/r); !!x. [| X = r^^{x}; x:A |] ==> P |] \ + "[| X:(A/r); !!x. [| X = r^^{x}; x:A |] ==> P |] \ \ ==> P"; by (resolve_tac [major RS UN_E] 1); by (rtac minor 1); @@ -173,8 +173,8 @@ (*type checking of UN x:r``{a}. b(x) *) val _::_::prems = goalw Equiv.thy [quotient_def] - "[| equiv A r; congruent r b; X: A/r; \ -\ !!x. x : A ==> b(x) : B |] \ + "[| equiv A r; congruent r b; X: A/r; \ +\ !!x. x : A ==> b(x) : B |] \ \ ==> (UN x:X. b(x)) : B"; by (cut_facts_tac prems 1); by (safe_tac rel_cs); @@ -188,7 +188,7 @@ val _::_::prems = goalw Equiv.thy [quotient_def] "[| equiv A r; congruent r b; \ \ (UN x:X. b(x))=(UN y:Y. b(y)); X: A/r; Y: A/r; \ -\ !!x y. [| x:A; y:A; b(x)=b(y) |] ==> (x,y):r |] \ +\ !!x y. [| x:A; y:A; b(x)=b(y) |] ==> (x,y):r |] \ \ ==> X=Y"; by (cut_facts_tac prems 1); by (safe_tac rel_cs); @@ -215,7 +215,7 @@ by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1); by (assume_tac 1); by (asm_simp_tac (!simpset addsimps [equivA RS UN_equiv_class, - congruent2_implies_congruent]) 1); + congruent2_implies_congruent]) 1); by (rewrite_goals_tac [congruent2_def,equiv_def,refl_def]); by (fast_tac rel_cs 1); qed "congruent2_implies_congruent_UN"; @@ -225,28 +225,28 @@ \ ==> (UN x1:r^^{a1}. UN x2:r^^{a2}. b x1 x2) = b a1 a2"; by (cut_facts_tac prems 1); by (asm_simp_tac (!simpset addsimps [equivA RS UN_equiv_class, - congruent2_implies_congruent, - congruent2_implies_congruent_UN]) 1); + congruent2_implies_congruent, + congruent2_implies_congruent_UN]) 1); qed "UN_equiv_class2"; (*type checking*) val prems = goalw Equiv.thy [quotient_def] "[| equiv A r; congruent2 r b; \ -\ X1: A/r; X2: A/r; \ -\ !!x1 x2. [| x1: A; x2: A |] ==> b x1 x2 : B |] \ +\ X1: A/r; X2: A/r; \ +\ !!x1 x2. [| x1: A; x2: A |] ==> b x1 x2 : B |] \ \ ==> (UN x1:X1. UN x2:X2. b x1 x2) : B"; by (cut_facts_tac prems 1); by (safe_tac rel_cs); by (REPEAT (ares_tac (prems@[UN_equiv_class_type, - congruent2_implies_congruent_UN, - congruent2_implies_congruent, quotientI]) 1)); + congruent2_implies_congruent_UN, + congruent2_implies_congruent, quotientI]) 1)); qed "UN_equiv_class_type2"; (*Suggested by John Harrison -- the two subproofs may be MUCH simpler than the direct proof*) val prems = goalw Equiv.thy [congruent2_def,equiv_def,refl_def] - "[| equiv A r; \ + "[| equiv A r; \ \ !! y z w. [| w: A; (y,z) : r |] ==> b y w = b z w; \ \ !! y z w. [| w: A; (y,z) : r |] ==> b w y = b w z \ \ |] ==> congruent2 r b"; @@ -258,9 +258,9 @@ qed "congruent2I"; val [equivA,commute,congt] = goal Equiv.thy - "[| equiv A r; \ + "[| equiv A r; \ \ !! y z. [| y: A; z: A |] ==> b y z = b z y; \ -\ !! y z w. [| w: A; (y,z): r |] ==> b w y = b w z \ +\ !! y z w. [| w: A; (y,z): r |] ==> b w y = b w z \ \ |] ==> congruent2 r b"; by (resolve_tac [equivA RS congruent2I] 1); by (rtac (commute RS trans) 1); diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Integ/Integ.ML --- a/src/HOL/Integ/Integ.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Integ/Integ.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,7 +1,7 @@ -(* Title: Integ.ML +(* Title: Integ.ML ID: $Id$ - Authors: Riccardo Mattolini, Dip. Sistemi e Informatica - Lawrence C Paulson, Cambridge University Computer Laboratory + Authors: Riccardo Mattolini, Dip. Sistemi e Informatica + Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 Universita' di Firenze Copyright 1993 University of Cambridge @@ -84,7 +84,7 @@ qed "inj_onto_Abs_Integ"; Addsimps [equiv_intrel_iff, inj_onto_Abs_Integ RS inj_onto_iff, - intrel_iff, intrel_in_integ, Abs_Integ_inverse]; + intrel_iff, intrel_in_integ, Abs_Integ_inverse]; goal Integ.thy "inj(Rep_Integ)"; by (rtac inj_inverseI 1); @@ -213,8 +213,8 @@ by (asm_simp_tac (!simpset addsimps [diff_add_inverse,diff_add_0]) 1); by (rtac impI 1); by (asm_simp_tac (!simpset addsimps - [diff_add_inverse, diff_add_0, diff_Suc_add_0, - diff_Suc_add_inverse]) 1); + [diff_add_inverse, diff_add_0, diff_Suc_add_0, + diff_Suc_add_inverse]) 1); qed "zmagnitude_congruent"; (*Resolve th against the corresponding facts for zmagnitude*) @@ -328,8 +328,8 @@ qed "zmult_congruent_lemma"; goal Integ.thy - "congruent2 intrel (%p1 p2. \ -\ split (%x1 y1. split (%x2 y2. \ + "congruent2 intrel (%p1 p2. \ +\ split (%x1 y1. split (%x2 y2. \ \ intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)"; by (rtac (equiv_intrel RS congruent2_commuteI) 1); by (safe_tac intrel_cs); @@ -351,7 +351,7 @@ val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2]; goalw Integ.thy [zmult_def] - "Abs_Integ((intrel^^{(x1,y1)})) * Abs_Integ((intrel^^{(x2,y2)})) = \ + "Abs_Integ((intrel^^{(x1,y1)})) * Abs_Integ((intrel^^{(x2,y2)})) = \ \ Abs_Integ(intrel ^^ {(x1*x2 + y1*y2, x1*y2 + y1*x2)})"; by (simp_tac (!simpset addsimps [zmult_ize UN_equiv_class2]) 1); qed "zmult"; @@ -433,7 +433,7 @@ val zminus_simps = [zminus_zminus, zminus_0, zminus_zadd_distrib]; val zmult_simps = [zmult_0, zmult_1, zmult_0_right, zmult_1_right, - zmult_zminus, zmult_zminus_right]; + zmult_zminus, zmult_zminus_right]; Addsimps (zadd_simps @ zminus_simps @ zmult_simps @ [zmagnitude_znat, zmagnitude_zminus_znat]); @@ -700,12 +700,12 @@ goal Integ.thy "!!i. [| i <= j; j <= k |] ==> i <= (k::int)"; by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq, - rtac zless_or_eq_imp_zle, fast_tac (HOL_cs addIs [zless_trans])]); + rtac zless_or_eq_imp_zle, fast_tac (HOL_cs addIs [zless_trans])]); qed "zle_trans"; goal Integ.thy "!!z. [| z <= w; w <= z |] ==> z = (w::int)"; by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq, - fast_tac (HOL_cs addEs [zless_anti_refl,zless_asym])]); + fast_tac (HOL_cs addEs [zless_anti_refl,zless_asym])]); qed "zle_anti_sym"; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Integ/ROOT.ML --- a/src/HOL/Integ/ROOT.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Integ/ROOT.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/Integ/ROOT +(* Title: HOL/Integ/ROOT ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1995 University of Cambridge The Integers in HOL (ported from ZF by Riccardo Mattolini) diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Lambda/Commutation.ML --- a/src/HOL/Lambda/Commutation.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Lambda/Commutation.ML Tue Jan 30 15:24:36 1996 +0100 @@ -27,21 +27,21 @@ goalw Commutation.thy [square_def] "!!R. square R S S T ==> square (R^*) S S (T^*)"; by(strip_tac 1); -be rtrancl_induct 1; +by (etac rtrancl_induct 1); by(fast_tac trancl_cs 1); by(fast_tac (HOL_cs addSEs [rtrancl_into_rtrancl]) 1); qed "square_rtrancl"; goalw Commutation.thy [commute_def] "!!R. square R S (S^*) (R^=) ==> commute (R^*) (S^*)"; -bd square_reflcl 1; -br subsetI 1; -be r_into_rtrancl 1; -bd square_sym 1; -bd square_rtrancl 1; +by (dtac square_reflcl 1); +by (rtac subsetI 1); +by (etac r_into_rtrancl 1); +by (dtac square_sym 1); +by (dtac square_rtrancl 1); by(Asm_full_simp_tac 1); -bd square_sym 1; -bd square_rtrancl 1; +by (dtac square_sym 1); +by (dtac square_rtrancl 1); by(Asm_full_simp_tac 1); qed "square_rtrancl_reflcl_commute"; @@ -68,7 +68,7 @@ qed "diamond_Un"; goalw Commutation.thy [diamond_def] "!!R. diamond R ==> confluent (R)"; -be commute_rtrancl 1; +by (etac commute_rtrancl 1); qed "diamond_confluent"; goalw Commutation.thy [diamond_def] @@ -94,12 +94,12 @@ goalw Commutation.thy [square_def,commute_def,diamond_def,Church_Rosser_def] "Church_Rosser(R) = confluent(R)"; -br iffI 1; +by (rtac iffI 1); by(fast_tac (HOL_cs addIs [Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans, rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD])1); by(safe_tac HOL_cs); -be rtrancl_induct 1; +by (etac rtrancl_induct 1); by(fast_tac trancl_cs 1); by(slow_tac (rel_cs addIs [r_into_rtrancl] addEs [rtrancl_trans,r_into_rtrancl RS rtrancl_trans]) 1); diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Lambda/Eta.ML --- a/src/HOL/Lambda/Eta.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Lambda/Eta.ML Tue Jan 30 15:24:36 1996 +0100 @@ -59,7 +59,7 @@ by(ALLGOALS(asm_full_simp_tac (addsplit (!simpset) addcongs [conj_cong]))); by(fast_tac HOL_cs 2); by(safe_tac (HOL_cs addSIs [iffI])); -bd Suc_mono 1; +by (dtac Suc_mono 1); by(ALLGOALS(Asm_full_simp_tac)); by(dtac less_trans_Suc 1 THEN atac 1); by(dtac less_trans_Suc 2 THEN atac 2); @@ -77,7 +77,7 @@ by(ALLGOALS(Asm_simp_tac)); by(fast_tac (HOL_cs addEs [less_imp_not_pred_less RS notE]) 1); by(fast_tac (HOL_cs addDs [less_not_sym]) 1); -bd Suc_mono 1; +by (dtac Suc_mono 1); by(dtac less_interval1 1 THEN atac 1); by(asm_full_simp_tac (simpset_of "Nat" addsimps [eq_sym_conv]) 1); by(dtac less_trans_Suc 1 THEN atac 1); @@ -86,7 +86,7 @@ Addsimps [free_subst]; goal Eta.thy "!!s. s -e> t ==> !i. free t i = free s i"; -be (eta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1; +by (etac (eta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1); by(ALLGOALS(asm_simp_tac (!simpset addsimps [decr_def] addcongs [conj_cong]))); bind_thm("free_eta",result() RS spec); @@ -102,24 +102,24 @@ bind_thm("subst_not_free", result() RS spec RS spec RS spec RS mp); goalw Eta.thy [decr_def] "!!s. ~free s i ==> s[t/i] = decr s i"; -be subst_not_free 1; +by (etac subst_not_free 1); qed "subst_decr"; goal Eta.thy "!!s. s -e> t ==> !u i. s[u/i] -e> t[u/i]"; -be (eta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1; +by (etac (eta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1); by(ALLGOALS(asm_simp_tac (!simpset addsimps [subst_subst RS sym,decr_def]))); by(asm_simp_tac (!simpset addsimps [subst_decr]) 1); bind_thm("eta_subst",result() RS spec RS spec); Addsimps [eta_subst]; goalw Eta.thy [decr_def] "!!s. s -e> t ==> decr s i -e> decr t i"; -be eta_subst 1; +by (etac eta_subst 1); qed "eta_decr"; (*** Confluence of eta ***) goalw Eta.thy [square_def,id_def] "square eta eta (eta^=) (eta^=)"; -br eta.mutual_induct 1; +by (rtac eta.mutual_induct 1); by(ALLGOALS(fast_tac (eta_cs addSEs [eta_decr,not_free_eta] addss !simpset))); val lemma = result(); @@ -130,17 +130,17 @@ (*** Congruence rules for -e>> ***) goal Eta.thy "!!s. s -e>> s' ==> Fun s -e>> Fun s'"; -be rtrancl_induct 1; +by (etac rtrancl_induct 1); by (ALLGOALS(fast_tac (eta_cs addIs [rtrancl_refl,rtrancl_into_rtrancl]))); qed "rtrancl_eta_Fun"; goal Eta.thy "!!s. s -e>> s' ==> s @ t -e>> s' @ t"; -be rtrancl_induct 1; +by (etac rtrancl_induct 1); by (ALLGOALS(fast_tac (eta_cs addIs [rtrancl_refl,rtrancl_into_rtrancl]))); qed "rtrancl_eta_AppL"; goal Eta.thy "!!s. t -e>> t' ==> s @ t -e>> s @ t'"; -be rtrancl_induct 1; +by (etac rtrancl_induct 1); by (ALLGOALS(fast_tac (eta_cs addIs [rtrancl_refl,rtrancl_into_rtrancl]))); qed "rtrancl_eta_AppR"; @@ -152,12 +152,12 @@ (*** Commutation of beta and eta ***) goal Eta.thy "!s t. s -> t --> (!i. free t i --> free s i)"; -br beta.mutual_induct 1; +by (rtac beta.mutual_induct 1); by(ALLGOALS(Asm_full_simp_tac)); bind_thm("free_beta", result() RS spec RS spec RS mp RS spec RS mp); goalw Eta.thy [decr_def] "!s t. s -> t --> (!i. decr s i -> decr t i)"; -br beta.mutual_induct 1; +by (rtac beta.mutual_induct 1); by(ALLGOALS(asm_full_simp_tac (!simpset addsimps [subst_subst RS sym]))); bind_thm("beta_decr", result() RS spec RS spec RS mp RS spec); @@ -186,7 +186,7 @@ Addsimps [decr_not_free]; goal Eta.thy "!s t. s -e> t --> (!i. lift s i -e> lift t i)"; -br eta.mutual_induct 1; +by (rtac eta.mutual_induct 1); by(ALLGOALS(asm_simp_tac (addsplit (!simpset) addsimps [decr_def]))); by(asm_simp_tac (addsplit (!simpset) addsimps [subst_decr]) 1); bind_thm("eta_lift",result() RS spec RS spec RS mp RS spec); @@ -201,10 +201,10 @@ bind_thm("rtrancl_eta_subst", result() RS spec RS spec RS spec RS mp); goalw Eta.thy [square_def] "square beta eta (eta^*) (beta^=)"; -br beta.mutual_induct 1; +by (rtac beta.mutual_induct 1); by(strip_tac 1); -bes eta_cases 1; -bes eta_cases 1; +by (eresolve_tac eta_cases 1); +by (eresolve_tac eta_cases 1); by(fast_tac (eta_cs addss (!simpset addsimps [subst_decr])) 1); by(fast_tac (eta_cs addIs [r_into_rtrancl,eta_subst]) 1); by(fast_tac (eta_cs addIs [rtrancl_eta_subst]) 1); diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Lambda/Lambda.ML --- a/src/HOL/Lambda/Lambda.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Lambda/Lambda.ML Tue Jan 30 15:24:36 1996 +0100 @@ -12,33 +12,33 @@ (*** Nat ***) goal Nat.thy "!!i. [| i < Suc j; j < k |] ==> i < k"; -br le_less_trans 1; -ba 2; +by (rtac le_less_trans 1); +by (assume_tac 2); by(asm_full_simp_tac (!simpset addsimps [le_def]) 1); by(fast_tac (HOL_cs addEs [less_asym,less_anti_refl]) 1); qed "lt_trans1"; goal Nat.thy "!!i. [| i < j; j < Suc(k) |] ==> i < k"; -be less_le_trans 1; +by (etac less_le_trans 1); by(asm_full_simp_tac (!simpset addsimps [le_def]) 1); by(fast_tac (HOL_cs addEs [less_asym,less_anti_refl]) 1); qed "lt_trans2"; val major::prems = goal Nat.thy "[| i < Suc j; i < j ==> P; i = j ==> P |] ==> P"; -br (major RS lessE) 1; +by (rtac (major RS lessE) 1); by(ALLGOALS Asm_full_simp_tac); by(resolve_tac prems 1 THEN etac sym 1); by(fast_tac (HOL_cs addIs prems) 1); qed "leqE"; goal Arith.thy "!!i. Suc i < j ==> i < pred j "; -by (resolve_tac [Suc_less_SucD] 1); +by (rtac Suc_less_SucD 1); by (Asm_simp_tac 1); qed "lt_pred"; goal Arith.thy "!!i. [| i < Suc j; k < i |] ==> pred i < j "; -by (resolve_tac [Suc_less_SucD] 1); +by (rtac Suc_less_SucD 1); by (Asm_simp_tac 1); qed "gt_pred"; @@ -56,17 +56,17 @@ (*** Congruence rules for ->> ***) goal Lambda.thy "!!s. s ->> s' ==> Fun s ->> Fun s'"; -be rtrancl_induct 1; +by (etac rtrancl_induct 1); by (ALLGOALS(fast_tac (lambda_cs addIs [rtrancl_refl,rtrancl_into_rtrancl]))); qed "rtrancl_beta_Fun"; goal Lambda.thy "!!s. s ->> s' ==> s @ t ->> s' @ t"; -be rtrancl_induct 1; +by (etac rtrancl_induct 1); by (ALLGOALS(fast_tac (lambda_cs addIs [rtrancl_refl,rtrancl_into_rtrancl]))); qed "rtrancl_beta_AppL"; goal Lambda.thy "!!s. t ->> t' ==> s @ t ->> s @ t'"; -be rtrancl_induct 1; +by (etac rtrancl_induct 1); by (ALLGOALS(fast_tac (lambda_cs addIs [rtrancl_refl,rtrancl_into_rtrancl]))); qed "rtrancl_beta_AppR"; @@ -157,7 +157,7 @@ by (excluded_middle_tac "nat < Suc(Suc j)" 1); by(Asm_full_simp_tac 1); by (forward_tac [lessI RS less_trans] 1); -by (eresolve_tac [leqE] 1); +by (etac leqE 1); by (asm_simp_tac (!simpset addsimps [lt_pred]) 2); by (forward_tac [Suc_mono RS less_trans] 1 THEN assume_tac 1); by (forw_inst_tac [("i","i")] (lessI RS less_trans) 1); diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Lambda/ParRed.ML --- a/src/HOL/Lambda/ParRed.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Lambda/ParRed.ML Tue Jan 30 15:24:36 1996 +0100 @@ -31,16 +31,16 @@ Addsimps [par_beta_refl]; goal ParRed.thy "beta <= par_beta"; -br subsetI 1; +by (rtac subsetI 1); by (split_all_tac 1); -be (beta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1; +by (etac (beta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1); by (ALLGOALS(fast_tac (parred_cs addSIs [par_beta_refl]))); qed "beta_subset_par_beta"; goal ParRed.thy "par_beta <= beta^*"; -br subsetI 1; +by (rtac subsetI 1); by (split_all_tac 1); -be (par_beta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1; +by (etac (par_beta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1); by (ALLGOALS(fast_tac (parred_cs addIs [rtrancl_beta_Fun,rtrancl_beta_App,rtrancl_refl, rtrancl_into_rtrancl] addEs [rtrancl_trans]))); @@ -70,7 +70,7 @@ (*** Confluence (directly) ***) goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)"; -br par_beta.mutual_induct 1; +by (rtac par_beta.mutual_induct 1); by(ALLGOALS(fast_tac (parred_cs addSIs [par_beta_subst]))); qed "diamond_par_beta"; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Lambda/ROOT.ML --- a/src/HOL/Lambda/ROOT.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Lambda/ROOT.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,10 +1,10 @@ -(* Title: HOL/Lambda/ROOT.ML +(* Title: HOL/Lambda/ROOT.ML ID: $Id$ - Author: Tobias Nipkow + Author: Tobias Nipkow Copyright 1995 TUM *) -HOL_build_completed; (*Make examples fail if HOL did*) +HOL_build_completed; (*Make examples fail if HOL did*) writeln"Root file for HOL/Lambda"; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Lex/Auto.ML --- a/src/HOL/Lex/Auto.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Lex/Auto.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/Lex/Auto.ML +(* Title: HOL/Lex/Auto.ML ID: $Id$ - Author: Richard Mayr & Tobias Nipkow + Author: Richard Mayr & Tobias Nipkow Copyright 1995 TUM *) diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Lex/AutoChopper.ML --- a/src/HOL/Lex/AutoChopper.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Lex/AutoChopper.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/Lex/AutoChopper.ML +(* Title: HOL/Lex/AutoChopper.ML ID: $Id$ - Author: Richard Mayr & Tobias Nipkow + Author: Richard Mayr & Tobias Nipkow Copyright 1995 TUM Main result: auto_chopper satisfies the is_auto_chopper specification. @@ -27,7 +27,7 @@ by (simp_tac (!simpset addcongs [conj_cong]) 1); by (simp_tac (!simpset setloop (split_tac[expand_if])) 1); by (strip_tac 1); -br conjI 1; +by (rtac conjI 1); by (fast_tac HOL_cs 1); by(simp_tac (!simpset addsimps [prefix_Cons] addcongs [conj_cong]) 1); by (strip_tac 1); @@ -100,7 +100,7 @@ by (fast_tac HOL_cs 1); by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1); by (strip_tac 1); -br conjI 1; +by (rtac conjI 1); by(res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1); by(rename_tac "vss lrst" 1); by(Asm_simp_tac 1); @@ -155,11 +155,11 @@ by (Asm_simp_tac 1); by (hyp_subst_tac 1); by (fast_tac (HOL_cs addSDs [no_acc]) 1); -be ((neq_Nil_conv RS iffD1) RS exE) 1; -be exE 1; +by (etac ((neq_Nil_conv RS iffD1) RS exE) 1); +by (etac exE 1); by (hyp_subst_tac 1); by (Simp_tac 1); -br trans 1; +by (rtac trans 1); be step2_a 1; by (simp_tac (!simpset setloop (split_tac [expand_if])) 1); val step2_d = (result() repeat_RS spec) RS mp; @@ -204,14 +204,14 @@ by (Asm_simp_tac 1); by (strip_tac 1); by (res_inst_tac [("x","[a]")] exI 1); -br conjI 1; +by (rtac conjI 1); by (subgoal_tac "r @ [a] ~= []" 1); by (fast_tac HOL_cs 1); by (Simp_tac 1); -br list_cases 1; +by (rtac list_cases 1); by (Simp_tac 1); by (asm_full_simp_tac (!simpset addsimps [acc_prefix_def] addcongs[conj_cong]) 1); -be thin_rl 1; (* speed up *) +by (etac thin_rl 1); (* speed up *) by (fast_tac HOL_cs 1); val step2_e = (result() repeat_RS spec) RS mp; Addsimps[split_paired_All]; @@ -223,18 +223,18 @@ br mp 1; be step2_b 2; by (simp_tac (!simpset setloop (split_tac [expand_if])) 1); -br conjI 1; +by (rtac conjI 1); br mp 1; be step2_c 2; by (simp_tac (!simpset setloop (split_tac [expand_if])) 1); by (fast_tac HOL_cs 1); -br conjI 1; +by (rtac conjI 1); by (asm_simp_tac (!simpset addsimps [step2_a] setloop (split_tac [expand_if])) 1); -br conjI 1; +by (rtac conjI 1); br mp 1; be step2_d 2; by (simp_tac (!simpset setloop (split_tac [expand_if])) 1); -br mp 1; +by (rtac mp 1); be step2_e 2; by (simp_tac (!simpset setloop (split_tac [expand_if])) 1); by (fast_tac HOL_cs 1); diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Lex/Prefix.ML --- a/src/HOL/Lex/Prefix.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Lex/Prefix.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,16 +1,16 @@ -(* Title: HOL/Lex/Prefix.thy +(* Title: HOL/Lex/Prefix.thy ID: $Id$ - Author: Richard Mayr & Tobias Nipkow + Author: Richard Mayr & Tobias Nipkow Copyright 1995 TUM *) open Prefix; val [maj,min] = goal Prefix.thy "[| Q([]); !! y ys. Q(y#ys) |] ==> ! l.Q(l)"; -br allI 1; +by (rtac allI 1); by (list.induct_tac "l" 1); -br maj 1; -br min 1; +by (rtac maj 1); +by (rtac min 1); val list_cases = result(); goalw Prefix.thy [prefix_def] "[] <= xs"; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Lex/ROOT.ML --- a/src/HOL/Lex/ROOT.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Lex/ROOT.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,9 +1,9 @@ -(* Title: HOL/Lex/ROOT.ML +(* Title: HOL/Lex/ROOT.ML ID: $Id$ - Author: Tobias Nipkow + Author: Tobias Nipkow Copyright 1995 TUM *) -HOL_build_completed; (*Make examples fail if HOL did*) +HOL_build_completed; (*Make examples fail if HOL did*) use_thy"AutoChopper"; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Lfp.ML --- a/src/HOL/Lfp.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Lfp.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/lfp.ML +(* Title: HOL/lfp.ML ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge For lfp.thy. The Knaster-Tarski Theorem @@ -25,12 +25,12 @@ val [mono] = goal Lfp.thy "mono(f) ==> f(lfp(f)) <= lfp(f)"; by (EVERY1 [rtac lfp_greatest, rtac subset_trans, - rtac (mono RS monoD), rtac lfp_lowerbound, atac, atac]); + rtac (mono RS monoD), rtac lfp_lowerbound, atac, atac]); qed "lfp_lemma2"; val [mono] = goal Lfp.thy "mono(f) ==> lfp(f) <= f(lfp(f))"; by (EVERY1 [rtac lfp_lowerbound, rtac (mono RS monoD), - rtac lfp_lemma2, rtac mono]); + rtac lfp_lemma2, rtac mono]); qed "lfp_lemma3"; val [mono] = goal Lfp.thy "mono(f) ==> lfp(f) = f(lfp(f))"; @@ -40,23 +40,23 @@ (*** General induction rule for least fixed points ***) val [lfp,mono,indhyp] = goal Lfp.thy - "[| a: lfp(f); mono(f); \ -\ !!x. [| x: f(lfp(f) Int {x.P(x)}) |] ==> P(x) \ + "[| a: lfp(f); mono(f); \ +\ !!x. [| x: f(lfp(f) Int {x.P(x)}) |] ==> P(x) \ \ |] ==> P(a)"; by (res_inst_tac [("a","a")] (Int_lower2 RS subsetD RS CollectD) 1); by (rtac (lfp RSN (2, lfp_lowerbound RS subsetD)) 1); by (EVERY1 [rtac Int_greatest, rtac subset_trans, - rtac (Int_lower1 RS (mono RS monoD)), - rtac (mono RS lfp_lemma2), - rtac (CollectI RS subsetI), rtac indhyp, atac]); + rtac (Int_lower1 RS (mono RS monoD)), + rtac (mono RS lfp_lemma2), + rtac (CollectI RS subsetI), rtac indhyp, atac]); qed "induct"; val major::prems = goal Lfp.thy "[| (a,b) : lfp f; mono f; \ \ !!a b. (a,b) : f(lfp f Int Collect(split P)) ==> P a b |] ==> P a b"; by(res_inst_tac [("c1","P")] (split RS subst) 1); -br (major RS induct) 1; -brs prems 1; +by (rtac (major RS induct) 1); +by (resolve_tac prems 1); by(res_inst_tac[("p","x")]PairE 1); by(hyp_subst_tac 1); by(asm_simp_tac (!simpset addsimps prems) 1); @@ -64,7 +64,7 @@ (*** Fixpoint induction a la David Park ***) goal Lfp.thy "!!f. [| mono f; f A <= A |] ==> lfp(f) <= A"; -br subsetI 1; +by (rtac subsetI 1); by(EVERY[etac induct 1, atac 1, etac subsetD 1, rtac subsetD 1, atac 2, fast_tac (set_cs addSEs [monoD]) 1]); qed "Park_induct"; @@ -77,15 +77,15 @@ qed "def_lfp_Tarski"; val rew::prems = goal Lfp.thy - "[| A == lfp(f); mono(f); a:A; \ -\ !!x. [| x: f(A Int {x.P(x)}) |] ==> P(x) \ + "[| A == lfp(f); mono(f); a:A; \ +\ !!x. [| x: f(A Int {x.P(x)}) |] ==> P(x) \ \ |] ==> P(a)"; -by (EVERY1 [rtac induct, (*backtracking to force correct induction*) - REPEAT1 o (ares_tac (map (rewrite_rule [rew]) prems))]); +by (EVERY1 [rtac induct, (*backtracking to force correct induction*) + REPEAT1 o (ares_tac (map (rewrite_rule [rew]) prems))]); qed "def_induct"; (*Monotonicity of lfp!*) val [prem] = goal Lfp.thy "[| !!Z. f(Z)<=g(Z) |] ==> lfp(f) <= lfp(g)"; -br (lfp_lowerbound RS lfp_greatest) 1; -be (prem RS subset_trans) 1; +by (rtac (lfp_lowerbound RS lfp_greatest) 1); +by (etac (prem RS subset_trans) 1); qed "lfp_mono"; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/List.ML --- a/src/HOL/List.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/List.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/List +(* Title: HOL/List ID: $Id$ - Author: Tobias Nipkow + Author: Tobias Nipkow Copyright 1994 TU Muenchen List lemmas diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/MiniML/I.ML --- a/src/HOL/MiniML/I.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/MiniML/I.ML Tue Jan 30 15:24:36 1996 +0100 @@ -17,18 +17,18 @@ (* case Abs e *) by (asm_full_simp_tac (!simpset setloop (split_tac [expand_bind])) 1); by (strip_tac 1); -br conjI 1; +by (rtac conjI 1); by (strip_tac 1); by (REPEAT (etac allE 1)); -be impE 1; +by (etac impE 1); by (fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst])) 2); by (fast_tac (HOL_cs addIs [new_tv_Suc_list RS mp,new_tv_subst_le, less_imp_le,lessI]) 1); by (strip_tac 1); by (REPEAT (etac allE 1)); -be impE 1; +by (etac impE 1); by (fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst])) 2); by (fast_tac (HOL_cs addIs [new_tv_Suc_list RS mp,new_tv_subst_le, less_imp_le,lessI]) 1); @@ -37,7 +37,7 @@ by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1); by (strip_tac 1); by (rename_tac "s1' t1 n1 s2' t2 n2 sa" 1); -br conjI 1; +by (rtac conjI 1); by (fast_tac (HOL_cs addss !simpset) 1); by (strip_tac 1); @@ -55,13 +55,13 @@ by (eres_inst_tac [("x","t2")] allE 1); by (eres_inst_tac [("x","n2")] allE 1); -br conjI 1; +by (rtac conjI 1); by (strip_tac 1); by (mp_tac 1); by (mp_tac 1); -be exE 1; -be conjE 1; -be impE 1; +by (etac exE 1); +by (etac conjE 1); +by (etac impE 1); by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); by ((dres_inst_tac [("xc","$ s a")] new_tv_W 1) THEN (atac 1)); by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] @@ -70,13 +70,13 @@ by (strip_tac 1); by (rename_tac "s2 t2' n2'" 1); -br conjI 1; +by (rtac conjI 1); by (strip_tac 1); by (mp_tac 1); by (mp_tac 1); -be exE 1; -be conjE 1; -be impE 1; +by (etac exE 1); +by (etac conjE 1); +by (etac impE 1); by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); by ((dres_inst_tac [("xc","$ s a")] new_tv_W 1) THEN (atac 1)); by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] @@ -86,9 +86,9 @@ by (strip_tac 1); by (mp_tac 1); by (mp_tac 1); -be exE 1; -be conjE 1; -be impE 1; +by (etac exE 1); +by (etac conjE 1); +by (etac impE 1); by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); by ((dres_inst_tac [("xc","$ s a")] new_tv_W 1) THEN (atac 1)); by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] @@ -99,7 +99,7 @@ by (REPEAT ((asm_full_simp_tac (!simpset addsimps [subst_comp_tel,subst_comp_te]) 1) THEN (REPEAT (etac conjE 1)) THEN (hyp_subst_tac 1) )); -br exI 1; +by (rtac exI 1); by (safe_tac HOL_cs); by (fast_tac HOL_cs 1); by (Simp_tac 2); diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/MiniML/Type.ML --- a/src/HOL/MiniML/Type.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/MiniML/Type.ML Tue Jan 30 15:24:36 1996 +0100 @@ -51,7 +51,7 @@ "!!v. [| v : free_tv(s n); v~=n |] ==> v : cod s"; by (Simp_tac 1); by (safe_tac (empty_cs addSIs [exI,conjI,notI])); -ba 2; +by (assume_tac 2); by (rotate_tac 1 1); by (Asm_full_simp_tac 1); qed "cod_app_subst"; @@ -135,7 +135,7 @@ goal thy "new_tv n = list_all (new_tv n)"; -br ext 1; +by (rtac ext 1); by(list.induct_tac "x" 1); by(ALLGOALS Asm_simp_tac); qed "new_tv_list"; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/MiniML/W.ML --- a/src/HOL/MiniML/W.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/MiniML/W.ML Tue Jan 30 15:24:36 1996 +0100 @@ -11,7 +11,7 @@ (* stronger version of Suc_leD *) goalw Nat.thy [le_def] - "!!m. Suc m <= n ==> m < n"; + "!!m. Suc m <= n ==> m < n"; by (Asm_full_simp_tac 1); by (cut_facts_tac [less_linear] 1); by (fast_tac HOL_cs 1); @@ -20,7 +20,7 @@ (* correctness of W with respect to has_type *) goal thy - "!a s t m n . Ok (s,t,m) = W e a n --> ($ s a |- e :: t)"; + "!a s t m n . Ok (s,t,m) = W e a n --> ($ s a |- e :: t)"; by (expr.induct_tac "e" 1); (* case Var n *) by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1); @@ -46,12 +46,12 @@ qed "W_correct"; val has_type_casesE = map(has_type.mk_cases expr.simps) - [" s |- Var n :: t"," s |- Abs e :: t","s |- App e1 e2 ::t"]; + [" s |- Var n :: t"," s |- Abs e :: t","s |- App e1 e2 ::t"]; (* the resulting type variable is always greater or equal than the given one *) goal thy - "!a n s t m. W e a n = Ok (s,t,m) --> n<=m"; + "!a n s t m. W e a n = Ok (s,t,m) --> n<=m"; by (expr.induct_tac "e" 1); (* case Var(n) *) by (fast_tac (HOL_cs addss (!simpset setloop (split_tac [expand_if]))) 1); @@ -83,7 +83,7 @@ Addsimps [W_var_ge]; goal thy - "!! s. Ok (s,t,m) = W e a n ==> n<=m"; + "!! s. Ok (s,t,m) = W e a n ==> n<=m"; by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1); qed "W_var_geD"; @@ -101,7 +101,7 @@ by (expr.induct_tac "e" 1); (* case Var n *) by (fast_tac (HOL_cs addss (!simpset - addsimps [id_subst_def,list_all_nth,new_tv_list,new_tv_subst] + addsimps [id_subst_def,list_all_nth,new_tv_list,new_tv_subst] setloop (split_tac [expand_if]))) 1); (* case Abs e *) @@ -111,7 +111,7 @@ by (eres_inst_tac [("x","Suc n")] allE 1); by (eres_inst_tac [("x","(TVar n)#a")] allE 1); by (fast_tac (HOL_cs addss (!simpset - addsimps [new_tv_subst,new_tv_Suc_list])) 1); + addsimps [new_tv_subst,new_tv_Suc_list])) 1); (* case App e1 e2 *) by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1); @@ -139,15 +139,15 @@ by (fast_tac (HOL_cs addDs [W_var_geD] addIs [new_tv_list_le,new_tv_subst_tel,lessI RS less_imp_le RS new_tv_subst_le]) 1); -be (sym RS mgu_new) 1; +by (etac (sym RS mgu_new) 1); by (fast_tac (HOL_cs addDs [W_var_geD] addIs [new_tv_subst_te,new_tv_list_le, new_tv_subst_tel,lessI RS less_imp_le RS new_tv_le,lessI RS less_imp_le RS new_tv_subst_le,new_tv_le]) 1); by (fast_tac (HOL_cs addDs [W_var_geD] addIs [new_tv_list_le,new_tv_subst_tel,new_tv_le] - addss (!simpset)) 1); -br (lessI RS new_tv_subst_var) 1; -be (sym RS mgu_new) 1; + addss (!simpset)) 1); +by (rtac (lessI RS new_tv_subst_var) 1); +by (etac (sym RS mgu_new) 1); by (fast_tac (HOL_cs addSIs [lessI RS less_imp_le RS new_tv_le,new_tv_subst_te] addDs [W_var_geD] addIs [new_tv_list_le,new_tv_subst_tel,lessI RS less_imp_le RS @@ -159,7 +159,7 @@ goal thy - "!n a s t m v. W e a n = Ok (s,t,m) --> \ + "!n a s t m v. W e a n = Ok (s,t,m) --> \ \ (v:free_tv s | v:free_tv t) --> v v:free_tv a"; by (expr.induct_tac "e" 1); (* case Var n *) @@ -198,8 +198,8 @@ by (eres_inst_tac [("x","v")] allE 1); by (safe_tac (empty_cs addSIs [conjI,impI] addSEs [conjE]) ); by (asm_full_simp_tac (!simpset addsimps [rotate_Ok]) 1); -bd W_var_geD 1; -bd W_var_geD 1; +by (dtac W_var_geD 1); +by (dtac W_var_geD 1); by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) ); by (fast_tac (HOL_cs addDs [free_tv_comp_subst RS subsetD,sym RS mgu_free, codD,free_tv_app_subst_te RS subsetD,free_tv_app_subst_tel RS subsetD, @@ -207,8 +207,8 @@ addEs [UnE] addss !simpset) 1); by (Asm_full_simp_tac 1); -bd (sym RS W_var_geD) 1; -bd (sym RS W_var_geD) 1; +by (dtac (sym RS W_var_geD) 1); +by (dtac (sym RS W_var_geD) 1); by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) ); by (fast_tac (HOL_cs addDs [mgu_free, codD,free_tv_subst_var RS subsetD, free_tv_app_subst_te RS subsetD,free_tv_app_subst_tel RS subsetD, @@ -223,10 +223,10 @@ (* Completeness of W w.r.t. has_type *) goal thy - "!s' a t' n. ($ s' a |- e :: t') --> new_tv n a --> \ -\ (? s t. (? m. W e a n = Ok (s,t,m) ) & \ -\ (? r. $ s' a = $ r ($ s a) & \ -\ t' = $ r t ) )"; + "!s' a t' n. ($ s' a |- e :: t') --> new_tv n a --> \ +\ (? s t. (? m. W e a n = Ok (s,t,m) ) & \ +\ (? r. $ s' a = $ r ($ s a) & \ +\ t' = $ r t ) )"; by (expr.induct_tac "e" 1); (* case Var n *) by (strip_tac 1); @@ -262,14 +262,14 @@ by (eres_inst_tac [("x","$ s a")] allE 1); by (eres_inst_tac [("x","t2")] allE 1); by (eres_inst_tac [("x","m")] allE 1); -bd asm_rl 1; -bd asm_rl 1; -bd asm_rl 1; +by (dtac asm_rl 1); +by (dtac asm_rl 1); +by (dtac asm_rl 1); by (Asm_full_simp_tac 1); by (safe_tac HOL_cs); by (fast_tac HOL_cs 1); by (fast_tac (HOL_cs addIs [sym RS W_var_geD,new_tv_W RS - conjunct1,new_tv_list_le,new_tv_subst_tel]) 1); + conjunct1,new_tv_list_le,new_tv_subst_tel]) 1); by (subgoal_tac "$ (%x.if x=ma then t' else (if x:(free_tv t - free_tv sa) then r x \ @@ -280,7 +280,7 @@ \ (if x:(free_tv t - free_tv sa) then r x else ra x)) ($ sa t)"), ("s","($ ra ta) -> t'")] ssubst 2); by (asm_simp_tac (!simpset addsimps [subst_comp_te]) 2); -br eq_free_eq_subst_te 2; +by (rtac eq_free_eq_subst_te 2); by (strip_tac 2); by (subgoal_tac "na ~=ma" 2); by (fast_tac (HOL_cs addDs [new_tv_W,sym RS W_var_geD, @@ -291,7 +291,7 @@ setloop (split_tac [expand_if])) 3); (* na : free_tv sa *) by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2); -bd eq_subst_tel_eq_free 2; +by (dtac eq_subst_tel_eq_free 2); by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2); by (Asm_simp_tac 2); by (case_tac "na:dom sa" 2); @@ -299,12 +299,12 @@ by (asm_full_simp_tac (!simpset addsimps [dom_def] setloop (split_tac [expand_if])) 3); (* na : dom sa *) -br eq_free_eq_subst_te 2; +by (rtac eq_free_eq_subst_te 2); by (strip_tac 2); by (subgoal_tac "nb ~= ma" 2); by ((forward_tac [new_tv_W] 3) THEN (atac 3)); -be conjE 3; -bd new_tv_subst_tel 3; +by (etac conjE 3); +by (dtac new_tv_subst_tel 3); by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 3); by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss (!simpset addsimps [cod_def,free_tv_subst])) 3); @@ -312,12 +312,12 @@ setloop (split_tac [expand_if]))) 2); by (Simp_tac 2); -br eq_free_eq_subst_te 2; +by (rtac eq_free_eq_subst_te 2); by (strip_tac 2 ); by (subgoal_tac "na ~= ma" 2); by ((forward_tac [new_tv_W] 3) THEN (atac 3)); -be conjE 3; -bd (sym RS W_var_geD) 3; +by (etac conjE 3); +by (dtac (sym RS W_var_geD) 3); by (fast_tac (HOL_cs addDs [new_tv_list_le,new_tv_subst_tel,new_tv_W,new_tv_not_free_tv]) 3); by (case_tac "na: free_tv t - free_tv sa" 2); (* case na ~: free_tv t - free_tv sa *) @@ -325,37 +325,37 @@ (* case na : free_tv t - free_tv sa *) by( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2); by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2); -bd eq_subst_tel_eq_free 2; +by (dtac eq_subst_tel_eq_free 2); by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2); by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def,not_disj]) 2); by (asm_simp_tac (!simpset setloop (split_tac [expand_bind])) 1); by (safe_tac HOL_cs ); -bd mgu_Ok 1; +by (dtac mgu_Ok 1); by( fast_tac (HOL_cs addss !simpset) 1); by (REPEAT (resolve_tac [exI,conjI] 1)); by (fast_tac HOL_cs 1); by (fast_tac HOL_cs 1); by ((dtac mgu_mg 1) THEN (atac 1)); -be exE 1; +by (etac exE 1); by (res_inst_tac [("x","rb")] exI 1); -br conjI 1; +by (rtac conjI 1); by (dres_inst_tac [("x","ma")] fun_cong 2); by( asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 2); by (simp_tac (!simpset addsimps [subst_comp_tel RS sym]) 1); by (res_inst_tac [("ts2","($ sa ($ s a))")] ((subst_comp_tel RS sym) RSN (2,trans)) 1); by( asm_full_simp_tac (!simpset addsimps [o_def,eq_sym_conv]) 1); -br eq_free_eq_subst_tel 1; +by (rtac eq_free_eq_subst_tel 1); by( safe_tac HOL_cs ); by (subgoal_tac "ma ~= na" 1); by ((forward_tac [new_tv_W] 2) THEN (atac 2)); -be conjE 2; -bd new_tv_subst_tel 2; +by (etac conjE 2); +by (dtac new_tv_subst_tel 2); by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 2); by (( forw_inst_tac [("xd","m")] (sym RSN (2,new_tv_W)) 2) THEN (atac 2)); -be conjE 2; -bd (free_tv_app_subst_tel RS subsetD) 2; +by (etac conjE 2); +by (dtac (free_tv_app_subst_tel RS subsetD) 2); by (fast_tac (set_cs addDs [W_var_geD,new_tv_list_le,codD, new_tv_not_free_tv]) 2); by (case_tac "na: free_tv t - free_tv sa" 1); @@ -363,7 +363,7 @@ by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2); (* case na : free_tv t - free_tv sa *) by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1); -bd (free_tv_app_subst_tel RS subsetD) 1; +by (dtac (free_tv_app_subst_tel RS subsetD) 1); by (fast_tac (set_cs addDs [codD,subst_comp_tel RSN (2,trans), eq_subst_tel_eq_free] addss ((!simpset addsimps [not_disj,free_tv_subst,dom_def]))) 1); diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Nat.ML --- a/src/HOL/Nat.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Nat.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/nat +(* Title: HOL/nat ID: $Id$ - Author: Tobias Nipkow, Cambridge University Computer Laboratory + Author: Tobias Nipkow, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge For nat.thy. Type nat is defined as a set (Nat) over the type ind. @@ -47,7 +47,7 @@ (*Perform induction on n. *) fun nat_ind_tac a i = EVERY [res_inst_tac [("n",a)] nat_induct i, - rename_last_tac a ["1"] (i+1)]; + rename_last_tac a ["1"] (i+1)]; (*A special form of induction for reasoning about m P"; by (rtac (major RS tranclE) 1); by (REPEAT_FIRST (bound_hyp_subst_tac ORELSE' - eresolve_tac (prems@[pred_natE, Pair_inject]))); + eresolve_tac (prems@[pred_natE, Pair_inject]))); by (rtac refl 1); qed "lessE"; @@ -271,7 +271,7 @@ goal Nat.thy "(m < Suc(n)) = (m < n | m = n)"; by (fast_tac (HOL_cs addSIs [lessI] - addEs [less_trans, less_SucE]) 1); + addEs [less_trans, less_SucE]) 1); qed "less_Suc_eq"; val prems = goal Nat.thy "m n ~= 0"; @@ -289,8 +289,8 @@ by (rtac impI 1); by (etac less_zeroE 1); by (fast_tac (HOL_cs addSIs [lessI RS less_SucI] - addSDs [Suc_inject] - addEs [less_trans, lessE]) 1); + addSDs [Suc_inject] + addEs [less_trans, lessE]) 1); qed "Suc_lessD"; val [major,minor] = goal Nat.thy @@ -315,8 +315,8 @@ by (rtac impI 1); by (etac less_zeroE 1); by (fast_tac (HOL_cs addSIs [lessI] - addSDs [Suc_inject] - addEs [less_trans, lessE]) 1); + addSDs [Suc_inject] + addEs [less_trans, lessE]) 1); qed "Suc_mono"; goal Nat.thy "(Suc(m) < Suc(n)) = (m a=a' & b=b'"; by (EVERY1 [rtac (major RS fun_cong RS fun_cong RS subst), - rtac conjI, rtac refl, rtac refl]); + rtac conjI, rtac refl, rtac refl]); qed "Pair_Rep_inject"; goal Prod.thy "inj_onto Abs_Prod Prod"; @@ -45,7 +45,7 @@ goalw Prod.thy [Pair_def] "? x y. p = (x,y)"; by (rtac (rewrite_rule [Prod_def] Rep_Prod RS CollectE) 1); by (EVERY1[etac exE, etac exE, rtac exI, rtac exI, - rtac (Rep_Prod_inverse RS sym RS trans), etac arg_cong]); + rtac (Rep_Prod_inverse RS sym RS trans), etac arg_cong]); qed "PairE_lemma"; val [prem] = goal Prod.thy "[| !!x y. p = (x,y) ==> Q |] ==> Q"; @@ -271,5 +271,5 @@ val prod_cs = set_cs addSIs [SigmaI, splitI, splitI2, mem_splitI, mem_splitI2] addIs [fst_imageI, snd_imageI, prod_fun_imageI] addSEs [SigmaE2, SigmaE, splitE, mem_splitE, - fst_imageE, snd_imageE, prod_fun_imageE, - Pair_inject]; + fst_imageE, snd_imageE, prod_fun_imageE, + Pair_inject]; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Relation.ML --- a/src/HOL/Relation.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Relation.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,7 +1,7 @@ -(* Title: Relation.ML +(* Title: Relation.ML ID: $Id$ - Authors: Riccardo Mattolini, Dip. Sistemi e Informatica - Lawrence C Paulson, Cambridge University Computer Laboratory + Authors: Riccardo Mattolini, Dip. Sistemi e Informatica + Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 Universita' di Firenze Copyright 1993 University of Cambridge *) @@ -100,7 +100,7 @@ (assume_tac 1) ]); val converse_cs = comp_cs addSIs [converseI] - addSEs [converseD,converseE]; + addSEs [converseD,converseE]; (** Domain **) @@ -138,13 +138,13 @@ qed_goal "Image_singleton_iff" Relation.thy "(b : r^^{a}) = ((a,b):r)" (fn _ => [ rtac (Image_iff RS trans) 1, - fast_tac comp_cs 1 ]); + fast_tac comp_cs 1 ]); qed_goalw "ImageI" Relation.thy [Image_def] "!!a b r. [| (a,b): r; a:A |] ==> b : r^^A" (fn _ => [ (REPEAT (ares_tac [CollectI,RangeI,bexI] 1)), (resolve_tac [conjI ] 1), - (resolve_tac [RangeI] 1), + (rtac RangeI 1), (REPEAT (fast_tac set_cs 1))]); qed_goalw "ImageE" Relation.thy [Image_def] diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Set.ML --- a/src/HOL/Set.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Set.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/set +(* Title: HOL/set ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge For set.thy. Set theory for higher-order logic. A set is simply a predicate. @@ -339,7 +339,7 @@ \ (UN x:A. C(x)) = (UN x:B. D(x))"; by (REPEAT (etac UN_E 1 ORELSE ares_tac ([UN_I,equalityI,subsetI] @ - (prems RL [equalityD1,equalityD2] RL [subsetD])) 1)); + (prems RL [equalityD1,equalityD2] RL [subsetD])) 1)); qed "UN_cong"; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Sexp.ML --- a/src/HOL/Sexp.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Sexp.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/Sexp +(* Title: HOL/Sexp ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge S-expressions, general binary trees for defining recursive data structures @@ -12,22 +12,22 @@ val sexp_free_cs = set_cs addSDs [Leaf_inject, Numb_inject, Scons_inject] - addSEs [Leaf_neq_Scons, Leaf_neq_Numb, - Numb_neq_Scons, Numb_neq_Leaf, - Scons_neq_Leaf, Scons_neq_Numb]; + addSEs [Leaf_neq_Scons, Leaf_neq_Numb, + Numb_neq_Scons, Numb_neq_Leaf, + Scons_neq_Leaf, Scons_neq_Numb]; goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)"; -by (resolve_tac [select_equality] 1); +by (rtac select_equality 1); by (ALLGOALS (fast_tac sexp_free_cs)); qed "sexp_case_Leaf"; goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Numb k) = d(k)"; -by (resolve_tac [select_equality] 1); +by (rtac select_equality 1); by (ALLGOALS (fast_tac sexp_free_cs)); qed "sexp_case_Numb"; goalw Sexp.thy [sexp_case_def] "sexp_case c d e (M$N) = e M N"; -by (resolve_tac [select_equality] 1); +by (rtac select_equality 1); by (ALLGOALS (fast_tac sexp_free_cs)); qed "sexp_case_Scons"; @@ -88,7 +88,7 @@ (*Proves goals of the form (M,N):pred_sexp^+ provided M,N:sexp*) Addsimps (sexp.intrs @ [pred_sexp_t1, pred_sexp_t2, - pred_sexp_trans1, pred_sexp_trans2, cut_apply]); + pred_sexp_trans1, pred_sexp_trans2, cut_apply]); val major::prems = goalw Sexp.thy [pred_sexp_def] "[| p : pred_sexp; \ diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Subst/AList.ML --- a/src/HOL/Subst/AList.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Subst/AList.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,5 +1,5 @@ -(* Title: Substitutions/AList.ML - Author: Martin Coen, Cambridge University Computer Laboratory +(* Title: Substitutions/AList.ML + Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge For AList.thy. @@ -30,4 +30,4 @@ (*Perform induction on xs. *) fun alist_ind_tac a M = EVERY [res_inst_tac [("l",a)] alist_induct M, - rename_last_tac a ["1"] (M+1)]; + rename_last_tac a ["1"] (M+1)]; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Subst/ROOT.ML --- a/src/HOL/Subst/ROOT.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Subst/ROOT.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/Subst/ROOT.ML +(* Title: HOL/Subst/ROOT.ML ID: $Id$ - Author: Martin Coen, Cambridge University Computer Laboratory + Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge Substitution and Unification in Higher-Order Logic. diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Subst/Setplus.ML --- a/src/HOL/Subst/Setplus.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Subst/Setplus.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,5 +1,5 @@ -(* Title: Substitutions/setplus.ML - Author: Martin Coen, Cambridge University Computer Laboratory +(* Title: Substitutions/setplus.ML + Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge For setplus.thy. diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Subst/Subst.ML --- a/src/HOL/Subst/Subst.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Subst/Subst.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/Subst/subst.ML +(* Title: HOL/Subst/subst.ML ID: $Id$ - Author: Martin Coen, Cambridge University Computer Laboratory + Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge For subst.thy. @@ -124,7 +124,7 @@ val [prem] = goal Subst.thy "q <> r =s= s ==> t <| q <| r = t <| s"; by (simp_tac (subst_ss addsimps [prem RS (subst_eq_iff RS iffD1), - subst_comp RS sym]) 1); + subst_comp RS sym]) 1); qed "comp_subst_subst"; (**** Domain and range of Substitutions ****) diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Subst/UTLemmas.ML --- a/src/HOL/Subst/UTLemmas.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Subst/UTLemmas.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/Subst/UTLemmas.ML +(* Title: HOL/Subst/UTLemmas.ML ID: $Id$ - Author: Martin Coen, Cambridge University Computer Laboratory + Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge For UTLemmas.thy. diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Subst/UTerm.ML --- a/src/HOL/Subst/UTerm.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Subst/UTerm.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/Subst/UTerm.ML +(* Title: HOL/Subst/UTerm.ML ID: $Id$ - Author: Martin Coen, Cambridge University Computer Laboratory + Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge Simple term structure for unifiation. @@ -50,7 +50,7 @@ (*Perform induction on xs. *) fun uterm_ind_tac a M = EVERY [res_inst_tac [("t",a)] uterm_induct M, - rename_last_tac a ["1"] (M+1)]; + rename_last_tac a ["1"] (M+1)]; (*** Isomorphisms ***) @@ -139,12 +139,12 @@ (*For reasoning about abstract uterm constructors*) val uterm_cs = set_cs addIs uterm.intrs @ [Rep_uterm] - addSEs [CONST_neq_COMB,COMB_neq_VAR,VAR_neq_CONST, - COMB_neq_CONST,VAR_neq_COMB,CONST_neq_VAR, - COMB_inject] - addSDs [VAR_inject,CONST_inject, - inj_onto_Abs_uterm RS inj_ontoD, - inj_Rep_uterm RS injD, Leaf_inject]; + addSEs [CONST_neq_COMB,COMB_neq_VAR,VAR_neq_CONST, + COMB_neq_CONST,VAR_neq_COMB,CONST_neq_VAR, + COMB_inject] + addSDs [VAR_inject,CONST_inject, + inj_onto_Abs_uterm RS inj_ontoD, + inj_Rep_uterm RS injD, Leaf_inject]; goalw UTerm.thy [Var_def] "(Var(x)=Var(y)) = (x=y)"; by (fast_tac uterm_cs 1); @@ -222,7 +222,7 @@ qed "UTerm_rec_CONST"; goalw UTerm.thy [COMB_def] - "!!M N. [| M: sexp; N: sexp |] ==> \ + "!!M N. [| M: sexp; N: sexp |] ==> \ \ UTerm_rec (COMB M N) b c d = \ \ d M N (UTerm_rec M b c d) (UTerm_rec N b c d)"; by (rtac (UTerm_rec_unfold RS trans) 1); diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Subst/Unifier.ML --- a/src/HOL/Subst/Unifier.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Subst/Unifier.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/Subst/unifier.ML +(* Title: HOL/Subst/unifier.ML ID: $Id$ - Author: Martin Coen, Cambridge University Computer Laboratory + Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge For unifier.thy. @@ -95,13 +95,13 @@ val [prem] = goalw Unifier.thy [Idem_def] "Idem(r) ==> Unifier s (t <| r) (u <| r) --> Unifier (r <> s) (t <| r) (u <| r)"; by (simp_tac (subst_ss addsimps - [Unifier_iff,subst_comp,prem RS comp_subst_subst]) 1); + [Unifier_iff,subst_comp,prem RS comp_subst_subst]) 1); val Unifier_Idem_subst = store_thm("Unifier_Idem_subst", result() RS mp); val [prem] = goal Unifier.thy "r <> s =s= s ==> Unifier s t u --> Unifier s (t <| r) (u <| r)"; by (simp_tac (subst_ss addsimps - [Unifier_iff,subst_comp,prem RS comp_subst_subst]) 1); + [Unifier_iff,subst_comp,prem RS comp_subst_subst]) 1); val Unifier_comp_subst = store_thm("Unifier_comp_subst", result() RS mp); (*** The domain of a MGIU is a subset of the variables in the terms ***) @@ -120,7 +120,7 @@ by (simp_tac (subst_ss addsimps [not_equal_iff]) 1); by (REPEAT (resolve_tac [impI,disjI2] 1)); by(res_inst_tac [("x","x")] exI 1); -br conjI 1; +by (rtac conjI 1); by (asm_simp_tac (subst_ss addsimps [Var_elim,subst_comp,repl_invariance]) 1); by (asm_simp_tac (subst_ss addsimps [Var_subst]) 1); val MGIU_sdom_lemma = store_thm("MGIU_sdom_lemma", result() RS mp RS mp RS lemma_lemma RS notE); @@ -184,7 +184,7 @@ goal Unifier.thy "MGIUnifier [] (Const n) (Const n)"; by (simp_tac (subst_ss addsimps - [MGIU_iff,MGU_iff,Unifier_iff,subst_eq_iff,Idem_Nil]) 1); + [MGIU_iff,MGU_iff,Unifier_iff,subst_eq_iff,Idem_Nil]) 1); qed "Unify1"; goal Unifier.thy "~m=n --> (ALL l.~Unifier l (Const m) (Const n))"; @@ -198,7 +198,7 @@ val [prem] = goal Unifier.thy "Var(v) <: t ==> (ALL l.~Unifier l (Var v) t)"; by (simp_tac (subst_ss addsimps - [Unifier_iff,prem RS subst_mono RS occs_irrefl2]) 1); + [Unifier_iff,prem RS subst_mono RS occs_irrefl2]) 1); qed "Unify4"; goal Unifier.thy "ALL l.~Unifier l (Const m) (Comb t u)"; @@ -221,7 +221,7 @@ \ (! q.Unifier q (t <| r) (u <| r) --> s <> q =s= q) |] ==> \ \ Idem(r <> s)"; by (cut_facts_tac [p1, - p2 RS (p1 RS Unifier_Idem_subst RS (p3 RS spec RS mp))] 1); + p2 RS (p1 RS Unifier_Idem_subst RS (p3 RS spec RS mp))] 1); by (REPEAT_SOME (etac rev_mp)); by (simp_tac (subst_ss addsimps [raw_Idem_iff,subst_eq_iff,subst_comp]) 1); qed "Unify8_lemma1"; @@ -232,7 +232,7 @@ \ r <> s <> q =s= q"; val pp = p1 RS (p3 RS spec RS mp); by (cut_facts_tac [pp, - p2 RS (pp RS Unifier_comp_subst) RS (p4 RS spec RS mp)] 1); + p2 RS (pp RS Unifier_comp_subst) RS (p4 RS spec RS mp)] 1); by (REPEAT_SOME (etac rev_mp)); by (simp_tac (subst_ss addsimps [subst_eq_iff,subst_comp]) 1); qed "Unify8_lemma2"; @@ -243,9 +243,9 @@ by (safe_tac HOL_cs); by (REPEAT (etac rev_mp 2)); by (simp_tac (subst_ss addsimps - [Unifier_iff,MGIU_iff,subst_comp,comp_assoc]) 2); + [Unifier_iff,MGIU_iff,subst_comp,comp_assoc]) 2); by (ALLGOALS (fast_tac (set_cs addEs - [Unifier_Comb,Unify8_lemma1,Unify8_lemma2]))); + [Unifier_Comb,Unify8_lemma1,Unify8_lemma2]))); qed "Unify8"; @@ -268,7 +268,7 @@ by (etac subset_trans 1); by (ALLGOALS (simp_tac (subst_ss addsimps [Var_intro,subset_iff]))); by (ALLGOALS (fast_tac (set_cs addDs - [Var_intro,prem RS MGIU_srange RS subsetD]))); + [Var_intro,prem RS MGIU_srange RS subsetD]))); qed "UWFD2_lemma1"; val [major,minor] = goal Unifier.thy diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Sum.ML --- a/src/HOL/Sum.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Sum.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/Sum.ML +(* Title: HOL/Sum.ML ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge For Sum.thy. The disjoint sum of two types @@ -28,9 +28,9 @@ goalw Sum.thy [Inl_Rep_def, Inr_Rep_def] "Inl_Rep(a) ~= Inr_Rep(b)"; by (EVERY1 [rtac notI, - etac (fun_cong RS fun_cong RS fun_cong RS iffE), - rtac (notE RS ccontr), etac (mp RS conjunct2), - REPEAT o (ares_tac [refl,conjI]) ]); + etac (fun_cong RS fun_cong RS fun_cong RS iffE), + rtac (notE RS ccontr), etac (mp RS conjunct2), + REPEAT o (ares_tac [refl,conjI]) ]); qed "Inl_Rep_not_Inr_Rep"; goalw Sum.thy [Inl_def,Inr_def] "Inl(a) ~= Inr(b)"; @@ -136,14 +136,14 @@ by (rtac (rewrite_rule [Sum_def] Rep_Sum RS CollectE) 1); by (REPEAT (eresolve_tac [disjE,exE] 1 ORELSE EVERY1 [resolve_tac prems, - etac subst, - rtac (Rep_Sum_inverse RS sym)])); + etac subst, + rtac (Rep_Sum_inverse RS sym)])); qed "sumE"; goal Sum.thy "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)"; by (EVERY1 [res_inst_tac [("s","s")] sumE, - etac ssubst, rtac sum_case_Inl, - etac ssubst, rtac sum_case_Inr]); + etac ssubst, rtac sum_case_Inl, + etac ssubst, rtac sum_case_Inr]); qed "surjective_sum"; goal Sum.thy "R(sum_case f g s) = \ diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Trancl.ML --- a/src/HOL/Trancl.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Trancl.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/trancl +(* Title: HOL/trancl ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge For trancl.thy. Theorems about the transitive closure of a relation @@ -56,7 +56,7 @@ val major::prems = goal Trancl.thy "[| (a::'a,b) : r^*; \ \ P(a); \ -\ !!y z.[| (a,y) : r^*; (y,z) : r; P(y) |] ==> P(z) |] \ +\ !!y z.[| (a,y) : r^*; (y,z) : r; P(y) |] ==> P(z) |] \ \ ==> P(b)"; (*by induction on this formula*) by (subgoal_tac "! y. (a::'a,b) = (a,y) --> P(y)" 1); @@ -76,8 +76,8 @@ (*elimination of rtrancl -- by induction on a special formula*) val major::prems = goal Trancl.thy - "[| (a::'a,b) : r^*; (a = b) ==> P; \ -\ !!y.[| (a,y) : r^*; (y,b) : r |] ==> P \ + "[| (a::'a,b) : r^*; (a = b) ==> P; \ +\ !!y.[| (a,y) : r^*; (y,b) : r |] ==> P \ \ |] ==> P"; by (subgoal_tac "(a::'a) = b | (? y. (a,y) : r^* & (y,b) : r)" 1); by (rtac (major RS rtrancl_induct) 2); @@ -123,7 +123,7 @@ val major::prems = goal Trancl.thy "[| (a::'a,b) : r^+; \ \ (a,b) : r ==> P; \ -\ !!y.[| (a,y) : r^+; (y,b) : r |] ==> P \ +\ !!y.[| (a,y) : r^+; (y,b) : r |] ==> P \ \ |] ==> P"; by (subgoal_tac "(a::'a,b) : r | (? y. (a,y) : r^+ & (y,b) : r)" 1); by (REPEAT (eresolve_tac ([asm_rl,disjE,exE,conjE]@prems) 1)); @@ -152,20 +152,20 @@ (** More about r^* **) goal Trancl.thy "(r^*)^* = r^*"; -br set_ext 1; +by (rtac set_ext 1); by(res_inst_tac [("p","x")] PairE 1); by(hyp_subst_tac 1); -br iffI 1; -be rtrancl_induct 1; -br rtrancl_refl 1; +by (rtac iffI 1); +by (etac rtrancl_induct 1); +by (rtac rtrancl_refl 1); by(fast_tac (HOL_cs addEs [rtrancl_trans]) 1); -be r_into_rtrancl 1; +by (etac r_into_rtrancl 1); qed "rtrancl_idemp"; Addsimps [rtrancl_idemp]; goal Trancl.thy "!!R. [| R <= S; S <= R^* |] ==> S^* = R^*"; -bd rtrancl_mono 1; -bd rtrancl_mono 1; +by (dtac rtrancl_mono 1); +by (dtac rtrancl_mono 1); by(Asm_full_simp_tac 1); by(fast_tac eq_cs 1); qed "rtrancl_subset"; @@ -181,16 +181,16 @@ Addsimps [rtrancl_reflcl]; goal Trancl.thy "!!r. (x,y) : (converse r)^* ==> (x,y) : converse(r^*)"; -br converseI 1; -be rtrancl_induct 1; -br rtrancl_refl 1; +by (rtac converseI 1); +by (etac rtrancl_induct 1); +by (rtac rtrancl_refl 1); by(fast_tac (rel_cs addIs [r_into_rtrancl,rtrancl_trans]) 1); qed "rtrancl_converseD"; goal Trancl.thy "!!r. (x,y) : converse(r^*) ==> (x,y) : (converse r)^*"; -bd converseD 1; -be rtrancl_induct 1; -br rtrancl_refl 1; +by (dtac converseD 1); +by (etac rtrancl_induct 1); +by (rtac rtrancl_refl 1); by(fast_tac (rel_cs addIs [r_into_rtrancl,rtrancl_trans]) 1); qed "rtrancl_converseI"; @@ -198,7 +198,7 @@ by(safe_tac (rel_eq_cs addSIs [rtrancl_converseI])); by(res_inst_tac [("p","x")] PairE 1); by(hyp_subst_tac 1); -be rtrancl_converseD 1; +by (etac rtrancl_converseD 1); qed "rtrancl_converse"; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/Univ.ML --- a/src/HOL/Univ.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Univ.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/univ +(* Title: HOL/univ ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge For univ.thy @@ -95,7 +95,7 @@ (*** Isomorphisms ***) goal Univ.thy "inj(Rep_Node)"; -by (rtac inj_inverseI 1); (*cannot combine by RS: multiple unifiers*) +by (rtac inj_inverseI 1); (*cannot combine by RS: multiple unifiers*) by (rtac Rep_Node_inverse 1); qed "inj_Rep_Node"; @@ -128,7 +128,7 @@ by (etac (equalityD2 RS subsetD RS UnE) 1); by (rtac singletonI 1); by (REPEAT (eresolve_tac [imageE, Abs_Node_inject RS apfst_convE, - Pair_inject, sym RS Push_neq_K0] 1 + Pair_inject, sym RS Push_neq_K0] 1 ORELSE resolve_tac [Node_K0_I, Rep_Node RS Node_Push_I] 1)); qed "Scons_not_Atom"; bind_thm ("Atom_not_Scons", (Scons_not_Atom RS not_sym)); @@ -183,13 +183,13 @@ val [major] = goalw Univ.thy [Scons_def] "M$N <= M'$N' ==> M<=M'"; by (cut_facts_tac [major] 1); by (fast_tac (set_cs addSDs [Suc_inject] - addSEs [Push_Node_inject, Zero_neq_Suc]) 1); + addSEs [Push_Node_inject, Zero_neq_Suc]) 1); qed "Scons_inject_lemma1"; val [major] = goalw Univ.thy [Scons_def] "M$N <= M'$N' ==> N<=N'"; by (cut_facts_tac [major] 1); by (fast_tac (set_cs addSDs [Suc_inject] - addSEs [Push_Node_inject, Suc_neq_Zero]) 1); + addSEs [Push_Node_inject, Suc_neq_Zero]) 1); qed "Scons_inject_lemma2"; val [major] = goal Univ.thy "M$N = M'$N' ==> M=M'"; @@ -274,7 +274,7 @@ by (stac (Rep_Node RS Node_Push_I RS Abs_Node_inverse) 1); by (cut_facts_tac [rewrite_rule [Node_def] Rep_Node] 1); by (safe_tac set_cs); -be ssubst 1; (*instantiates type variables!*) +by (etac ssubst 1); (*instantiates type variables!*) by (Simp_tac 1); by (rtac Least_equality 1); by (rewtac Push_def); @@ -309,8 +309,8 @@ by (safe_tac (set_cs addSIs [equalityI,imageI])); by (REPEAT (stac ndepth_Push_Node 3 THEN etac Suc_mono 3)); by (REPEAT (rtac Suc_less_SucD 1 THEN - rtac (ndepth_Push_Node RS subst) 1 THEN - assume_tac 1)); + rtac (ndepth_Push_Node RS subst) 1 THEN + assume_tac 1)); qed "ntrunc_Scons"; (** Injection nodes **) @@ -413,7 +413,7 @@ val [major] = goalw Univ.thy [ntrunc_def] "(!!k. ntrunc k M <= N) ==> M<=N"; by (fast_tac (set_cs addIs [less_add_Suc1, less_add_Suc2, - major RS subsetD]) 1); + major RS subsetD]) 1); qed "ntrunc_subsetD"; (*A generalized form of the take-lemma*) @@ -462,12 +462,12 @@ goalw Univ.thy [Case_def] "Case c d (In0 M) = c(M)"; by (fast_tac (set_cs addIs [select_equality] - addEs [make_elim In0_inject, In0_neq_In1]) 1); + addEs [make_elim In0_inject, In0_neq_In1]) 1); qed "Case_In0"; goalw Univ.thy [Case_def] "Case c d (In1 N) = d(N)"; by (fast_tac (set_cs addIs [select_equality] - addEs [make_elim In1_inject, In1_neq_In0]) 1); + addEs [make_elim In1_inject, In1_neq_In0]) 1); qed "Case_In1"; (**** UN x. B(x) rules ****) @@ -485,11 +485,11 @@ qed "Scons_UN1_y"; goalw Univ.thy [In0_def] "In0(UN x.f(x)) = (UN x. In0(f(x)))"; -br Scons_UN1_y 1; +by (rtac Scons_UN1_y 1); qed "In0_UN1"; goalw Univ.thy [In1_def] "In1(UN x.f(x)) = (UN x. In1(f(x)))"; -br Scons_UN1_y 1; +by (rtac Scons_UN1_y 1); qed "In1_UN1"; @@ -606,7 +606,7 @@ goal Univ.thy "fst `` (r<++>s) = (fst``r) <+> (fst``s)"; by (fast_tac (prod_cs addIs [equalityI, usum_In0I, usum_In1I, - dsum_In0I, dsum_In1I] + dsum_In0I, dsum_In1I] addSEs [usumE, dsumE]) 1); qed "fst_image_dsum"; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/WF.ML --- a/src/HOL/WF.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/WF.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,9 +1,9 @@ -(* Title: HOL/wf.ML +(* Title: HOL/WF.ML ID: $Id$ - Author: Tobias Nipkow + Author: Tobias Nipkow Copyright 1992 University of Cambridge -For wf.thy. Well-founded Recursion +For WF.thy. Well-founded Recursion *) open WF; @@ -33,8 +33,8 @@ (*Perform induction on i, then prove the wf(r) subgoal using prems. *) fun wf_ind_tac a prems i = EVERY [res_inst_tac [("a",a)] wf_induct i, - rename_last_tac a ["1"] (i+1), - ares_tac prems i]; + rename_last_tac a ["1"] (i+1), + ares_tac prems i]; val prems = goal WF.thy "[| wf(r); (a,x):r; (x,a):r |] ==> P"; by (subgoal_tac "! x. (a,x):r --> (x,a):r --> P" 1); @@ -92,14 +92,14 @@ ares_tac (TrueI::hyps) ORELSE' (cut_facts_tac hyps THEN' DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE' - eresolve_tac [transD, mp, allE])); + eresolve_tac [transD, mp, allE])); (*** NOTE! some simplifications need a different finish_tac!! ***) fun indhyp_tac hyps = resolve_tac (TrueI::refl::hyps) ORELSE' (cut_facts_tac hyps THEN' DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE' - eresolve_tac [transD, mp, allE])); + eresolve_tac [transD, mp, allE])); val wf_super_ss = !simpset setsolver indhyp_tac; val prems = goalw WF.thy [is_recfun_def,cut_def] @@ -167,14 +167,14 @@ "!!r. [| wf(r); trans(r) |] ==> \ \ wftrec r a H = H a (cut (%x.wftrec r x H) r a)"; by (EVERY1 [stac (rewrite_rule [is_recfun_def] unfold_the_recfun), - REPEAT o atac, rtac H_cong1]); + REPEAT o atac, rtac H_cong1]); by (asm_simp_tac (!simpset addsimps [cut_cut_eq,the_recfun_cut]) 1); qed "wftrec"; (*Unused but perhaps interesting*) val prems = goal WF.thy "[| wf(r); trans(r); !!f x. H x (cut f r x) = H x f |] ==> \ -\ wftrec r a H = H a (%x.wftrec r x H)"; +\ wftrec r a H = H a (%x.wftrec r x H)"; by (rtac (wftrec RS trans) 1); by (REPEAT (resolve_tac prems 1)); qed "wftrec2"; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/add_ind_def.ML --- a/src/HOL/add_ind_def.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/add_ind_def.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/add_ind_def.ML +(* Title: HOL/add_ind_def.ML ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge Fixedpoint definition module -- for Inductive/Coinductive Definitions @@ -29,11 +29,11 @@ ((a+(b+c))+(d+(e+f))) for 6 *) -signature FP = (** Description of a fixed point operator **) +signature FP = (** Description of a fixed point operator **) sig - val oper : string * typ * term -> term (*fixed point operator*) - val Tarski : thm (*Tarski's fixed point theorem*) - val induct : thm (*induction/coinduction rule*) + val oper : string * typ * term -> term (*fixed point operator*) + val Tarski : thm (*Tarski's fixed point theorem*) + val induct : thm (*induction/coinduction rule*) end; @@ -58,8 +58,8 @@ val rec_hds = map head_of rec_tms; val _ = assert_all is_Const rec_hds - (fn t => "Recursive set not previously declared as constant: " ^ - Sign.string_of_term sign t); + (fn t => "Recursive set not previously declared as constant: " ^ + Sign.string_of_term sign t); (*Now we know they are all Consts, so get their names, type and params*) val rec_names = map (#1 o dest_Const) rec_hds @@ -71,16 +71,16 @@ local (*Checking the introduction rules*) val intr_sets = map (#2 o rule_concl_msg sign) intr_tms; fun intr_ok set = - case head_of set of Const(a,_) => a mem rec_names | _ => false; + case head_of set of Const(a,_) => a mem rec_names | _ => false; in val _ = assert_all intr_ok intr_sets - (fn t => "Conclusion of rule does not name a recursive set: " ^ - Sign.string_of_term sign t); + (fn t => "Conclusion of rule does not name a recursive set: " ^ + Sign.string_of_term sign t); end; val _ = assert_all is_Free rec_params - (fn t => "Param in recursion term not a free variable: " ^ - Sign.string_of_term sign t); + (fn t => "Param in recursion term not a free variable: " ^ + Sign.string_of_term sign t); (*** Construct the lfp definition ***) val mk_variant = variant (foldr add_term_names (intr_tms,[])); @@ -89,7 +89,7 @@ (*Mutual recursion ?? *) val domTs = summands (dest_setT (body_type recT)); - (*alternative defn: map (dest_setT o fastype_of) rec_tms *) + (*alternative defn: map (dest_setT o fastype_of) rec_tms *) val dom_sumT = fold_bal mk_sum domTs; val dom_set = mk_setT dom_sumT; @@ -99,35 +99,35 @@ fun dest_tprop (Const("Trueprop",_) $ P) = P | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^ - Sign.string_of_term sign Q); + Sign.string_of_term sign Q); (*Makes a disjunct from an introduction rule*) fun lfp_part intr = (*quantify over rule's free vars except parameters*) let val prems = map dest_tprop (Logic.strip_imp_prems intr) - val _ = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds - val exfrees = term_frees intr \\ rec_params - val zeq = eq_const dom_sumT $ freez $ (#1 (rule_concl intr)) + val _ = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds + val exfrees = term_frees intr \\ rec_params + val zeq = eq_const dom_sumT $ freez $ (#1 (rule_concl intr)) in foldr mk_exists (exfrees, fold_bal (app conj) (zeq::prems)) end; (*The Part(A,h) terms -- compose injections to make h*) - fun mk_Part (Bound 0, _) = freeX (*no mutual rec, no Part needed*) + fun mk_Part (Bound 0, _) = freeX (*no mutual rec, no Part needed*) | mk_Part (h, domT) = - let val goodh = mend_sum_types (h, dom_sumT) + let val goodh = mend_sum_types (h, dom_sumT) and Part_const = - Const("Part", [dom_set, domT-->dom_sumT]---> dom_set) + Const("Part", [dom_set, domT-->dom_sumT]---> dom_set) in Part_const $ freeX $ Abs(w,domT,goodh) end; (*Access to balanced disjoint sums via injections*) val parts = map mk_Part - (accesses_bal (ap Inl, ap Inr, Bound 0) (length domTs) ~~ - domTs); + (accesses_bal (ap Inl, ap Inr, Bound 0) (length domTs) ~~ + domTs); (*replace each set by the corresponding Part(A,h)*) val part_intrs = map (subst_free (rec_tms ~~ parts) o lfp_part) intr_tms; val lfp_rhs = Fp.oper(X, dom_sumT, - mk_Collect(z, dom_sumT, - fold_bal (app disj) part_intrs)) + mk_Collect(z, dom_sumT, + fold_bal (app disj) part_intrs)) (*** Make the new theory ***) @@ -142,18 +142,18 @@ (*The individual sets must already be declared*) val axpairs = map mk_defpair - ((big_rec_tm, lfp_rhs) :: - (case parts of - [_] => [] (*no mutual recursion*) - | _ => rec_tms ~~ (*define the sets as Parts*) - map (subst_atomic [(freeX, big_rec_tm)]) parts)); + ((big_rec_tm, lfp_rhs) :: + (case parts of + [_] => [] (*no mutual recursion*) + | _ => rec_tms ~~ (*define the sets as Parts*) + map (subst_atomic [(freeX, big_rec_tm)]) parts)); val _ = seq (writeln o Sign.string_of_term sign o #2) axpairs (*Detect occurrences of operator, even with other types!*) val _ = (case rec_names inter (add_term_names (lfp_rhs,[])) of - [] => () - | x::_ => error ("Illegal occurrence of recursion op: " ^ x ^ + [] => () + | x::_ => error ("Illegal occurrence of recursion op: " ^ x ^ "\n\t*Consider adding type constraints*")) in thy |> add_defs_i axpairs end @@ -166,7 +166,7 @@ fun add_constructs_def (rec_names, con_ty_lists) thy = * let * val _ = writeln" Defining the constructor functions..."; -* val case_name = "f"; (*name for case variables*) +* val case_name = "f"; (*name for case variables*) * (** Define the constructors **) @@ -176,16 +176,16 @@ * fun mk_inject n k u = access_bal(ap Inl, ap Inr, u) n k; -* val npart = length rec_names; (*total # of mutually recursive parts*) +* val npart = length rec_names; (*total # of mutually recursive parts*) * (*Make constructor definition; kpart is # of this mutually recursive part*) * fun mk_con_defs (kpart, con_ty_list) = -* let val ncon = length con_ty_list (*number of constructors*) - fun mk_def (((id,T,syn), name, args, prems), kcon) = - (*kcon is index of constructor*) - mk_defpair (list_comb (Const(name,T), args), - mk_inject npart kpart - (mk_inject ncon kcon (mk_tuple args))) +* let val ncon = length con_ty_list (*number of constructors*) + fun mk_def (((id,T,syn), name, args, prems), kcon) = + (*kcon is index of constructor*) + mk_defpair (list_comb (Const(name,T), args), + mk_inject npart kpart + (mk_inject ncon kcon (mk_tuple args))) * in map mk_def (con_ty_list ~~ (1 upto ncon)) end; * (** Define the case operator **) @@ -193,25 +193,25 @@ * (*Combine split terms using case; yields the case operator for one part*) * fun call_case case_list = * let fun call_f (free,args) = - ap_split T free (map (#2 o dest_Free) args) + ap_split T free (map (#2 o dest_Free) args) * in fold_bal (app sum_case) (map call_f case_list) end; * (** Generating function variables for the case definition - Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **) + Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **) * (*Treatment of a single constructor*) * fun add_case (((id,T,syn), name, args, prems), (opno,cases)) = - if Syntax.is_identifier id - then (opno, - (Free(case_name ^ "_" ^ id, T), args) :: cases) - else (opno+1, - (Free(case_name ^ "_op_" ^ string_of_int opno, T), args) :: - cases) + if Syntax.is_identifier id + then (opno, + (Free(case_name ^ "_" ^ id, T), args) :: cases) + else (opno+1, + (Free(case_name ^ "_op_" ^ string_of_int opno, T), args) :: + cases) * (*Treatment of a list of constructors, for one part*) * fun add_case_list (con_ty_list, (opno,case_lists)) = - let val (opno',case_list) = foldr add_case (con_ty_list, (opno,[])) - in (opno', case_list :: case_lists) end; + let val (opno',case_list) = foldr add_case (con_ty_list, (opno,[])) + in (opno', case_list :: case_lists) end; * (*Treatment of all parts*) * val (_, case_lists) = foldr add_case_list (con_ty_lists, (1,[])); @@ -226,18 +226,18 @@ * val big_case_args = flat (map (map #1) case_lists); * val big_case_tm = - list_comb (Const(big_case_name, big_case_typ), big_case_args); + list_comb (Const(big_case_name, big_case_typ), big_case_args); * val big_case_def = mk_defpair - (big_case_tm, fold_bal (app sum_case) (map call_case case_lists)); + (big_case_tm, fold_bal (app sum_case) (map call_case case_lists)); * (** Build the new theory **) * val const_decs = - (big_case_name, big_case_typ, NoSyn) :: map #1 (flat con_ty_lists); + (big_case_name, big_case_typ, NoSyn) :: map #1 (flat con_ty_lists); * val axpairs = - big_case_def :: flat (map mk_con_defs ((1 upto npart) ~~ con_ty_lists)) + big_case_def :: flat (map mk_con_defs ((1 upto npart) ~~ con_ty_lists)) * in thy |> add_consts_i const_decs |> add_defs_i axpairs end; ****************************************************************) diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/datatype.ML --- a/src/HOL/datatype.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/datatype.ML Tue Jan 30 15:24:36 1996 +0100 @@ -32,22 +32,22 @@ let fun subst (Abs(a,T,t)) = Abs(a,T,subst t) | subst (funct $ body) = - let val (f,b) = strip_comb (funct$body) - in - if is_Const f andalso fst(dest_Const f) = fname - then - let val (ls,rest) = (take(rpos,b), drop(rpos,b)); - val (xk,rs) = (hd rest,tl rest) - handle LIST _ => raise RecError "not enough arguments \ - \ in recursive application on rhs" + let val (f,b) = strip_comb (funct$body) + in + if is_Const f andalso fst(dest_Const f) = fname + then + let val (ls,rest) = (take(rpos,b), drop(rpos,b)); + val (xk,rs) = (hd rest,tl rest) + handle LIST _ => raise RecError "not enough arguments \ + \ in recursive application on rhs" in - (case assoc (pairs,xk) of - None => raise RecError - ("illegal occurence of " ^ fname ^ " on rhs") - | Some(U) => list_comb(U,map subst (ls @ rs))) - end - else list_comb(f, map subst b) - end + (case assoc (pairs,xk) of + None => raise RecError + ("illegal occurence of " ^ fname ^ " on rhs") + | Some(U) => list_comb(U,map subst (ls @ rs))) + end + else list_comb(f, map subst b) + end | subst(t) = t in subst t end; @@ -55,11 +55,11 @@ fun abst_rec (fname,rpos,tc,ls,cargs,rs,rhs) = let val rargs = (map fst o - (filter (fn (a,T) => is_dtRek T))) (cargs ~~ tc); + (filter (fn (a,T) => is_dtRek T))) (cargs ~~ tc); val subs = map (fn (s,T) => (s,dummyT)) - (rev(rename_wrt_term rhs rargs)); + (rev(rename_wrt_term rhs rargs)); val subst_rhs = subst_apps (fname,rpos) - (map Free rargs ~~ map Free subs) rhs; + (map Free rargs ~~ map Free subs) rhs; in list_abs_free (cargs @ subs @ ls @ rs, subst_rhs) end; @@ -79,17 +79,17 @@ val (c,cargs') = strip_comb (hd middle) handle LIST "hd" => raise RecError "constructor missing"; val (ls,cargs,rs) = (map dest_Free ls', map dest_Free cargs' - , map dest_Free rs') + , map dest_Free rs') handle TERM ("dest_Free",_) => - raise RecError "constructor has illegal argument in pattern"; + raise RecError "constructor has illegal argument in pattern"; in if length middle > 1 then raise RecError "more than one non-variable in pattern" else if not(null(findrep (map fst (ls @ rs @ cargs)))) then raise RecError "repeated variable name in pattern" - else (fst(dest_Const name) handle TERM _ => - raise RecError "function is not declared as constant in theory" - ,rpos,ls,fst( dest_Const c),cargs,rs,rhs) + else (fst(dest_Const name) handle TERM _ => + raise RecError "function is not declared as constant in theory" + ,rpos,ls,fst( dest_Const c),cargs,rs,rhs) end; (* check function specified for all constructors and sort function terms *) @@ -107,32 +107,32 @@ | trans_recs thy cs' (eq1::eqs) = let val (name1,rpos1,ls1,_,_,_,_) = dest_rec eq1 handle RecError s => - error("Primrec definition error: " ^ s ^ ":\n" - ^ " " ^ Sign.string_of_term (sign_of thy) eq1); + error("Primrec definition error: " ^ s ^ ":\n" + ^ " " ^ Sign.string_of_term (sign_of thy) eq1); val tcs = map (fn (_,c,T,_,_) => (c,T)) cs'; val cs = map fst tcs; fun trans_recs' _ [] = [] | trans_recs' cis (eq::eqs) = - let val (name,rpos,ls,c,cargs,rs,rhs) = dest_rec eq; - val tc = assoc(tcs,c); - val i = (1 + find (c,cs)) handle LIST "find" => 0; - in - if name <> name1 then - raise RecError "function names inconsistent" - else if rpos <> rpos1 then - raise RecError "position of rec. argument inconsistent" - else if i = 0 then - raise RecError "illegal argument in pattern" - else if i mem cis then - raise RecError "constructor already occured as pattern " - else (i,abst_rec (name,rpos,the tc,ls,cargs,rs,rhs)) - :: trans_recs' (i::cis) eqs - end - handle RecError s => - error("Primrec definition error\n" ^ s ^ "\n" - ^ " " ^ Sign.string_of_term (sign_of thy) eq); + let val (name,rpos,ls,c,cargs,rs,rhs) = dest_rec eq; + val tc = assoc(tcs,c); + val i = (1 + find (c,cs)) handle LIST "find" => 0; + in + if name <> name1 then + raise RecError "function names inconsistent" + else if rpos <> rpos1 then + raise RecError "position of rec. argument inconsistent" + else if i = 0 then + raise RecError "illegal argument in pattern" + else if i mem cis then + raise RecError "constructor already occured as pattern " + else (i,abst_rec (name,rpos,the tc,ls,cargs,rs,rhs)) + :: trans_recs' (i::cis) eqs + end + handle RecError s => + error("Primrec definition error\n" ^ s ^ "\n" + ^ " " ^ Sign.string_of_term (sign_of thy) eq); in ( name1, ls1 - , check_and_sort (length cs, trans_recs' [] (eq1::eqs))) + , check_and_sort (length cs, trans_recs' [] (eq1::eqs))) end ; in @@ -155,24 +155,24 @@ (*search for free type variables and convert recursive *) fun analyse_types (cons, types, syn) = - let fun analyse(t as dtVar v) = + let fun analyse(t as dtVar v) = if t mem typevars then t else error ("Free type variable " ^ v ^ " on rhs.") - | analyse(dtTyp(typl,s)) = - if tname <> s then dtTyp(analyses typl, s) + | analyse(dtTyp(typl,s)) = + if tname <> s then dtTyp(analyses typl, s) else if typevars = typl then dtRek(typl, s) else error (s ^ " used in different ways") - | analyse(dtRek _) = raise Impossible - and analyses ts = map analyse ts; - in (cons, Syntax.const_name cons syn, analyses types, + | analyse(dtRek _) = raise Impossible + and analyses ts = map analyse ts; + in (cons, Syntax.const_name cons syn, analyses types, mk_var_names types, syn) end; (*test if all elements are recursive, i.e. if the type is empty*) fun non_empty (cs : ('a * 'b * dt_type list * 'c *'d) list) = - not(forall (exists is_dtRek o #3) cs) orelse - error("Empty datatype not allowed!"); + not(forall (exists is_dtRek o #3) cs) orelse + error("Empty datatype not allowed!"); val cons_list = map analyse_types cons_list'; val dummy = non_empty cons_list; @@ -182,7 +182,7 @@ (*generate 'var_n, ..., var_m'*) fun Args(var, delim, n, m) = - space_implode delim (map (fn n => var^string_of_int(n)) (n upto m)); + space_implode delim (map (fn n => var^string_of_int(n)) (n upto m)); fun C_exp name vns = name ^ opt_parens(space_implode ") (" vns); @@ -195,85 +195,85 @@ pp_typlist1: parentheses, pp_typlist2: brackets*) fun pp_typ (dtVar s) = "(" ^ s ^ "::term)" | pp_typ (dtTyp (typvars, id)) = - if null typvars then id else (pp_typlist1 typvars) ^ id + if null typvars then id else (pp_typlist1 typvars) ^ id | pp_typ (dtRek (typvars, id)) = (pp_typlist1 typvars) ^ id and - pp_typlist' ts = commas (map pp_typ ts) + pp_typlist' ts = commas (map pp_typ ts) and - pp_typlist1 ts = if null ts then "" else parens (pp_typlist' ts); + pp_typlist1 ts = if null ts then "" else parens (pp_typlist' ts); fun pp_typlist2 ts = if null ts then "" else brackets (pp_typlist' ts); (* Generate syntax translation for case rules *) fun calc_xrules c_nr y_nr ((_, name, _, vns, _) :: cs) = - let val arity = length vns; - val body = "z" ^ string_of_int(c_nr); - val args1 = if arity=0 then "" - else " " ^ Args ("y", " ", y_nr, y_nr+arity-1); - val args2 = if arity=0 then "" - else "(% " ^ Args ("y", " ", y_nr, y_nr+arity-1) - ^ ". "; - val (rest1,rest2) = - if null cs then ("","") - else let val (h1, h2) = calc_xrules (c_nr+1) (y_nr+arity) cs - in (" | " ^ h1, " " ^ h2) end; - in (name ^ args1 ^ " => " ^ body ^ rest1, + let val arity = length vns; + val body = "z" ^ string_of_int(c_nr); + val args1 = if arity=0 then "" + else " " ^ Args ("y", " ", y_nr, y_nr+arity-1); + val args2 = if arity=0 then "" + else "(% " ^ Args ("y", " ", y_nr, y_nr+arity-1) + ^ ". "; + val (rest1,rest2) = + if null cs then ("","") + else let val (h1, h2) = calc_xrules (c_nr+1) (y_nr+arity) cs + in (" | " ^ h1, " " ^ h2) end; + in (name ^ args1 ^ " => " ^ body ^ rest1, args2 ^ body ^ (if args2 = "" then "" else ")") ^ rest2) end | calc_xrules _ _ [] = raise Impossible; val xrules = - let val (first_part, scnd_part) = calc_xrules 1 1 cons_list - in [("logic", "case x of " ^ first_part) <-> - ("logic", tname ^ "_case " ^ scnd_part ^ " x")] - end; + let val (first_part, scnd_part) = calc_xrules 1 1 cons_list + in [("logic", "case x of " ^ first_part) <-> + ("logic", tname ^ "_case " ^ scnd_part ^ " x")] + end; (*type declarations for constructors*) fun const_type (id, _, typlist, _, syn) = - (id, - (if null typlist then "" else pp_typlist2 typlist ^ " => ") ^ - pp_typlist1 typevars ^ tname, syn); + (id, + (if null typlist then "" else pp_typlist2 typlist ^ " => ") ^ + pp_typlist1 typevars ^ tname, syn); fun assumpt (dtRek _ :: ts, v :: vs ,found) = - let val h = if found then ";P(" ^ v ^ ")" else "[| P(" ^ v ^ ")" - in h ^ (assumpt (ts, vs, true)) end + let val h = if found then ";P(" ^ v ^ ")" else "[| P(" ^ v ^ ")" + in h ^ (assumpt (ts, vs, true)) end | assumpt (t :: ts, v :: vs, found) = assumpt (ts, vs, found) | assumpt ([], [], found) = if found then "|] ==>" else "" | assumpt _ = raise Impossible; fun t_inducting ((_, name, types, vns, _) :: cs) = - let - val h = if null types then " P(" ^ name ^ ")" - else " !!" ^ (space_implode " " vns) ^ "." ^ - (assumpt (types, vns, false)) ^ + let + val h = if null types then " P(" ^ name ^ ")" + else " !!" ^ (space_implode " " vns) ^ "." ^ + (assumpt (types, vns, false)) ^ "P(" ^ C_exp name vns ^ ")"; - val rest = t_inducting cs; - in if rest = "" then h else h ^ "; " ^ rest end + val rest = t_inducting cs; + in if rest = "" then h else h ^ "; " ^ rest end | t_inducting [] = ""; fun t_induct cl typ_name = "[|" ^ t_inducting cl ^ "|] ==> P(" ^ typ_name ^ ")"; fun gen_typlist typevar f ((_, _, ts, _, _) :: cs) = - let val h = if (length ts) > 0 - then pp_typlist2(f ts) ^ "=>" - else "" - in h ^ typevar ^ "," ^ (gen_typlist typevar f cs) end + let val h = if (length ts) > 0 + then pp_typlist2(f ts) ^ "=>" + else "" + in h ^ typevar ^ "," ^ (gen_typlist typevar f cs) end | gen_typlist _ _ [] = ""; (* -------------------------------------------------------------------- *) -(* The case constant and rules *) - +(* The case constant and rules *) + val t_case = tname ^ "_case"; fun case_rule n (id, name, _, vns, _) = - let val args = if vns = [] then "" else " " ^ space_implode " " vns - in (t_case ^ "_" ^ id, - t_case ^ " " ^ Args("f", " ", 1, num_of_cons) - ^ " (" ^ name ^ args ^ ") = f"^string_of_int(n) ^ args) - end + let val args = if vns = [] then "" else " " ^ space_implode " " vns + in (t_case ^ "_" ^ id, + t_case ^ " " ^ Args("f", " ", 1, num_of_cons) + ^ " (" ^ name ^ args ^ ") = f"^string_of_int(n) ^ args) + end fun case_rules n (c :: cs) = case_rule n c :: case_rules(n+1) cs | case_rules _ [] = []; @@ -285,124 +285,124 @@ val arities = let val term_list = replicate datatype_arity termS; in [(tname, term_list, termS)] - end; + end; val datatype_name = pp_typlist1 typevars ^ tname; val new_tvar_name = variant (map (fn dtVar s => s) typevars) "'z"; val case_const = - (t_case, - "[" ^ gen_typlist new_tvar_name I cons_list - ^ pp_typlist1 typevars ^ tname ^ "] =>" ^ new_tvar_name^"::term", - NoSyn); + (t_case, + "[" ^ gen_typlist new_tvar_name I cons_list + ^ pp_typlist1 typevars ^ tname ^ "] =>" ^ new_tvar_name^"::term", + NoSyn); val rules_case = case_rules 1 cons_list; (* -------------------------------------------------------------------- *) -(* The prim-rec combinator *) +(* The prim-rec combinator *) val t_rec = tname ^ "_rec" (* adding type variables for dtRek types to end of list of dt_types *) fun add_reks ts = - ts @ map (fn _ => dtVar new_tvar_name) (filter is_dtRek ts); + ts @ map (fn _ => dtVar new_tvar_name) (filter is_dtRek ts); (* positions of the dtRek types in a list of dt_types, starting from 1 *) fun rek_vars ts vns = map snd (filter (is_dtRek o fst) (ts ~~ vns)) fun rec_rule n (id,name,ts,vns,_) = - let val args = opt_parens(space_implode ") (" vns) - val fargs = opt_parens(Args("f", ") (", 1, num_of_cons)) - fun rarg vn = t_rec ^ fargs ^ " (" ^ vn ^ ")" - val rargs = opt_parens(space_implode ") (" + let val args = opt_parens(space_implode ") (" vns) + val fargs = opt_parens(Args("f", ") (", 1, num_of_cons)) + fun rarg vn = t_rec ^ fargs ^ " (" ^ vn ^ ")" + val rargs = opt_parens(space_implode ") (" (map rarg (rek_vars ts vns))) - in - (t_rec ^ "_" ^ id, - t_rec ^ fargs ^ " (" ^ name ^ args ^ ") = f" - ^ string_of_int(n) ^ args ^ rargs) - end + in + (t_rec ^ "_" ^ id, + t_rec ^ fargs ^ " (" ^ name ^ args ^ ") = f" + ^ string_of_int(n) ^ args ^ rargs) + end fun rec_rules n (c::cs) = rec_rule n c :: rec_rules (n+1) cs - | rec_rules _ [] = []; + | rec_rules _ [] = []; val rec_const = - (t_rec, - "[" ^ (gen_typlist new_tvar_name add_reks cons_list) - ^ (pp_typlist1 typevars) ^ tname ^ "] =>" ^ new_tvar_name^"::term", - NoSyn); + (t_rec, + "[" ^ (gen_typlist new_tvar_name add_reks cons_list) + ^ (pp_typlist1 typevars) ^ tname ^ "] =>" ^ new_tvar_name^"::term", + NoSyn); val rules_rec = rec_rules 1 cons_list (* -------------------------------------------------------------------- *) val consts = - map const_type cons_list - @ (if num_of_cons < dtK then [] - else [(tname ^ "_ord", datatype_name ^ "=>nat", NoSyn)]) - @ [case_const,rec_const]; + map const_type cons_list + @ (if num_of_cons < dtK then [] + else [(tname ^ "_ord", datatype_name ^ "=>nat", NoSyn)]) + @ [case_const,rec_const]; fun Ci_ing ((id, name, _, vns, _) :: cs) = - if null vns then Ci_ing cs - else let val vns' = variantlist(vns,vns) + if null vns then Ci_ing cs + else let val vns' = variantlist(vns,vns) in ("inject_" ^ id, - "(" ^ (C_exp name vns) ^ "=" ^ (C_exp name vns') - ^ ") = (" ^ (arg_eqs vns vns') ^ ")") :: (Ci_ing cs) + "(" ^ (C_exp name vns) ^ "=" ^ (C_exp name vns') + ^ ") = (" ^ (arg_eqs vns vns') ^ ")") :: (Ci_ing cs) end - | Ci_ing [] = []; + | Ci_ing [] = []; fun Ci_negOne (id1,name1,_,vns1,_) (id2,name2,_,vns2,_) = let val vns2' = variantlist(vns2,vns1) val ax = C_exp name1 vns1 ^ "~=" ^ C_exp name2 vns2' - in (id1 ^ "_not_" ^ id2, ax) end; + in (id1 ^ "_not_" ^ id2, ax) end; fun Ci_neg1 [] = [] - | Ci_neg1 (c1::cs) = (map (Ci_negOne c1) cs) @ Ci_neg1 cs; + | Ci_neg1 (c1::cs) = (map (Ci_negOne c1) cs) @ Ci_neg1 cs; fun suc_expr n = - if n=0 then "0" else "Suc(" ^ suc_expr(n-1) ^ ")"; + if n=0 then "0" else "Suc(" ^ suc_expr(n-1) ^ ")"; fun Ci_neg2() = - let val ord_t = tname ^ "_ord"; - val cis = cons_list ~~ (0 upto (num_of_cons - 1)) - fun Ci_neg2equals ((id, name, _, vns, _), n) = - let val ax = ord_t ^ "(" ^ (C_exp name vns) ^ ") = " ^ (suc_expr n) - in (ord_t ^ "_" ^ id, ax) end - in (ord_t ^ "_distinct", ord_t^"(x) ~= "^ord_t^"(y) ==> x ~= y") :: - (map Ci_neg2equals cis) - end; + let val ord_t = tname ^ "_ord"; + val cis = cons_list ~~ (0 upto (num_of_cons - 1)) + fun Ci_neg2equals ((id, name, _, vns, _), n) = + let val ax = ord_t ^ "(" ^ (C_exp name vns) ^ ") = " ^ (suc_expr n) + in (ord_t ^ "_" ^ id, ax) end + in (ord_t ^ "_distinct", ord_t^"(x) ~= "^ord_t^"(y) ==> x ~= y") :: + (map Ci_neg2equals cis) + end; val rules_distinct = if num_of_cons < dtK then Ci_neg1 cons_list - else Ci_neg2(); + else Ci_neg2(); val rules_inject = Ci_ing cons_list; val rule_induct = (tname ^ "_induct", t_induct cons_list tname); val rules = rule_induct :: - (rules_inject @ rules_distinct @ rules_case @ rules_rec); + (rules_inject @ rules_distinct @ rules_case @ rules_rec); fun add_primrec eqns thy = - let val rec_comb = Const(t_rec,dummyT) - val teqns = map (fn neq => snd(read_axm (sign_of thy) neq)) eqns - val (fname,ls,fns) = trans_recs thy cons_list teqns - val rhs = - list_abs_free - (ls @ [(tname,dummyT)] - ,list_comb(rec_comb - , fns @ map Bound (0 ::(length ls downto 1)))); + let val rec_comb = Const(t_rec,dummyT) + val teqns = map (fn neq => snd(read_axm (sign_of thy) neq)) eqns + val (fname,ls,fns) = trans_recs thy cons_list teqns + val rhs = + list_abs_free + (ls @ [(tname,dummyT)] + ,list_comb(rec_comb + , fns @ map Bound (0 ::(length ls downto 1)))); val sg = sign_of thy; val defpair = mk_defpair (Const(fname,dummyT),rhs) - val defpairT as (_, _ $ Const(_,T) $ _ ) = inferT_axm sg defpair; - val varT = Type.varifyT T; + val defpairT as (_, _ $ Const(_,T) $ _ ) = inferT_axm sg defpair; + val varT = Type.varifyT T; val ftyp = the (Sign.const_type sg fname); - in - if Type.typ_instance (#tsig(Sign.rep_sg sg), ftyp, varT) - then add_defs_i [defpairT] thy - else error("Primrec definition error: \ntype of " ^ fname - ^ " is not instance of type deduced from equations") - end; + in + if Type.typ_instance (#tsig(Sign.rep_sg sg), ftyp, varT) + then add_defs_i [defpairT] thy + else error("Primrec definition error: \ntype of " ^ fname + ^ " is not instance of type deduced from equations") + end; in datatypes := map (fn (x,_,_) => x) cons_list' @ (!datatypes); @@ -480,9 +480,9 @@ order of parameters is corrected by setting the rhs equal to list_abs_free - (ls @ [(tname,dummyT)] - ,list_comb(rec_comb - , fns @ map Bound (0 ::(length ls downto 1)))); + (ls @ [(tname,dummyT)] + ,list_comb(rec_comb + , fns @ map Bound (0 ::(length ls downto 1)))); Note the de-Bruijn indices counting the number of lambdas between the variable and its binding. diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/equalities.ML --- a/src/HOL/equalities.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/equalities.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/equalities +(* Title: HOL/equalities ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge Equalities involving union, intersection, inclusion, etc. diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/ex/Acc.ML --- a/src/HOL/ex/Acc.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/ex/Acc.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/ex/Acc +(* Title: HOL/ex/Acc ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge Inductive definition of acc(r) @@ -15,7 +15,7 @@ val prems = goal Acc.thy "[| !!b. (b,a):r ==> b: acc(r) |] ==> a: acc(r)"; by (fast_tac (set_cs addIs (prems @ - map (rewrite_rule [pred_def]) acc.intrs)) 1); + map (rewrite_rule [pred_def]) acc.intrs)) 1); qed "accI"; goal Acc.thy "!!a b r. [| b: acc(r); (a,b): r |] ==> a: acc(r)"; @@ -25,8 +25,8 @@ qed "acc_downward"; val [major,indhyp] = goal Acc.thy - "[| a : acc(r); \ -\ !!x. [| x: acc(r); ALL y. (y,x):r --> P(y) |] ==> P(x) \ + "[| a : acc(r); \ +\ !!x. [| x: acc(r); ALL y. (y,x):r --> P(y) |] ==> P(x) \ \ |] ==> P(a)"; by (rtac (major RS acc.induct) 1); by (rtac indhyp 1); @@ -55,7 +55,7 @@ by (rtac subsetI 1); by (res_inst_tac [("p", "x")] PairE 1); by (fast_tac (set_cs addSIs [SigmaI, - major RS acc_wfD_lemma RS spec RS mp]) 1); + major RS acc_wfD_lemma RS spec RS mp]) 1); qed "acc_wfD"; goal Acc.thy "wf(r) = (r <= Sigma (acc r) (%u. acc(r)))"; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/ex/BT.ML --- a/src/HOL/ex/BT.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/ex/BT.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/ex/BT.ML +(* Title: HOL/ex/BT.ML ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1995 University of Cambridge Datatype definition of binary trees diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/ex/InSort.ML --- a/src/HOL/ex/InSort.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/ex/InSort.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/ex/insort.ML +(* Title: HOL/ex/insort.ML ID: $Id$ - Author: Tobias Nipkow + Author: Tobias Nipkow Copyright 1994 TU Muenchen Correctness proof of insertion sort. diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/ex/LList.ML --- a/src/HOL/ex/LList.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/ex/LList.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/llist +(* Title: HOL/llist ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge SHOULD LListD_Fun_CONS_I, etc., be equations (for rewriting)? @@ -82,13 +82,13 @@ qed "CONS_mono"; Addsimps [LList_corec_fun_def RS def_nat_rec_0, - LList_corec_fun_def RS def_nat_rec_Suc]; + LList_corec_fun_def RS def_nat_rec_Suc]; (** The directions of the equality are proved separately **) goalw LList.thy [LList_corec_def] "LList_corec a f <= sum_case (%u.NIL) \ -\ (split(%z w. CONS z (LList_corec w f))) (f a)"; +\ (split(%z w. CONS z (LList_corec w f))) (f a)"; by (rtac UN1_least 1); by (res_inst_tac [("n","k")] natE 1); by (ALLGOALS (Asm_simp_tac)); @@ -106,14 +106,14 @@ (*the recursion equation for LList_corec -- NOT SUITABLE FOR REWRITING!*) goal LList.thy "LList_corec a f = sum_case (%u. NIL) \ -\ (split(%z w. CONS z (LList_corec w f))) (f a)"; +\ (split(%z w. CONS z (LList_corec w f))) (f a)"; by (REPEAT (resolve_tac [equalityI, LList_corec_subset1, - LList_corec_subset2] 1)); + LList_corec_subset2] 1)); qed "LList_corec"; (*definitional version of same*) val [rew] = goal LList.thy - "[| !!x. h(x) == LList_corec x f |] ==> \ + "[| !!x. h(x) == LList_corec x f |] ==> \ \ h(a) = sum_case (%u.NIL) (split(%z w. CONS z (h w))) (f a)"; by (rewtac rew); by (rtac LList_corec 1); @@ -183,7 +183,7 @@ by (safe_tac HOL_cs); by (rtac diag_eqI 1); by (rtac (LListD_implies_ntrunc_equality RS spec RS spec RS mp RS - ntrunc_equality) 1); + ntrunc_equality) 1); by (assume_tac 1); by (etac (fst_imageI RS (fst_image_LListD RS subsetD)) 1); qed "LListD_subset_diag"; @@ -225,12 +225,12 @@ by (eresolve_tac [llist.elim] 1); by (ALLGOALS (asm_simp_tac (!simpset addsimps [diagI, LListD_Fun_NIL_I, - LListD_Fun_CONS_I]))); + LListD_Fun_CONS_I]))); qed "diag_subset_LListD"; goal LList.thy "LListD(diag(A)) = diag(llist(A))"; by (REPEAT (resolve_tac [equalityI, LListD_subset_diag, - diag_subset_LListD] 1)); + diag_subset_LListD] 1)); qed "LListD_eq_diag"; goal LList.thy @@ -264,14 +264,14 @@ by (rtac ext 1); (*next step avoids an unknown (and flexflex pair) in simplification*) by (res_inst_tac [("A", "{u.True}"), - ("r", "range(%u. (h1(u),h2(u)))")] LList_equalityI 1); + ("r", "range(%u. (h1(u),h2(u)))")] LList_equalityI 1); by (rtac rangeI 1); by (safe_tac set_cs); by (stac prem1 1); by (stac prem2 1); by (simp_tac (!simpset addsimps [LListD_Fun_NIL_I, - CollectI RS LListD_Fun_CONS_I] - |> add_eqI) 1); + CollectI RS LListD_Fun_CONS_I] + |> add_eqI) 1); qed "LList_corec_unique"; val [prem] = goal LList.thy @@ -377,7 +377,7 @@ goalw LList.thy [LCons_def] "Rep_llist(LCons x l) = CONS (Leaf x) (Rep_llist l)"; by (REPEAT (resolve_tac [llist.CONS_I RS Abs_llist_inverse, - rangeI, Rep_llist] 1)); + rangeI, Rep_llist] 1)); qed "Rep_llist_LCons"; (** Injectiveness of CONS and LCons **) @@ -391,9 +391,9 @@ (*For reasoning about abstract llist constructors*) val llist_cs = set_cs addIs [Rep_llist]@llist.intrs - addSEs [CONS_neq_NIL,NIL_neq_CONS,CONS_inject] - addSDs [inj_onto_Abs_llist RS inj_ontoD, - inj_Rep_llist RS injD, Leaf_inject]; + addSEs [CONS_neq_NIL,NIL_neq_CONS,CONS_inject] + addSDs [inj_onto_Abs_llist RS inj_ontoD, + inj_Rep_llist RS injD, Leaf_inject]; goalw LList.thy [LCons_def] "(LCons x xs=LCons y ys) = (x=y & xs=ys)"; by (fast_tac llist_cs 1); @@ -413,12 +413,12 @@ (*A special case of list_equality for functions over lazy lists*) val [Mlist,gMlist,NILcase,CONScase] = goal LList.thy - "[| M: llist(A); g(NIL): llist(A); \ -\ f(NIL)=g(NIL); \ -\ !!x l. [| x:A; l: llist(A) |] ==> \ -\ (f(CONS x l),g(CONS x l)) : \ + "[| M: llist(A); g(NIL): llist(A); \ +\ f(NIL)=g(NIL); \ +\ !!x l. [| x:A; l: llist(A) |] ==> \ +\ (f(CONS x l),g(CONS x l)) : \ \ LListD_Fun (diag A) ((%u.(f(u),g(u)))``llist(A) Un \ -\ diag(llist(A))) \ +\ diag(llist(A))) \ \ |] ==> f(M) = g(M)"; by (rtac LList_equalityI 1); by (rtac (Mlist RS imageI) 1); @@ -454,7 +454,7 @@ by (etac llist.elim 1); by (ALLGOALS (asm_simp_tac (!simpset addsimps [Lmap_NIL,Lmap_CONS]))); by (REPEAT (ares_tac [list_Fun_NIL_I, list_Fun_CONS_I, - minor, imageI, UnI1] 1)); + minor, imageI, UnI1] 1)); qed "Lmap_type"; (*This type checking rule synthesises a sufficiently large set for f*) @@ -472,7 +472,7 @@ by (etac llist.elim 1); by (ALLGOALS (asm_simp_tac (!simpset addsimps [Lmap_NIL,Lmap_CONS]))); by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI, UnI1, - rangeI RS LListD_Fun_CONS_I] 1)); + rangeI RS LListD_Fun_CONS_I] 1)); qed "Lmap_compose"; val [prem] = goal LList.thy "M: llist(A) ==> Lmap (%x.x) M = M"; @@ -481,7 +481,7 @@ by (etac llist.elim 1); by (ALLGOALS (asm_simp_tac (!simpset addsimps [Lmap_NIL,Lmap_CONS]))); by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI RS UnI1, - rangeI RS LListD_Fun_CONS_I] 1)); + rangeI RS LListD_Fun_CONS_I] 1)); qed "Lmap_ident"; @@ -505,7 +505,7 @@ qed "Lappend_CONS"; Addsimps [llist.NIL_I, Lappend_NIL_NIL, Lappend_NIL_CONS, - Lappend_CONS, LListD_Fun_CONS_I, range_eqI, image_eqI]; + Lappend_CONS, LListD_Fun_CONS_I, range_eqI, image_eqI]; Delsimps [Pair_eq]; goal LList.thy "!!M. M: llist(A) ==> Lappend NIL M = M"; @@ -582,7 +582,7 @@ goalw LList.thy [llist_corec_def,LNil_def,LCons_def] "llist_corec a f = sum_case (%u. LNil) \ -\ (split(%z w. LCons z (llist_corec w f))) (f a)"; +\ (split(%z w. LCons z (llist_corec w f))) (f a)"; by (stac LList_corec 1); by (res_inst_tac [("s","f(a)")] sumE 1); by (asm_simp_tac (!simpset addsimps [LList_corec_type2]) 1); @@ -594,7 +594,7 @@ (*definitional version of same*) val [rew] = goal LList.thy - "[| !!x. h(x) == llist_corec x f |] ==> \ + "[| !!x. h(x) == llist_corec x f |] ==> \ \ h(a) = sum_case (%u.LNil) (split(%z w. LCons z (h w))) (f a)"; by (rewtac rew); by (rtac llist_corec 1); @@ -641,8 +641,8 @@ "[| (l1,l2) : r; r <= llistD_Fun(r Un range(%x.(x,x))) |] ==> l1=l2"; by (rtac (inj_Rep_llist RS injD) 1); by (res_inst_tac [("r", "prod_fun Rep_llist Rep_llist ``r"), - ("A", "range(Leaf)")] - LList_equalityI 1); + ("A", "range(Leaf)")] + LList_equalityI 1); by (rtac (prem1 RS prod_fun_imageI) 1); by (rtac (prem2 RS image_mono RS subset_trans) 1); by (rtac (image_compose RS subst) 1); @@ -677,10 +677,10 @@ (*A special case of list_equality for functions over lazy lists*) val [prem1,prem2] = goal LList.thy - "[| f(LNil)=g(LNil); \ -\ !!x l. (f(LCons x l),g(LCons x l)) : \ -\ llistD_Fun(range(%u. (f(u),g(u))) Un range(%v. (v,v))) \ -\ |] ==> f(l) = (g(l :: 'a llist) :: 'b llist)"; + "[| f(LNil)=g(LNil); \ +\ !!x l. (f(LCons x l),g(LCons x l)) : \ +\ llistD_Fun(range(%u. (f(u),g(u))) Un range(%v. (v,v))) \ +\ |] ==> f(l) = (g(l :: 'a llist) :: 'b llist)"; by (res_inst_tac [("r", "range(%u. (f(u),g(u)))")] llist_equalityI 1); by (rtac rangeI 1); by (rtac subsetI 1); @@ -696,7 +696,7 @@ (*simpset for llist bisimulations*) Addsimps [llist_case_LNil, llist_case_LCons, - llistD_Fun_LNil_I, llistD_Fun_LCons_I]; + llistD_Fun_LNil_I, llistD_Fun_LCons_I]; (*** The functional "lmap" ***) @@ -752,7 +752,7 @@ (** Two lemmas about natrec n x (%m.g), which is essentially (g^n)(x) **) goal LList.thy - "nat_rec n (LCons b l) (%m. lmap(f)) = \ + "nat_rec n (LCons b l) (%m. lmap(f)) = \ \ LCons (nat_rec n b (%m. f)) (nat_rec n l (%m. lmap(f)))"; by (nat_ind_tac "n" 1); by (ALLGOALS (asm_simp_tac (!simpset addsimps [lmap_LCons]))); diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/ex/LexProd.ML --- a/src/HOL/ex/LexProd.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/ex/LexProd.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/ex/lex-prod.ML +(* Title: HOL/ex/lex-prod.ML ID: $Id$ - Author: Tobias Nipkow, TU Munich + Author: Tobias Nipkow, TU Munich Copyright 1993 TU Munich For lex-prod.thy. diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/ex/MT.ML --- a/src/HOL/ex/MT.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/ex/MT.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/ex/MT.ML +(* Title: HOL/ex/MT.ML ID: $Id$ - Author: Jacob Frost, Cambridge University Computer Laboratory + Author: Jacob Frost, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge Based upon the article @@ -766,7 +766,7 @@ by (safe_tac HOL_cs); by (DEPTH_SOLVE (ares_tac [consistency_const, consistency_var, consistency_fn, - consistency_fix, consistency_app1, consistency_app2] 1)); + consistency_fix, consistency_app1, consistency_app2] 1)); qed "consistency"; (* ############################################################ *) diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/ex/NatSum.ML --- a/src/HOL/ex/NatSum.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/ex/NatSum.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/ex/natsum.ML +(* Title: HOL/ex/natsum.ML ID: $Id$ - Author: Tobias Nipkow + Author: Tobias Nipkow Copyright 1994 TU Muenchen Summing natural numbers, squares and cubes. Could be continued... diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/ex/Perm.ML --- a/src/HOL/ex/Perm.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/ex/Perm.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/ex/Perm.ML +(* Title: HOL/ex/Perm.ML ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1995 University of Cambridge Permutations: example of an inductive definition @@ -74,7 +74,7 @@ goal Perm.thy "a # xs <~~> xs @ [a]"; by (rtac perm.trans 1); -br perm_append_swap 2; +by (rtac perm_append_swap 2); by (simp_tac (!simpset addsimps [perm_refl]) 1); qed "perm_append_single"; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/ex/PropLog.ML --- a/src/HOL/ex/PropLog.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/ex/PropLog.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/ex/pl.ML +(* Title: HOL/ex/pl.ML ID: $Id$ - Author: Tobias Nipkow & Lawrence C Paulson + Author: Tobias Nipkow & Lawrence C Paulson Copyright 1994 TU Muenchen & University of Cambridge Soundness and completeness of propositional logic w.r.t. truth-tables. @@ -107,7 +107,7 @@ by(PropLog.pl.induct_tac "p" 1); by (ALLGOALS (simp_tac (!simpset addsimps [thms_I, thms.H]))); by (fast_tac (set_cs addIs [weaken_left_Un1, weaken_left_Un2, - weaken_right, imp_false] + weaken_right, imp_false] addSEs [false_imp]) 1); qed "hyps_thms_if"; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/ex/Puzzle.ML --- a/src/HOL/ex/Puzzle.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/ex/Puzzle.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/ex/puzzle.ML +(* Title: HOL/ex/puzzle.ML ID: $Id$ - Author: Tobias Nipkow + Author: Tobias Nipkow Copyright 1993 TU Muenchen For puzzle.thy. A question from "Bundeswettbewerb Mathematik" diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/ex/Qsort.ML --- a/src/HOL/ex/Qsort.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/ex/Qsort.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/ex/qsort.ML +(* Title: HOL/ex/qsort.ML ID: $Id$ - Author: Tobias Nipkow + Author: Tobias Nipkow Copyright 1994 TU Muenchen Two verifications of Quicksort diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/ex/ROOT.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/ex/ROOT +(* Title: HOL/ex/ROOT ID: $Id$ - Author: Tobias Nipkow, Cambridge University Computer Laboratory + Author: Tobias Nipkow, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge Executes miscellaneous examples for Higher-Order Logic. diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/ex/SList.ML --- a/src/HOL/ex/SList.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/ex/SList.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/ex/SList.ML +(* Title: HOL/ex/SList.ML ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge Definition of type 'a list by a least fixed point @@ -45,7 +45,7 @@ (*Perform induction on xs. *) fun list_ind_tac a M = EVERY [res_inst_tac [("l",a)] list_induct2 M, - rename_last_tac a ["1"] (M+1)]; + rename_last_tac a ["1"] (M+1)]; (*** Isomorphisms ***) @@ -89,9 +89,9 @@ (*For reasoning about abstract list constructors*) val list_cs = set_cs addIs [Rep_list] @ list.intrs - addSEs [CONS_neq_NIL,NIL_neq_CONS,CONS_inject] - addSDs [inj_onto_Abs_list RS inj_ontoD, - inj_Rep_list RS injD, Leaf_inject]; + addSEs [CONS_neq_NIL,NIL_neq_CONS,CONS_inject] + addSDs [inj_onto_Abs_list RS inj_ontoD, + inj_Rep_list RS injD, Leaf_inject]; goalw SList.thy [Cons_def] "(x#xs=y#ys) = (x=y & xs=ys)"; by (fast_tac list_cs 1); @@ -167,10 +167,10 @@ "(CONS M1 M2, N) : pred_sexp^+ ==> \ \ (M1,N) : pred_sexp^+ & (M2,N) : pred_sexp^+"; by (rtac (prem RS (pred_sexp_subset_Sigma RS trancl_subset_Sigma RS - subsetD RS SigmaE2)) 1); + subsetD RS SigmaE2)) 1); by (etac (sexp_CONS_D RS conjE) 1); by (REPEAT (ares_tac [conjI, pred_sexp_CONS_I1, pred_sexp_CONS_I2, - prem RSN (2, trans_trancl RS transD)] 1)); + prem RSN (2, trans_trancl RS transD)] 1)); qed "pred_sexp_CONS_D"; (** Conversion rules for List_rec **) @@ -211,8 +211,8 @@ (*Type checking. Useful?*) val major::A_subset_sexp::prems = goal SList.thy - "[| M: list(A); \ -\ A<=sexp; \ + "[| M: list(A); \ +\ A<=sexp; \ \ c: C(NIL); \ \ !!x y r. [| x: A; y: list(A); r: C(y) |] ==> h x y r: C(CONS x y) \ \ |] ==> List_rec M c h : C(M :: 'a item)"; @@ -373,7 +373,7 @@ qed "map_compose2"; goal SList.thy "!!f. (!!x. f(x): sexp) ==> \ -\ Abs_map g (Rep_map f xs) = map (%t. g(f(t))) xs"; +\ Abs_map g (Rep_map f xs) = map (%t. g(f(t))) xs"; by (list_ind_tac "xs" 1); by(ALLGOALS(asm_simp_tac(!simpset addsimps [Rep_map_type,list_sexp RS subsetD]))); diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/ex/Simult.ML --- a/src/HOL/ex/Simult.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/ex/Simult.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/ex/Simult.ML +(* Title: HOL/ex/Simult.ML ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge Primitives for simultaneous recursive type definitions @@ -18,7 +18,7 @@ goal Simult.thy "mono(%Z. A <*> Part Z In1 \ \ <+> ({Numb(0)} <+> Part Z In0 <*> Part Z In1))"; by (REPEAT (ares_tac [monoI, subset_refl, usum_mono, uprod_mono, - Part_mono] 1)); + Part_mono] 1)); qed "TF_fun_mono"; val TF_unfold = TF_fun_mono RS (TF_def RS def_lfp_Tarski); @@ -44,14 +44,14 @@ val major::prems = goalw Simult.thy TF_Rep_defs "[| i: TF(A); \ -\ !!M N. [| M: A; N: Part (TF A) In1; R(N) |] ==> R(TCONS M N); \ -\ R(FNIL); \ +\ !!M N. [| M: A; N: Part (TF A) In1; R(N) |] ==> R(TCONS M N); \ +\ R(FNIL); \ \ !!M N. [| M: Part (TF A) In0; N: Part (TF A) In1; R(M); R(N) \ \ |] ==> R(FCONS M N) \ \ |] ==> R(i)"; by (rtac ([TF_def, TF_fun_mono, major] MRS def_induct) 1); by (fast_tac (set_cs addIs (prems@[PartI]) - addEs [usumE, uprodE, PartE]) 1); + addEs [usumE, uprodE, PartE]) 1); qed "TF_induct"; (*This lemma replaces a use of subgoal_tac to prove tree_forest_induct*) @@ -62,8 +62,8 @@ qed "TF_induct_lemma"; val uplus_cs = set_cs addSIs [PartI] - addSDs [In0_inject, In1_inject] - addSEs [In0_neq_In1, In1_neq_In0, PartE]; + addSDs [In0_inject, In1_inject] + addSEs [In0_neq_In1, In1_neq_In0, PartE]; (*Could prove ~ TCONS M N : Part (TF A) In1 etc. *) @@ -84,20 +84,20 @@ (*Induction for the abstract types 'a tree, 'a forest*) val prems = goalw Simult.thy [Tcons_def,Fnil_def,Fcons_def] "[| !!x ts. Q(ts) ==> P(Tcons x ts); \ -\ Q(Fnil); \ +\ Q(Fnil); \ \ !!t ts. [| P(t); Q(ts) |] ==> Q(Fcons t ts) \ \ |] ==> (! t. P(t)) & (! ts. Q(ts))"; by (res_inst_tac [("P1","%z.P(Abs_Tree(z))"), - ("Q1","%z.Q(Abs_Forest(z))")] + ("Q1","%z.Q(Abs_Forest(z))")] (Tree_Forest_induct RS conjE) 1); (*Instantiates ?A1 to range(Leaf). *) by (fast_tac (set_cs addSEs [Rep_Tree_inverse RS subst, - Rep_Forest_inverse RS subst] - addSIs [Rep_Tree,Rep_Forest]) 4); + Rep_Forest_inverse RS subst] + addSIs [Rep_Tree,Rep_Forest]) 4); (*Cannot use simplifier: the rewrites work in the wrong direction!*) by (ALLGOALS (fast_tac (set_cs addSEs [Abs_Tree_inverse RS subst, Abs_Forest_inverse RS subst] - addSIs prems))); + addSIs prems))); qed "tree_forest_induct"; @@ -132,7 +132,7 @@ (*For reasoning about the representation*) val TF_Rep_cs = uplus_cs addIs [TF_I, uprodI, usum_In0I, usum_In1I] - addSEs [Scons_inject]; + addSEs [Scons_inject]; val prems = goalw Simult.thy TF_Rep_defs "[| a: A; M: Part (TF A) In1 |] ==> TCONS a M : Part (TF A) In0"; @@ -195,14 +195,14 @@ (*For reasoning about abstract constructors*) val TF_cs = set_cs addSIs [Rep_Tree, Rep_Forest, TCONS_I, FNIL_I, FCONS_I] - addSEs [TCONS_inject, FCONS_inject, - TCONS_neq_FNIL, FNIL_neq_TCONS, - FCONS_neq_FNIL, FNIL_neq_FCONS, - TCONS_neq_FCONS, FCONS_neq_TCONS] - addSDs [inj_onto_Abs_Tree RS inj_ontoD, - inj_onto_Abs_Forest RS inj_ontoD, - inj_Rep_Tree RS injD, inj_Rep_Forest RS injD, - Leaf_inject]; + addSEs [TCONS_inject, FCONS_inject, + TCONS_neq_FNIL, FNIL_neq_TCONS, + FCONS_neq_FNIL, FNIL_neq_FCONS, + TCONS_neq_FCONS, FCONS_neq_TCONS] + addSDs [inj_onto_Abs_Tree RS inj_ontoD, + inj_onto_Abs_Forest RS inj_ontoD, + inj_Rep_Tree RS injD, inj_Rep_Forest RS injD, + Leaf_inject]; goalw Simult.thy [Tcons_def] "(Tcons x xs=Tcons y ys) = (x=y & xs=ys)"; by (fast_tac TF_cs 1); @@ -233,7 +233,7 @@ (** conversion rules for TF_rec **) goalw Simult.thy [TCONS_def] - "!!M N. [| M: sexp; N: sexp |] ==> \ + "!!M N. [| M: sexp; N: sexp |] ==> \ \ TF_rec (TCONS M N) b c d = b M N (TF_rec N b c d)"; by (rtac (TF_rec_unfold RS trans) 1); by (simp_tac (!simpset addsimps [Case_In0, Split]) 1); @@ -246,7 +246,7 @@ qed "TF_rec_FNIL"; goalw Simult.thy [FCONS_def] - "!!M N. [| M: sexp; N: sexp |] ==> \ + "!!M N. [| M: sexp; N: sexp |] ==> \ \ TF_rec (FCONS M N) b c d = d M N (TF_rec M b c d) (TF_rec N b c d)"; by (rtac (TF_rec_unfold RS trans) 1); by (simp_tac (HOL_ss addsimps [Case_In1, List_case_CONS]) 1); diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/ex/Sorting.ML --- a/src/HOL/ex/Sorting.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/ex/Sorting.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/ex/sorting.ML +(* Title: HOL/ex/sorting.ML ID: $Id$ - Author: Tobias Nipkow + Author: Tobias Nipkow Copyright 1994 TU Muenchen Some general lemmas diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/ex/Term.ML --- a/src/HOL/ex/Term.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/ex/Term.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/ex/Term +(* Title: HOL/ex/Term ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge Terms over a given alphabet -- function applications; illustrates list functor @@ -42,7 +42,7 @@ \ |] ==> R(M)"; by (rtac (major RS term.induct) 1); by (REPEAT (eresolve_tac ([minor] @ - ([Int_lower1,Int_lower2] RL [list_mono RS subsetD])) 1)); + ([Int_lower1,Int_lower2] RL [list_mono RS subsetD])) 1)); (*Proof could also use mono_Int RS subsetD RS IntE *) qed "Term_induct"; @@ -74,7 +74,7 @@ list_subset_sexp, range_Leaf_subset_sexp] 1 ORELSE etac rev_subsetD 1)); by (eres_inst_tac [("A1","term(?u)"), ("f1","Rep_term"), ("g1","Abs_term")] - (Abs_map_inverse RS subst) 1); + (Abs_map_inverse RS subst) 1); by (rtac (range_Leaf_subset_sexp RS term_subset_sexp) 1); by (etac Abs_term_inverse 1); by (etac rangeE 1); @@ -104,7 +104,7 @@ (*Perform induction on xs. *) fun term_ind2_tac a i = EVERY [res_inst_tac [("t",a)] term_induct2 i, - rename_last_tac a ["1","s"] (i+1)]; + rename_last_tac a ["1","s"] (i+1)]; @@ -155,7 +155,7 @@ in val term_rec = prove_goalw Term.thy - [term_rec_def, App_def, Rep_Tlist_def, Abs_Tlist_def] + [term_rec_def, App_def, Rep_Tlist_def, Abs_Tlist_def] "term_rec (App f ts) d = d f ts (map (%t. term_rec t d) ts)" (fn _ => [simp_tac term_rec_ss 1]) diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/ex/cla.ML --- a/src/HOL/ex/cla.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/ex/cla.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/ex/cla +(* Title: HOL/ex/cla ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge Higher-Order Logic: predicate calculus problems @@ -217,8 +217,8 @@ result(); writeln"Problem 26"; -goal HOL.thy "((? x. p(x)) = (? x. q(x))) & \ -\ (! x. ! y. p(x) & q(y) --> (r(x) = s(y))) \ +goal HOL.thy "((? x. p(x)) = (? x. q(x))) & \ +\ (! x. ! y. p(x) & q(y) --> (r(x) = s(y))) \ \ --> ((! x. p(x)-->r(x)) = (! x. q(x)-->s(x)))"; by (fast_tac HOL_cs 1); result(); @@ -278,9 +278,9 @@ writeln"Problem 34 AMENDED (TWICE!!) NOT PROVED AUTOMATICALLY"; (*Andrews's challenge*) -goal HOL.thy "((? x. ! y. p(x) = p(y)) = \ -\ ((? x. q(x)) = (! y. p(y)))) = \ -\ ((? x. ! y. q(x) = q(y)) = \ +goal HOL.thy "((? x. ! y. p(x) = p(y)) = \ +\ ((? x. q(x)) = (! y. p(y)))) = \ +\ ((? x. ! y. q(x) = q(y)) = \ \ ((? x. p(x)) = (! y. q(y))))"; by (deepen_tac HOL_cs 3 1); (*slower with smaller bounds*) @@ -294,7 +294,7 @@ writeln"Problem 36"; goal HOL.thy "(! x. ? y. J x y) & \ \ (! x. ? y. G x y) & \ -\ (! x y. J x y | G x y --> \ +\ (! x y. J x y | G x y --> \ \ (! z. J y z | G y z --> H x z)) \ \ --> (! x. ? y. H x y)"; by (fast_tac HOL_cs 1); @@ -311,10 +311,10 @@ writeln"Problem 38"; goal HOL.thy - "(! x. p(a) & (p(x) --> (? y. p(y) & r x y)) --> \ -\ (? z. ? w. p(z) & r x w & r w z)) = \ -\ (! x. (~p(a) | p(x) | (? z. ? w. p(z) & r x w & r w z)) & \ -\ (~p(a) | ~(? y. p(y) & r x y) | \ + "(! x. p(a) & (p(x) --> (? y. p(y) & r x y)) --> \ +\ (? z. ? w. p(z) & r x w & r w z)) = \ +\ (! x. (~p(a) | p(x) | (? z. ? w. p(z) & r x w & r w z)) & \ +\ (~p(a) | ~(? y. p(y) & r x y) | \ \ (? z. ? w. p(z) & r x w & r w z)))"; writeln"Problem 39"; @@ -329,7 +329,7 @@ result(); writeln"Problem 41"; -goal HOL.thy "(! z. ? y. ! x. f x y = (f x z & ~ f x x)) \ +goal HOL.thy "(! z. ? y. ! x. f x y = (f x z & ~ f x x)) \ \ --> ~ (? z. ! x. f x z)"; by (best_tac HOL_cs 1); result(); @@ -341,25 +341,25 @@ writeln"Problem 43 NOT PROVED AUTOMATICALLY"; goal HOL.thy - "(! x::'a. ! y::'a. q x y = (! z. p z x = (p z y::bool))) \ + "(! x::'a. ! y::'a. q x y = (! z. p z x = (p z y::bool))) \ \ --> (! x. (! y. q x y = (q y x::bool)))"; writeln"Problem 44"; -goal HOL.thy "(! x. f(x) --> \ +goal HOL.thy "(! x. f(x) --> \ \ (? y. g(y) & h x y & (? y. g(y) & ~ h x y))) & \ -\ (? x. j(x) & (! y. g(y) --> h x y)) \ +\ (? x. j(x) & (! y. g(y) --> h x y)) \ \ --> (? x. j(x) & ~f(x))"; by (fast_tac HOL_cs 1); result(); writeln"Problem 45"; goal HOL.thy - "(! x. f(x) & (! y. g(y) & h x y --> j x y) \ -\ --> (! y. g(y) & h x y --> k(y))) & \ -\ ~ (? y. l(y) & k(y)) & \ -\ (? x. f(x) & (! y. h x y --> l(y)) \ -\ & (! y. g(y) & h x y --> j x y)) \ + "(! x. f(x) & (! y. g(y) & h x y --> j x y) \ +\ --> (! y. g(y) & h x y --> k(y))) & \ +\ ~ (? y. l(y) & k(y)) & \ +\ (? x. f(x) & (! y. h x y --> l(y)) \ +\ & (! y. g(y) & h x y --> j x y)) \ \ --> (? x. f(x) & ~ (? y. g(y) & h x y))"; by (best_tac HOL_cs 1); result(); @@ -376,7 +376,7 @@ (*Hard because it involves substitution for Vars; the type constraint ensures that x,y,z have the same type as a,b,u. *) goal HOL.thy "(? x y::'a. ! z. z=x | z=y) & P(a) & P(b) & (~a=b) \ -\ --> (! u::'a.P(u))"; +\ --> (! u::'a.P(u))"; by (Classical.safe_tac HOL_cs); by (res_inst_tac [("x","a")] allE 1); by (assume_tac 1); @@ -454,8 +454,8 @@ writeln"Problem 62 as corrected in AAR newletter #31"; goal HOL.thy - "(ALL x. p a & (p x --> p(f x)) --> p(f(f x))) = \ -\ (ALL x. (~ p a | p x | p(f(f x))) & \ + "(ALL x. p a & (p x --> p(f x)) --> p(f(f x))) = \ +\ (ALL x. (~ p a | p x | p(f(f x))) & \ \ (~ p a | ~ p(f x) | p(f(f x))))"; by (fast_tac HOL_cs 1); result(); diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/ex/meson.ML --- a/src/HOL/ex/meson.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/ex/meson.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/ex/meson +(* Title: HOL/ex/meson ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge The MESON resolution proof procedure for HOL @@ -13,7 +13,7 @@ (*Prove theorems using fast_tac*) fun prove_fun s = prove_goal HOL.thy s - (fn prems => [ cut_facts_tac prems 1, fast_tac HOL_cs 1 ]); + (fn prems => [ cut_facts_tac prems 1, fast_tac HOL_cs 1 ]); (**** Negation Normal Form ****) @@ -160,38 +160,38 @@ (*Permits forward proof from rules that discharge assumptions*) fun forward_res nf state = case Sequence.pull - (tapply(ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)), - state)) + (tapply(ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)), + state)) of Some(th,_) => th | None => raise THM("forward_res", 0, [state]); (*Negation Normal Form*) val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD, - not_impD, not_iffD, not_allD, not_exD, not_notD]; + not_impD, not_iffD, not_allD, not_exD, not_notD]; fun make_nnf th = make_nnf (tryres(th, nnf_rls)) handle THM _ => - forward_res make_nnf - (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward])) + forward_res make_nnf + (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward])) handle THM _ => th; (*Are any of the constants in "bs" present in the term?*) fun has_consts bs = let fun has (Const(a,_)) = a mem bs - | has (f$u) = has f orelse has u - | has (Abs(_,_,t)) = has t - | has _ = false + | has (f$u) = has f orelse has u + | has (Abs(_,_,t)) = has t + | has _ = false in has end; (*Pull existential quantifiers (Skolemization)*) fun skolemize th = if not (has_consts ["Ex"] (prop_of th)) then th else skolemize (tryres(th, [choice, conj_exD1, conj_exD2, - disj_exD, disj_exD1, disj_exD2])) + disj_exD, disj_exD1, disj_exD2])) handle THM _ => - skolemize (forward_res skolemize - (tryres (th, [conj_forward, disj_forward, all_forward]))) + skolemize (forward_res skolemize + (tryres (th, [conj_forward, disj_forward, all_forward]))) handle THM _ => forward_res skolemize (th RS ex_forward); @@ -235,14 +235,14 @@ else if not (has_consts ["All","op &"] (prop_of th)) then th::ths else (*conjunction?*) cnf_aux seen (th RS conjunct1, - cnf_aux seen (th RS conjunct2, ths)) + cnf_aux seen (th RS conjunct2, ths)) handle THM _ => (*universal quant?*) - cnf_aux seen (freeze_spec th, ths) + cnf_aux seen (freeze_spec th, ths) handle THM _ => (*disjunction?*) let val tac = - (METAHYPS (resop (cnf_nil seen)) 1) THEN - (STATE (fn st' => - METAHYPS (resop (cnf_nil (literals (concl_of st') @ seen))) 1)) + (METAHYPS (resop (cnf_nil seen)) 1) THEN + (STATE (fn st' => + METAHYPS (resop (cnf_nil (literals (concl_of st') @ seen))) 1)) in Sequence.list_of_s (tapply(tac, th RS disj_forward)) @ ths end and cnf_nil seen th = cnf_aux seen (th,[]); @@ -268,9 +268,9 @@ (*Forward proof, passing extra assumptions as theorems to the tactic*) fun forward_res2 nf hyps state = case Sequence.pull - (tapply(REPEAT - (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1), - state)) + (tapply(REPEAT + (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1), + state)) of Some(th,_) => th | None => raise THM("forward_res2", 0, [state]); @@ -279,7 +279,7 @@ fun nodups_aux rls th = nodups_aux rls (th RS disj_assoc) handle THM _ => tryres(th,rls) handle THM _ => tryres(forward_res2 nodups_aux rls (th RS disj_forward2), - [disj_FalseD1, disj_FalseD2, asm_rl]) + [disj_FalseD1, disj_FalseD2, asm_rl]) handle THM _ => th; (*Remove duplicate literals, if there are any*) @@ -292,7 +292,7 @@ (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*) fun assoc_right th = assoc_right (th RS disj_assoc) - handle THM _ => th; + handle THM _ => th; (*Must check for negative literal first!*) val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule]; @@ -318,15 +318,15 @@ (*Create a Horn clause*) fun make_horn crules th = make_horn crules (tryres(th,crules)) - handle THM _ => th; + handle THM _ => th; (*Generate Horn clauses for all contrapositives of a clause*) fun add_contras crules (th,hcs) = let fun rots (0,th) = hcs - | rots (k,th) = zero_var_indexes (make_horn crules th) :: - rots(k-1, assoc_right (th RS disj_comm)) + | rots (k,th) = zero_var_indexes (make_horn crules th) :: + rots(k-1, assoc_right (th RS disj_comm)) in case nliterals(prop_of th) of - 1 => th::hcs + 1 => th::hcs | n => rots(n, assoc_right th) end; @@ -342,7 +342,7 @@ (***** MESON PROOF PROCEDURE *****) fun rhyps (Const("==>",_) $ (Const("Trueprop",_) $ A) $ phi, - As) = rhyps(phi, A::As) + As) = rhyps(phi, A::As) | rhyps (_, As) = As; (** Detecting repeated assumptions in a subgoal **) @@ -355,7 +355,7 @@ | has_reps [_] = false | has_reps [t,u] = (t aconv u) | has_reps ts = (foldl ins_term (Net.empty, ts); false) - handle INSERT => true; + handle INSERT => true; (*Loop checking: FAIL if trying to prove the same thing twice -- repeated literals*) @@ -394,24 +394,24 @@ fun MESON sko_tac = SELECT_GOAL (EVERY1 [rtac ccontr, - METAHYPS (fn negs => - EVERY1 [skolemize_tac negs, - METAHYPS (sko_tac o make_clauses)])]); + METAHYPS (fn negs => + EVERY1 [skolemize_tac negs, + METAHYPS (sko_tac o make_clauses)])]); fun best_meson_tac sizef = MESON (fn cls => - resolve_tac (gocls cls) 1 - THEN_BEST_FIRST - (has_fewer_prems 1, sizef, - prolog_step_tac (make_horns cls) 1)); + resolve_tac (gocls cls) 1 + THEN_BEST_FIRST + (has_fewer_prems 1, sizef, + prolog_step_tac (make_horns cls) 1)); (*First, breaks the goal into independent units*) val safe_meson_tac = SELECT_GOAL (TRY (safe_tac HOL_cs) THEN - TRYALL (best_meson_tac size_of_subgoals)); + TRYALL (best_meson_tac size_of_subgoals)); val depth_meson_tac = MESON (fn cls => EVERY [resolve_tac (gocls cls) 1, - depth_prolog_tac (make_horns cls)]); + depth_prolog_tac (make_horns cls)]); writeln"Reached end of file."; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/ex/mesontest.ML --- a/src/HOL/ex/mesontest.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/ex/mesontest.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/ex/meson +(* Title: HOL/ex/meson ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge Test data for the MESON proof procedure @@ -14,7 +14,7 @@ val xsko = skolemize nnf; by (cut_facts_tac [xsko] 1 THEN REPEAT (etac exE 1)); val [_,sko] = gethyps 1; -val clauses = make_clauses [sko]; +val clauses = make_clauses [sko]; val horns = make_horns clauses; val go::_ = neg_clauses clauses; @@ -45,8 +45,8 @@ val xsko25 = skolemize nnf25; by (cut_facts_tac [xsko25] 1 THEN REPEAT (etac exE 1)); val [_,sko25] = gethyps 1; -val clauses25 = make_clauses [sko25]; (*7 clauses*) -val horns25 = make_horns clauses25; (*16 Horn clauses*) +val clauses25 = make_clauses [sko25]; (*7 clauses*) +val horns25 = make_horns clauses25; (*16 Horn clauses*) val go25::_ = neg_clauses clauses25; goal HOL.thy "False"; @@ -55,8 +55,8 @@ writeln"Problem 26"; -goal HOL.thy "((? x. p(x)) = (? x. q(x))) & \ -\ (! x. ! y. p(x) & q(y) --> (r(x) = s(y))) \ +goal HOL.thy "((? x. p(x)) = (? x. q(x))) & \ +\ (! x. ! y. p(x) & q(y) --> (r(x) = s(y))) \ \ --> ((! x. p(x)-->r(x)) = (! x. q(x)-->s(x)))"; by (rtac ccontr 1); val [prem26] = gethyps 1; @@ -64,18 +64,18 @@ val xsko26 = skolemize nnf26; by (cut_facts_tac [xsko26] 1 THEN REPEAT (etac exE 1)); val [_,sko26] = gethyps 1; -val clauses26 = make_clauses [sko26]; (*9 clauses*) -val horns26 = make_horns clauses26; (*24 Horn clauses*) +val clauses26 = make_clauses [sko26]; (*9 clauses*) +val horns26 = make_horns clauses26; (*24 Horn clauses*) val go26::_ = neg_clauses clauses26; goal HOL.thy "False"; by (rtac (make_goal go26) 1); -by (depth_prolog_tac horns26); (*6 secs*) +by (depth_prolog_tac horns26); (*6 secs*) writeln"Problem 43 NOW PROVED AUTOMATICALLY!!"; -goal HOL.thy "(! x. ! y. q x y = (! z. p z x = (p z y::bool))) \ +goal HOL.thy "(! x. ! y. q x y = (! z. p z x = (p z y::bool))) \ \ --> (! x. (! y. q x y = (q y x::bool)))"; by (rtac ccontr 1); val [prem43] = gethyps 1; @@ -83,8 +83,8 @@ val xsko43 = skolemize nnf43; by (cut_facts_tac [xsko43] 1 THEN REPEAT (etac exE 1)); val [_,sko43] = gethyps 1; -val clauses43 = make_clauses [sko43]; (*6*) -val horns43 = make_horns clauses43; (*16*) +val clauses43 = make_clauses [sko43]; (*6*) +val horns43 = make_horns clauses43; (*16*) val go43::_ = neg_clauses clauses43; goal HOL.thy "False"; @@ -276,8 +276,8 @@ result(); writeln"Problem 26"; -goal HOL.thy "((? x. p(x)) = (? x. q(x))) & \ -\ (! x. ! y. p(x) & q(y) --> (r(x) = s(y))) \ +goal HOL.thy "((? x. p(x)) = (? x. q(x))) & \ +\ (! x. ! y. p(x) & q(y) --> (r(x) = s(y))) \ \ --> ((! x. p(x)-->r(x)) = (! x. q(x)-->s(x)))"; by (safe_meson_tac 1); result(); @@ -303,7 +303,7 @@ goal HOL.thy "(? x. F(x)) & (? y. G(y)) \ \ --> ( ((! x. F(x)-->H(x)) & (! y. G(y)-->J(y))) = \ \ (! x y. F(x) & G(y) --> H(x) & J(y)))"; -by (safe_meson_tac 1); (*5 secs*) +by (safe_meson_tac 1); (*5 secs*) result(); writeln"Problem 30"; @@ -332,16 +332,16 @@ writeln"Problem 33"; goal HOL.thy "(! x. P(a) & (P(x)-->P(b))-->P(c)) = \ \ (! x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))"; -by (safe_meson_tac 1); (*5.6 secs*) +by (safe_meson_tac 1); (*5.6 secs*) result(); writeln"Problem 34 AMENDED (TWICE!!)"; (*Andrews's challenge*) -goal HOL.thy "((? x. ! y. p(x) = p(y)) = \ -\ ((? x. q(x)) = (! y. p(y)))) = \ -\ ((? x. ! y. q(x) = q(y)) = \ +goal HOL.thy "((? x. ! y. p(x) = p(y)) = \ +\ ((? x. q(x)) = (! y. p(y)))) = \ +\ ((? x. ! y. q(x) = q(y)) = \ \ ((? x. p(x)) = (! y. q(y))))"; -by (safe_meson_tac 1); (*90 secs*) +by (safe_meson_tac 1); (*90 secs*) result(); writeln"Problem 35"; @@ -352,7 +352,7 @@ writeln"Problem 36"; goal HOL.thy "(! x. ? y. J x y) & \ \ (! x. ? y. G x y) & \ -\ (! x y. J x y | G x y --> \ +\ (! x y. J x y | G x y --> \ \ (! z. J y z | G y z --> H x z)) \ \ --> (! x. ? y. H x y)"; by (safe_meson_tac 1); @@ -369,12 +369,12 @@ writeln"Problem 38"; goal HOL.thy - "(! x. p(a) & (p(x) --> (? y. p(y) & r x y)) --> \ -\ (? z. ? w. p(z) & r x w & r w z)) = \ -\ (! x. (~p(a) | p(x) | (? z. ? w. p(z) & r x w & r w z)) & \ -\ (~p(a) | ~(? y. p(y) & r x y) | \ + "(! x. p(a) & (p(x) --> (? y. p(y) & r x y)) --> \ +\ (? z. ? w. p(z) & r x w & r w z)) = \ +\ (! x. (~p(a) | p(x) | (? z. ? w. p(z) & r x w & r w z)) & \ +\ (~p(a) | ~(? y. p(y) & r x y) | \ \ (? z. ? w. p(z) & r x w & r w z)))"; -by (safe_meson_tac 1); (*62 secs*) +by (safe_meson_tac 1); (*62 secs*) result(); writeln"Problem 39"; @@ -389,7 +389,7 @@ result(); writeln"Problem 41"; -goal HOL.thy "(! z. (? y. (! x. f x y = (f x z & ~ f x x)))) \ +goal HOL.thy "(! z. (? y. (! x. f x y = (f x z & ~ f x x)))) \ \ --> ~ (? z. ! x. f x z)"; by (safe_meson_tac 1); result(); @@ -400,54 +400,54 @@ result(); writeln"Problem 43 NOW PROVED AUTOMATICALLY!!"; -goal HOL.thy "(! x. ! y. q x y = (! z. p z x = (p z y::bool))) \ +goal HOL.thy "(! x. ! y. q x y = (! z. p z x = (p z y::bool))) \ \ --> (! x. (! y. q x y = (q y x::bool)))"; by (safe_meson_tac 1); result(); writeln"Problem 44"; -goal HOL.thy "(! x. f(x) --> \ -\ (? y. g(y) & h x y & (? y. g(y) & ~ h x y))) & \ -\ (? x. j(x) & (! y. g(y) --> h x y)) \ +goal HOL.thy "(! x. f(x) --> \ +\ (? y. g(y) & h x y & (? y. g(y) & ~ h x y))) & \ +\ (? x. j(x) & (! y. g(y) --> h x y)) \ \ --> (? x. j(x) & ~f(x))"; by (safe_meson_tac 1); result(); writeln"Problem 45"; -goal HOL.thy "(! x. f(x) & (! y. g(y) & h x y --> j x y) \ -\ --> (! y. g(y) & h x y --> k(y))) & \ -\ ~ (? y. l(y) & k(y)) & \ -\ (? x. f(x) & (! y. h x y --> l(y)) \ -\ & (! y. g(y) & h x y --> j x y)) \ +goal HOL.thy "(! x. f(x) & (! y. g(y) & h x y --> j x y) \ +\ --> (! y. g(y) & h x y --> k(y))) & \ +\ ~ (? y. l(y) & k(y)) & \ +\ (? x. f(x) & (! y. h x y --> l(y)) \ +\ & (! y. g(y) & h x y --> j x y)) \ \ --> (? x. f(x) & ~ (? y. g(y) & h x y))"; -by (safe_meson_tac 1); (*11 secs*) +by (safe_meson_tac 1); (*11 secs*) result(); writeln"Problem 46"; goal HOL.thy - "(! x. f(x) & (! y. f(y) & h y x --> g(y)) --> g(x)) & \ -\ ((? x.f(x) & ~g(x)) --> \ -\ (? x. f(x) & ~g(x) & (! y. f(y) & ~g(y) --> j x y))) & \ -\ (! x y. f(x) & f(y) & h x y --> ~j y x) \ + "(! x. f(x) & (! y. f(y) & h y x --> g(y)) --> g(x)) & \ +\ ((? x.f(x) & ~g(x)) --> \ +\ (? x. f(x) & ~g(x) & (! y. f(y) & ~g(y) --> j x y))) & \ +\ (! x y. f(x) & f(y) & h x y --> ~j y x) \ \ --> (! x. f(x) --> g(x))"; -by (safe_meson_tac 1); (*11 secs*) +by (safe_meson_tac 1); (*11 secs*) result(); (*The Los problem? Circulated by John Harrison*) -goal HOL.thy "(! x y z. P x y & P y z --> P x z) & \ -\ (! x y z. Q x y & Q y z --> Q x z) & \ -\ (! x y. P x y --> P y x) & \ -\ (! (x::'a) y. P x y | Q x y) \ +goal HOL.thy "(! x y z. P x y & P y z --> P x z) & \ +\ (! x y z. Q x y & Q y z --> Q x z) & \ +\ (! x y. P x y --> P y x) & \ +\ (! (x::'a) y. P x y | Q x y) \ \ --> (! x y. P x y) | (! x y. Q x y)"; by (safe_meson_tac 1); result(); (*A similar example, suggested by Johannes Schumann and credited to Pelletier*) goal HOL.thy "(!x y z. P x y --> P y z --> P x z) --> \ -\ (!x y z. Q x y --> Q y z --> Q x z) --> \ -\ (!x y.Q x y --> Q y x) --> (!x y. P x y | Q x y) --> \ -\ (!x y.P x y) | (!x y.Q x y)"; -by (safe_meson_tac 1); (*32 secs*) +\ (!x y z. Q x y --> Q y z --> Q x z) --> \ +\ (!x y.Q x y --> Q y x) --> (!x y. P x y | Q x y) --> \ +\ (!x y.P x y) | (!x y.Q x y)"; +by (safe_meson_tac 1); (*32 secs*) result(); writeln"Problem 50"; @@ -498,8 +498,8 @@ writeln"Problem 62 as corrected in AAR newletter #31"; goal HOL.thy - "(ALL x. p a & (p x --> p(f x)) --> p(f(f x))) = \ -\ (ALL x. (~ p a | p x | p(f(f x))) & \ + "(ALL x. p a & (p x --> p(f x)) --> p(f(f x))) = \ +\ (ALL x. (~ p a | p x | p(f(f x))) & \ \ (~ p a | ~ p(f x) | p(f(f x))))"; by (safe_meson_tac 1); result(); diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/ex/rel.ML --- a/src/HOL/ex/rel.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/ex/rel.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/ex/rel +(* Title: HOL/ex/rel ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge Domain, range of a relation or function -- NOT YET WORKING @@ -11,9 +11,9 @@ val thy = extend_theory Univ.thy "Rel" ([], [], [], [], [ - (["domain"], "('a * 'b)set => 'a set"), - (["range2"], "('a * 'b)set => 'b set"), - (["field"], "('a * 'a)set => 'a set") + (["domain"], "('a * 'b)set => 'a set"), + (["range2"], "('a * 'b)set => 'b set"), + (["field"], "('a * 'a)set => 'a set") ], None) [ diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/ex/set.ML --- a/src/HOL/ex/set.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/ex/set.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/ex/set.ML +(* Title: HOL/ex/set.ML ID: $Id$ - Author: Tobias Nipkow, Cambridge University Computer Laboratory + Author: Tobias Nipkow, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge Cantor's Theorem; the Schroeder-Berstein Theorem. @@ -62,8 +62,8 @@ val [compl,fg,Xa] = goal Lfp.thy "[| Compl(f``X) = g``Compl(X); f(a)=g(b); a:X |] ==> b:X"; by (EVERY1 [rtac (not_Compl RS subst), rtac contra_imageI, - rtac (compl RS subst), rtac (fg RS subst), stac not_Compl, - rtac imageI, rtac Xa]); + rtac (compl RS subst), rtac (fg RS subst), stac not_Compl, + rtac imageI, rtac Xa]); qed "disj_lemma"; goal Lfp.thy "range(%z. if z:X then f(z) else g(z)) = f``X Un g``Compl(X)"; @@ -122,11 +122,11 @@ by (rtac exI 1); by (rtac bij_if_then_else 1); by (EVERY [rtac refl 4, rtac (injf RS inj_imp) 1, - rtac (injg RS inj_onto_Inv) 1]); + rtac (injg RS inj_onto_Inv) 1]); by (EVERY1 [etac ssubst, stac double_complement, rtac subsetI, - etac imageE, etac ssubst, rtac rangeI]); + etac imageE, etac ssubst, rtac rangeI]); by (EVERY1 [etac ssubst, stac double_complement, - rtac (injg RS inv_image_comp RS sym)]); + rtac (injg RS inv_image_comp RS sym)]); qed "schroeder_bernstein"; writeln"Reached end of file."; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/ex/unsolved.ML --- a/src/HOL/ex/unsolved.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/ex/unsolved.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/ex/unsolved +(* Title: HOL/ex/unsolved ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge Problems that currently defeat the MESON procedure as well as best_tac @@ -14,22 +14,22 @@ writeln"Problem 47 Schubert's Steamroller"; goal HOL.thy - "(! x. P1(x) --> P0(x)) & (? x.P1(x)) & \ -\ (! x. P2(x) --> P0(x)) & (? x.P2(x)) & \ -\ (! x. P3(x) --> P0(x)) & (? x.P3(x)) & \ -\ (! x. P4(x) --> P0(x)) & (? x.P4(x)) & \ -\ (! x. P5(x) --> P0(x)) & (? x.P5(x)) & \ -\ (! x. Q1(x) --> Q0(x)) & (? x.Q1(x)) & \ -\ (! x. P0(x) --> ((! y.Q0(y)-->R(x,y)) | \ -\ (! y.P0(y) & S(y,x) & \ -\ (? z.Q0(z)&R(y,z)) --> R(x,y)))) & \ -\ (! x y. P3(y) & (P5(x)|P4(x)) --> S(x,y)) & \ -\ (! x y. P3(x) & P2(y) --> S(x,y)) & \ -\ (! x y. P2(x) & P1(y) --> S(x,y)) & \ -\ (! x y. P1(x) & (P2(y)|Q1(y)) --> ~R(x,y)) & \ -\ (! x y. P3(x) & P4(y) --> R(x,y)) & \ -\ (! x y. P3(x) & P5(y) --> ~R(x,y)) & \ -\ (! x. (P4(x)|P5(x)) --> (? y.Q0(y) & R(x,y))) \ + "(! x. P1(x) --> P0(x)) & (? x.P1(x)) & \ +\ (! x. P2(x) --> P0(x)) & (? x.P2(x)) & \ +\ (! x. P3(x) --> P0(x)) & (? x.P3(x)) & \ +\ (! x. P4(x) --> P0(x)) & (? x.P4(x)) & \ +\ (! x. P5(x) --> P0(x)) & (? x.P5(x)) & \ +\ (! x. Q1(x) --> Q0(x)) & (? x.Q1(x)) & \ +\ (! x. P0(x) --> ((! y.Q0(y)-->R(x,y)) | \ +\ (! y.P0(y) & S(y,x) & \ +\ (? z.Q0(z)&R(y,z)) --> R(x,y)))) & \ +\ (! x y. P3(y) & (P5(x)|P4(x)) --> S(x,y)) & \ +\ (! x y. P3(x) & P2(y) --> S(x,y)) & \ +\ (! x y. P2(x) & P1(y) --> S(x,y)) & \ +\ (! x y. P1(x) & (P2(y)|Q1(y)) --> ~R(x,y)) & \ +\ (! x y. P3(x) & P4(y) --> R(x,y)) & \ +\ (! x y. P3(x) & P5(y) --> ~R(x,y)) & \ +\ (! x. (P4(x)|P5(x)) --> (? y.Q0(y) & R(x,y))) \ \ --> (? x y. P0(x) & P0(y) & (? z. Q1(z) & R(y,z) & R(x,y)))"; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/ind_syntax.ML --- a/src/HOL/ind_syntax.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/ind_syntax.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/ind_syntax.ML +(* Title: HOL/ind_syntax.ML ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge Abstract Syntax functions for Inductive Definitions @@ -69,9 +69,9 @@ (** Disjoint sum type **) fun mk_sum (T1,T2) = Type("+", [T1,T2]); -val Inl = Const("Inl", dummyT) -and Inr = Const("Inr", dummyT); (*correct types added later!*) -(*val elim = Const("case", [iT-->iT, iT-->iT, iT]--->iT)*) +val Inl = Const("Inl", dummyT) +and Inr = Const("Inr", dummyT); (*correct types added later!*) +(*val elim = Const("case", [iT-->iT, iT-->iT, iT]--->iT)*) fun summands (Type("+", [T1,T2])) = summands T1 @ summands T2 | summands T = [T]; @@ -79,32 +79,32 @@ (*Given the destination type, fills in correct types of an Inl/Inr nest*) fun mend_sum_types (h,T) = (case (h,T) of - (Const("Inl",_) $ h1, Type("+", [T1,T2])) => - Const("Inl", T1 --> T) $ (mend_sum_types (h1, T1)) + (Const("Inl",_) $ h1, Type("+", [T1,T2])) => + Const("Inl", T1 --> T) $ (mend_sum_types (h1, T1)) | (Const("Inr",_) $ h2, Type("+", [T1,T2])) => - Const("Inr", T2 --> T) $ (mend_sum_types (h2, T2)) + Const("Inr", T2 --> T) $ (mend_sum_types (h2, T2)) | _ => h); (*simple error-checking in the premises of an inductive definition*) fun chk_prem rec_hd (Const("op &",_) $ _ $ _) = - error"Premises may not be conjuctive" + error"Premises may not be conjuctive" | chk_prem rec_hd (Const("op :",_) $ t $ X) = - deny (Logic.occs(rec_hd,t)) "Recursion term on left of member symbol" + deny (Logic.occs(rec_hd,t)) "Recursion term on left of member symbol" | chk_prem rec_hd t = - deny (Logic.occs(rec_hd,t)) "Recursion term in side formula"; + deny (Logic.occs(rec_hd,t)) "Recursion term in side formula"; (*Return the conclusion of a rule, of the form t:X*) fun rule_concl rl = let val Const("Trueprop",_) $ (Const("op :",_) $ t $ X) = - Logic.strip_imp_concl rl + Logic.strip_imp_concl rl in (t,X) end; (*As above, but return error message if bad*) fun rule_concl_msg sign rl = rule_concl rl handle Bind => error ("Ill-formed conclusion of introduction rule: " ^ - Sign.string_of_term sign rl); + Sign.string_of_term sign rl); (*For simplifying the elimination rule*) val sumprod_free_SEs = @@ -123,7 +123,7 @@ (*Includes rules for Suc and Pair since they are common constructions*) val elim_rls = [asm_rl, FalseE, (*Suc_neq_Zero, Zero_neq_Suc, - make_elim Suc_inject, *) - refl_thin, conjE, exE, disjE]; + make_elim Suc_inject, *) + refl_thin, conjE, exE, disjE]; end; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/indrule.ML --- a/src/HOL/indrule.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/indrule.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/indrule.ML +(* Title: HOL/indrule.ML ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge Induction rule module -- for Inductive/Coinductive Definitions @@ -10,14 +10,14 @@ signature INDRULE = sig - val induct : thm (*main induction rule*) - val mutual_induct : thm (*mutual induction rule*) + val induct : thm (*main induction rule*) + val mutual_induct : thm (*mutual induction rule*) end; functor Indrule_Fun (structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end and - Intr_elim: sig include INTR_ELIM INTR_ELIM_AUX end) : INDRULE = + Intr_elim: sig include INTR_ELIM INTR_ELIM_AUX end) : INDRULE = let val sign = sign_of Inductive.thy; @@ -32,7 +32,7 @@ (*** Prove the main induction rule ***) -val pred_name = "P"; (*name for predicate variables*) +val pred_name = "P"; (*name for predicate variables*) val big_rec_def::part_rec_defs = Intr_elim.defs; @@ -40,25 +40,25 @@ ind_alist = [(rec_tm1,pred1),...] -- associates predicates with rec ops prem is a premise of an intr rule*) fun add_induct_prem ind_alist (prem as Const("Trueprop",_) $ - (Const("op :",_)$t$X), iprems) = + (Const("op :",_)$t$X), iprems) = (case gen_assoc (op aconv) (ind_alist, X) of - Some pred => prem :: Ind_Syntax.mk_Trueprop (pred $ t) :: iprems - | None => (*possibly membership in M(rec_tm), for M monotone*) - let fun mk_sb (rec_tm,pred) = - (case binder_types (fastype_of pred) of - [T] => (rec_tm, - Ind_Syntax.Int_const T $ rec_tm $ - (Ind_Syntax.Collect_const T $ pred)) - | _ => error - "Bug: add_induct_prem called with non-unary predicate") - in subst_free (map mk_sb ind_alist) prem :: iprems end) + Some pred => prem :: Ind_Syntax.mk_Trueprop (pred $ t) :: iprems + | None => (*possibly membership in M(rec_tm), for M monotone*) + let fun mk_sb (rec_tm,pred) = + (case binder_types (fastype_of pred) of + [T] => (rec_tm, + Ind_Syntax.Int_const T $ rec_tm $ + (Ind_Syntax.Collect_const T $ pred)) + | _ => error + "Bug: add_induct_prem called with non-unary predicate") + in subst_free (map mk_sb ind_alist) prem :: iprems end) | add_induct_prem ind_alist (prem,iprems) = prem :: iprems; (*Make a premise of the induction rule.*) fun induct_prem ind_alist intr = let val quantfrees = map dest_Free (term_frees intr \\ rec_params) val iprems = foldr (add_induct_prem ind_alist) - (Logic.strip_imp_prems intr,[]) + (Logic.strip_imp_prems intr,[]) val (t,X) = Ind_Syntax.rule_concl intr val (Some pred) = gen_assoc (op aconv) (ind_alist, X) val concl = Ind_Syntax.mk_Trueprop (pred $ t) @@ -68,8 +68,8 @@ (*Avoids backtracking by delivering the correct premise to each goal*) fun ind_tac [] 0 = all_tac | ind_tac(prem::prems) i = - DEPTH_SOLVE_1 (ares_tac [Part_eqI, prem, refl] i) THEN - ind_tac prems (i-1); + DEPTH_SOLVE_1 (ares_tac [Part_eqI, prem, refl] i) THEN + ind_tac prems (i-1); val pred = Free(pred_name, elem_type --> Ind_Syntax.boolT); @@ -85,15 +85,15 @@ prove_goalw_cterm part_rec_defs (cterm_of sign (Logic.list_implies (ind_prems, - Ind_Syntax.mk_Trueprop (Ind_Syntax.mk_all_imp - (big_rec_tm,pred))))) + Ind_Syntax.mk_Trueprop (Ind_Syntax.mk_all_imp + (big_rec_tm,pred))))) (fn prems => [rtac (impI RS allI) 1, - DETERM (etac Intr_elim.raw_induct 1), - asm_full_simp_tac (!simpset addsimps [Part_Collect]) 1, - REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE, disjE] - ORELSE' hyp_subst_tac)), - ind_tac (rev prems) (length prems)]) + DETERM (etac Intr_elim.raw_induct 1), + asm_full_simp_tac (!simpset addsimps [Part_Collect]) 1, + REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE, disjE] + ORELSE' hyp_subst_tac)), + ind_tac (rev prems) (length prems)]) handle e => print_sign_exn sign e; (*** Prove the simultaneous induction rule ***) @@ -109,11 +109,11 @@ val pfree = Free(pred_name ^ "_" ^ rec_name, T) val frees = mk_frees "za" (binder_types T) val qconcl = - foldr Ind_Syntax.mk_all - (frees, - Ind_Syntax.imp $ (Ind_Syntax.mk_mem - (foldr1 Ind_Syntax.mk_Pair frees, rec_tm)) - $ (list_comb (pfree,frees))) + foldr Ind_Syntax.mk_all + (frees, + Ind_Syntax.imp $ (Ind_Syntax.mk_mem + (foldr1 Ind_Syntax.mk_Pair frees, rec_tm)) + $ (list_comb (pfree,frees))) in (Ind_Syntax.ap_split Ind_Syntax.boolT pfree (binder_types T), qconcl) end; @@ -129,21 +129,21 @@ Ind_Syntax.mk_Trueprop (Ind_Syntax.mk_all_imp (big_rec_tm, - Abs("z", elem_type, - fold_bal (app Ind_Syntax.conj) - (map mk_rec_imp (Inductive.rec_tms~~preds))))) + Abs("z", elem_type, + fold_bal (app Ind_Syntax.conj) + (map mk_rec_imp (Inductive.rec_tms~~preds))))) and mutual_induct_concl = Ind_Syntax.mk_Trueprop (fold_bal (app Ind_Syntax.conj) qconcls); val lemma = (*makes the link between the two induction rules*) prove_goalw_cterm part_rec_defs - (cterm_of sign (Logic.mk_implies (induct_concl, - mutual_induct_concl))) - (fn prems => - [cut_facts_tac prems 1, - REPEAT (eresolve_tac [asm_rl, conjE, PartE, mp] 1 - ORELSE resolve_tac [allI, impI, conjI, Part_eqI, refl] 1 - ORELSE dresolve_tac [spec, mp, splitD] 1)]) + (cterm_of sign (Logic.mk_implies (induct_concl, + mutual_induct_concl))) + (fn prems => + [cut_facts_tac prems 1, + REPEAT (eresolve_tac [asm_rl, conjE, PartE, mp] 1 + ORELSE resolve_tac [allI, impI, conjI, Part_eqI, refl] 1 + ORELSE dresolve_tac [spec, mp, splitD] 1)]) handle e => print_sign_exn sign e; (*Mutual induction follows by freeness of Inl/Inr.*) @@ -164,43 +164,43 @@ | mutual_ind_tac(prem::prems) i = DETERM (SELECT_GOAL - ( - (*Simplify the assumptions and goal by unfolding Part and - using freeness of the Sum constructors; proves all but one + ( + (*Simplify the assumptions and goal by unfolding Part and + using freeness of the Sum constructors; proves all but one conjunct by contradiction*) - rewrite_goals_tac all_defs THEN - simp_tac (mut_ss addsimps [Part_def]) 1 THEN - IF_UNSOLVED (*simp_tac may have finished it off!*) - ((*simplify assumptions, but don't accept new rewrite rules!*) - asm_full_simp_tac (mut_ss setmksimps K[]) 1 THEN - (*unpackage and use "prem" in the corresponding place*) - REPEAT (rtac impI 1) THEN - rtac (rewrite_rule all_defs prem) 1 THEN - (*prem must not be REPEATed below: could loop!*) - DEPTH_SOLVE (FIRSTGOAL (ares_tac [impI] ORELSE' - eresolve_tac (conjE::mp::cmonos)))) - ) i) + rewrite_goals_tac all_defs THEN + simp_tac (mut_ss addsimps [Part_def]) 1 THEN + IF_UNSOLVED (*simp_tac may have finished it off!*) + ((*simplify assumptions, but don't accept new rewrite rules!*) + asm_full_simp_tac (mut_ss setmksimps K[]) 1 THEN + (*unpackage and use "prem" in the corresponding place*) + REPEAT (rtac impI 1) THEN + rtac (rewrite_rule all_defs prem) 1 THEN + (*prem must not be REPEATed below: could loop!*) + DEPTH_SOLVE (FIRSTGOAL (ares_tac [impI] ORELSE' + eresolve_tac (conjE::mp::cmonos)))) + ) i) THEN mutual_ind_tac prems (i-1); val _ = writeln " Proving the mutual induction rule..."; val mutual_induct_split = prove_goalw_cterm [] - (cterm_of sign - (Logic.list_implies (map (induct_prem (Inductive.rec_tms ~~ preds)) - Inductive.intr_tms, - mutual_induct_concl))) - (fn prems => - [rtac (quant_induct RS lemma) 1, - mutual_ind_tac (rev prems) (length prems)]) + (cterm_of sign + (Logic.list_implies (map (induct_prem (Inductive.rec_tms ~~ preds)) + Inductive.intr_tms, + mutual_induct_concl))) + (fn prems => + [rtac (quant_induct RS lemma) 1, + mutual_ind_tac (rev prems) (length prems)]) handle e => print_sign_exn sign e; (*Attempts to remove all occurrences of split*) val split_tac = REPEAT (SOMEGOAL (FIRST' [rtac splitI, - dtac splitD, - etac splitE, - bound_hyp_subst_tac])) + dtac splitD, + etac splitE, + bound_hyp_subst_tac])) THEN prune_params_tac; in @@ -210,7 +210,7 @@ val mutual_induct = if length Intr_elim.rec_names > 1 orelse - length (Ind_Syntax.factors elem_type) > 1 + length (Ind_Syntax.factors elem_type) > 1 then rule_by_tactic split_tac mutual_induct_split else TrueI; end diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/intr_elim.ML --- a/src/HOL/intr_elim.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/intr_elim.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,39 +1,39 @@ -(* Title: HOL/intr_elim.ML +(* Title: HOL/intr_elim.ML ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge Introduction/elimination rule module -- for Inductive/Coinductive Definitions *) -signature INDUCTIVE_ARG = (** Description of a (co)inductive def **) +signature INDUCTIVE_ARG = (** Description of a (co)inductive def **) sig val thy : theory (*new theory with inductive defs*) - val monos : thm list (*monotonicity of each M operator*) - val con_defs : thm list (*definitions of the constructors*) + val monos : thm list (*monotonicity of each M operator*) + val con_defs : thm list (*definitions of the constructors*) end; -signature INDUCTIVE_I = (** Terms read from the theory section **) +signature INDUCTIVE_I = (** Terms read from the theory section **) sig - val rec_tms : term list (*the recursive sets*) - val intr_tms : term list (*terms for the introduction rules*) + val rec_tms : term list (*the recursive sets*) + val intr_tms : term list (*terms for the introduction rules*) end; signature INTR_ELIM = sig val thy : theory (*copy of input theory*) - val defs : thm list (*definitions made in thy*) - val mono : thm (*monotonicity for the lfp definition*) - val intrs : thm list (*introduction rules*) - val elim : thm (*case analysis theorem*) - val mk_cases : thm list -> string -> thm (*generates case theorems*) + val defs : thm list (*definitions made in thy*) + val mono : thm (*monotonicity for the lfp definition*) + val intrs : thm list (*introduction rules*) + val elim : thm (*case analysis theorem*) + val mk_cases : thm list -> string -> thm (*generates case theorems*) end; -signature INTR_ELIM_AUX = (** Used to make induction rules **) +signature INTR_ELIM_AUX = (** Used to make induction rules **) sig - val raw_induct : thm (*raw induction rule from Fp.induct*) - val rec_names : string list (*names of recursive sets*) + val raw_induct : thm (*raw induction rule from Fp.induct*) + val rec_names : string list (*names of recursive sets*) end; (*prove intr/elim rules for a fixedpoint definition*) @@ -47,7 +47,7 @@ val _ = deny (big_rec_name mem map ! (stamps_of_thy Inductive.thy)) ("Definition " ^ big_rec_name ^ - " would clash with the theory of the same name!"); + " would clash with the theory of the same name!"); (*fetch fp definitions from the theory*) val big_rec_def::part_rec_defs = @@ -69,10 +69,10 @@ val mono = prove_goalw_cterm [] (cterm_of sign (Ind_Syntax.mk_Trueprop - (Const("mono", monoT --> Ind_Syntax.boolT) $ fp_abs))) + (Const("mono", monoT --> Ind_Syntax.boolT) $ fp_abs))) (fn _ => [rtac monoI 1, - REPEAT (ares_tac (basic_monos @ Inductive.monos) 1)]); + REPEAT (ares_tac (basic_monos @ Inductive.monos) 1)]); val unfold = standard (mono RS (big_rec_def RS Fp.Tarski)); @@ -97,12 +97,12 @@ (*combines disjI1 and disjI2 to access the corresponding nested disjunct...*) val mk_disj_rls = let fun f rl = rl RS disjI1 - and g rl = rl RS disjI2 + and g rl = rl RS disjI2 in accesses_bal(f, g, asm_rl) end; val intrs = map (uncurry (prove_goalw_cterm part_rec_defs)) (map (cterm_of sign) Inductive.intr_tms ~~ - map intro_tacsf (mk_disj_rls(length Inductive.intr_tms))); + map intro_tacsf (mk_disj_rls(length Inductive.intr_tms))); (********) val _ = writeln " Proving the elimination rule..."; @@ -110,8 +110,8 @@ (*Breaks down logical connectives in the monotonic function*) val basic_elim_tac = REPEAT (SOMEGOAL (eresolve_tac (Ind_Syntax.elim_rls @ - Ind_Syntax.sumprod_free_SEs) - ORELSE' bound_hyp_subst_tac)) + Ind_Syntax.sumprod_free_SEs) + ORELSE' bound_hyp_subst_tac)) THEN prune_params_tac; (*Applies freeness of the given constructors, which *must* be unfolded by @@ -122,7 +122,7 @@ *) fun con_elim_tac simps = let val elim_tac = REPEAT o (eresolve_tac (Ind_Syntax.elim_rls @ - Ind_Syntax.sumprod_free_SEs)) + Ind_Syntax.sumprod_free_SEs)) in ALLGOALS(EVERY'[elim_tac, asm_full_simp_tac (simpset_of "Nat" addsimps simps), elim_tac, @@ -144,7 +144,7 @@ (*String s should have the form t:Si where Si is an inductive set*) fun mk_cases defs s = rule_by_tactic (con_elim_tac defs) - (assume_read Inductive.thy s RS elim); + (assume_read Inductive.thy s RS elim); val raw_induct = standard ([big_rec_def, mono] MRS Fp.induct) and rec_names = rec_names diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/mono.ML --- a/src/HOL/mono.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/mono.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/mono.ML +(* Title: HOL/mono.ML ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge Monotonicity of various operations @@ -119,5 +119,5 @@ (*Used in intr_elim.ML and in individual datatype definitions*) val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono, - ex_mono, Collect_mono, Part_mono, in_mono]; + ex_mono, Collect_mono, Part_mono, in_mono]; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/simpdata.ML --- a/src/HOL/simpdata.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/simpdata.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/simpdata.ML +(* Title: HOL/simpdata.ML ID: $Id$ - Author: Tobias Nipkow + Author: Tobias Nipkow Copyright 1991 University of Cambridge Instantiation of the generic simplifier @@ -32,9 +32,9 @@ in atoms end; fun mk_meta_eq r = case concl_of r of - Const("==",_)$_$_ => r - | _$(Const("op =",_)$_$_) => r RS eq_reflection - | _$(Const("not",_)$_) => r RS not_P_imp_P_eq_False + Const("==",_)$_$_ => r + | _$(Const("op =",_)$_$_) => r RS eq_reflection + | _$(Const("not",_)$_) => r RS not_P_imp_P_eq_False | _ => r RS P_imp_P_eq_True; (* last 2 lines requires all formulae to be of the from Trueprop(.) *) @@ -42,7 +42,7 @@ val imp_cong = impI RSN (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))" - (fn _=> [fast_tac HOL_cs 1]) RS mp RS mp); + (fn _=> [fast_tac HOL_cs 1]) RS mp RS mp); val o_apply = prove_goalw HOL.thy [o_def] "(f o g)(x) = f(g(x))" (fn _ => [rtac refl 1]); @@ -86,9 +86,9 @@ val expand_if = prove_goal HOL.thy "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))" (fn _=> [ (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1), - rtac (if_P RS ssubst) 2, - rtac (if_not_P RS ssubst) 1, - REPEAT(fast_tac HOL_cs 1) ]); + rtac (if_P RS ssubst) 2, + rtac (if_not_P RS ssubst) 1, + REPEAT(fast_tac HOL_cs 1) ]); val if_bool_eq = prove_goal HOL.thy "(if P then Q else R) = ((P-->Q) & (~P-->R))" @@ -141,7 +141,7 @@ val conj_cong = impI RSN (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))" - (fn _=> [fast_tac HOL_cs 1]) RS mp RS mp); + (fn _=> [fast_tac HOL_cs 1]) RS mp RS mp); (** 'if' congruence rules: neither included by default! *) diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/subset.ML --- a/src/HOL/subset.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/subset.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/subset +(* Title: HOL/subset ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge Derived rules involving subsets @@ -21,7 +21,7 @@ val [prem] = goal Set.thy "[| !!X. X:A ==> X<=C |] ==> Union(A) <= C"; -br subsetI 1; +by (rtac subsetI 1); by (REPEAT (eresolve_tac [asm_rl, UnionE, prem RS subsetD] 1)); qed "Union_least"; @@ -34,7 +34,7 @@ val [prem] = goal Set.thy "[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A. B(x)) <= C"; -br subsetI 1; +by (rtac subsetI 1); by (REPEAT (eresolve_tac [asm_rl, UN_E, prem RS subsetD] 1)); qed "UN_least"; @@ -43,7 +43,7 @@ qed "UN1_upper"; val [prem] = goal Set.thy "[| !!x. B(x)<=C |] ==> (UN x. B(x)) <= C"; -br subsetI 1; +by (rtac subsetI 1); by (REPEAT (eresolve_tac [asm_rl, UN1_E, prem RS subsetD] 1)); qed "UN1_least"; @@ -51,35 +51,35 @@ (*** Big Intersection -- greatest lower bound of a set ***) val prems = goal Set.thy "B:A ==> Inter(A) <= B"; -br subsetI 1; +by (rtac subsetI 1); by (REPEAT (resolve_tac prems 1 ORELSE etac InterD 1)); qed "Inter_lower"; val [prem] = goal Set.thy "[| !!X. X:A ==> C<=X |] ==> C <= Inter(A)"; -br (InterI RS subsetI) 1; +by (rtac (InterI RS subsetI) 1); by (REPEAT (eresolve_tac [asm_rl, prem RS subsetD] 1)); qed "Inter_greatest"; val prems = goal Set.thy "a:A ==> (INT x:A. B(x)) <= B(a)"; -br subsetI 1; +by (rtac subsetI 1); by (REPEAT (resolve_tac prems 1 ORELSE etac INT_D 1)); qed "INT_lower"; val [prem] = goal Set.thy "[| !!x. x:A ==> C<=B(x) |] ==> C <= (INT x:A. B(x))"; -br (INT_I RS subsetI) 1; +by (rtac (INT_I RS subsetI) 1); by (REPEAT (eresolve_tac [asm_rl, prem RS subsetD] 1)); qed "INT_greatest"; goal Set.thy "(INT x. B(x)) <= B(a)"; -br subsetI 1; +by (rtac subsetI 1); by (REPEAT (resolve_tac prems 1 ORELSE etac INT1_D 1)); qed "INT1_lower"; val [prem] = goal Set.thy "[| !!x. C<=B(x) |] ==> C <= (INT x. B(x))"; -br (INT1_I RS subsetI) 1; +by (rtac (INT1_I RS subsetI) 1); by (REPEAT (eresolve_tac [asm_rl, prem RS subsetD] 1)); qed "INT1_greatest"; diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/thy_data.ML --- a/src/HOL/thy_data.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/thy_data.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/thy_data.ML +(* Title: HOL/thy_data.ML ID: $Id$ - Author: Carsten Clasohm + Author: Carsten Clasohm Copyright 1995 TU Muenchen Definitions that have to be reread after init_thy_reader has been invoked diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/thy_syntax.ML --- a/src/HOL/thy_syntax.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/thy_syntax.ML Tue Jan 30 15:24:36 1996 +0100 @@ -72,7 +72,7 @@ \\t val thy\t\t= thy\n\ \\t val monos\t\t= " ^ monos ^ "\n\ \\t val con_defs\t\t= " ^ con_defs ^ ");\n\n\ - \ in\n\ + \ in\n\ \ struct\n\ \ val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\ \ open Result\n\