(* Title: CTT/CTT.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
*)
theory CTT
imports Pure
begin
section ‹Constructive Type
Theory: axiomatic basis
›
ML_file
‹~~/src/Provers/typedsimp.ML
›
setup Pure_Thy.old_appl_syntax_setup
typedecl i
typedecl t
typedecl o
consts
🍋 ‹Judgments
›
Type ::
"t \ prop" (
‹(
‹notation=
‹postfix Type
››_ type)
› [10] 5)
Eqtype ::
"[t,t]\prop" (
‹(
‹notation=
‹infix Eqtype
››_ =/ _)
› [10,10] 5)
Elem ::
"[i, t]\prop" (
‹(
‹notation=
‹infix Elem
››_ /: _)
› [10,10] 5)
Eqelem ::
"[i,i,t]\prop" (
‹(
‹notation=
‹mixfix Eqelem
››_ =/ _ :/ _)
› [10,10,10] 5)
Reduce ::
"[i,i]\prop" (
‹Reduce[_,_]
›)
🍋 ‹Types for truth values
›
F ::
"t"
T ::
"t" 🍋 ‹‹F
› is empty,
‹T
› contains one element
›
contr ::
"i\i"
tt ::
"i"
🍋 ‹Natural numbers
›
N ::
"t"
Zero ::
"i" (
‹0
›)
succ ::
"i\i"
rec ::
"[i, i, [i,i]\i] \ i"
🍋 ‹Binary sum
›
Plus ::
"[t,t]\t" (
infixr ‹+
› 40)
inl ::
"i\i"
inr ::
"i\i"
"when" ::
"[i, i\i, i\i]\i"
🍋 ‹General sum
and binary product
›
Sum ::
"[t, i\t]\t"
pair ::
"[i,i]\i" (
‹(
‹indent=1
notation=
‹mixfix pair
››<_,/_>)
›)
fst ::
"i\i"
snd ::
"i\i"
split ::
"[i, [i,i]\i] \i"
🍋 ‹General product
and function space
›
Prod ::
"[t, i\t]\t"
lambda ::
"(i \ i) \ i" (
binder ‹🚫λ
› 10)
app ::
"[i,i]\i" (
infixl ‹`
› 60)
🍋 ‹Equality type
›
Eq ::
"[t,i,i]\t"
eq ::
"i"
text ‹Some inexplicable syntactic dependencies;
in particular,
"0"
must be introduced after the
judgment forms.
›
syntax
"_PROD" ::
"[idt,t,t]\t" (
‹(
‹indent=3
notation=
‹binder ∏››∏_:_./ _)
› 10)
"_SUM" ::
"[idt,t,t]\t" (
‹(
‹indent=3
notation=
‹binder ∑››∑_:_./ _)
› 10)
syntax_consts
"_PROD" ⇌ Prod
and
"_SUM" ⇌ Sum
translations
"\x:A. B" ⇌ "CONST Prod(A, \x. B)"
"\x:A. B" ⇌ "CONST Sum(A, \x. B)"
abbreviation Arrow ::
"[t,t]\t" (
infixr ‹⟶› 30)
where "A \ B \ \_:A. B"
abbreviation Times ::
"[t,t]\t" (
infixr ‹×› 50)
where "A \ B \ \_:A. B"
text ‹
Reduction: a weaker notion than equality; a hack
for simplification.
‹Reduce[a,b]
› means either that
‹a = b : A
› for some
‹A
› or else
that
‹a
› and ‹b
› are textually identical.
Does not verify
‹a:A
›! Sound because only
‹trans_red
› uses a
‹Reduce
›
premise. No new
theorems can be proved about the standard judgments.
›
axiomatization
where
refl_red:
"\a. Reduce[a,a]" and
red_if_equal:
"\a b A. a = b : A \ Reduce[a,b]" and
trans_red:
"\a b c A. \a = b : A; Reduce[b,c]\ \ a = c : A" and
🍋 ‹Reflexivity
›
refl_type:
"\A. A type \ A = A" and
refl_elem:
"\a A. a : A \ a = a : A" and
🍋 ‹Symmetry
›
sym_type:
"\A B. A = B \ B = A" and
sym_elem:
"\a b A. a = b : A \ b = a : A" and
🍋 ‹Transitivity
›
trans_type:
"\A B C. \A = B; B = C\ \ A = C" and
trans_elem:
"\a b c A. \a = b : A; b = c : A\ \ a = c : A" and
equal_types:
"\a A B. \a : A; A = B\ \ a : B" and
equal_typesL:
"\a b A B. \a = b : A; A = B\ \ a = b : B" and
🍋 ‹Substitution
›
subst_type:
"\a A B. \a : A; \z. z:A \ B(z) type\ \ B(a) type" and
subst_typeL:
"\a c A B D. \a = c : A; \z. z:A \ B(z) = D(z)\ \ B(a) = D(c)" and
subst_elem:
"\a b A B. \a : A; \z. z:A \ b(z):B(z)\ \ b(a):B(a)" and
subst_elemL:
"\a b c d A B. \a = c : A; \z. z:A \ b(z)=d(z) : B(z)\ \ b(a)=d(c) : B(a)" and
🍋 ‹The type
‹N
› -- natural numbers
›
NF:
"N type" and
NI0:
"0 : N" and
NI_succ:
"\a. a : N \ succ(a) : N" and
NI_succL:
"\a b. a = b : N \ succ(a) = succ(b) : N" and
NE:
"\p a b C. \p: N; a: C(0); \u v. \u: N; v: C(u)\ \ b(u,v): C(succ(u))\
==> rec(p, a, λu v. b(u,v)) : C(p)
" and
NEL:
"\p q a b c d C. \p = q : N; a = c : C(0);
∧u v.
[u: N; v: C(u)
] ==> b(u,v) = d(u,v): C(succ(u))
]
==> rec(p, a, λu v. b(u,v)) = rec(q,c,d) : C(p)
" and
NC0:
"\a b C. \a: C(0); \u v. \u: N; v: C(u)\ \ b(u,v): C(succ(u))\
==> rec(0, a, λu v. b(u,v)) = a : C(0)
" and
NC_succ:
"\p a b C. \p: N; a: C(0); \u v. \u: N; v: C(u)\ \ b(u,v): C(succ(u))\ \
rec(succ(p), a, λu v. b(u,v)) = b(p, rec(p, a, λu v. b(u,v))) : C(succ(p))
" and
🍋 ‹The fourth Peano axiom. See page 91 of Martin-Löf
's book.\
zero_ne_succ:
"\a. \a: N; 0 = succ(a) : N\ \ 0: F" and
🍋 ‹The Product of a family of
types›
ProdF:
"\A B. \A type; \x. x:A \ B(x) type\ \ \x:A. B(x) type" and
ProdFL:
"\A B C D. \A = C; \x. x:A \ B(x) = D(x)\ \ \x:A. B(x) = \x:C. D(x)" and
ProdI:
"\b A B. \A type; \x. x:A \ b(x):B(x)\ \ \<^bold>\x. b(x) : \x:A. B(x)" and
ProdIL:
"\b c A B. \A type; \x. x:A \ b(x) = c(x) : B(x)\ \
🚫λx. b(x) =
🚫λx. c(x) :
∏x:A. B(x)
" and
ProdE:
"\p a A B. \p : \x:A. B(x); a : A\ \ p`a : B(a)" and
ProdEL:
"\p q a b A B. \p = q: \x:A. B(x); a = b : A\ \ p`a = q`b : B(a)" and
ProdC:
"\a b A B. \a : A; \x. x:A \ b(x) : B(x)\ \ (\<^bold>\x. b(x)) ` a = b(a) : B(a)" and
ProdC2:
"\p A B. p : \x:A. B(x) \ (\<^bold>\x. p`x) = p : \x:A. B(x)" and
🍋 ‹The Sum of a family of
types›
SumF:
"\A B. \A type; \x. x:A \ B(x) type\ \ \x:A. B(x) type" and
SumFL:
"\A B C D. \A = C; \x. x:A \ B(x) = D(x)\ \ \x:A. B(x) = \x:C. D(x)" and
SumI:
"\a b A B. \a : A; b : B(a)\ \ : \x:A. B(x)" and
SumIL:
"\a b c d A B. \ a = c : A; b = d : B(a)\ \ = : \x:A. B(x)" and
SumE:
"\p c A B C. \p: \x:A. B(x); \x y. \x:A; y:B(x)\ \ c(x,y): C()\
==> split(p, λx y. c(x,y)) : C(p)
" and
SumEL:
"\p q c d A B C. \p = q : \x:A. B(x);
∧x y.
[x:A; y:B(x)
] ==> c(x,y)=d(x,y): C(<x,y>)
]
==> split(p, λx y. c(x,y)) = split(q, λx y. d(x,y)) : C(p)
" and
SumC:
"\a b c A B C. \a: A; b: B(a); \x y. \x:A; y:B(x)\ \ c(x,y): C()\
==> split(<a,b>, λx y. c(x,y)) = c(a,b) : C(<a,b>)
" and
fst_def:
"\a. fst(a) \ split(a, \x y. x)" and
snd_def:
"\a. snd(a) \ split(a, \x y. y)" and
🍋 ‹The sum of two
types›
PlusF:
"\A B. \A type; B type\ \ A+B type" and
PlusFL:
"\A B C D. \A = C; B = D\ \ A+B = C+D" and
PlusI_inl:
"\a A B. \a : A; B type\ \ inl(a) : A+B" and
PlusI_inlL:
"\a c A B. \a = c : A; B type\ \ inl(a) = inl(c) : A+B" and
PlusI_inr:
"\b A B. \A type; b : B\ \ inr(b) : A+B" and
PlusI_inrL:
"\b d A B. \A type; b = d : B\ \ inr(b) = inr(d) : A+B" and
PlusE:
"\p c d A B C. \p: A+B;
∧x. x:A
==> c(x): C(inl(x));
∧y. y:B
==> d(y): C(inr(y))
] ==> when(p, λx. c(x), λy. d(y)) : C(p)
" and
PlusEL:
"\p q c d e f A B C. \p = q : A+B;
∧x. x: A
==> c(x) = e(x) : C(inl(x));
∧y. y: B
==> d(y) = f(y) : C(inr(y))
]
==> when(p, λx. c(x), λy. d(y)) = when(q, λx. e(x), λy. f(y)) : C(p)
" and
PlusC_inl:
"\a c d A B C. \a: A;
∧x. x:A
==> c(x): C(inl(x));
∧y. y:B
==> d(y): C(inr(y))
]
==> when(inl(a), λx. c(x), λy. d(y)) = c(a) : C(inl(a))
" and
PlusC_inr:
"\b c d A B C. \b: B;
∧x. x:A
==> c(x): C(inl(x));
∧y. y:B
==> d(y): C(inr(y))
]
==> when(inr(b), λx. c(x), λy. d(y)) = d(b) : C(inr(b))
" and
🍋 ‹The type
‹Eq
››
EqF:
"\a b A. \A type; a : A; b : A\ \ Eq(A,a,b) type" and
EqFL:
"\a b c d A B. \A = B; a = c : A; b = d : A\ \ Eq(A,a,b) = Eq(B,c,d)" and
EqI:
"\a b A. a = b : A \ eq : Eq(A,a,b)" and
EqE:
"\p a b A. p : Eq(A,a,b) \ a = b : A" and
🍋 ‹By equality of
types, can prove
‹C(p)
› from ‹C(eq)
›, an elimination rule
›
EqC:
"\p a b A. p : Eq(A,a,b) \ p = eq : Eq(A,a,b)" and
🍋 ‹The type
‹F
››
FF:
"F type" and
FE:
"\p C. \p: F; C type\ \ contr(p) : C" and
FEL:
"\p q C. \p = q : F; C type\ \ contr(p) = contr(q) : C" and
🍋 ‹The type T
›
🍋 ‹Martin-Löf
's book (page 68) discusses elimination and computation.
Elimination can be derived
by computation
and equality of
types,
but
with an extra premise
‹C(x)
› type
‹x:T
›.
Also computation can be derived
from elimination.
›
TF:
"T type" and
TI:
"tt : T" and
TE:
"\p c C. \p : T; c : C(tt)\ \ c : C(p)" and
TEL:
"\p q c d C. \p = q : T; c = d : C(tt)\ \ c = d : C(p)" and
TC:
"\p. p : T \ p = tt : T"
subsection "Tactics and derived rules for Constructive Type Theory"
text ‹Formation rules.
›
lemmas form_rls = NF ProdF SumF PlusF EqF FF TF
and formL_rls = ProdFL SumFL PlusFL EqFL
text ‹
Introduction rules. OMITTED:
🚫 ‹EqI
›, because its premise
is an
‹eqelem
›, not an
‹elem
›.
›
lemmas intr_rls = NI0 NI_succ ProdI SumI PlusI_inl PlusI_inr TI
and intrL_rls = NI_succL ProdIL SumIL PlusI_inlL PlusI_inrL
text ‹
Elimination rules. OMITTED:
🚫 ‹EqE
›, because its conclusion
is an
‹eqelem
›, not an
‹elem
›
🚫 ‹TE
›, because it does not involve a constructor.
›
lemmas elim_rls = NE ProdE SumE PlusE FE
and elimL_rls = NEL ProdEL SumEL PlusEL FEL
text ‹OMITTED:
‹eqC
› are
‹TC
› because they make rewriting loop:
‹p = un = un =
…››
lemmas comp_rls = NC0 NC_succ ProdC SumC PlusC_inl PlusC_inr
text ‹Rules
with conclusion
‹a:A
›, an elem
judgment.
›
lemmas element_rls = intr_rls elim_rls
text ‹Definitions are (meta)equality
axioms.
›
lemmas basic_defs = fst_def snd_def
text ‹Compare
with standard version:
‹B
› is applied
to UNSIMPLIFIED expression!
›
lemma SumIL2:
"\c = a : A; d = b : B(a)\ \ = : Sum(A,B)"
by (rule sym_elem) (rule SumIL; rule sym_elem)
lemmas intrL2_rls = NI_succL ProdIL SumIL2 PlusI_inlL PlusI_inrL
text ‹
Exploit
‹p:Prod(A,B)
› to create the assumption
‹z:B(a)
›.
A more natural form of product elimination.
›
lemma subst_prodE:
assumes "p: Prod(A,B)"
and "a: A"
and "\z. z: B(a) \ c(z): C(z)"
shows "c(p`a): C(p`a)"
by (rule assms ProdE)+
subsection ‹Tactics
for type checking
›
ML
‹
local
fun is_rigid_elem
🍋‹Elem
for a _
› = not(is_Var (head_of a))
| is_rigid_elem
🍋‹Eqelem
for a _ _
› = not(is_Var (head_of a))
| is_rigid_elem
🍋‹Type
for a
› = not(is_Var (head_of a))
| is_rigid_elem _ = false
in
(*Try solving a:A or a=b:A by assumption provided a is rigid!*)
fun test_assume_tac ctxt = SUBGOAL (fn (prem, i) =>
if is_rigid_elem (Logic.strip_assums_concl prem)
then assume_tac ctxt i else no_tac)
fun ASSUME ctxt tf i = test_assume_tac ctxt i ORELSE tf i
end
›
text ‹
For simplification: type formation
and checking,
but no equalities between terms.
›
lemmas routine_rls = form_rls formL_rls refl_type element_rls
ML
‹
fun routine_tac rls ctxt prems =
ASSUME ctxt (Bires.filt_resolve_from_net_tac ctxt 4 (Bires.build_net (prems @ rls)));
(*Solve all subgoals "A type" using formation rules. *)
val form_net = Bires.build_net @{thms form_rls};
fun form_tac ctxt =
REPEAT_FIRST (
ASSUME ctxt (Bires.filt_resolve_from_net_tac ctxt 1 form_net));
(*Type checking: solve a:A (a rigid, A flexible) by intro and elim rules. *)
fun typechk_tac ctxt thms =
let val tac =
Bires.filt_resolve_from_net_tac ctxt 3
(Bires.build_net (thms @ @{thms form_rls} @ @{thms element_rls}))
in REPEAT_FIRST (
ASSUME ctxt tac)
end
(*Solve a:A (a flexible, A rigid) by introduction rules.
Cannot use stringtrees (filt_resolve_tac) since
goals like ?a:SUM(A,B) have a trivial head-string *)
fun intr_tac ctxt thms =
let val tac =
Bires.filt_resolve_from_net_tac ctxt 1
(Bires.build_net (thms @ @{thms form_rls} @ @{thms intr_rls}))
in REPEAT_FIRST (
ASSUME ctxt tac)
end
(*Equality proving: solve a=b:A (where a is rigid) by long rules. *)
fun equal_tac ctxt thms =
REPEAT_FIRST
(
ASSUME ctxt
(Bires.filt_resolve_from_net_tac ctxt 3
(Bires.build_net (thms @ @{thms form_rls element_rls intrL_rls elimL_rls refl_elem}))))
›
method_setup form =
‹Scan.succeed (fn ctxt => SIMPLE_METHOD (form_tac ctxt))
›
method_setup typechk =
‹Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (typechk_tac ctxt ths))
›
method_setup intr =
‹Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (intr_tac ctxt ths))
›
method_setup equal =
‹Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (equal_tac ctxt ths))
›
subsection ‹Simplification
›
text ‹To simplify the type
in a goal.
›
lemma replace_type:
"\B = A; a : A\ \ a : B"
apply (rule equal_types)
apply (rule_tac [2] sym_type)
apply assumption+
done
text ‹Simplify the parameter of a unary type operator.
›
lemma subst_eqtyparg:
assumes 1:
"a=c : A"
and 2:
"\z. z:A \ B(z) type"
shows "B(a) = B(c)"
apply (rule subst_typeL)
apply (rule_tac [2] refl_type)
apply (rule 1)
apply (erule 2)
done
text ‹Simplification rules
for Constructive Type
Theory.
›
lemmas reduction_rls = comp_rls [
THEN trans_elem]
ML
‹
(*Converts each goal "e : Eq(A,a,b)" into "a=b:A" for simplification.
Uses other intro rules to avoid changing flexible goals.*)
val eqintr_net = Bires.build_net @{thms EqI intr_rls}
fun eqintr_tac ctxt =
REPEAT_FIRST (
ASSUME ctxt (Bires.filt_resolve_from_net_tac ctxt 1 eqintr_net))
(** Tactics that instantiate CTT-rules.
Vars in the given terms will be incremented!
The (rtac EqE i) lets them apply to equality judgments. **)
fun NE_tac ctxt sp i =
TRY (resolve_tac ctxt @{thms EqE} i)
THEN
Rule_Insts.res_inst_tac ctxt [(((
"p", 0), Position.none), sp)] [] @{
thm NE} i
fun SumE_tac ctxt sp i =
TRY (resolve_tac ctxt @{thms EqE} i)
THEN
Rule_Insts.res_inst_tac ctxt [(((
"p", 0), Position.none), sp)] [] @{
thm SumE} i
fun PlusE_tac ctxt sp i =
TRY (resolve_tac ctxt @{thms EqE} i)
THEN
Rule_Insts.res_inst_tac ctxt [(((
"p", 0), Position.none), sp)] [] @{
thm PlusE} i
(** Predicate logic reasoning, WITH THINNING!! Procedures adapted from NJ. **)
(*Finds f:Prod(A,B) and a:A in the assumptions, concludes there is z:B(a) *)
fun add_mp_tac ctxt i =
resolve_tac ctxt @{thms subst_prodE} i
THEN assume_tac ctxt i
THEN assume_tac ctxt i
(*Finds P\<longrightarrow>Q and P in the assumptions, replaces implication by Q *)
fun mp_tac ctxt i = eresolve_tac ctxt @{thms subst_prodE} i
THEN assume_tac ctxt i
(*"safe" when regarded as predicate calculus rules*)
val safe_brls = sort Bires.subgoals_ord
[ (true, @{
thm FE}), (true,asm_rl),
(false, @{
thm ProdI}), (true, @{
thm SumE}), (true, @{
thm PlusE}) ]
val unsafe_brls =
[ (false, @{
thm PlusI_inl}), (false, @{
thm PlusI_inr}), (false, @{
thm SumI}),
(true, @{
thm subst_prodE}) ]
(*0 subgoals vs 1 or more*)
val (safe0_brls, safep_brls) =
List.partition Bires.no_subgoals safe_brls
fun safestep_tac ctxt thms i =
form_tac ctxt ORELSE
resolve_tac ctxt thms i ORELSE
biresolve_tac ctxt safe0_brls i ORELSE mp_tac ctxt i ORELSE
DETERM (biresolve_tac ctxt safep_brls i)
fun safe_tac ctxt thms i = DEPTH_SOLVE_1 (safestep_tac ctxt thms i)
fun step_tac ctxt thms = safestep_tac ctxt thms ORELSE
' biresolve_tac ctxt unsafe_brls
(*Fails unless it solves the goal!*)
fun pc_tac ctxt thms = DEPTH_SOLVE_1 o (step_tac ctxt thms)
›
method_setup eqintr =
‹Scan.succeed (SIMPLE_METHOD o eqintr_tac)
›
method_setup NE =
‹
Scan.lift Parse.embedded_inner_syntax >> (fn s => fn ctxt => SIMPLE_METHOD
' (NE_tac ctxt s))
›
method_setup pc =
‹Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD
' (pc_tac ctxt ths))\
method_setup add_mp =
‹Scan.succeed (SIMPLE_METHOD
' o add_mp_tac)\
ML_file
‹rew.ML
›
method_setup rew =
‹Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (rew_tac ctxt ths))
›
method_setup hyp_rew =
‹Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (hyp_rew_tac ctxt ths))
›
subsection ‹The elimination rules
for fst/snd
›
lemma SumE_fst:
"p : Sum(A,B) \ fst(p) : A"
unfolding basic_defs
apply (erule SumE)
apply assumption
done
text ‹The first premise must be
‹p:Sum(A,B)
›!!.
›
lemma SumE_snd:
assumes major:
"p: Sum(A,B)"
and "A type"
and "\x. x:A \ B(x) type"
shows "snd(p) : B(fst(p))"
unfolding basic_defs
apply (rule major [
THEN SumE])
apply (rule SumC [
THEN subst_eqtyparg,
THEN replace_type])
apply (typechk assms)
done
section ‹The two-element type (booleans
and conditionals)
›
definition Bool ::
"t"
where "Bool \ T+T"
definition true ::
"i"
where "true \ inl(tt)"
definition false ::
"i"
where "false \ inr(tt)"
definition cond ::
"[i,i,i]\i"
where "cond(a,b,c) \ when(a, \_. b, \_. c)"
lemmas bool_defs = Bool_def true_def false_def cond_def
subsection ‹Derivation of rules
for the type
‹Bool
››
text ‹Formation rule.
›
lemma boolF:
"Bool type"
unfolding bool_defs
by typechk
text ‹Introduction rules
for ‹true
›,
‹false
›.
›
lemma boolI_true:
"true : Bool"
unfolding bool_defs
by typechk
lemma boolI_false:
"false : Bool"
unfolding bool_defs
by typechk
text ‹Elimination rule: typing of
‹cond
›.
›
lemma boolE:
"\p:Bool; a : C(true); b : C(false)\ \ cond(p,a,b) : C(p)"
unfolding bool_defs
apply (typechk; erule TE)
apply typechk
done
lemma boolEL:
"\p = q : Bool; a = c : C(true); b = d : C(false)\
==> cond(p,a,b) = cond(q,c,d) : C(p)
"
unfolding bool_defs
apply (rule PlusEL)
apply (erule asm_rl refl_elem [
THEN TEL])+
done
text ‹Computation rules
for ‹true
›,
‹false
›.
›
lemma boolC_true:
"\a : C(true); b : C(false)\ \ cond(true,a,b) = a : C(true)"
unfolding bool_defs
apply (rule comp_rls)
apply typechk
apply (erule_tac [!] TE)
apply typechk
done
lemma boolC_false:
"\a : C(true); b : C(false)\ \ cond(false,a,b) = b : C(false)"
unfolding bool_defs
apply (rule comp_rls)
apply typechk
apply (erule_tac [!] TE)
apply typechk
done
section ‹Elementary arithmetic
›
subsection ‹Arithmetic operators
and their definitions
›
definition add ::
"[i,i]\i" (
infixr ‹#+
› 65)
where "a#+b \ rec(a, b, \u v. succ(v))"
definition diff ::
"[i,i]\i" (
infixr ‹-
› 65)
where "a-b \ rec(b, a, \u v. rec(v, 0, \x y. x))"
definition absdiff ::
"[i,i]\i" (
infixr ‹|-|
› 65)
where "a|-|b \ (a-b) #+ (b-a)"
definition mult ::
"[i,i]\i" (
infixr ‹#*
› 70)
where "a#*b \ rec(a, 0, \u v. b #+ v)"
definition mod ::
"[i,i]\i" (
infixr ‹mod
› 70)
where "a mod b \ rec(a, 0, \u v. rec(succ(v) |-| b, 0, \x y. succ(v)))"
definition div ::
"[i,i]\i" (
infixr ‹div
› 70)
where "a div b \ rec(a, 0, \u v. rec(succ(u) mod b, succ(v), \x y. v))"
lemmas arith_defs = add_def diff_def absdiff_def mult_def mod_def div_def
subsection ‹Proofs about elementary arithmetic: addition, multiplication, etc.
›
subsubsection
‹Addition
›
text ‹Typing of
‹add
›: short
and long versions.
›
lemma add_typing:
"\a:N; b:N\ \ a #+ b : N"
unfolding arith_defs
by typechk
lemma add_typingL:
"\a = c:N; b = d:N\ \ a #+ b = c #+ d : N"
unfolding arith_defs
by equal
text ‹Computation
for ‹add
›: 0
and successor cases.
›
lemma addC0:
"b:N \ 0 #+ b = b : N"
unfolding arith_defs
by rew
lemma addC_succ:
"\a:N; b:N\ \ succ(a) #+ b = succ(a #+ b) : N"
unfolding arith_defs
by rew
subsubsection
‹Multiplication
›
text ‹Typing of
‹mult
›: short
and long versions.
›
lemma mult_typing:
"\a:N; b:N\ \ a #* b : N"
unfolding arith_defs
by (typechk add_typing)
lemma mult_typingL:
"\a = c:N; b = d:N\ \ a #* b = c #* d : N"
unfolding arith_defs
by (equal add_typingL)
text ‹Computation
for ‹mult
›: 0
and successor cases.
›
lemma multC0:
"b:N \ 0 #* b = 0 : N"
unfolding arith_defs
by rew
lemma multC_succ:
"\a:N; b:N\ \ succ(a) #* b = b #+ (a #* b) : N"
unfolding arith_defs
by rew
subsubsection
‹Difference
›
text ‹Typing of difference.
›
lemma diff_typing:
"\a:N; b:N\ \ a - b : N"
unfolding arith_defs
by typechk
lemma diff_typingL:
"\a = c:N; b = d:N\ \ a - b = c - d : N"
unfolding arith_defs
by equal
text ‹Computation
for difference: 0
and successor cases.
›
lemma diffC0:
"a:N \ a - 0 = a : N"
unfolding arith_defs
by rew
text ‹Note:
‹rec(a, 0, λz w.z)
› is ‹pred(a).
››
lemma diff_0_eq_0:
"b:N \ 0 - b = 0 : N"
unfolding arith_defs
by (NE b) hyp_rew
text ‹
Essential
to simplify FIRST!! (Else we get a critical pair)
‹succ(a) - succ(b)
› rewrites
to ‹pred(succ(a) - b)
›.
›
lemma diff_succ_succ:
"\a:N; b:N\ \ succ(a) - succ(b) = a - b : N"
unfolding arith_defs
apply hyp_rew
apply (NE b)
apply hyp_rew
done
subsection ‹Simplification
›
lemmas arith_typing_rls = add_typing mult_typing diff_typing
and arith_congr_rls = add_typingL mult_typingL diff_typingL
lemmas congr_rls = arith_congr_rls intrL2_rls elimL_rls
lemmas arithC_rls =
addC0 addC_succ
multC0 multC_succ
diffC0 diff_0_eq_0 diff_succ_succ
ML
‹
structure Arith_simp = TSimpFun(
val refl = @{
thm refl_elem}
val sym = @{
thm sym_elem}
val trans = @{
thm trans_elem}
val refl_red = @{
thm refl_red}
val trans_red = @{
thm trans_red}
val red_if_equal = @{
thm red_if_equal}
val default_rls = @{thms arithC_rls comp_rls}
val routine_tac = routine_tac @{thms arith_typing_rls routine_rls}
)
fun arith_rew_tac ctxt prems =
make_rew_tac ctxt (Arith_simp.norm_tac ctxt (@{thms congr_rls}, prems))
fun hyp_arith_rew_tac ctxt prems =
make_rew_tac ctxt
(Arith_simp.cond_norm_tac ctxt (prove_cond_tac ctxt, @{thms congr_rls}, prems))
›
method_setup arith_rew =
‹
Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (arith_rew_tac ctxt ths))
›
method_setup hyp_arith_rew =
‹
Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (hyp_arith_rew_tac ctxt ths))
›
subsection ‹Addition
›
text ‹Associative law
for addition.
›
lemma add_assoc:
"\a:N; b:N; c:N\ \ (a #+ b) #+ c = a #+ (b #+ c) : N"
by (NE a) hyp_arith_rew
text ‹Commutative law
for addition. Can be proved
using three inductions.
Must simplify after first
induction! Orientation of rewrites
is delicate.
›
lemma add_commute:
"\a:N; b:N\ \ a #+ b = b #+ a : N"
apply (NE a)
apply hyp_arith_rew
apply (rule sym_elem)
prefer 2
apply (NE b)
prefer 4
apply (NE b)
apply hyp_arith_rew
done
subsection ‹Multiplication
›
text ‹Right annihilation
in product.
›
lemma mult_0_right:
"a:N \ a #* 0 = 0 : N"
apply (NE a)
apply hyp_arith_rew
done
text ‹Right successor law
for multiplication.
›
lemma mult_succ_right:
"\a:N; b:N\ \ a #* succ(b) = a #+ (a #* b) : N"
apply (NE a)
apply (hyp_arith_rew add_assoc [
THEN sym_elem])
apply (assumption | rule add_commute mult_typingL add_typingL intrL_rls refl_elem)+
done
text ‹Commutative law
for multiplication.
›
lemma mult_commute:
"\a:N; b:N\ \ a #* b = b #* a : N"
apply (NE a)
apply (hyp_arith_rew mult_0_right mult_succ_right)
done
text ‹Addition distributes over multiplication.
›
lemma add_mult_distrib:
"\a:N; b:N; c:N\ \ (a #+ b) #* c = (a #* c) #+ (b #* c) : N"
apply (NE a)
apply (hyp_arith_rew add_assoc [
THEN sym_elem])
done
text ‹Associative law
for multiplication.
›
lemma mult_assoc:
"\a:N; b:N; c:N\ \ (a #* b) #* c = a #* (b #* c) : N"
apply (NE a)
apply (hyp_arith_rew add_mult_distrib)
done
subsection ‹Difference
›
text ‹
Difference on natural numbers, without negative numbers
🚫 ‹a - b = 0
› iff
‹a
≤ b
›
🚫 ‹a - b = succ(c)
› iff
‹a > b
›
›
lemma diff_self_eq_0:
"a:N \ a - a = 0 : N"
apply (NE a)
apply hyp_arith_rew
done
lemma add_0_right:
"\c : N; 0 : N; c : N\ \ c #+ 0 = c : N"
by (rule addC0 [
THEN [3] add_commute [
THEN trans_elem]])
text ‹
Addition
is the inverse of subtraction:
if ‹b
≤ x
› then ‹b #+ (x - b) = x
›.
An example of
induction over a quantified formula (a product).
Uses rewriting
with a quantified, implicative
inductive hypothesis.
›
schematic_goal add_diff_inverse_lemma:
"b:N \ ?a : \x:N. Eq(N, b-x, 0) \ Eq(N, b #+ (x-b), x)"
apply (NE b)
🍋 ‹strip one
"universal quantifier" but not the
"implication"›
apply (rule_tac [3] intr_rls)
🍋 ‹case analysis on
‹x
› in ‹succ(u)
≤ x
⟶ succ(u) #+ (x - succ(u)) = x
››
prefer 4
apply (NE x)
apply assumption
🍋 ‹Prepare
for simplification of
types -- the antecedent
‹succ(u)
≤ x
››
apply (rule_tac [2] replace_type)
apply (rule_tac [1] replace_type)
apply arith_rew
🍋 ‹Solves first 0 goal, simplifies others. Two sugbgoals remain.
Both follow
by rewriting, (2)
using quantified
induction hyp.
›
apply intr
🍋 ‹strips remaining
‹∏›s
›
apply (hyp_arith_rew add_0_right)
apply assumption
done
text ‹
Version of above
with premise
‹b - a = 0
› i.e.
‹a
≥ b
›.
Using @{
thm ProdE} does not work --
for ‹?B(?a)
› is ambiguous.
Instead, @{
thm add_diff_inverse_lemma}
states the desired
induction scheme;
the
use of
‹THEN› below instantiates Vars
in @{
thm ProdE} automatically.
›
lemma add_diff_inverse:
"\a:N; b:N; b - a = 0 : N\ \ b #+ (a-b) = a : N"
apply (rule EqE)
apply (rule add_diff_inverse_lemma [
THEN ProdE,
THEN ProdE])
apply (assumption | rule EqI)+
done
subsection ‹Absolute difference
›
text ‹Typing of absolute difference: short
and long versions.
›
lemma absdiff_typing:
"\a:N; b:N\ \ a |-| b : N"
unfolding arith_defs
by typechk
lemma absdiff_typingL:
"\a = c:N; b = d:N\ \ a |-| b = c |-| d : N"
unfolding arith_defs
by equal
lemma absdiff_self_eq_0:
"a:N \ a |-| a = 0 : N"
unfolding absdiff_def
by (arith_rew diff_self_eq_0)
lemma absdiffC0:
"a:N \ 0 |-| a = a : N"
unfolding absdiff_def
by hyp_arith_rew
lemma absdiff_succ_succ:
"\a:N; b:N\ \ succ(a) |-| succ(b) = a |-| b : N"
unfolding absdiff_def
by hyp_arith_rew
text ‹Note how easy
using commutative laws can be? ...not always...
›
lemma absdiff_commute:
"\a:N; b:N\ \ a |-| b = b |-| a : N"
unfolding absdiff_def
by (rule add_commute) (typechk diff_typing)
text ‹If ‹a + b = 0
› then ‹a = 0
›. Surprisingly tedious.
›
schematic_goal add_eq0_lemma:
"\a:N; b:N\ \ ?c : Eq(N,a#+b,0) \ Eq(N,a,0)"
apply (NE a)
apply (rule_tac [3] replace_type)
apply arith_rew
apply intr
🍋 ‹strips remaining
‹∏›s
›
apply (rule_tac [2] zero_ne_succ [
THEN FE])
apply (erule_tac [3] EqE [
THEN sym_elem])
apply (typechk add_typing)
done
text ‹
Version of above
with the premise
‹a + b = 0
›.
Again, resolution instantiates variables
in @{
thm ProdE}.
›
lemma add_eq0:
"\a:N; b:N; a #+ b = 0 : N\ \ a = 0 : N"
apply (rule EqE)
apply (rule add_eq0_lemma [
THEN ProdE])
apply (rule_tac [3] EqI)
apply typechk
done
text ‹Here
is a
lemma to infer
‹a - b = 0
› and ‹b - a = 0
› from ‹a |-| b = 0
›, below.
›
schematic_goal absdiff_eq0_lem:
"\a:N; b:N; a |-| b = 0 : N\ \ ?a : Eq(N, a-b, 0) \ Eq(N, b-a, 0)"
unfolding absdiff_def
apply intr
apply eqintr
apply (rule_tac [2] add_eq0)
apply (rule add_eq0)
apply (rule_tac [6] add_commute [
THEN trans_elem])
apply (typechk diff_typing)
done
text ‹If ‹a |-| b = 0
› then ‹a = b
›
proof:
‹a - b = 0
› and ‹b - a = 0
›, so
‹b = a + (b - a) = a + 0 = a
›.
›
lemma absdiff_eq0:
"\a |-| b = 0 : N; a:N; b:N\ \ a = b : N"
apply (rule EqE)
apply (rule absdiff_eq0_lem [
THEN SumE])
apply eqintr
apply (rule add_diff_inverse [
THEN sym_elem,
THEN trans_elem])
apply (erule_tac [3] EqE)
apply (hyp_arith_rew add_0_right)
done
subsection ‹Remainder
and Quotient
›
text ‹Typing of remainder: short
and long versions.
›
lemma mod_typing:
"\a:N; b:N\ \ a mod b : N"
unfolding mod_def
by (typechk absdiff_typing)
lemma mod_typingL:
"\a = c:N; b = d:N\ \ a mod b = c mod d : N"
unfolding mod_def
by (equal absdiff_typingL)
text ‹Computation
for ‹mod
›: 0
and successor cases.
›
lemma modC0:
"b:N \ 0 mod b = 0 : N"
unfolding mod_def
by (rew absdiff_typing)
lemma modC_succ:
"\a:N; b:N\ \
succ(a) mod b = rec(succ(a mod b) |-| b, 0, λx y. succ(a mod b)) : N
"
unfolding mod_def
by (rew absdiff_typing)
text ‹Typing of quotient: short
and long versions.
›
lemma div_typing:
"\a:N; b:N\ \ a div b : N"
unfolding div_def by (typechk absdiff_typing mod_typing)
lemma div_typingL:
"\a = c:N; b = d:N\ \ a div b = c div d : N"
unfolding div_def by (
equal absdiff_typingL mod_typingL)
lemmas div_typing_rls = mod_typing div_typing absdiff_typing
text \<open>Computation for quotient: 0
and successor cases.\<close>
lemma divC0:
"b:N \ 0 div b = 0 : N"
unfolding div_def by (rew mod_typing absdiff_typing)
lemma divC_succ:
"\a:N; b:N\ \
succ(a) div b = rec(succ(a) mod b, succ(a div b), \<
lambda>x y. a div b) : N
"
unfolding div_def by (rew mod_typing)
text \<open>Version of above with same condition as the \<open>mod\<close> one.\<close>
lemma divC_succ2:
"\a:N; b:N\ \
succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), \<
lambda>x y. a div b) : N
"
apply (rule divC_succ [THEN trans_elem])
apply (rew div_typing_rls modC_succ)
apply (NE
"succ (a mod b) |-|b")
apply (rew mod_typing div_typing absdiff_typing)
done
text \<open>For
case analysis on whether a number is 0
or a successor.\<close>
lemma iszero_decidable:
"a:N \ rec(a, inl(eq), \ka kb. inr()) :
Eq(N,a,0) + (\<Sum>x:N.
Eq(N,a, succ(x)))
"
apply (NE a)
apply (rule_tac [3] PlusI_inr)
apply (rule_tac [2] PlusI_inl)
apply eqintr
apply equal
done
text \<open>Main Result. Holds when \<open>b\<close> is 0 since \<open>a mod 0 = a\<close>
and \<open>a div 0
= 0\<close>.\<close>
lemma mod_div_equality: "\a:N; b:N\ \ a mod b #+ (a div b) #* b = a : N"
apply (NE a)
apply (arith_rew div_typing_rls modC0 modC_succ divC0 divC_succ2)
apply (rule EqE)
\<comment> \<open>case analysis on \<open>succ(u mod b) |-| b\<close>\<close>
apply (rule_tac a1 = "succ (u mod b) |-| b" in iszero_decidable [THEN PlusE])
apply (erule_tac [3] SumE)
apply (hyp_arith_rew div_typing_rls modC0 modC_succ divC0 divC_succ2)
\<comment> \<open>Replace one occurrence of \<open>b\<close> by \<open>succ(u mod b)\<close>. Clumsy!\<close>
apply (rule add_typingL [THEN trans_elem])
apply (erule EqE [THEN absdiff_eq0, THEN sym_elem])
apply (rule_tac [3] refl_elem)
apply (hyp_arith_rew div_typing_rls)
done
end
