From 716564e6b9d7ffb50aad800a87b48623c4008866 Mon Sep 17 00:00:00 2001 From: "Chun Tian (binghe)" Date: Tue, 21 May 2024 18:47:26 +1000 Subject: [PATCH] [ringLib] RING_TAC|RULE ported from HOL-Light --- examples/algebra/ring/Holmakefile | 20 +- examples/algebra/ring/ringLib.sig | 15 + examples/algebra/ring/ringLib.sml | 483 +++++++++++++++++ examples/algebra/ring/ringLibScript.sml | 669 ++++++++++++++++++------ examples/algebra/ring/ringSyntax.sig | 35 ++ examples/algebra/ring/ringSyntax.sml | 188 +++++++ examples/algebra/ring/selftest.sml | 81 +++ src/integer/intReduce.sig | 2 + src/integer/intReduce.sml | 17 +- src/integer/selftest.sml | 6 +- src/lite/liteLib.sig | 6 +- src/lite/liteLib.sml | 8 +- src/meson/src/Canon_Port.sml | 2 - 13 files changed, 1360 insertions(+), 172 deletions(-) create mode 100644 examples/algebra/ring/ringLib.sig create mode 100644 examples/algebra/ring/ringLib.sml create mode 100644 examples/algebra/ring/ringSyntax.sig create mode 100644 examples/algebra/ring/ringSyntax.sml create mode 100644 examples/algebra/ring/selftest.sml diff --git a/examples/algebra/ring/Holmakefile b/examples/algebra/ring/Holmakefile index 569d887cd3..d36c612e9d 100644 --- a/examples/algebra/ring/Holmakefile +++ b/examples/algebra/ring/Holmakefile @@ -1,21 +1,31 @@ INCLUDES = $(HOLDIR)/src/pred_set/src/more_theories $(HOLDIR)/src/integer \ $(HOLDIR)/src/algebra/construction -ifdef POLY +all: $(DEFAULT_TARGETS) selftest.exe +.PHONY: all + HOLHEAP = heap +EXTRA_CLEANS = $(HOLHEAP) selftest.exe ring-selftest.log + +selftest.exe: selftest.uo ringLib.uo + $(HOLMOSMLC) -o $@ $< + +ifdef POLY OBJS = pred_set/src/more_theories/cardinalTheory integer/intLib \ algebra/construction/ringTheory FULL_OBJPATHS = $(patsubst %,$(HOLDIR)/src/%.uo,$(OBJS)) -EXTRA_CLEANS = $(HOLHEAP) - all: $(HOLHEAP) $(HOLHEAP): $(FULL_OBJPATHS) $(HOLDIR)/bin/hol.state $(protect $(HOLDIR)/bin/buildheap) $(DEBUG_FLAG) -o $@ $(FULL_OBJPATHS) endif -all: $(DEFAULT_TARGETS) +ifdef HOLSELFTESTLEVEL +all: ring-selftest.log -.PHONY: all +ring-selftest.log: selftest.exe + $(tee ./selftest.exe 2>&1, $@) + +endif diff --git a/examples/algebra/ring/ringLib.sig b/examples/algebra/ring/ringLib.sig new file mode 100644 index 0000000000..6f8a97b010 --- /dev/null +++ b/examples/algebra/ring/ringLib.sig @@ -0,0 +1,15 @@ +(* ========================================================================= *) +(* A decision procedure for the universal theory of rings *) +(* *) +(* John Harrison, University of Cambridge Computer Laboratory *) +(* (c) Copyright, University of Cambridge 1998 *) +(* ========================================================================= *) + +signature ringLib = +sig + + include Abbrev + + val RING_RULE : term -> thm + val RING_TAC : tactic +end diff --git a/examples/algebra/ring/ringLib.sml b/examples/algebra/ring/ringLib.sml new file mode 100644 index 0000000000..d46ce25685 --- /dev/null +++ b/examples/algebra/ring/ringLib.sml @@ -0,0 +1,483 @@ +(* ========================================================================= *) +(* A decision procedure for the universal theory of rings *) +(* *) +(* John Harrison, University of Cambridge Computer Laboratory *) +(* (c) Copyright, University of Cambridge 1998 *) +(* *) +(* ------------------------------------------------------------------------- *) +(* Ported by Chun Tian. The Australian National University (ANU), May 2024 *) +(* ========================================================================= *) + +structure ringLib :> ringLib = +struct + +open HolKernel boolLib bossLib; + +open pred_setTheory cardinalTheory ringTheory ringLibTheory Grobner Normalizer + integerTheory intReduce intLib tautLib normalForms Canon Canon_Port + pairSyntax intSyntax ringSyntax pred_setSyntax Ho_Rewrite liteLib; + +(* ------------------------------------------------------------------------- *) +(* Establish the required grammar(s) for executing this file *) +(* ------------------------------------------------------------------------- *) + +structure Parse = struct + open Parse + val (Type,Term) = parse_from_grammars ringLib_grammars +end + +open Parse; + +val ERR = mk_HOL_ERR "ringLib"; +fun failwith s = raise ERR "?" s + +(* |- !P Q. P /\ (?x. Q x) <=> ?x. P /\ Q x *) +val RIGHT_AND_EXISTS_THM = GSYM RIGHT_EXISTS_AND_THM + +(* |- !P Q. (?x. P x) /\ Q <=> ?x. P x /\ Q *) +val LEFT_AND_EXISTS_THM = GSYM LEFT_EXISTS_AND_THM + +(* |- p ==> q ==> r <=> p /\ q ==> r *) +val IMP_IMP = Q.SPECL [‘p’, ‘q’, ‘r’] AND_IMP_INTRO; + +val PRENEX_CONV = Canon.PRENEX_CONV; +val CNF_CONV = Canon.CNF_CONV; + +val ring_tyname = "Ring"; (* There are also other occurrences of it. *) + +(* ------------------------------------------------------------------------- *) +(* Instantiate the normalizer and ring procedure for the case of a ring *) +(* "r:A ring" with the whole type A as the carrier. Since all the machinery *) +(* of the normalizer is designed for such "universal" rings, this is the *) +(* best we can do, but below we use this to define a general procedure. *) +(* The RING instantiation is called RING_INTEGRAL_DOMAIN_UNIVERSAL since *) +(* it in general assumes "integral_domain r" and may also assume that *) +(* "ring_char r = 0". Later we use the other cofactors function to give *) +(* a better decision procedure for general rings, but the integral *) +(* domain one may be independently useful for proofs involving cancellation *) +(* in such domains. *) +(* ------------------------------------------------------------------------- *) + +(* 1. RING_POLY_UNIVERSAL_CONV *) +local + val pth = (UNDISCH o SPEC_ALL o prove) + (“!r. ring_carrier r = univ(:'a) + ==> (!x y z. ring_add r x (ring_add r y z) = + ring_add r (ring_add r x y) z) /\ + (!x y. ring_add r x y = ring_add r y x) /\ + (!x. ring_add r (ring_of_int r (&0)) x = x) /\ + (!x y z. ring_mul r x (ring_mul r y z) = + ring_mul r (ring_mul r x y) z) /\ + (!x y. ring_mul r x y = ring_mul r y x) /\ + (!x. ring_mul r (ring_of_int r (&1)) x = x) /\ + (!x. ring_mul r (ring_of_int r (&0)) x = ring_of_int r (&0)) /\ + (!x y z. ring_mul r x (ring_add r y z) = + ring_add r (ring_mul r x y) (ring_mul r x z)) /\ + (!x. ring_pow r x 0 = ring_of_int r (&1)) /\ + (!x n. ring_pow r x (SUC n) = ring_mul r x (ring_pow r x n))”, + REWRITE_TAC[RING_OF_INT_OF_NUM, RING_OF_NUM_1, CONJUNCT1 ring_of_num] THEN + SIMP_TAC std_ss[RING_ADD_LZERO, RING_MUL_LID, RING_MUL_LZERO, IN_UNIV] THEN + SIMP_TAC std_ss[ring_pow, RING_ADD_LDISTRIB, IN_UNIV] THEN + SIMP_TAC std_ss[RING_ADD_AC, RING_MUL_AC, IN_UNIV]); + val sth = (UNDISCH o SPEC_ALL o prove) + (“!r. ring_carrier r = univ(:'a) + ==> (!x. ring_neg r x = ring_mul r (ring_of_int r (- &1)) x) /\ + (!x y. ring_sub r x y = + ring_add r x (ring_mul r (ring_of_int r (- &1)) y))”, + SIMP_TAC std_ss[RING_OF_INT_NEG, RING_MUL_LNEG, IN_UNIV, ring_sub] THEN + REWRITE_TAC[RING_OF_INT_OF_NUM, RING_OF_NUM_1, CONJUNCT1 ring_of_num] THEN + SIMP_TAC std_ss[ring_sub, RING_MUL_LNEG, RING_MUL_LID, IN_UNIV]); + val RING_INT_ADD_CONV = + GEN_REWRITE_CONV I [GSYM RING_OF_INT_ADD] THENC + RAND_CONV INT_ADD_CONV; + val RING_INT_MUL_CONV = + GEN_REWRITE_CONV I [GSYM RING_OF_INT_MUL] THENC + RAND_CONV INT_MUL_CONV; + val RING_INT_POW_CONV = + GEN_REWRITE_CONV I [GSYM RING_OF_INT_POW] THENC + RAND_CONV INT_POW_CONV; + val ith = prove + (“ring_0 r = ring_of_int r (&0) /\ + ring_1 r = ring_of_int r (&1)”, + REWRITE_TAC[RING_OF_INT_OF_NUM, RING_OF_NUM_1, CONJUNCT1 ring_of_num]); + fun term_lt u t = (Term.compare(u,t) = LESS); + val (_,_,_,_,_,RING_POLY_CONV) = + SEMIRING_NORMALIZERS_CONV pth sth + (is_ringconst, + RING_INT_ADD_CONV,RING_INT_MUL_CONV,RING_INT_POW_CONV) + term_lt +in +val RING_POLY_UNIVERSAL_CONV = + GEN_REWRITE_CONV ONCE_DEPTH_CONV [ith, GSYM RING_OF_INT_OF_NUM] + THENC RING_POLY_CONV +end; + +(* 2. RING_INTEGRAL_DOMAIN_UNIVERSAL and ring_ring_cofactors_universal *) +local + val RING_INTEGRAL = repeat UNDISCH RING_INTEGRAL_LEMMA; + val neth_b = prove + (“ring_of_int r n :'a = ring_of_int r n <=> T”, + REWRITE_TAC[]); + val neth_l = (UNDISCH o prove) + (“integral_domain (r :'a Ring) + ==> ((ring_of_int r (&1) = ring_of_int r (&0)) <=> F)”, + REWRITE_TAC[RING_OF_INT_OF_NUM, RING_OF_NUM_0, RING_OF_NUM_1] THEN + SIMP_TAC std_ss[integral_domain]); + val neth_r = (UNDISCH o prove) + (“integral_domain (r :'a Ring) + ==> (ring_of_int r (&0) = ring_of_int r (&1) <=> F)”, + REWRITE_TAC[RING_OF_INT_OF_NUM, RING_OF_NUM_0, RING_OF_NUM_1] THEN + SIMP_TAC std_ss[integral_domain]); + val neth_g = prove + (“(ring_of_int r m :'a = ring_of_int r n <=> F) <=> + ~(&(ring_char r) int_divides (m - n))”, + REWRITE_TAC[RING_OF_INT_EQ]); + val neth_h = prove + (“(&(ring_char(r :'a Ring)) int_divides -(&n) <=> ring_char r divides n) /\ + (&(ring_char(r :'a Ring)) int_divides &n <=> ring_char r divides n)”, + REWRITE_TAC[num_divides, INT_DIVIDES_NEG]); + val rule1 = PART_MATCH (lhand o lhand) neth_g; + val conv1 = + RAND_CONV INT_SUB_CONV THENC + GEN_REWRITE_CONV TRY_CONV [neth_h]; + fun RING_EQ_CONV tm = + PART_MATCH lhand neth_b tm + handle HOL_ERR _ => + PART_MATCH lhand neth_l tm + handle HOL_ERR _ => + PART_MATCH lhand neth_r tm + handle HOL_ERR _ => + let val th1 = rule1 tm; + val th2 = CONV_RULE(RAND_CONV(RAND_CONV conv1)) th1 + in + UNDISCH(snd(EQ_IMP_RULE th2)) + end + handle HOL_ERR _ => failwith "RING_EQ_CONV"; + val dest_intconst = Arbrat.fromAInt o int_of_term; + val mk_intconst = term_of_int o Arbrat.toAInt; + fun dest_ringconst tm = + if is_ring_of_int tm then + dest_intconst (snd (dest_ring_of_int tm)) + else + failwith "dest_ringconst"; + val mk_ringconst = + let val ptm = “ring_of_int (r :'a Ring)” in + fn n => mk_comb(ptm,mk_intconst n) + end; + val cth = prove + (“ring_0 r :'a = ring_of_int r (&0) /\ + ring_1 r :'a = ring_of_int r (&1)”, + REWRITE_TAC[RING_OF_INT_OF_NUM, RING_OF_NUM_0, RING_OF_NUM_1]); + val decorule = + GEN_REWRITE_CONV ONCE_DEPTH_CONV [cth, GSYM RING_OF_INT_OF_NUM]; + val (basic_rule,idealconv) = + RING_AND_IDEAL_CONV + (dest_ringconst, + mk_ringconst, + RING_EQ_CONV, + “ring_neg(r :'a Ring)”, + “ring_add(r :'a Ring)”, + “ring_sub(r :'a Ring)”, + “ring_inv(r :'a Ring)”, + “ring_mul(r :'a Ring)”, + “ring_div(r :'a Ring)”, + “ring_pow(r :'a Ring)”, + RING_INTEGRAL,TRUTH,RING_POLY_UNIVERSAL_CONV); + fun rule tm = + let val th = decorule tm in + EQ_MP (SYM th) (basic_rule(rand(concl th))) + end +in +val (RING_INTEGRAL_DOMAIN_UNIVERSAL,ring_ring_cofactors_universal) = + (rule,idealconv) +end; + +(* ------------------------------------------------------------------------- *) +(* Derived rule to take a theorem asserting a monomorphism between r and r' *) +(* and a term that is some Boolean combination of equations in the ring r *) +(* and prove it equivalent to a "transferred" version in r' where all the *) +(* variables x (in r) in the original map to "f x" (in r'). *) +(* ------------------------------------------------------------------------- *) + +(* 3. RING_MONOMORPHIC_IMAGE_RULE *) +fun RING_MONOMORPHIC_IMAGE_RULE hth = let + val pth = RING_MONOMORPHIC_IMAGE_RULE_THM; + val ([pth_eq, pth_asm, + pth_0, pth_1, + pth_num, pth_int, + pth_neg, pth_pow, + pth_add, pth_sub], pth_mul) = splitlist CONJ_PAIR (MATCH_MP pth hth) + and htm = rand(concl hth); + fun mterm tm = + if is_ring_0 tm then + pth_0 + else if is_ring_1 tm then + pth_1 + else if is_ring_of_num tm then + SPEC (snd (dest_ring_of_num tm)) pth_num + else if is_ring_of_int tm then + SPEC (snd (dest_ring_of_int tm)) pth_int + else if is_ring_neg tm then + MATCH_MP pth_neg (mterm (snd (dest_ring_neg tm))) + else if is_ring_pow tm then + let val (_,s,n) = dest_ring_pow tm in + MATCH_MP (SPEC n pth_pow) (mterm s) + end + else if is_ring_add tm then + let val (_,s,t) = dest_ring_add tm in + MATCH_MP pth_add (CONJ (mterm s) (mterm t)) + end + else if is_ring_sub tm then + let val (_,s,t) = dest_ring_sub tm in + MATCH_MP pth_sub (CONJ (mterm s) (mterm t)) + end + else if is_ring_mul tm then + let val (_,s,t) = dest_ring_mul tm in + MATCH_MP pth_mul (CONJ (mterm s) (mterm t)) + end + else + UNDISCH(SPEC tm pth_asm); + fun mform tm = + if is_neg tm then + RAND_CONV mform tm + else if is_iff tm orelse is_imp tm orelse is_conj tm orelse is_disj tm then + BINOP_CONV mform tm + else if is_eq tm then + let val (s,t) = dest_eq tm in + MATCH_MP pth_eq (CONJ (mterm s) (mterm t)) + end + else + failwith "RING_MONOMORPHIC_IMAGE_RULE: unhandled formula"; +in + mform +end; + +(* ------------------------------------------------------------------------- *) +(* A decision procedure for the universal theory of rings, mapping *) +(* momomorphically into a "total" ring to leverage earlier stuff. *) +(* It will prove either the exact thing you request, or if you omit some *) +(* carrier membership hypotheses, will add those as an antecedent. *) +(* ------------------------------------------------------------------------- *) + +(* 4. RING_WORD_UNIVERSAL *) +local + val cth = prove + (“ring_0 r = ring_of_int (r :'a Ring) (&0) /\ + ring_1 r = ring_of_int (r :'a Ring) (&1)”, + REWRITE_TAC[RING_OF_INT_OF_NUM, RING_OF_NUM_0, RING_OF_NUM_1]); + val pth = (UNDISCH o prove) + (“ring_carrier r = univ(:'a) ==> + (x = y <=> ring_sub r x y = ring_of_int r (&0))”, + SIMP_TAC bool_ss[RING_SUB_EQ_0, IN_UNIV, RING_OF_INT_OF_NUM, RING_OF_NUM_0]); + val bth = REFL “ring_of_int r (&0) :'a”; + val mth = (UNDISCH o prove) + (“ring_carrier r = univ(:'a) ==> + p = ring_of_int r (&0) ==> !c. ring_mul r c p = ring_of_int r (&0)”, + SIMP_TAC bool_ss[RING_MUL_RZERO, RING_OF_INT_OF_NUM, RING_OF_NUM_0, IN_UNIV]); + val dth = (UNDISCH o prove) + (“ring_carrier r = univ(:'a) ==> + p = ring_of_int r (&0) /\ q = ring_of_int r (&0) ==> + ring_add r p q = ring_of_int r (&0)”, + SIMP_TAC bool_ss[RING_ADD_RZERO, RING_OF_INT_OF_NUM, RING_OF_NUM_0, IN_UNIV]); + val decorule = + GEN_REWRITE_RULE (RAND_CONV o ONCE_DEPTH_CONV) + [cth, GSYM RING_OF_INT_OF_NUM] o + PART_MATCH lhand pth +in +fun RING_WORD_UNIVERSAL tm = let + val (avs,bod) = strip_forall tm + in + if is_imp bod then let + val (ant,con) = dest_imp bod; + val aths = + mapfilter (CONV_RULE decorule) (CONJUNCTS(ASSUME ant)) + and cth = decorule con; + val atms = map (lhand o concl) aths + and ctm = lhand(rand(concl cth)); + val ctms = ring_ring_cofactors_universal atms ctm; + val zths = map2 (fn c => fn th => SPEC c (MATCH_MP mth th)) ctms aths; + val zth = + end_itlist (fn th1 => fn th2 => MATCH_MP dth (CONJ th1 th2)) zths; + val eth = + TRANS (RING_POLY_UNIVERSAL_CONV ctm) + (SYM(RING_POLY_UNIVERSAL_CONV (lhand(concl zth)))) + in + GENL avs (DISCH ant (EQ_MP (SYM cth) (TRANS eth zth))) + end + else + let val th1 = decorule tm; + val th2 = CONV_RULE + (RAND_CONV (LAND_CONV RING_POLY_UNIVERSAL_CONV)) th1 + in + EQ_MP (SYM th2) bth + end + end +end; + +(* 5. RING_RING_WORD *) +local + (* NOTE: These rules require Ho_Rewrite.GEN_REWRITE_RULE *) + val imp_imp_rule = GEN_REWRITE_RULE TRY_CONV [IMP_IMP]; + val left_exists_rule = GEN_REWRITE_RULE TRY_CONV + [LEFT_FORALL_IMP_THM]; + val or_elim_rule = GEN_REWRITE_RULE TRY_CONV + [TAUT `(p ==> q) /\ (p' ==> q) <=> p \/ p' ==> q`]; +in + fun RING_RING_WORD ths tm = let + val dty = type_of(rand tm); + val rty = mk_type(ring_tyname,[dty]); + val rtms = filter (curry (=) rty o type_of) (freesl(tm::map concl ths)) + in + if length rtms <> 1 + then failwith "RING_RULE: can't deduce which ring" else + let val rtm = hd rtms; + val tvs = itlist (union o type_vars_in_term o concl) ths + (type_vars_in_term tm); + val dty' = mk_vartype("Z"^itlist (curry (^) o dest_vartype) tvs ""); + val rty' = mk_type(ring_tyname,[dty']); + val avvers = HOLset.listItems + (itlist (fn th => fn s => + HOLset.addList (s,all_vars (concl th))) ths + (HOLset.addList (empty_tmset, all_vars tm))); + val rtm' = variant avvers (mk_var("r'",rty')) + and htm = variant avvers (mk_var("h",dty --> dty')); + val hasm = list_mk_icomb ring_monomorphism_tm [mk_pair(rtm,rtm'), htm]; + val hth = ASSUME hasm; + val ths' = mapfilter (CONV_RULE(RING_MONOMORPHIC_IMAGE_RULE hth)) ths; + val th' = RING_MONOMORPHIC_IMAGE_RULE hth tm; + val utm = + if null ths' then rand(concl th') + else mk_imp(list_mk_conj (map concl ths'),rand(concl th')); + (* NOTE: HOL-Light's "find_terms" also removes duplication, we can use + liteLib.setify_term in addition to HOL4's find_terms. *) + val hvs = find_terms + (fn t => is_comb t andalso + rator t ~~ htm andalso is_var(rand t)) utm |> setify_term; + val gvs = map (genvar o type_of) hvs; + (* "let vtm = subst (zip gvs hvs) utm in" (hvs |-> gvs) *) + val vtm = subst (map2 (fn s => fn t => s |-> t) hvs gvs) utm; + val aty = Type.alpha; + val arty = mk_type(ring_tyname,[aty]); + val atm = + subst [mk_var(fst(dest_var rtm'),arty) |-> mk_var("r",arty)] + (inst [dty' |-> aty] vtm); + val th1 = RING_WORD_UNIVERSAL atm; + val th2 = INST_TYPE [aty |-> dty'] th1; + val th3 = INST [mk_var("r",rty') |-> rtm'] th2; + (* "let th4 = INST (zip hvs gvs) th3 in" (gvs |-> hvs) *) + val th4 = INST (map2 (fn s => fn t => s |-> t) gvs hvs) th3; + val th5 = if null ths' then th4 + else MP th4 (end_itlist CONJ ths'); + val th6 = itlist PROVE_HYP ths (EQ_MP (SYM th') th5); + val ueq = mk_eq(list_mk_icomb ring_carrier_tm [rtm'], + inst [aty |-> dty'] univ_tm); + val th7 = imp_imp_rule (DISCH ueq (DISCH hasm th6)); + val th8 = left_exists_rule(GEN htm th7); + val th9 = left_exists_rule(GEN rtm' th8); + val th10 = ISPEC rtm RING_TOTALIZATION; + val th11 = CONJ (PART_MATCH lhand th9 (lhand(concl th10))) + (PART_MATCH lhand th9 (rand(concl th10))); + in + MP (or_elim_rule th11) th10 + end + end +end; + +(* 6. RING_RING_HORN *) +local + val ddj_conv = + GEN_REWRITE_CONV (RAND_CONV o DEPTH_CONV) + [TAUT ‘~p \/ ~q <=> ~(p /\ q)’] THENC + GEN_REWRITE_CONV TRY_CONV [TAUT ‘p \/ ~q <=> q ==> p’] +in + fun RING_RING_HORN tm = + if not(is_disj tm) then RING_RING_WORD [] tm else + let val th0 = ddj_conv tm; + val tm' = rand(concl th0); + val abod = lhand tm'; + val ths = CONJUNCTS(ASSUME abod); + val th1 = RING_RING_WORD ths (rand tm') + in + EQ_MP (SYM th0) (DISCH abod (itlist PROVE_HYP ths th1)) + end +end; + +(* 7. RING_RING_CORE *) +local + val pth = TAUT ‘p ==> q <=> (p \/ q <=> q)’ + and ptm = “p:bool” and qtm = “q:bool” +in + fun RING_RING_CORE tm = let + val (negdjs,posdjs) = partition is_neg (strip_disj tm); + val th = tryfind + (fn p => RING_RING_HORN (list_mk_disj(p::negdjs))) posdjs; + val th1 = INST [ptm |-> concl th, qtm |-> tm] pth; + val tm2 = rand(concl th1); + in + MP (EQ_MP (SYM th1) (DISJ_ACI_RULE tm2)) th + end +end; + +(* 8. init_conv *) +val init_conv = + TOP_DEPTH_CONV BETA_CONV THENC + PRESIMP_CONV THENC + CONDS_ELIM_CONV THENC + NNFC_CONV THENC CNF_CONV THENC + SKOLEM_CONV THENC PRENEX_CONV THENC + GEN_REWRITE_CONV REDEPTH_CONV + [RIGHT_AND_EXISTS_THM, LEFT_AND_EXISTS_THM] THENC + GEN_REWRITE_CONV TOP_DEPTH_CONV [GSYM DISJ_ASSOC] THENC + GEN_REWRITE_CONV TOP_DEPTH_CONV [GSYM CONJ_ASSOC]; + +(* 9. RING_RULE_BASIC *) +fun RING_RULE_BASIC tm = let + val (avs,bod) = strip_forall tm; + val th1 = init_conv bod; + val tm' = rand(concl th1); + val (avs',bod') = strip_forall tm'; + val th2 = end_itlist CONJ (map RING_RING_CORE (strip_conj bod')); + val th3 = EQ_MP (SYM th1) (GENL avs' th2); + val imps = hyp th3; + val th4 = + if null imps then th3 + else DISCH_ALL + (itlist PROVE_HYP (CONJUNCTS(ASSUME(list_mk_conj imps))) th3) +in + GENL avs th4 +end; + +(* 10. RING_RULE + + The final version of RULE_RULE only temporarily changes the type variable + alpha of input term to something fresh and then call RING_RULE_BASIC to + do the actual job. + *) +fun RING_RULE tm = let + val tvs = type_vars_in_term tm; + val ty = mk_vartype("Y" ^ itlist (curry (^) o dest_vartype) tvs ""); + val aty = Type.alpha; + val tm' = inst [aty |-> ty] tm; +in + INST_TYPE [ty |-> aty] (RING_RULE_BASIC tm') +end; + +(* ------------------------------------------------------------------------- *) +(* A naive tactic form, pulling in equations in the assumptions and *) +(* either solving outright or leaving some ring carrier membership *) +(* ------------------------------------------------------------------------- *) + +(* 11. RING_TAC *) +val RING_TAC = let + fun check p x = if p x then x else failwith "check in RING_TAC" +in + REPEAT GEN_TAC THEN + REPEAT(FIRST_X_ASSUM(MP_TAC o check (is_eq o concl))) THEN + W(fn (asl,w) => + let val th = RING_RULE w in + (MATCH_ACCEPT_TAC th ORELSE + ((fn g => MATCH_MP_TAC th g) THEN ASM_REWRITE_TAC[])) + end) +end; + +end (* struct *) diff --git a/examples/algebra/ring/ringLibScript.sml b/examples/algebra/ring/ringLibScript.sml index 208f409ddf..4f22a2ed77 100644 --- a/examples/algebra/ring/ringLibScript.sml +++ b/examples/algebra/ring/ringLibScript.sml @@ -12,7 +12,7 @@ open HolKernel boolLib bossLib Parse; open combinTheory pred_setTheory pred_setLib arithmeticTheory integerTheory numLib intLib mesonLib hurdUtils cardinalTheory oneTheory newtypeTools - tautLib liteLib; + tautLib metisLib liteLib Ho_Rewrite; open monoidTheory groupTheory ringTheory; @@ -39,10 +39,12 @@ val _ = hide "trivial_ring"; val _ = hide "ring"; (* |- !P Q. P /\ (?x. Q x) <=> ?x. P /\ Q x *) -val RIGHT_AND_EXISTS_THM = GSYM RIGHT_EXISTS_AND_THM +val RIGHT_AND_EXISTS_THM = GSYM RIGHT_EXISTS_AND_THM; (* |- !P Q. (?x. P x) /\ Q <=> ?x. P x /\ Q *) -val LEFT_AND_EXISTS_THM = GSYM LEFT_EXISTS_AND_THM +val LEFT_AND_EXISTS_THM = GSYM LEFT_EXISTS_AND_THM; + +val IMP_CONJ = DECIDE “p /\ q ==> r <=> p ==> q ==> r”; (* ------------------------------------------------------------------------- *) (* 'a Ring as type bijections of a subset of 'a ring *) @@ -112,7 +114,7 @@ Definition ring_add_def : End val _ = hide "ring_sub"; -Definition ring_sub : +Definition ring_sub_def : ring_sub (r :'a Ring) = ring$ring_sub (fromRing r) End @@ -124,7 +126,21 @@ Definition ring_pow_def : ring_pow (r :'a Ring) = (fromRing r).prod.exp End -(* NOTE: not used, only to make sure ‘ring_inv’ is not treated as variables *) +Theorem ring_pow : + ring_pow r x 0 = ring_1 r /\ + ring_pow r x (SUC n) = ring_mul r x (ring_pow r x n) +Proof + Q.ID_SPEC_TAC ‘r’ + >> Q.X_GEN_TAC ‘r0’ + >> REWRITE_TAC [ring_pow_def, ring_1_def, ring_mul_def] + >> Q.ABBREV_TAC ‘r = fromRing r0’ + >> REWRITE_TAC [ring_exp_0, ring_exp_SUC] +QED + +(* NOTE: not used, only to make sure ‘ring_inv’ is not treated as variables + + |- !r. ring_inv r = Inv (fromRing r) + *) Definition ring_inv_def : ring_inv (r :'a Ring) = (Invertibles ((fromRing r).prod)).inv End @@ -177,14 +193,30 @@ Proof >> rw [Abbr ‘r’] QED +Theorem ring_sub : + !r x y. ring_sub r x y = ring_add r x (ring_neg r y) +Proof + Q.X_GEN_TAC ‘r0’ + >> Q.ABBREV_TAC ‘r = fromRing r0’ + >> rw [ring_sub_def, ring_add_def, ring_neg_def] +QED + fun xfer th :tactic = Q.X_GEN_TAC ‘r0’ >> Q.ABBREV_TAC ‘r = fromRing r0’ - >> RW_TAC std_ss [ring_carrier_def, ring_pow_def, ring_add_def, ring_sub, + >> RW_TAC std_ss [ring_carrier_def, ring_pow_def, ring_add_def, ring_sub_def, ring_mul_def, ring_0_def, ring_1_def, ring_neg_def] >> irule th >> rw [Abbr ‘r’]; +Theorem RING_NEG_EQ_0 : + !r (x :'a). + x IN ring_carrier r + ==> (ring_neg r x = ring_0 r <=> x = ring_0 r) +Proof + xfer ring_neg_eq_zero +QED + Theorem RING_POW : !r x n. x IN ring_carrier r ==> ring_pow r x n IN ring_carrier (r :'a Ring) Proof @@ -269,6 +301,22 @@ Proof xfer ring_mult_rzero QED +Theorem RING_MUL_LNEG : + !r x (y :'a). + x IN ring_carrier r /\ y IN ring_carrier r + ==> ring_mul r (ring_neg r x) y = ring_neg r (ring_mul r x y) +Proof + xfer ring_mult_lneg +QED + +Theorem RING_MUL_RNEG : + !r x (y :'a). + x IN ring_carrier r /\ y IN ring_carrier r + ==> ring_mul r x (ring_neg r y) = ring_neg r (ring_mul r x y) +Proof + xfer ring_mult_rneg +QED + Theorem RING_MUL_SYM : !r x y. x IN ring_carrier r /\ y IN ring_carrier (r :'a Ring) ==> ring_mul r x y = ring_mul r y x @@ -284,6 +332,24 @@ Proof xfer (GSYM ring_mult_assoc) QED +Theorem RING_ADD_LDISTRIB : + !r x y (z :'a). + x IN ring_carrier r /\ y IN ring_carrier r /\ z IN ring_carrier r + ==> ring_mul r x (ring_add r y z) = + ring_add r (ring_mul r x y) (ring_mul r x z) +Proof + xfer ring_mult_radd +QED + +Theorem RING_ADD_RDISTRIB : + !r x y (z :'a). + x IN ring_carrier r /\ y IN ring_carrier r /\ z IN ring_carrier r + ==> ring_mul r (ring_add r x y) z = + ring_add r (ring_mul r x z) (ring_mul r y z) +Proof + xfer ring_mult_ladd +QED + Theorem RING_ADD_EQ_0 : !r x y. x IN ring_carrier r /\ y IN ring_carrier (r :'a Ring) @@ -318,6 +384,15 @@ Proof xfer ring_neg_neg QED +Theorem RING_NEG_ADD : + !r x (y :'a). + x IN ring_carrier r /\ y IN ring_carrier r + ==> ring_neg r (ring_add r x y) = + ring_add r (ring_neg r x) (ring_neg r y) +Proof + xfer ring_neg_add +QED + Theorem RING_ADD_LCANCEL : !r x y (z :'a). x IN ring_carrier r /\ y IN ring_carrier r /\ z IN ring_carrier r @@ -380,6 +455,334 @@ Proof xfer ring_sub_eq_zero QED +Theorem RING_SUB_LZERO : + !r (x :'a). x IN ring_carrier r ==> ring_sub r (ring_0 r) x = ring_neg r x +Proof + xfer ring_zero_sub +QED + +Theorem RING_SUB_RZERO : + !r (x :'a). x IN ring_carrier r ==> ring_sub r x (ring_0 r) = x +Proof + xfer ring_sub_zero +QED + +Theorem RING_EQ_SUB_LADD : + !r x y (z :'a). + x IN ring_carrier r /\ y IN ring_carrier r /\ z IN ring_carrier r + ==> (x = ring_sub r y z <=> ring_add r x z = y) +Proof + Q.X_GEN_TAC ‘r0’ + >> Q.ABBREV_TAC ‘r = fromRing r0’ + >> RW_TAC std_ss [ring_carrier_def, ring_sub_def, ring_add_def] + >> MP_TAC (Q.SPEC ‘r’ ring_sub_eq_add) + >> ANTS_TAC >- rw [Abbr ‘r’] + >> DISCH_THEN (MP_TAC o (Q.SPECL [‘y’, ‘z’, ‘x’])) + >> ‘Ring r’ by rw [Abbr ‘r’] + >> METIS_TAC [ring_add_comm] +QED + +Theorem RING_ADD_AC : + !(r :'a Ring). + (!x y. x IN ring_carrier r /\ y IN ring_carrier r + ==> ring_add r x y = ring_add r y x) /\ + (!x y z. x IN ring_carrier r /\ y IN ring_carrier r /\ + z IN ring_carrier r + ==> ring_add r (ring_add r x y) z = + ring_add r x (ring_add r y z)) /\ + (!x y z. x IN ring_carrier r /\ y IN ring_carrier r /\ + z IN ring_carrier r + ==> ring_add r x (ring_add r y z) = + ring_add r y (ring_add r x z)) +Proof + MESON_TAC[RING_ADD_SYM, RING_ADD_ASSOC, RING_ADD] +QED + +Theorem RING_MUL_AC : + !(r :'a Ring). + (!x y. x IN ring_carrier r /\ y IN ring_carrier r + ==> ring_mul r x y = ring_mul r y x) /\ + (!x y z. x IN ring_carrier r /\ y IN ring_carrier r /\ + z IN ring_carrier r + ==> ring_mul r (ring_mul r x y) z = + ring_mul r x (ring_mul r y z)) /\ + (!x y z. x IN ring_carrier r /\ y IN ring_carrier r /\ + z IN ring_carrier r + ==> ring_mul r x (ring_mul r y z) = + ring_mul r y (ring_mul r x z)) +Proof + MESON_TAC[RING_MUL_SYM, RING_MUL_ASSOC, RING_MUL] +QED + +(* ------------------------------------------------------------------------- *) +(* Mapping natural numbers and integers into a ring in the obvious way. *) +(* ------------------------------------------------------------------------- *) + +(* ##n *) +Definition ring_of_num_def : + ring_of_num (r :'a Ring) = (fromRing r).sum.exp (ring_1 r) +End + +Theorem ring_of_num : + ring_of_num r (0 :num) = ring_0 (r :'a Ring) /\ + ring_of_num r (SUC n) = ring_add r (ring_of_num r n) (ring_1 r) +Proof + Q.ID_SPEC_TAC ‘r’ + >> Q.X_GEN_TAC ‘r0’ + >> Q.ABBREV_TAC ‘r = fromRing r0’ + >> RW_TAC std_ss [ring_num_0, ring_of_num_def, ring_0_def, ring_1_def, + ring_add_def] + >> ‘Ring r’ by rw [Abbr ‘r’] + >> Know ‘##n + #1 = #1 + ##n’ + >- (irule ring_add_comm >> rw []) + >> Rewr' + >> MATCH_MP_TAC ring_num_SUC >> art [] +QED + +Theorem RING_OF_NUM : + !r n. ring_of_num r n IN ring_carrier (r :'a Ring) +Proof + qx_genl_tac [‘r0’, ‘n’] + >> Q.ABBREV_TAC ‘r = fromRing r0’ + >> RW_TAC std_ss [ring_carrier_def, ring_of_num_def, ring_1_def] + >> MATCH_MP_TAC ring_num_element + >> rw [Abbr ‘r’] +QED + +Theorem RING_OF_NUM_0 : + !(r :'a Ring). ring_of_num r 0 = ring_0 r +Proof + REWRITE_TAC[ring_of_num] +QED + +Theorem RING_OF_NUM_1 : + !(r :'a Ring). ring_of_num r 1 = ring_1 r +Proof + SIMP_TAC bool_ss[num_CONV “1:num”, ring_of_num, RING_ADD_LZERO, RING_1] +QED + +Theorem RING_OF_NUM_ADD : + !(r :'a Ring) m n. + ring_of_num r (m + n) = ring_add r (ring_of_num r m) (ring_of_num r n) +Proof + Q.X_GEN_TAC ‘r0’ + >> Q.ABBREV_TAC ‘r = fromRing r0’ + >> rw [ring_of_num_def, ring_1_def, ring_add_def] + >> irule ring_num_add + >> rw [Abbr ‘r’] +QED + +Theorem RING_OF_NUM_MUL : + !(r :'a Ring) m n. + ring_of_num r (m * n) = ring_mul r (ring_of_num r m) (ring_of_num r n) +Proof + Q.X_GEN_TAC ‘r0’ + >> Q.ABBREV_TAC ‘r = fromRing r0’ + >> rw [ring_of_num_def, ring_mul_def, ring_1_def] + >> irule (GSYM ring_num_mult) + >> rw [Abbr ‘r’] +QED + +Definition ring_of_int : + ring_of_int (r :'a Ring) (n :int) = + if &0 <= n then ring_of_num r (num_of_int n) + else ring_neg r (ring_of_num r (num_of_int (-n))) +End + +Theorem RING_OF_INT : + !r n. ring_of_int r n IN ring_carrier (r :'a Ring) +Proof + REPEAT GEN_TAC THEN REWRITE_TAC[ring_of_int] THEN COND_CASES_TAC THEN + ASM_SIMP_TAC std_ss [RING_NEG, RING_OF_NUM] +QED + +(* |- !n. num_of_int(&n) = n *) +Theorem NUM_OF_INT_OF_NUM = NUM_OF_INT; + +Theorem RING_OF_INT_OF_NUM : + !r n. ring_of_int r (&n) = ring_of_num (r :'a Ring) n +Proof + REWRITE_TAC[ring_of_int, INT_POS, NUM_OF_INT_OF_NUM] +QED + +(* NOTE: The proof is a direct translation from OCaml to SML *) +Theorem RING_OF_INT_CASES : + (!r n. ring_of_int r (&n) = ring_of_num (r : 'a Ring) n) /\ + (!r n. ring_of_int r (-&n) = ring_neg r (ring_of_num r n)) +Proof + REPEAT STRIP_TAC THEN REWRITE_TAC[RING_OF_INT_OF_NUM] THEN + REWRITE_TAC[ring_of_int, INT_ARITH “0:int <= - &n <=> &n:int = &0”] THEN + SIMP_TAC std_ss[INT_NEG_NEG, INT_OF_NUM_EQ, INT_NEG_0, NUM_OF_INT_OF_NUM] THEN + COND_CASES_TAC THEN ASM_REWRITE_TAC[ring_of_num, RING_NEG_0] +QED + +Theorem RING_OF_INT_NEG : + !(r :'a Ring) n. ring_of_int r (-n) = ring_neg r (ring_of_int r n) +Proof + SIMP_TAC std_ss[FORALL_INT_CASES, RING_OF_INT_CASES, INT_NEG_NEG, + RING_NEG_NEG, RING_OF_NUM] +QED + +val lemma1 = + METIS_PROVE[RING_ADD_SYM, RING_NEG] + “!x y. x IN ring_carrier r /\ y IN ring_carrier r + ==> ring_add r (ring_neg r x) y = ring_add r y (ring_neg r x)”; + +Theorem RING_OF_INT_ADD : + !(r :'a Ring) m n. + ring_of_int r (m + n) = ring_add r (ring_of_int r m) (ring_of_int r n) +Proof + SUBGOAL_THEN + “!(r :'a Ring) m n p. + m + n = p ==> + ring_of_int r p = ring_add r (ring_of_int r m) (ring_of_int r n)” + (fn th => MESON_TAC[th]) THEN + GEN_TAC THEN SIMP_TAC std_ss[FORALL_INT_CASES, RING_OF_INT_CASES] THEN + ONCE_REWRITE_TAC[INT_ARITH “-b + (a:int) = a + -b”] THEN + REWRITE_TAC[GSYM INT_NEG_ADD, INT_NEG_EQ, INT_NEG_NEG] THEN + REWRITE_TAC[INT_ARITH + “(&a + &b:int = - &c <=> &a:int = &0 /\ &b:int = &0 /\ &c:int = &0) /\ + (!m n p. m + -n:int = &p <=> m = n + &p) /\ + (!m n p. m + -n:int = - &p <=> m + &p = n)”] THEN + REWRITE_TAC[INT_OF_NUM_ADD, INT_OF_NUM_EQ] THEN + REPEAT STRIP_TAC + (* 8 subgoals here *) + >- (POP_ASSUM (ONCE_REWRITE_TAC o wrap o SYM) \\ + REWRITE_TAC [RING_OF_NUM_ADD]) + (* 7 subgoals left *) + >- (rw [GSYM RING_OF_NUM_ADD, RING_OF_NUM_0, RING_NEG_0]) + (* 6 subgoals left *) + >- (POP_ORW \\ + REWRITE_TAC[RING_OF_NUM_ADD] \\ + REWRITE_TAC[GSYM ring_sub] \\ + SIMP_TAC std_ss[RING_EQ_SUB_LADD, RING_SUB, RING_OF_NUM, RING_ADD] \\ + SIMP_TAC std_ss[Once RING_ADD_SYM, RING_OF_NUM]) + (* 5 subgoals left *) + >- (POP_ASSUM (ONCE_REWRITE_TAC o wrap o SYM) \\ + REWRITE_TAC [RING_OF_NUM_ADD] \\ + REWRITE_TAC[GSYM ring_sub] \\ + SIMP_TAC std_ss[RING_EQ_SUB_LADD, RING_NEG, RING_SUB, RING_OF_NUM, RING_ADD] \\ + SIMP_TAC std_ss[Once RING_ADD_SYM, RING_OF_NUM, RING_ADD, RING_NEG, + GSYM RING_ADD_ASSOC] \\ + REWRITE_TAC[GSYM ring_sub] \\ + Know ‘ring_sub r (ring_of_num r n'') (ring_of_num r n'') = ring_0 r’ + >- (SIMP_TAC std_ss[RING_SUB_EQ_0, RING_OF_NUM, RING_0]) >> Rewr' \\ + SIMP_TAC std_ss[RING_ADD_RZERO, RING_OF_NUM]) + (* 4 subgoals left *) + >- (POP_ORW \\ + REWRITE_TAC [RING_OF_NUM_ADD] \\ + SIMP_TAC std_ss[RING_ADD_ASSOC, RING_OF_NUM, RING_NEG, RING_ADD] \\ + Know ‘ring_add r (ring_neg r (ring_of_num r n)) (ring_of_num r n) = + ring_add r (ring_of_num r n) (ring_neg r (ring_of_num r n))’ + >- (SIMP_TAC std_ss[Once RING_ADD_SYM, RING_OF_NUM, RING_NEG]) >> Rewr' \\ + REWRITE_TAC[GSYM ring_sub] \\ + Know ‘ring_sub r (ring_of_num r n) (ring_of_num r n) = ring_0 r’ + >- (SIMP_TAC std_ss[RING_SUB_EQ_0, RING_OF_NUM, RING_0]) >> Rewr' \\ + SIMP_TAC std_ss[RING_ADD_LZERO, RING_OF_NUM]) + (* 3 subgoals left *) + >- (POP_ASSUM (ONCE_REWRITE_TAC o wrap o SYM) \\ + REWRITE_TAC [RING_OF_NUM_ADD] \\ + SIMP_TAC std_ss[lemma1, RING_OF_NUM, RING_NEG, RING_ADD] \\ + SIMP_TAC std_ss[RING_NEG_ADD, RING_OF_NUM] \\ + SIMP_TAC std_ss[RING_ADD_ASSOC, RING_OF_NUM, RING_NEG, RING_ADD] \\ + REWRITE_TAC[GSYM ring_sub] \\ + Know ‘ring_sub r (ring_of_num r n') (ring_of_num r n') = ring_0 r’ + >- (SIMP_TAC std_ss[RING_SUB_EQ_0, RING_OF_NUM, RING_0]) >> Rewr' \\ + SIMP_TAC std_ss[RING_SUB_LZERO, RING_OF_NUM]) + (* 2 subgoals left *) + >- (rw [GSYM RING_OF_NUM_ADD, RING_OF_NUM_0, RING_NEG_0] \\ + SIMP_TAC std_ss[RING_ADD_LZERO, RING_0]) + (* final subgoal *) + >> SIMP_TAC std_ss[GSYM RING_NEG_ADD, RING_OF_NUM, RING_NEG] + >> AP_TERM_TAC + >> POP_ASSUM (ONCE_REWRITE_TAC o wrap o SYM) + >> REWRITE_TAC [RING_OF_NUM_ADD] + >> SIMP_TAC std_ss[Once RING_ADD_SYM, RING_OF_NUM] +QED + +Theorem RING_OF_INT_SUB : + !(r :'a Ring) m n. + ring_of_int r (m - n) = ring_sub r (ring_of_int r m) (ring_of_int r n) +Proof + SIMP_TAC std_ss[int_sub, ring_sub, RING_OF_INT_ADD, RING_OF_INT_NEG, + RING_NEG, RING_OF_INT] +QED + +Theorem RING_OF_INT_MUL : + !(r :'a Ring) m n. + ring_of_int r (m * n) = ring_mul r (ring_of_int r m) (ring_of_int r n) +Proof + SIMP_TAC std_ss[FORALL_INT_CASES, INT_MUL_LNEG, INT_MUL_RNEG, INT_NEG_NEG] THEN + REWRITE_TAC[RING_OF_INT_CASES, INT_OF_NUM_MUL, RING_OF_NUM_MUL] THEN + SIMP_TAC std_ss[RING_MUL_LNEG, RING_MUL_RNEG, RING_OF_NUM, RING_NEG, + RING_NEG_NEG, RING_MUL] +QED + +Theorem RING_OF_INT_0 : + !(r :'a Ring). ring_of_int r (&0) = ring_0 r +Proof + REWRITE_TAC[RING_OF_INT_OF_NUM, RING_OF_NUM_0] +QED + +Theorem RING_OF_INT_1 : + !(r :'a Ring). ring_of_int r (&1) = ring_1 r +Proof + REWRITE_TAC[RING_OF_INT_OF_NUM, RING_OF_NUM_1] +QED + +Theorem RING_OF_INT_POW : + !(r :'a Ring) x n. + ring_of_int r (x ** n) = ring_pow r (ring_of_int r x) n +Proof + GEN_TAC THEN GEN_TAC THEN + INDUCT_TAC THEN ASM_REWRITE_TAC[ring_pow, INT_POW, RING_OF_INT_1] THEN + ASM_REWRITE_TAC[RING_OF_INT_MUL] +QED + +(* ------------------------------------------------------------------------- *) +(* Characteristic of a ring, characterized by RING_OF_NUM_EQ_0. *) +(* ------------------------------------------------------------------------- *) + +Definition ring_char_def : + ring_char (r :'a Ring) = char (fromRing r) +End + +Theorem RING_OF_NUM_EQ_0 : + !(r :'a Ring) n. ring_of_num r n = ring_0 r <=> ring_char r divides n +Proof + Q.X_GEN_TAC ‘r0’ + >> Q.ABBREV_TAC ‘r = fromRing r0’ + >> rw [ring_of_num_def, ring_0_def, ring_1_def, ring_char_def] + >> irule ring_char_divides + >> rw [Abbr ‘r’] +QED + +Theorem RING_OF_INT_EQ_0 : + !(r :'a Ring) n. + ring_of_int r n = ring_0 r <=> &(ring_char r) int_divides n +Proof + SIMP_TAC std_ss[FORALL_INT_CASES, RING_OF_INT_CASES] THEN + SIMP_TAC std_ss[RING_NEG_EQ_0, RING_OF_NUM, RING_OF_NUM_EQ_0] THEN + REWRITE_TAC[num_divides] THEN REPEAT STRIP_TAC THEN + REWRITE_TAC [INT_DIVIDES_NEG] (* was: INTEGER_TAC *) +QED + +(* The original statement was: (m == n) (mod &(ring_char r)) + + NOTE: In HOL-Light, ‘(m == n) f’ (cong) means ‘f m n’ (int.ml). But this + syntax is now used by ‘fequiv’, which means ‘f m = f n’ (fequiv_def). + *) +Theorem RING_OF_INT_EQ : + !(r :'a Ring) m n. + ring_of_int r m = ring_of_int r n <=> + &(ring_char r) int_divides (m - n) +Proof + REPEAT STRIP_TAC THEN + W(MP_TAC o PART_MATCH (rand o rand) RING_SUB_EQ_0 o lhand o snd) THEN + REWRITE_TAC[RING_OF_INT, GSYM RING_OF_INT_SUB] THEN + DISCH_THEN(SUBST1_TAC o SYM) THEN REWRITE_TAC[RING_OF_INT_EQ_0] +QED + (* ------------------------------------------------------------------------- *) (* Homomorphisms etc. *) (* ------------------------------------------------------------------------- *) @@ -483,6 +886,9 @@ Proof >> irule ring_homo_mult >> art [] QED +val lemma = REWRITE_RULE [ringTheory.ring_sub_def, ring_add_def, ring_neg_def] + (Q.SPECL [‘r’, ‘r'’] ring_homo_sub); + Theorem RING_HOMOMORPHISM_SUB : !r r' (f :'a -> 'b). ring_homomorphism(r,r') f ==> !x y. x IN ring_carrier r /\ y IN ring_carrier r @@ -493,7 +899,8 @@ Proof >> Q.ABBREV_TAC ‘r = fromRing r0’ >> Q.ABBREV_TAC ‘r' = fromRing r1’ >> ‘Ring r /\ Ring r'’ by rw [Abbr ‘r’, Abbr ‘r'’] - >> irule (REWRITE_RULE [ring_sub_def] ring_homo_sub) >> art [] + >> rw [ring_add_def, ring_neg_def] + >> irule lemma >> art [] QED Theorem RING_HOMOMORPHISM_POW : @@ -509,80 +916,6 @@ Proof >> irule ring_homo_exp >> art [] QED -Definition ring_monomorphism : - ring_monomorphism (r,r') (f :'a -> 'b) <=> - ring_homomorphism (r,r') f /\ - !x y. x IN ring_carrier r /\ y IN ring_carrier r /\ f x = f y ==> x = y -End - -(* ------------------------------------------------------------------------- *) -(* Mapping natural numbers and integers into a ring in the obvious way. *) -(* ------------------------------------------------------------------------- *) - -(* ##n *) -Definition ring_of_num_def : - ring_of_num (r :'a Ring) = (fromRing r).sum.exp (ring_1 r) -End - -Theorem ring_of_num : - !r. ring_of_num r (0 :num) = ring_0 (r :'a Ring) /\ - !n. ring_of_num r (SUC n) = ring_add r (ring_of_num r n) (ring_1 r) -Proof - Q.X_GEN_TAC ‘r0’ - >> Q.ABBREV_TAC ‘r = fromRing r0’ - >> RW_TAC std_ss [ring_num_0, ring_of_num_def, ring_0_def, ring_1_def, - ring_add_def] - >> ‘Ring r’ by rw [Abbr ‘r’] - >> Know ‘##n + #1 = #1 + ##n’ - >- (irule ring_add_comm >> rw []) - >> Rewr' - >> MATCH_MP_TAC ring_num_SUC >> art [] -QED - -Theorem RING_OF_NUM : - !r n. ring_of_num r n IN ring_carrier (r :'a Ring) -Proof - qx_genl_tac [‘r0’, ‘n’] - >> Q.ABBREV_TAC ‘r = fromRing r0’ - >> RW_TAC std_ss [ring_carrier_def, ring_of_num_def, ring_1_def] - >> MATCH_MP_TAC ring_num_element - >> rw [Abbr ‘r’] -QED - -Theorem RING_OF_NUM_0 : - !(r :'a Ring). ring_of_num r 0 = ring_0 r -Proof - REWRITE_TAC[ring_of_num] -QED - -Theorem RING_OF_NUM_1 : - !(r :'a Ring). ring_of_num r 1 = ring_1 r -Proof - SIMP_TAC bool_ss[num_CONV “1:num”, ring_of_num, RING_ADD_LZERO, RING_1] -QED - -Definition ring_of_int : - ring_of_int (r :'a Ring) (n :int) = - if &0 <= n then ring_of_num r (num_of_int n) - else ring_neg r (ring_of_num r (num_of_int (-n))) -End - -Theorem RING_OF_INT : - !r n. ring_of_int r n IN ring_carrier (r :'a Ring) -Proof - REPEAT GEN_TAC THEN REWRITE_TAC[ring_of_int] THEN COND_CASES_TAC THEN - ASM_SIMP_TAC std_ss [RING_NEG, RING_OF_NUM] -QED - -(* |- !n. num_of_int(&n) = n *) -Theorem NUM_OF_INT_OF_NUM = NUM_OF_INT; - -Theorem RING_OF_INT_OF_NUM : - !r n. ring_of_int r (&n) = ring_of_num (r :'a Ring) n -Proof - REWRITE_TAC[ring_of_int, INT_POS, NUM_OF_INT_OF_NUM] -QED - Theorem RING_HOMOMORPHISM_RING_OF_NUM : !r r' (f :'a -> 'b). ring_homomorphism(r,r') f ==> !n. f(ring_of_num r n) = ring_of_num r' n @@ -595,23 +928,6 @@ Proof >> irule ring_homo_num >> art [] QED -(* |- |- !x. --x = x *) -Theorem INT_NEG_NEG = INT_NEGNEG - -(* |- !m n. &m = &n <=> m = n *) -Theorem INT_OF_NUM_EQ = INT_INJ - -(* NOTE: The proof is a direct translation from OCaml to SML *) -Theorem RING_OF_INT_CASES : - (!r n. ring_of_int r (&n) = ring_of_num (r : 'a Ring) n) /\ - (!r n. ring_of_int r (-&n) = ring_neg r (ring_of_num r n)) -Proof - REPEAT STRIP_TAC THEN REWRITE_TAC[RING_OF_INT_OF_NUM] THEN - REWRITE_TAC[ring_of_int, INT_ARITH “0:int <= - &n <=> &n:int = &0”] THEN - SIMP_TAC std_ss[INT_NEG_NEG, INT_OF_NUM_EQ, INT_NEG_0, NUM_OF_INT_OF_NUM] THEN - COND_CASES_TAC THEN ASM_REWRITE_TAC[ring_of_num, RING_NEG_0] -QED - (* NOTE: The proof is a direct translation from OCaml to SML *) Theorem RING_HOMOMORPHISM_RING_OF_INT : !r r' (f :'a -> 'b). ring_homomorphism(r,r') f @@ -625,6 +941,12 @@ Proof ASM_SIMP_TAC std_ss [MATCH_MP RING_HOMOMORPHISM_RING_OF_NUM th]) QED +Definition ring_monomorphism : + ring_monomorphism (r,r') (f :'a -> 'b) <=> + ring_homomorphism (r,r') f /\ + !x y. x IN ring_carrier r /\ y IN ring_carrier r /\ f x = f y ==> x = y +End + (* NOTE: This theorem was part of HOL-Light's RING_MONOMORPHIC_IMAGE_RULE *) Theorem RING_MONOMORPHIC_IMAGE_RULE_THM : !r r' (f :'a -> 'b). @@ -665,7 +987,7 @@ Theorem RING_MONOMORPHIC_IMAGE_RULE_THM : f(ring_mul r x y) = ring_mul r' x' y') Proof rpt GEN_TAC >> REWRITE_TAC[ring_monomorphism] - >> GEN_REWRITE_TAC LAND_CONV empty_rewrites [CONJ_SYM] + >> GEN_REWRITE_TAC LAND_CONV [CONJ_SYM] >> MATCH_MP_TAC MONO_AND >> CONJ_TAC >- MESON_TAC[] >> METIS_TAC[RING_0, RING_1, RING_OF_NUM, RING_OF_INT, RING_NEG, @@ -1026,7 +1348,7 @@ Theorem RING_HOMOMORPHISM_FROM_TRIVIAL_RING : trivial_ring r' /\ IMAGE f (ring_carrier r) = {ring_0 r'}) Proof REPEAT GEN_TAC THEN - GEN_REWRITE_TAC LAND_CONV empty_rewrites [trivial_ring] THEN + GEN_REWRITE_TAC LAND_CONV [trivial_ring] THEN DISCH_TAC THEN EQ_TAC THENL [ (* goal 1 (of 2) *) ASM_SIMP_TAC std_ss[ring_homomorphism, TRIVIAL_RING_10] THEN @@ -1290,32 +1612,6 @@ QED Theorem PRODUCT_RING_NEG' = PRODUCT_RING_NEG |> SIMP_RULE std_ss [PRODUCT_RING, IN_CARTESIAN_PRODUCT] -Theorem RING_TOTALIZATION_lemma[local] : - !r :'a Ring. - ~(trivial_ring r) /\ INFINITE univ(:'b) /\ univ(:'a) <=_c univ(:'b) - ==> ring_carrier(product_ring univ(:'b) (\(i :'b). r)) =_c univ(:'b -> bool) -Proof - rpt STRIP_TAC - >> REWRITE_TAC[PRODUCT_RING, CARTESIAN_PRODUCT_CONST, UNIV_fun_exp] - >> MATCH_MP_TAC CARD_EXP_ABSORB >> art [] - >> CONJ_TAC (* 2 subgoals *) - >| [ (* goal 1 (of 2) *) - TRANS_TAC CARD_LE_TRANS “{ring_0 r:'a;ring_1 r:'a}” \\ - CONJ_TAC >| (* 2 subgoals *) - [ (* goal 1.1 (of 2) *) - RULE_ASSUM_TAC(REWRITE_RULE[TRIVIAL_RING_10]) \\ - rw [CARD_LE_CARD, FINITE_INSERT, FINITE_EMPTY, FINITE_BOOL, - CARD_BOOL, CARD_CLAUSES], - (* goal 1.2 (of 2) *) - MATCH_MP_TAC CARD_LE_SUBSET \\ - REWRITE_TAC[INSERT_SUBSET, EMPTY_SUBSET, RING_0, RING_1] ], - (* goal 2 (of 2) *) - TRANS_TAC CARD_LE_TRANS “univ(:'a)” \\ - ASM_SIMP_TAC std_ss [CARD_LE_SUBSET, SUBSET_UNIV] \\ - TRANS_TAC CARD_LE_TRANS “univ(:'b)” >> art [] \\ - SIMP_TAC std_ss[CARD_EXP_CANTOR, CARD_LT_IMP_LE] ] -QED - Theorem RING_MONOMORPHISM_COMPOSE : !r1 r2 r3 (f :'a -> 'b) (g :'b -> 'c). ring_monomorphism(r1,r2) f /\ ring_monomorphism(r2,r3) g @@ -1392,9 +1688,35 @@ Proof SET_TAC[] QED +Theorem RING_TOTALIZATION_lemma[local] : + !r :'a Ring. + ~(trivial_ring r) /\ INFINITE univ(:'b) /\ univ(:'a) <=_c univ(:'b) + ==> ring_carrier(product_ring univ(:'b) (\(i :'b). r)) =_c univ(:'b -> bool) +Proof + rpt STRIP_TAC + >> REWRITE_TAC[PRODUCT_RING, CARTESIAN_PRODUCT_CONST, UNIV_fun_exp] + >> MATCH_MP_TAC CARD_EXP_ABSORB >> art [] + >> CONJ_TAC (* 2 subgoals *) + >| [ (* goal 1 (of 2) *) + TRANS_TAC CARD_LE_TRANS “{ring_0 r:'a;ring_1 r:'a}” \\ + CONJ_TAC >| (* 2 subgoals *) + [ (* goal 1.1 (of 2) *) + RULE_ASSUM_TAC(REWRITE_RULE[TRIVIAL_RING_10]) \\ + rw [CARD_LE_CARD, FINITE_INSERT, FINITE_EMPTY, FINITE_BOOL, + CARD_BOOL, CARD_CLAUSES], + (* goal 1.2 (of 2) *) + MATCH_MP_TAC CARD_LE_SUBSET \\ + REWRITE_TAC[INSERT_SUBSET, EMPTY_SUBSET, RING_0, RING_1] ], + (* goal 2 (of 2) *) + TRANS_TAC CARD_LE_TRANS “univ(:'a)” \\ + ASM_SIMP_TAC std_ss [CARD_LE_SUBSET, SUBSET_UNIV] \\ + TRANS_TAC CARD_LE_TRANS “univ(:'b)” >> art [] \\ + SIMP_TAC std_ss[CARD_EXP_CANTOR, CARD_LT_IMP_LE] ] +QED + Theorem RING_TOTALIZATION : !r :'a Ring. - (?r' f. ring_carrier r' = {()} /\ + (?r' f. ring_carrier r' = univ(:unit) /\ ring_monomorphism(r,r') f) \/ (?r' f. ring_carrier r' = univ(:(num # 'a) -> bool)/\ ring_monomorphism(r,r') f) @@ -1405,7 +1727,8 @@ Proof ASM_SIMP_TAC std_ss[RING_MONOMORPHISM_FROM_TRIVIAL_RING, RING_HOMOMORPHISM_FROM_TRIVIAL_RING] THEN ASM_SIMP_TAC std_ss[TRIVIAL_RING_SINGLETON_RING, SINGLETON_RING] THEN - REWRITE_TAC[IMAGE_CONST, RING_CARRIER_NONEMPTY] ) + REWRITE_TAC[IMAGE_CONST, RING_CARRIER_NONEMPTY] THEN + rw [Once EXTENSION] ) >> DISJ2_TAC >> MP_TAC(snd(EQ_IMP_RULE(ISPECL [“product_ring univ(:num # 'a) (\i. (r :'a Ring))”, “univ(:num # 'a -> bool)”] @@ -1416,13 +1739,13 @@ Proof ASM_REWRITE_TAC[GSYM MUL_C_UNIV, CARD_MUL_FINITE_EQ] THEN REWRITE_TAC[UNIV_NOT_EMPTY, DE_MORGAN_THM] THEN REWRITE_TAC[num_INFINITE, MUL_C_UNIV] THEN - REWRITE_TAC[le_c] THEN EXISTS_TAC “\x:'a. (0,x)” THEN + REWRITE_TAC[le_c] THEN EXISTS_TAC “\x:'a. (0:num,x)” THEN SIMP_TAC std_ss[IN_UNIV], (* goal 2 (of 2) *) HO_MATCH_MP_TAC MONO_EXISTS THEN Q.X_GEN_TAC ‘r'’ THEN STRIP_TAC THEN ASM_REWRITE_TAC[] ] THEN (* stage work *) - FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I empty_rewrites [isomorphic_ring]) THEN + FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [isomorphic_ring]) THEN DISCH_THEN(Q.X_CHOOSE_TAC ‘f’) THEN Q.EXISTS_TAC ‘f o (\x i. x)’ THEN MATCH_MP_TAC RING_MONOMORPHISM_COMPOSE THEN @@ -1431,33 +1754,71 @@ Proof ASM_SIMP_TAC std_ss[RING_ISOMORPHISM_IMP_MONOMORPHISM] QED -Theorem RING_WORD_UNIVERSAL_LEMMA1 : - ring_0 r = ring_of_int (r :'a Ring) (&0) /\ - ring_1 r = ring_of_int (r :'a Ring) (&1) -Proof - REWRITE_TAC[RING_OF_INT_OF_NUM, RING_OF_NUM_0, RING_OF_NUM_1] -QED - -Theorem RING_WORD_UNIVERSAL_LEMMA2 : - ring_carrier r = univ(:'a) ==> - (x = y <=> ring_sub r x y = ring_of_int r (&0)) -Proof - SIMP_TAC bool_ss[RING_SUB_EQ_0, IN_UNIV, RING_OF_INT_OF_NUM, RING_OF_NUM_0] -QED +(* ------------------------------------------------------------------------- *) +(* Integral domain and field. *) +(* ------------------------------------------------------------------------- *) -Theorem RING_WORD_UNIVERSAL_LEMMA3 : - ring_carrier r = univ(:'a) ==> - p = ring_of_int r (&0) ==> !c. ring_mul r c p = ring_of_int r (&0) -Proof - SIMP_TAC bool_ss[RING_MUL_RZERO, RING_OF_INT_OF_NUM, RING_OF_NUM_0, IN_UNIV] -QED +Definition integral_domain_def : + integral_domain (r :'a Ring) = IntegralDomain (fromRing r) +End -Theorem RING_WORD_UNIVERSAL_LEMMA4 : - ring_carrier r = univ(:'a) ==> - p = ring_of_int r (&0) /\ q = ring_of_int r (&0) ==> - ring_add r p q = ring_of_int r (&0) +Theorem integral_domain : + integral_domain (r :'a Ring) <=> + ~(ring_1 r = ring_0 r) /\ + (!x y. x IN ring_carrier r /\ + y IN ring_carrier r /\ + ring_mul r x y = ring_0 r + ==> x = ring_0 r \/ y = ring_0 r) Proof - SIMP_TAC bool_ss[RING_ADD_RZERO, RING_OF_INT_OF_NUM, RING_OF_NUM_0, IN_UNIV] + Q.ID_SPEC_TAC ‘r’ + >> Q.X_GEN_TAC ‘r0’ + >> Q.ABBREV_TAC ‘r = fromRing r0’ + >> rw [integral_domain_def, ring_1_def, ring_0_def, ring_carrier_def, + ring_mul_def] + >> ‘Ring r’ by rw [Abbr ‘r’] + >> rw [IntegralDomain_def] + >> EQ_TAC >> rw [] >- METIS_TAC [] + >> EQ_TAC >> rw [] + >| [ (* goal 1 (of 2) *) + rw [ring_mult_lzero], + (* goal 2 (of 2) *) + rw [ring_mult_rzero] ] +QED + +Theorem INTEGRAL_DOMAIN_MUL_EQ_0 : + !r a (b :'a). + integral_domain r /\ a IN ring_carrier r /\ b IN ring_carrier r + ==> (ring_mul r a b = ring_0 r <=> a = ring_0 r \/ b = ring_0 r) +Proof + REWRITE_TAC[integral_domain] THEN + MESON_TAC[RING_MUL_LZERO, RING_MUL_RZERO] +QED + +Theorem RING_INTEGRAL_LEMMA : + integral_domain r + ==> ring_carrier r = univ(:'a) + ==> (!x. ring_mul r (ring_of_int r (&0)) x = ring_of_int r (&0)) /\ + (!x y z. ring_add r x y = ring_add r x z <=> y = z) /\ + (!w x y z. + ring_add r (ring_mul r w y) (ring_mul r x z) = + ring_add r (ring_mul r w z) (ring_mul r x y) <=> + w = x \/ y = z) +Proof + REPEAT GEN_TAC THEN REPEAT DISCH_TAC THEN + REWRITE_TAC[RING_OF_INT_OF_NUM, RING_OF_NUM_0] THEN + ASM_SIMP_TAC std_ss[RING_MUL_LZERO, RING_ADD_LCANCEL, IN_UNIV] THEN + REPEAT GEN_TAC THEN + MP_TAC(ISPEC “r :'a Ring” RING_SUB_EQ_0) THEN + ASM_REWRITE_TAC[IN_UNIV] THEN + DISCH_THEN(fn th => ONCE_REWRITE_TAC[GSYM th]) THEN + FIRST_X_ASSUM(MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ] + INTEGRAL_DOMAIN_MUL_EQ_0)) THEN + ASM_REWRITE_TAC[IN_UNIV] THEN + DISCH_THEN(fn th => ONCE_REWRITE_TAC[GSYM th]) THEN + AP_THM_TAC THEN AP_TERM_TAC THEN + ASM_SIMP_TAC std_ss[ring_sub, IN_UNIV, RING_ADD_LDISTRIB, RING_ADD_RDISTRIB, + RING_NEG_NEG, RING_NEG_ADD, RING_MUL_LNEG, RING_MUL_RNEG] THEN + ASM_SIMP_TAC std_ss[RING_ADD_AC, IN_UNIV] QED val _ = export_theory(); diff --git a/examples/algebra/ring/ringSyntax.sig b/examples/algebra/ring/ringSyntax.sig new file mode 100644 index 0000000000..d53d592970 --- /dev/null +++ b/examples/algebra/ring/ringSyntax.sig @@ -0,0 +1,35 @@ +signature ringSyntax = +sig + + include Abbrev + + val ring_add_tm : term + val ring_sub_tm : term + val ring_mul_tm : term + val ring_pow_tm : term + val ring_neg_tm : term + val ring_of_num_tm : term + val ring_of_int_tm : term + val ring_carrier_tm : term + val ring_monomorphism_tm : term + + val is_ring_0 : term -> bool + val is_ring_1 : term -> bool + val is_ring_of_num : term -> bool + val is_ring_of_int : term -> bool + val is_ring_neg : term -> bool + val is_ring_pow : term -> bool + val is_ring_add : term -> bool + val is_ring_sub : term -> bool + val is_ring_mul : term -> bool + val is_ringconst : term -> bool + + val dest_ring_of_num : term -> term * term + val dest_ring_of_int : term -> term * term + val dest_ring_neg : term -> term * term + val dest_ring_pow : term -> term * term * term + val dest_ring_add : term -> term * term * term + val dest_ring_sub : term -> term * term * term + val dest_ring_mul : term -> term * term * term + +end diff --git a/examples/algebra/ring/ringSyntax.sml b/examples/algebra/ring/ringSyntax.sml new file mode 100644 index 0000000000..e4c8a8cc00 --- /dev/null +++ b/examples/algebra/ring/ringSyntax.sml @@ -0,0 +1,188 @@ +structure ringSyntax :> ringSyntax = +struct + +open HolKernel boolLib bossLib intSyntax ringLibTheory; + +(* ------------------------------------------------------------------------- *) +(* Establish the required grammar(s) for executing this file *) +(* ------------------------------------------------------------------------- *) + +structure Parse = struct + open Parse + val (Type,Term) = parse_from_grammars ringLib_grammars +end + +open Parse; + +val ERR = mk_HOL_ERR "ringSyntax"; +fun failwith s = raise ERR "?" s + +val ring_add_tm = “ring_add :'a Ring -> 'a -> 'a -> 'a”; +val ring_sub_tm = “ring_sub :'a Ring -> 'a -> 'a -> 'a”; +val ring_mul_tm = “ring_mul :'a Ring -> 'a -> 'a -> 'a”; +val ring_pow_tm = “ring_pow :'a Ring -> 'a -> num -> 'a”; +val ring_neg_tm = “ring_neg :'a Ring -> 'a -> 'a”; +val ring_of_num_tm = “ring_of_num :'a Ring -> num -> 'a”; +val ring_of_int_tm = “ring_of_int :'a Ring -> int -> 'a”; + +val ring_carrier_tm = + “ring_carrier :'a Ring -> 'a -> bool”; + +val ring_monomorphism_tm = + “ring_monomorphism :'a Ring # 'b Ring -> ('a -> 'b) -> bool”; + +val dest_ring_add = dest_triop ring_add_tm (Fail "not a ring_add"); +val dest_ring_sub = dest_triop ring_sub_tm (Fail "not a ring_sub"); +val dest_ring_mul = dest_triop ring_mul_tm (Fail "not a ring_mul"); +val dest_ring_pow = dest_triop ring_pow_tm (Fail "not a ring_pow"); +val dest_ring_neg = dest_binop ring_neg_tm (Fail "not a ring_neg"); +val dest_ring_of_num = dest_binop ring_of_num_tm (Fail "not a ring_of_num"); +val dest_ring_of_int = dest_binop ring_of_int_tm (Fail "not a ring_of_num"); + +fun is_ring_0 tm = + is_comb tm andalso let + val (op',_) = dest_comb tm + in + is_const op' andalso let + val {Name: string, Thy: string, Ty: hol_type} = dest_thy_const op' + in + Thy = "ringLib" andalso Name = "ring_0" + end + end; + +fun is_ring_1 tm = + is_comb tm andalso let + val (op',_) = dest_comb tm + in + is_const op' andalso let + val {Name: string, Thy: string, Ty: hol_type} = dest_thy_const op' + in + Thy = "ringLib" andalso Name = "ring_1" + end + end; + +fun is_ring_of_num tm = + is_comb tm andalso let + val (op',_) = dest_comb tm + in + is_comb op' andalso let + val (op'',_) = dest_comb op' + in + is_const op'' andalso let + val {Name: string, Thy: string, Ty: hol_type} = dest_thy_const op'' + in + Thy = "ringLib" andalso Name = "ring_of_num" + end + end + end; + +fun is_ring_of_int tm = + is_comb tm andalso let + val (op',_) = dest_comb tm + in + is_comb op' andalso let + val (op'',_) = dest_comb op' + in + is_const op'' andalso let + val {Name: string, Thy: string, Ty: hol_type} = dest_thy_const op'' + in + Thy = "ringLib" andalso Name = "ring_of_int" + end + end + end; + +fun is_ring_neg tm = + is_comb tm andalso let + val (op',_) = dest_comb tm + in + is_comb op' andalso let + val (op'',_) = dest_comb op' + in + is_const op'' andalso let + val {Name: string, Thy: string, Ty: hol_type} = dest_thy_const op'' + in + Thy = "ringLib" andalso Name = "ring_neg" + end + end + end; + +fun is_ring_pow tm = + is_comb tm andalso let + val (op',_) = dest_comb tm + in + is_comb op' andalso let + val (op'',_) = dest_comb op' + in + is_comb op'' andalso let + val (op''',_) = dest_comb op'' + in + is_const op''' andalso let + val {Name: string, Thy: string, Ty: hol_type} = dest_thy_const op''' + in + Thy = "ringLib" andalso Name = "ring_pow" + end + end + end + end; + +fun is_ring_add tm = + is_comb tm andalso let + val (op',_) = dest_comb tm + in + is_comb op' andalso let + val (op'',_) = dest_comb op' + in + is_comb op'' andalso let + val (op''',_) = dest_comb op'' + in + is_const op''' andalso let + val {Name: string, Thy: string, Ty: hol_type} = dest_thy_const op''' + in + Thy = "ringLib" andalso Name = "ring_add" + end + end + end + end; + +fun is_ring_sub tm = + is_comb tm andalso let + val (op',_) = dest_comb tm + in + is_comb op' andalso let + val (op'',_) = dest_comb op' + in + is_comb op'' andalso let + val (op''',_) = dest_comb op'' + in + is_const op''' andalso let + val {Name: string, Thy: string, Ty: hol_type} = dest_thy_const op''' + in + Thy = "ringLib" andalso Name = "ring_sub" + end + end + end + end; + +fun is_ring_mul tm = + is_comb tm andalso let + val (op',_) = dest_comb tm + in + is_comb op' andalso let + val (op'',_) = dest_comb op' + in + is_comb op'' andalso let + val (op''',_) = dest_comb op'' + in + is_const op''' andalso let + val {Name: string, Thy: string, Ty: hol_type} = dest_thy_const op''' + in + Thy = "ringLib" andalso Name = "ring_mul" + end + end + end + end; + +fun is_ringconst tm = + is_ring_of_int tm andalso is_int_literal (snd (dest_ring_of_int tm)); + +end (* struct *) diff --git a/examples/algebra/ring/selftest.sml b/examples/algebra/ring/selftest.sml new file mode 100644 index 0000000000..7243e809b6 --- /dev/null +++ b/examples/algebra/ring/selftest.sml @@ -0,0 +1,81 @@ +(* ========================================================================= *) +(* A decision procedure for the universal theory of rings (test cases) *) +(* *) +(* John Harrison, University of Cambridge Computer Laboratory *) +(* (c) Copyright, University of Cambridge 1998 *) +(* ========================================================================= *) + +open HolKernel Portable Parse boolLib; + +open ringLib testutils; + +(* Tests for RING_RULE + + NOTE: RING_RULE may output theorem with extra antecedents in comparison with + the input term. + *) +fun rule_test prover (r as (n,tm)) = + let + fun check res = let + val input = tm and output = concl res; + in + input ~~ output orelse + if is_imp output then + input ~~ rand output + else + false + end + in + tprint (n ^ ": " ^ term_to_string tm); + require_msg (check_result check) (term_to_string o concl) prover tm + end; + +(* NOTE: These test cases were taken from calls of RING_RULE in HOL-Light's + "ringtheory.ml". + *) +val _ = List.app (rule_test RING_RULE) [ + ("RING_RULE_00", + “ring_mul r y1 (ring_inv r y1) = ring_1 r /\ + ring_mul r y2 (ring_inv r y2) = ring_1 r /\ + ring_mul r x1 y2 = ring_mul r x2 y1 + ==> ring_mul r x1 (ring_inv r y1) = ring_mul r x2 (ring_inv r y2)”), + ("RING_RULE_01", + “z IN ring_carrier r + ==> ring_add r z (ring_1 r) = ring_add r (ring_1 r) z /\ + ring_sub r z (ring_1 r) = ring_neg r (ring_sub r (ring_1 r) z)”), + ("RING_RULE_02", + “ring_1 r = ring_sub r (ring_1 r) (ring_0 r)”), + ("RING_RULE_03", + “u IN ring_carrier r /\ v IN ring_carrier r /\ z IN ring_carrier r /\ + ring_mul r u (v :'a) = ring_1 r + ==> ring_add r u z = + ring_mul r u (ring_add r (ring_1 r) (ring_mul r v z)) /\ + ring_add r z u = + ring_mul r u (ring_add r (ring_1 r) (ring_mul r v z)) /\ + ring_sub r u z = + ring_mul r u (ring_sub r (ring_1 r) (ring_mul r v z)) /\ + ring_sub r z u = + ring_mul r u (ring_neg r + (ring_sub r (ring_1 r) (ring_mul r v z)))”), + ("RING_RULE_04", + “~(ring_mul r x y = ring_0 r) + ==> x IN ring_carrier r /\ y IN ring_carrier r + ==> ~(x = ring_0 r) /\ ~(y = ring_0 r)”), + ("RING_RULE_05", + “a IN ring_carrier r /\ b IN ring_carrier r /\ c IN ring_carrier r /\ + x IN ring_carrier r /\ y IN ring_carrier r /\ + ring_mul r a b = c + ==> ring_mul r (ring_mul r x y) c = + ring_mul r (ring_mul r x a) (ring_mul r y b)”), + ("RING_RULE_06", + “x IN ring_carrier r /\ y IN ring_carrier r /\ + (x = ring_0 r \/ y = ring_0 r) + ==> ring_mul r x y = ring_0 r”), + ("RING_RULE_07", + “(x IN ring_carrier r /\ y IN ring_carrier r) /\ + (x = ring_0 r \/ y = ring_0 r) + ==> ring_mul r x y = ring_0 r”), + ("RING_RULE_08", + “x IN ring_carrier r /\ y IN ring_carrier r + ==> x = ring_add r y (ring_sub r x y)”) + ]; diff --git a/src/integer/intReduce.sig b/src/integer/intReduce.sig index b4113074be..ca9a24ed25 100644 --- a/src/integer/intReduce.sig +++ b/src/integer/intReduce.sig @@ -19,6 +19,8 @@ sig val INT_GT_CONV : conv val INT_EQ_CONV : conv val INT_ADD_CONV : conv + val INT_SUB_CONV : conv + val INT_NEG_CONV : conv val INT_MUL_CONV : conv val INT_POW_CONV : conv diff --git a/src/integer/intReduce.sml b/src/integer/intReduce.sml index e7d3a8f4db..c4a5965cba 100644 --- a/src/integer/intReduce.sml +++ b/src/integer/intReduce.sml @@ -213,6 +213,15 @@ val (INT_LE_CONV,INT_LT_CONV,INT_GE_CONV,INT_GT_CONV,INT_EQ_CONV) = INT_GE_CONV,INT_GT_CONV,INT_EQ_CONV); end; +val INT_NEG_CONV = + let val pth = prove + (“(-(&0) = &0) /\ + (-(-(&x)) = &x)”, + REWRITE_TAC[INT_NEG_NEG, INT_NEG_0]) + in + GEN_REWRITE_CONV I empty_rewrites[pth] + end; + (*-----------------------------------------------------------------------*) (* INT_ADD_CONV "[x] + [y]" = |- [x] + [y] = [x+y] *) (*-----------------------------------------------------------------------*) @@ -313,6 +322,11 @@ val INT_ADD_CONV = handle HOL_ERR _ => failwith "INT_ADD_CONV") end (* local *) +val INT_SUB_CONV = + GEN_REWRITE_CONV I empty_rewrites[int_sub] THENC + TRY_CONV(RAND_CONV INT_NEG_CONV) THENC + INT_ADD_CONV; + (*-----------------------------------------------------------------------*) (* INT_MUL_CONV "[x] * [y]" = |- [x] * [y] = [x * y] *) (*-----------------------------------------------------------------------*) @@ -337,7 +351,8 @@ val INT_MUL_CONV = FIRST_CONV [GEN_REWRITE_CONV I empty_rewrites[pth0], GEN_REWRITE_CONV I empty_rewrites[pth1] THENC RAND_CONV NUM_MULT_CONV, - GEN_REWRITE_CONV I empty_rewrites[pth2] THENC RAND_CONV(RAND_CONV NUM_MULT_CONV)]; + GEN_REWRITE_CONV I empty_rewrites[pth2] THENC + RAND_CONV(RAND_CONV NUM_MULT_CONV)]; end; (*-----------------------------------------------------------------------*) diff --git a/src/integer/selftest.sml b/src/integer/selftest.sml index 3a63f783b8..91a36f7793 100644 --- a/src/integer/selftest.sml +++ b/src/integer/selftest.sml @@ -88,7 +88,11 @@ val _ = List.app (rule_test INTEGER_RULE) [ ("INTEGER_RULE_00", “w * y + x * z - (w * z + x * y) = (w - x) * (y - z:int)”), ("INTEGER_RULE_01", - “a int_divides &n <=> a int_divides -&n”) + “a int_divides &n <=> a int_divides -&n”), + ("INTEGER_RULE_02", + “d int_divides m ==> d int_divides (m * n:int) /\ d int_divides -(m * n)”), + ("INTEGER_RULE_03", + “d int_divides m ==> d int_divides (m * n:int)”) ]; val _ = Process.exit Process.success; diff --git a/src/lite/liteLib.sig b/src/lite/liteLib.sig index 68fb142913..0068c9f566 100644 --- a/src/lite/liteLib.sig +++ b/src/lite/liteLib.sig @@ -88,7 +88,6 @@ sig val eager: 'a -> ('b,'a) lazy; val eval : ('a,'b)lazy -> 'b; - (*--------------------------------------------------------------------* * Term operators * *--------------------------------------------------------------------*) @@ -154,15 +153,12 @@ sig val SIMPLE_DISJ_CASES : thm -> thm -> thm val SIMPLE_CHOOSE : term -> thm -> thm -(*--------------------------------------------------------------------* - * HOL-Light compatible type operators * - *--------------------------------------------------------------------*) - val bool_ty : hol_type val dest_fun_ty : hol_type -> hol_type * hol_type val mk_fun_ty : hol_type -> hol_type -> hol_type val setify_term : term list -> term list + val freesl : term list -> term list val ANTS_TAC : tactic end diff --git a/src/lite/liteLib.sml b/src/lite/liteLib.sml index e31153f1dd..508e3f586a 100644 --- a/src/lite/liteLib.sml +++ b/src/lite/liteLib.sml @@ -5,9 +5,9 @@ structure liteLib :> liteLib = struct -open Feedback Thm Conv Abbrev Tactic; +open HolKernel boolLib Parse; -val aconv = Term.aconv +infix 3 |> thenf orelsef; (*--------------------------------------------------------------------------- * Fake for NJSML: it does not use Interrupt anyway so it won't ever @@ -45,8 +45,6 @@ fun option_cases f e (SOME x) = f x fun option_app f (SOME x) = SOME (f x) | option_app f NONE = NONE - -infix 3 |> thenf orelsef; fun (x |> f) = f x; fun (f thenf g) x = g(f x); @@ -230,6 +228,8 @@ val is_imp = is_binop boolSyntax.implication; val dest_imp = dest_binop boolSyntax.implication; val strip_imp = splitlist dest_imp; +(* Moved here from Canon_Port *) +val freesl = free_varsl; (* ------------------------------------------------------------------------- *) (* Grabbing left operand of a binary operator (or something coextensive!) *) diff --git a/src/meson/src/Canon_Port.sml b/src/meson/src/Canon_Port.sml index 7bfb5f8890..0ec46178c2 100644 --- a/src/meson/src/Canon_Port.sml +++ b/src/meson/src/Canon_Port.sml @@ -18,8 +18,6 @@ val RIGHT_IMP_FORALL_THM = GSYM RIGHT_FORALL_IMP_THM; val LEFT_IMP_EXISTS_THM = boolTheory.LEFT_EXISTS_IMP_THM; val RIGHT_IMP_EXISTS_THM = GSYM RIGHT_EXISTS_IMP_THM; -val freesl = free_varsl - fun is_eqc tm = same_const equality tm local