# HG changeset patch # User paulson # Date 906539137 -7200 # Node ID 0f16c3b66ab4d479cf4edad7ab1096675f054616 # Parent 25e743eef48a39f91a9276e7b95821f3d46f2dab much renaming and reorganization diff -r 25e743eef48a -r 0f16c3b66ab4 src/HOL/Integ/Bin.ML --- a/src/HOL/Integ/Bin.ML Wed Sep 23 10:17:11 1998 +0200 +++ b/src/HOL/Integ/Bin.ML Wed Sep 23 10:25:37 1998 +0200 @@ -25,10 +25,6 @@ "NCons Min True = Min" (fn _ => [(Simp_tac 1)]); -qed_goal "NCons_BIT" Bin.thy - "NCons (w BIT x) b = (w BIT x) BIT b" - (fn _ => [(Simp_tac 1)]); - qed_goal "bin_succ_1" Bin.thy "bin_succ(w BIT True) = (bin_succ w) BIT False" (fn _ => [(Simp_tac 1)]); @@ -136,7 +132,7 @@ by (simp_tac (simpset() addsimps bin_add_simps) 1); by (rtac allI 1); by (induct_tac "w" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)))); +by (ALLGOALS (asm_simp_tac (simpset() addsimps bin_add_simps @ zadd_ac))); qed_spec_mp "integ_of_add"; val bin_mult_simps = [zmult_zminus, integ_of_minus, integ_of_add]; @@ -147,8 +143,7 @@ by (simp_tac (simpset() addsimps bin_mult_simps) 1); by (simp_tac (simpset() addsimps bin_mult_simps) 1); by (asm_simp_tac - (simpset() addsimps (bin_mult_simps @ [zadd_zmult_distrib] @ - zadd_ac)) 1); + (simpset() addsimps bin_mult_simps @ [zadd_zmult_distrib] @ zadd_ac) 1); qed "integ_of_mult"; @@ -218,13 +213,13 @@ qed "add1_zle_eq"; Addsimps [add1_zle_eq]; -Goal "znegative x = (x < #0)"; -by (simp_tac (simpset() addsimps [znegative_eq_less_nat0]) 1); -qed "znegative_eq_less_0"; +Goal "neg x = (x < #0)"; +by (simp_tac (simpset() addsimps [neg_eq_less_nat0]) 1); +qed "neg_eq_less_0"; -Goal "(~znegative x) = ($# 0 <= x)"; -by (simp_tac (simpset() addsimps [not_znegative_eq_ge_nat0]) 1); -qed "not_znegative_eq_ge_0"; +Goal "(~neg x) = ($# 0 <= x)"; +by (simp_tac (simpset() addsimps [not_neg_eq_ge_nat0]) 1); +qed "not_neg_eq_ge_0"; @@ -252,9 +247,9 @@ by (Simp_tac 1); by (int_case_tac "integ_of w" 1); by (ALLGOALS (asm_simp_tac - (simpset() addsimps (zcompare_rls @ - [zminus_zadd_distrib RS sym, - add_znat])))); + (simpset() addsimps zcompare_rls @ + [zminus_zadd_distrib RS sym, + add_nat]))); qed "iszero_integ_of_BIT"; @@ -262,25 +257,24 @@ Goalw [zless_def,zdiff_def] "integ_of x < integ_of y \ -\ = znegative (integ_of (bin_add x (bin_minus y)))"; +\ = neg (integ_of (bin_add x (bin_minus y)))"; by (simp_tac (simpset() addsimps bin_mult_simps) 1); -qed "less_integ_of_eq_zneg"; +qed "less_integ_of_eq_neg"; -Goal "~ znegative (integ_of Pls)"; +Goal "~ neg (integ_of Pls)"; by (Simp_tac 1); qed "not_neg_integ_of_Pls"; -Goal "znegative (integ_of Min)"; +Goal "neg (integ_of Min)"; by (Simp_tac 1); qed "neg_integ_of_Min"; -Goal "znegative (integ_of (w BIT x)) = znegative (integ_of w)"; +Goal "neg (integ_of (w BIT x)) = neg (integ_of w)"; by (Asm_simp_tac 1); by (int_case_tac "integ_of w" 1); by (ALLGOALS (asm_simp_tac - (simpset() addsimps ([add_znat, znegative_eq_less_nat0, - symmetric zdiff_def] @ - zcompare_rls)))); + (simpset() addsimps [add_nat, neg_eq_less_nat0, + symmetric zdiff_def] @ zcompare_rls))); qed "neg_integ_of_BIT"; @@ -290,11 +284,12 @@ by (simp_tac (simpset() addsimps [zle_def]) 1); qed "le_integ_of_eq_not_less"; +(*Delete the original rewrites, with their clumsy conditional expressions*) +Delsimps [succ_BIT, pred_BIT, minus_BIT, + NCons_Pls, NCons_Min, add_BIT, mult_BIT]; (*Hide the binary representation of integer constants*) -Delsimps [succ_BIT, pred_BIT, minus_BIT, add_BIT, mult_BIT, - integ_of_Pls, integ_of_Min, integ_of_BIT, - norm_Pls, norm_Min, NCons]; +Delsimps [integ_of_Pls, integ_of_Min, integ_of_BIT]; (*Add simplification of arithmetic operations on integer constants*) Addsimps [integ_of_add RS sym, @@ -313,7 +308,7 @@ (*... and simplification of relational operations*) Addsimps [eq_integ_of_eq, iszero_integ_of_Pls, nonzero_integ_of_Min, iszero_integ_of_BIT, - less_integ_of_eq_zneg, + less_integ_of_eq_neg, not_neg_integ_of_Pls, neg_integ_of_Min, neg_integ_of_BIT, le_integ_of_eq_not_less]; @@ -329,7 +324,7 @@ (** Simplification of inequalities involving numerical constants **) Goal "(w <= z + #1) = (w<=z | w = z + #1)"; -by (simp_tac (simpset() addsimps [zle_eq_zless_or_eq, zless_add1_eq]) 1); +by (simp_tac (simpset() addsimps [integ_le_less, zless_add1_eq]) 1); qed "zle_add1_eq"; Goal "(w <= z - #1) = (w w < z"; -bd zless_zadd_imp_zless 1; -ba 2; +by (dtac zless_zadd_imp_zless 1); +by (assume_tac 2); by (Simp_tac 1); qed "zless_zadd1_imp_zless"; diff -r 25e743eef48a -r 0f16c3b66ab4 src/HOL/Integ/Bin.thy --- a/src/HOL/Integ/Bin.thy Wed Sep 23 10:17:11 1998 +0200 +++ b/src/HOL/Integ/Bin.thy Wed Sep 23 10:25:37 1998 +0200 @@ -43,9 +43,9 @@ (*NCons inserts a bit, suppressing leading 0s and 1s*) primrec - norm_Pls "NCons Pls b = (if b then (Pls BIT b) else Pls)" - norm_Min "NCons Min b = (if b then Min else (Min BIT b))" - NCons "NCons (w' BIT x') b = (w' BIT x') BIT b" + NCons_Pls "NCons Pls b = (if b then (Pls BIT b) else Pls)" + NCons_Min "NCons Min b = (if b then Min else (Min BIT b))" + NCons_BIT "NCons (w BIT x) b = (w BIT x) BIT b" primrec integ_of_Pls "integ_of Pls = $# 0" @@ -89,7 +89,7 @@ primrec mult_Pls "bin_mult Pls w = Pls" mult_Min "bin_mult Min w = bin_minus w" - mult_BIT "bin_mult (v BIT x) w = + mult_BIT "bin_mult (v BIT x) w = (if x then (bin_add (NCons (bin_mult v w) False) w) else (NCons (bin_mult v w) False))" @@ -141,9 +141,13 @@ fun dest_bin tm = let - fun bin_of (Const ("Pls", _)) = [] - | bin_of (Const ("Min", _)) = [~1] - | bin_of (Const ("op BIT", _) $ bs $ b) = dest_bit b :: bin_of bs + (*We consider both "spellings", since Min might be declared elsewhere*) + fun bin_of (Const ("Pls", _)) = [] + | bin_of (Const ("bin.Pls", _)) = [] + | bin_of (Const ("Min", _)) = [~1] + | bin_of (Const ("bin.Min", _)) = [~1] + | bin_of (Const ("op BIT", _) $ bs $ b) = dest_bit b :: bin_of bs + | bin_of (Const ("bin.op BIT", _) $ bs $ b) = dest_bit b :: bin_of bs | bin_of _ = raise Match; fun int_of [] = 0 diff -r 25e743eef48a -r 0f16c3b66ab4 src/HOL/Integ/IntDef.ML --- a/src/HOL/Integ/IntDef.ML Wed Sep 23 10:17:11 1998 +0200 +++ b/src/HOL/Integ/IntDef.ML Wed Sep 23 10:25:37 1998 +0200 @@ -81,11 +81,11 @@ qed "inj_Rep_Integ"; -(** znat: the injection from nat to Integ **) +(** nat: the injection from nat to Integ **) -Goal "inj(znat)"; +Goal "inj(nat)"; by (rtac injI 1); -by (rewtac znat_def); +by (rewtac nat_def); by (dtac (inj_on_Abs_Integ RS inj_onD) 1); by (REPEAT (rtac intrel_in_integ 1)); by (dtac eq_equiv_class 1); @@ -93,7 +93,7 @@ by (Fast_tac 1); by Safe_tac; by (Asm_full_simp_tac 1); -qed "inj_znat"; +qed "inj_nat"; (**** zminus: unary negation on Integ ****) @@ -137,26 +137,26 @@ by (Asm_full_simp_tac 1); qed "inj_zminus"; -Goalw [znat_def] "- ($# 0) = $# 0"; +Goalw [nat_def] "- ($# 0) = $# 0"; by (simp_tac (simpset() addsimps [zminus]) 1); qed "zminus_nat0"; Addsimps [zminus_nat0]; -(**** znegative: the test for negative integers ****) +(**** neg: the test for negative integers ****) -Goalw [znegative_def, znat_def] "~ znegative($# n)"; +Goalw [neg_def, nat_def] "~ neg($# n)"; by (Simp_tac 1); by Safe_tac; -qed "not_znegative_znat"; +qed "not_neg_nat"; -Goalw [znegative_def, znat_def] "znegative(- $# Suc(n))"; +Goalw [neg_def, nat_def] "neg(- $# Suc(n))"; by (simp_tac (simpset() addsimps [zminus]) 1); -qed "znegative_zminus_znat"; +qed "neg_zminus_nat"; -Addsimps [znegative_zminus_znat, not_znegative_znat]; +Addsimps [neg_zminus_nat, not_neg_nat]; (**** zadd: addition on Integ ****) @@ -194,7 +194,7 @@ Goal "(z::int) + w = w + z"; by (res_inst_tac [("z","z")] eq_Abs_Integ 1); by (res_inst_tac [("z","w")] eq_Abs_Integ 1); -by (asm_simp_tac (simpset() addsimps (add_ac @ [zadd])) 1); +by (asm_simp_tac (simpset() addsimps add_ac @ [zadd]) 1); qed "zadd_commute"; Goal "((z1::int) + z2) + z3 = z1 + (z2 + z3)"; @@ -214,15 +214,15 @@ (*Integer addition is an AC operator*) val zadd_ac = [zadd_assoc,zadd_commute,zadd_left_commute]; -Goalw [znat_def] "($#m) + ($#n) = $# (m + n)"; +Goalw [nat_def] "($#m) + ($#n) = $# (m + n)"; by (simp_tac (simpset() addsimps [zadd]) 1); -qed "add_znat"; +qed "add_nat"; Goal "$# (Suc m) = $# 1 + ($# m)"; -by (simp_tac (simpset() addsimps [add_znat]) 1); -qed "znat_Suc"; +by (simp_tac (simpset() addsimps [add_nat]) 1); +qed "nat_Suc"; -Goalw [znat_def] "$# 0 + z = z"; +Goalw [nat_def] "$# 0 + z = z"; by (res_inst_tac [("z","z")] eq_Abs_Integ 1); by (asm_simp_tac (simpset() addsimps [zadd]) 1); qed "zadd_nat0"; @@ -232,7 +232,7 @@ by (rtac zadd_nat0 1); qed "zadd_nat0_right"; -Goalw [znat_def] "z + (- z) = $# 0"; +Goalw [nat_def] "z + (- z) = $# 0"; by (res_inst_tac [("z","z")] eq_Abs_Integ 1); by (asm_simp_tac (simpset() addsimps [zminus, zadd, add_commute]) 1); qed "zadd_zminus_inverse_nat"; @@ -309,28 +309,28 @@ Goal "(- z) * w = - (z * (w::int))"; by (res_inst_tac [("z","z")] eq_Abs_Integ 1); by (res_inst_tac [("z","w")] eq_Abs_Integ 1); -by (asm_simp_tac (simpset() addsimps ([zminus, zmult] @ add_ac)) 1); +by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 1); qed "zmult_zminus"; Goal "(- z) * (- w) = (z * (w::int))"; by (res_inst_tac [("z","z")] eq_Abs_Integ 1); by (res_inst_tac [("z","w")] eq_Abs_Integ 1); -by (asm_simp_tac (simpset() addsimps ([zminus, zmult] @ add_ac)) 1); +by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 1); qed "zmult_zminus_zminus"; Goal "(z::int) * w = w * z"; by (res_inst_tac [("z","z")] eq_Abs_Integ 1); by (res_inst_tac [("z","w")] eq_Abs_Integ 1); -by (asm_simp_tac (simpset() addsimps ([zmult] @ add_ac @ mult_ac)) 1); +by (asm_simp_tac (simpset() addsimps [zmult] @ add_ac @ mult_ac) 1); qed "zmult_commute"; Goal "((z1::int) * z2) * z3 = z1 * (z2 * z3)"; by (res_inst_tac [("z","z1")] eq_Abs_Integ 1); by (res_inst_tac [("z","z2")] eq_Abs_Integ 1); by (res_inst_tac [("z","z3")] eq_Abs_Integ 1); -by (asm_simp_tac (simpset() addsimps ([add_mult_distrib2,zmult] @ - add_ac @ mult_ac)) 1); +by (asm_simp_tac (simpset() addsimps [add_mult_distrib2,zmult] @ + add_ac @ mult_ac) 1); qed "zmult_assoc"; (*For AC rewriting*) @@ -348,8 +348,8 @@ by (res_inst_tac [("z","z2")] eq_Abs_Integ 1); by (res_inst_tac [("z","w")] eq_Abs_Integ 1); by (asm_simp_tac - (simpset() addsimps ([add_mult_distrib2, zadd, zmult] @ - add_ac @ mult_ac)) 1); + (simpset() addsimps [add_mult_distrib2, zadd, zmult] @ + add_ac @ mult_ac) 1); qed "zadd_zmult_distrib"; val zmult_commute'= read_instantiate [("z","w")] zmult_commute; @@ -362,12 +362,12 @@ by (simp_tac (simpset() addsimps [zmult_commute',zadd_zmult_distrib]) 1); qed "zadd_zmult_distrib2"; -Goalw [znat_def] "$# 0 * z = $# 0"; +Goalw [nat_def] "$# 0 * z = $# 0"; by (res_inst_tac [("z","z")] eq_Abs_Integ 1); by (asm_simp_tac (simpset() addsimps [zmult]) 1); qed "zmult_nat0"; -Goalw [znat_def] "$# 1 * z = z"; +Goalw [nat_def] "$# 1 * z = z"; by (res_inst_tac [("z","z")] eq_Abs_Integ 1); by (asm_simp_tac (simpset() addsimps [zmult]) 1); qed "zmult_nat1"; @@ -393,7 +393,7 @@ (* Theorems about less and less_equal *) (*This lemma allows direct proofs of other <-properties*) -Goalw [zless_def, znegative_def, zdiff_def, znat_def] +Goalw [zless_def, neg_def, zdiff_def, nat_def] "(w < z) = (EX n. z = w + $#(Suc n))"; by (res_inst_tac [("z","z")] eq_Abs_Integ 1); by (res_inst_tac [("z","w")] eq_Abs_Integ 1); @@ -407,24 +407,24 @@ Goal "z < z + $# (Suc n)"; by (auto_tac (claset(), simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc, - add_znat])); + add_nat])); qed "zless_zadd_Suc"; Goal "[| z1 z1 < (z3::int)"; by (auto_tac (claset(), simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc, - add_znat])); + add_nat])); qed "zless_trans"; Goal "!!w::int. z ~w m P *) -bind_thm ("zless_asym", (zless_not_sym RS swap)); +bind_thm ("zless_asym", zless_not_sym RS swap); Goal "!!z::int. ~ z z <= (w::int)"; @@ -527,7 +527,7 @@ (* Axiom 'linorder_linear' of class 'linorder': *) Goal "(z::int) <= w | w <= z"; -by (simp_tac (simpset() addsimps [zle_eq_zless_or_eq]) 1); +by (simp_tac (simpset() addsimps [integ_le_less]) 1); by (cut_facts_tac [zless_linear] 1); by (Blast_tac 1); qed "zle_linear"; @@ -567,19 +567,19 @@ (*** Subtraction laws ***) Goal "x + (y - z) = (x + y) - (z::int)"; -by (simp_tac (simpset() addsimps (zdiff_def::zadd_ac)) 1); +by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1); qed "zadd_zdiff_eq"; Goal "(x - y) + z = (x + z) - (y::int)"; -by (simp_tac (simpset() addsimps (zdiff_def::zadd_ac)) 1); +by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1); qed "zdiff_zadd_eq"; Goal "(x - y) - z = x - (y + (z::int))"; -by (simp_tac (simpset() addsimps (zdiff_def::zadd_ac)) 1); +by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1); qed "zdiff_zdiff_eq"; Goal "x - (y - z) = (x + z) - (y::int)"; -by (simp_tac (simpset() addsimps (zdiff_def::zadd_ac)) 1); +by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1); qed "zdiff_zdiff_eq2"; Goalw [zless_def, zdiff_def] "(x-y < z) = (x < z + (y::int))"; @@ -636,10 +636,10 @@ Goal "(w < z + $# 1) = (w int ("$# _" [80] 80) + nat :: nat => int ("$# _" [80] 80) "$# m == Abs_Integ(intrel ^^ {(m,0)})" - znegative :: int => bool - "znegative(Z) == EX x y. x bool + "neg(Z) == EX x y. x bool @@ -41,7 +41,7 @@ zdiff_def "Z1 - Z2 == Z1 + -(Z2::int)" - zless_def "Z1 $# (zmagnitude z) = z"; -by (dtac (not_znegative_eq_ge_nat0 RS iffD1) 1); +Goal "~ neg z ==> $# (nat_of z) = z"; +by (dtac (not_neg_eq_ge_nat0 RS iffD1) 1); by (dtac zle_imp_zless_or_eq 1); by (auto_tac (claset(), simpset() addsimps [zless_iff_Suc_zadd])); -qed "not_zneg_mag"; +qed "not_neg_nat_of"; -Goal "znegative x ==> ? n. x = - $# Suc n"; +Goal "neg x ==> ? n. x = - $# Suc n"; by (auto_tac (claset(), - simpset() addsimps [znegative_eq_less_nat0, zless_iff_Suc_zadd, + simpset() addsimps [neg_eq_less_nat0, zless_iff_Suc_zadd, zdiff_eq_eq RS sym, zdiff_def])); -qed "znegativeD"; +qed "negD"; -Goal "znegative z ==> $# (zmagnitude z) = -z"; -bd znegativeD 1; +Goal "neg z ==> $# (nat_of z) = -z"; +by (dtac negD 1); by Auto_tac; -qed "zneg_mag"; +qed "neg_nat_of"; (* a case theorem distinguishing positive and negative int *) val prems = Goal "[|!! n. P ($# n); !! n. P (- $# Suc n) |] ==> P z"; -by (case_tac "znegative z" 1); -by (blast_tac (claset() addSDs [znegativeD] addSIs prems) 1); -be (not_zneg_mag RS subst) 1; -brs prems 1; +by (case_tac "neg z" 1); +by (blast_tac (claset() addSDs [negD] addSIs prems) 1); +by (etac (not_neg_nat_of RS subst) 1); +by (resolve_tac prems 1); qed "int_cases"; fun int_case_tac x = res_inst_tac [("z",x)] int_cases; diff -r 25e743eef48a -r 0f16c3b66ab4 src/HOL/Integ/Integ.thy --- a/src/HOL/Integ/Integ.thy Wed Sep 23 10:17:11 1998 +0200 +++ b/src/HOL/Integ/Integ.thy Wed Sep 23 10:25:37 1998 +0200 @@ -12,7 +12,7 @@ instance int :: linorder (zle_linear) constdefs - zmagnitude :: int => nat - "zmagnitude(Z) == @m. Z = $# m | -Z = $# m" + nat_of :: int => nat + "nat_of(Z) == @m. Z = $# m | -Z = $# m" end