(def-script set-equality-script 0
(
(label-node top)
(apply-macete-with-minor-premises tr%subseteq-antisymmetry)
direct-and-antecedent-inference-strategy
(jump-to-node top)
(for-nodes
(unsupported-descendents)
(block
insistent-direct-inference
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly))
))
(def-theorem gcd-for-zero
"forall(a:zz, 0<=a implies gcd(a,0)=a)"
(theory h-o-real-arithmetic)
(proof
(
(unfold-single-defined-constant (0) gcd)
simplify
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises iota-free-characterization-of-generator)
direct-and-antecedent-inference-strategy
set-equality-script
(block
(script-comment "`set-equality-script' at (0 0 0 0 0)")
direct-and-antecedent-inference-strategy
(unfold-single-defined-constant (0) princ%ideal)
(case-split ("a=0"))
(block
(script-comment "`case-split' at (1)")
simplify
(simplify-antecedent "with(a,r,x_$2:zz,x_$2=r*a);"))
(block
(script-comment "`case-split' at (2)")
simplify
(apply-macete-with-minor-premises divisibility-lemma)
auto-instantiate-existential))
(block
(script-comment "`set-equality-script' at (0 1 0 0 0)")
(unfold-single-defined-constant (0) princ%ideal)
(case-split ("a=0"))
simplify
(block
(script-comment "`case-split' at (2)")
simplify
(apply-macete-with-minor-premises divisibility-lemma)))
(unfold-single-defined-constant (0) princ%ideal)
)))
(def-theorem gcd-of-negative
"forall(u,v:zz, gcd(u,v)=gcd(-u,v))"
(theory h-o-real-arithmetic)
reverse
(proof
(
unfold-defined-constants
direct-and-antecedent-inference-strategy
(cut-with-single-formula
"indic{x:zz, forsome(r,s:zz,x=r*(-u)+s*v)}=
indic{x:zz, forsome(r,s:zz,x=r*u+s*v)}")
(block
(script-comment "`cut-with-single-formula' at (0)")
(backchain "with(p:prop,p);")
simplify
(apply-macete-with-minor-premises definedness-of-generator)
(force-substitution "v*s+u*r" "r*u+s*v" (0))
(move-to-sibling 1)
simplify
(apply-macete-with-minor-premises integer-combinations-form-an-ideal))
(block
(script-comment "`cut-with-single-formula' at (1)")
set-equality-script
(block
(script-comment "`set-equality-script' at (0 0 0 0 0)")
direct-and-antecedent-inference-strategy
(instantiate-existential ("-r" "s"))
(backchain "with(p:prop,p);")
(weaken (0))
simplify)
(block
(script-comment "`set-equality-script' at (0 1 0 0 0)")
direct-and-antecedent-inference-strategy
(instantiate-existential ("-r" "s"))
(backchain "with(r:rr,x_$1:zz,x_$1=r);")
(weaken (0))
simplify))
)))
(def-theorem invariance-of-gcd-special-case
"forall(u,v:zz, 0<v implies gcd(u,v)=gcd(mod(u,v),v))"
(theory h-o-real-arithmetic)
lemma
(proof
(
direct-and-antecedent-inference-strategy
(cut-with-single-formula "forsome(z:zz, u mod v = z)")
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,forsome(z:zz,p));")
(backchain "with(z:zz,r:rr,r=z);")
(incorporate-antecedent "with(z:zz,r:rr,r=z);")
(apply-macete-with-minor-premises mod-characterization)
(apply-macete-with-minor-premises divisibility-lemma)
direct-and-antecedent-inference-strategy
(cut-with-single-formula "z=u-k*v")
(move-to-sibling 1)
simplify
(block
(script-comment "`cut-with-single-formula' at (0)")
(backchain "with(r:rr,u,z:zz,z=u-r);")
(weaken (0 1 2 3))
(unfold-single-defined-constant-globally gcd)
(cut-with-single-formula "indic{x:zz, forsome(r,s:zz,x=r*u+s*v)}=indic{x:zz, forsome(r,s:zz,x=r*(u-k*v)+s*v)}")
(block
(script-comment "`cut-with-single-formula' at (0)")
(backchain-backwards "with(f:sets[zz],f=f);")
simplify
(apply-macete-with-minor-premises definedness-of-generator)
(force-substitution "v*s+u*r" "r*u+s*v" (0))
(move-to-sibling 1)
simplify
(apply-macete-with-minor-premises integer-combinations-form-an-ideal))
(block
(script-comment "`cut-with-single-formula' at (1)")
set-equality-script
(block
(script-comment "`set-equality-script' at (0 0 0 0 0)")
direct-and-antecedent-inference-strategy
(backchain "with(r:rr,x_$2:zz,x_$2=r);")
(weaken (0))
(instantiate-existential ("r" "r*k+s"))
simplify)
(block
(script-comment "`set-equality-script' at (0 1 0 0 0)")
direct-and-antecedent-inference-strategy
(backchain "with(r:rr,x_$1:zz,x_$1=r);")
(weaken (0 1))
(instantiate-existential ("r" "s-r*k"))
simplify))))
(block
(script-comment "`cut-with-single-formula' at (1)")
(instantiate-existential ("u mod v"))
(block
(script-comment "`instantiate-existential' at (0)")
simplify
(unfold-single-defined-constant (0) mod)
simplify)
(apply-macete-with-minor-premises mod-of-integer-is-integer))
)))
(def-theorem invariance-of-gcd
"forall(u,v:zz, not(v=0) implies gcd(u,v)=gcd(mod(u,v),v))"
(theory h-o-real-arithmetic)
reverse
(proof
(
direct-and-antecedent-inference-strategy
(case-split ("0<v"))
(instantiate-theorem invariance-of-gcd-special-case ("u" "v"))
(block
(script-comment "`case-split' at (2)")
(force-substitution "gcd(u mod v,v)" "gcd((-u) mod (-v),-v)" (0))
(move-to-sibling 1)
(block
(script-comment "`force-substitution' at (1)")
(apply-macete-with-minor-premises mod-of-negative)
(apply-macete-with-minor-premises rev%gcd-of-negative)
(apply-macete-with-minor-premises symmetry-of-gcd)
(apply-macete-with-minor-premises rev%gcd-of-negative)
(apply-macete-with-minor-premises mod-of-integer-is-integer)
direct-and-antecedent-inference-strategy)
(block
(script-comment "`force-substitution' at (0)")
(instantiate-theorem invariance-of-gcd-special-case ("-u" "-v"))
(simplify-antecedent "with(v:zz,not(0<-v));")
(block
(script-comment "`instantiate-theorem' at (0 1)")
(backchain-backwards "with(z:zz,z=z);")
(apply-macete-with-minor-premises rev%gcd-of-negative)
(apply-macete-with-minor-premises symmetry-of-gcd)
(apply-macete-with-minor-premises rev%gcd-of-negative)
simplify
(unfold-single-defined-constant (0) gcd)
(apply-macete-with-minor-premises definedness-of-generator)
(apply-macete-with-minor-premises integer-combinations-form-an-ideal))))
)))
(def-theorem gcd-of-multiple
"forall(a,m:zz, 0<m and m divides a implies gcd(a,m)=m)"
(theory h-o-real-arithmetic)
(proof
(
(unfold-single-defined-constant (0) gcd)
(apply-macete-with-minor-premises iota-free-characterization-of-generator)
(unfold-single-defined-constant (0) princ%ideal)
simplify
(apply-macete-with-minor-premises divisibility-lemma)
(block
(script-comment "`apply-macete-with-minor-premises' at (0)")
direct-and-antecedent-inference-strategy
(backchain "with(r:rr,a:zz,a=r);")
(weaken (0))
set-equality-script
(block
(script-comment "`set-equality-script' at (0 0 0 0 0)")
direct-and-antecedent-inference-strategy
(backchain "with(r:rr,x:zz,x=r);")
(weaken (0))
(instantiate-existential ("r*k+s"))
simplify)
(block
(script-comment "`set-equality-script' at (0 1 0 0 0)")
direct-and-antecedent-inference-strategy
(backchain "with(r:rr,x_$0:zz,x_$0=r);")
(weaken (0))
(instantiate-existential ("1" "(-k+k_$0)"))
simplify))
)))
(def-theorem gcd-is-gcd-of-absolute-value
"forall(u,v:zz, gcd(u,v)=gcd(abs(u),abs(v)))"
(theory h-o-real-arithmetic)
(proof
(
direct-and-antecedent-inference-strategy
(case-split ("0<=u" "0<=v"))
(block
(script-comment "`case-split' at (1)")
(apply-macete-with-minor-premises absolute-value-non-negative)
simplify
(unfold-single-defined-constant (0) gcd)
(apply-macete-with-minor-premises definedness-of-generator)
(apply-macete-with-minor-premises integer-combinations-form-an-ideal))
(block
(script-comment "`case-split' at (2)")
(apply-macete absolute-value-non-positive)
(apply-macete-with-minor-premises absolute-value-non-negative)
(apply-macete-with-minor-premises symmetry-of-gcd)
(apply-macete-with-minor-premises rev%gcd-of-negative)
simplify
(unfold-single-defined-constant (0) gcd)
(apply-macete-with-minor-premises definedness-of-generator)
(apply-macete-with-minor-premises integer-combinations-form-an-ideal))
(block
(script-comment "`case-split' at (3)")
(apply-macete absolute-value-non-positive)
(apply-macete-with-minor-premises absolute-value-non-negative)
(apply-macete-with-minor-premises rev%gcd-of-negative)
simplify
(unfold-single-defined-constant (0) gcd)
(apply-macete-with-minor-premises definedness-of-generator)
(apply-macete-with-minor-premises integer-combinations-form-an-ideal))
(block
(script-comment "`case-split' at (4)")
(apply-macete-with-minor-premises absolute-value-non-positive)
(apply-macete-with-minor-premises rev%gcd-of-negative)
(apply-macete-with-minor-premises symmetry-of-gcd)
(apply-macete-with-minor-premises rev%gcd-of-negative)
simplify
(unfold-single-defined-constant (0) gcd)
(apply-macete-with-minor-premises definedness-of-generator)
(apply-macete-with-minor-premises integer-combinations-form-an-ideal))
)))
(def-recursive-constant gcd_rho
"lambda(f:[zz,zz->zz],
lambda(u,v:zz, if(0<=v and 0<=u,if(u=0, v,v=0,u,f(v,mod(u,v))), ?zz)))"
(definition-name gcd_rho)
(theory h-o-real-arithmetic))
(def-theorem gcd_rho-defined-for-nonnegative-args
"forall(a,b:zz, 0<=a and 0<=b implies #(gcd_rho(a,b)))"
(theory h-o-real-arithmetic)
(proof
(
(cut-with-single-formula
"forall(b:zz, 0<=b implies forall(a:zz, 0<=a implies
#(gcd_rho(a,b))))")
(block
(script-comment "`cut-with-single-formula' at (0)")
direct-and-antecedent-inference-strategy
(backchain "with(p:prop,forall(b:zz,p));")
direct-and-antecedent-inference-strategy)
(block
(script-comment "`cut-with-single-formula' at (1)")
(induction complete-inductor ("b"))
(case-split ("a=0"))
simplify
(block
(script-comment "`case-split' at (2)")
simplify
(case-split ("m=0"))
simplify
(block
(script-comment "`case-split' at (2)")
simplify
beta-reduce-with-minor-premises
(move-to-sibling 1)
(apply-macete-with-minor-premises mod-of-integer-is-integer)
(block
(script-comment "`beta-reduce-with-minor-premises' at (0)")
(instantiate-theorem division-with-remainder
("m" "a"))
(simplify-antecedent "with(m:zz,not(0<m));")
(block
(script-comment "`instantiate-theorem' at (0 1 0)")
simplify
(case-split ("a mod m = 0"))
simplify
(block
(script-comment "`case-split' at (2)")
simplify
(backchain "with(p:prop,forall(k:zz,p));")
(block
(script-comment "`backchain' at (0)")
(instantiate-theorem division-with-remainder
("a mod m" "m"))
(simplify-antecedent "with(r:rr,not(0<r));")
(block
(script-comment "`instantiate-theorem' at (0 1 0)")
direct-and-antecedent-inference-strategy
simplify))
(apply-macete-with-minor-premises mod-of-integer-is-integer)))))))
)))
(def-theorem gcd_rho-is-gcd
"forall(x,y:zz, 0<=x and 0<=y implies gcd_rho(x,y)=gcd(x,y))"
(theory h-o-real-arithmetic)
(proof
(
direct-and-antecedent-inference-strategy
(instantiate-theorem gcd_rho-strong-minimality_h-o-real-arithmetic ("gcd"))
(block
(script-comment "`instantiate-theorem' at (0 0 0 0)")
(contrapose "with(p:prop,not(p));")
(case-split ("0<=u_1 and 0<=u_0"))
simplify
(case-split ("u_0=0"))
(block
(script-comment "`case-split' at (1)")
simplify
(apply-macete-with-minor-premises symmetry-of-gcd)
(apply-macete-with-minor-premises gcd-for-zero))
(block
(script-comment "`case-split' at (2)")
simplify
(case-split ("u_1=0"))
(block
(script-comment "`case-split' at (1)")
simplify
(apply-macete-with-minor-premises gcd-for-zero))
(block
(script-comment "`case-split' at (2)")
simplify
(apply-macete-with-minor-premises symmetry-of-gcd)
(apply-macete-with-minor-premises rev%invariance-of-gcd)
(apply-macete-locally symmetry-of-gcd (0) "gcd(u_0,u_1)")
simplify
(unfold-single-defined-constant (0) gcd)
(apply-macete-with-minor-premises definedness-of-generator)
(apply-macete-with-minor-premises integer-combinations-form-an-ideal))))
(block
(script-comment "`instantiate-theorem' at (0 1)")
(backchain "with(p:prop,forall(u_0,u_1:zz,p));")
(apply-macete-with-minor-premises gcd_rho-defined-for-nonnegative-args)
direct-and-antecedent-inference-strategy)
)))
(def-recursive-constant gcd_ma
"lambda(f:[int,int->int],
lambda(u,v:int, if(0<=v and 0<=u,if(u=0, v,v=0,u,f(v,mod_ma(u,v))), abs_ma(0))))"
(definition-name gcd_ma)
(theory machine-arithmetic))
(def-theorem gcd_ma-restricts-gcd
"forall(a,b:int, 0<=a and 0<=b implies gcd_ma(a,b)=gcd(a,b))"
(theory machine-arithmetic)
(proof
(
(cut-with-single-formula
"forall(b:zz, 0<=b and b<=maxint
implies
forall(a:zz, 0<=a and a<=maxint implies gcd_ma(a,b)=gcd(a,b)))")
(block
(script-comment "`cut-with-single-formula' at (0)")
direct-and-antecedent-inference-strategy
(backchain "with(p:prop,forall(b:zz,p));")
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 1)")
(cut-with-single-formula "#(b,int)")
(incorporate-antecedent "with(b:int,#(b,int));")
(apply-macete-with-minor-premises int-defining-axiom_machine-arithmetic)
beta-reduce-repeatedly
direct-and-antecedent-inference-strategy)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1 1 0)")
(cut-with-single-formula "#(a,int)")
(incorporate-antecedent "with(a:int,#(a,int));")
(apply-macete-with-minor-premises int-defining-axiom_machine-arithmetic)
beta-reduce-repeatedly
direct-and-antecedent-inference-strategy))
(block
(script-comment "`cut-with-single-formula' at (1)")
(induction complete-inductor ("b"))
(case-split ("a=0"))
(block
(script-comment "`case-split' at (1)")
simplify
(apply-macete-with-minor-premises symmetry-of-gcd)
(apply-macete-with-minor-premises gcd-for-zero))
(block
(script-comment "`case-split' at (2)")
simplify
(case-split ("m=0"))
(block
(script-comment "`case-split' at (1)")
simplify
(apply-macete-with-minor-premises gcd-for-zero))
(block
(script-comment "`case-split' at (2)")
simplify
beta-reduce-with-minor-premises
(move-to-sibling 1)
(block
(script-comment "`beta-reduce-with-minor-premises' at (1)")
(unfold-single-defined-constant (0) mod_ma)
(cut-with-single-formula "#(a mod m ,zz)")
(apply-macete-with-minor-premises mod-of-integer-is-integer))
(block
(script-comment "`beta-reduce-with-minor-premises' at (0)")
(unfold-single-defined-constant-globally mod_ma)
(instantiate-theorem division-with-remainder
("m" "a"))
(simplify-antecedent "with(m:zz,not(0<m));")
(block
(script-comment "`instantiate-theorem' at (0 1 0)")
simplify
(case-split ("a mod m = 0"))
(block
(script-comment "`case-split' at (1)")
simplify
(contrapose "with(r:rr,r=0);")
(apply-macete-with-minor-premises mod-characterization)
simplify
(contrapose "with(a,m:zz,not(m=gcd(a,m)));")
(apply-macete-with-minor-premises gcd-of-multiple))
(block
(script-comment "`case-split' at (2)")
simplify
(backchain "with(p:prop,forall(k:zz,p));")
(move-to-sibling 1)
(apply-macete-with-minor-premises mod-of-integer-is-integer)
(block
(script-comment "`backchain' at (0)")
(instantiate-theorem division-with-remainder
("a mod m" "m"))
(simplify-antecedent "with(r:rr,not(0<r));")
(block
(script-comment "`instantiate-theorem' at (0 1 0)")
direct-and-antecedent-inference-strategy
simplify
simplify
(block
(script-comment
"`direct-and-antecedent-inference-strategy' at (1 1 1 0 0)")
(apply-macete-with-minor-premises symmetry-of-gcd)
(block
(script-comment "`apply-macete-with-minor-premises' at (0)")
(apply-macete-with-minor-premises rev%invariance-of-gcd)
(apply-macete-with-minor-premises symmetry-of-gcd)
(apply-macete-with-minor-premises rev%invariance-of-gcd)
simplify
(unfold-single-defined-constant (0) gcd)
(apply-macete-with-minor-premises definedness-of-generator)
(apply-macete-with-minor-premises
integer-combinations-form-an-ideal))
(apply-macete-with-minor-premises mod-of-integer-is-integer))))))))))
)
))