# HG changeset patch # User wenzelm # Date 1491760612 -7200 # Node ID fae6051ec19242de361a7625fc9fb815c2d26a30 # Parent ed18feb34c071f0626a106473925b94f697b62c6 clarified main CTT.thy, and avoid name clash with global HOL/Main.thy; diff -r ed18feb34c07 -r fae6051ec192 src/CTT/Arith.thy --- a/src/CTT/Arith.thy Sun Apr 09 19:03:55 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,415 +0,0 @@ -(* Title: CTT/Arith.thy - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1991 University of Cambridge -*) - -section \Elementary arithmetic\ - -theory Arith - imports Bool -begin - -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 - apply (NE b) - apply hyp_rew - done - -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" - apply (NE a) - apply hyp_arith_rew - done - -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 - \<^item> \a - b = 0\ iff \a \ b\ - \<^item> \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 - apply (rule add_commute) - apply (typechk diff_typing) - done - -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)" - apply (unfold 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 \Computation for quotient: 0 and successor cases.\ - -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), \x y. a div b) : N" - unfolding div_def by (rew mod_typing) - - -text \Version of above with same condition as the \mod\ one.\ -lemma divC_succ2: "\a:N; b:N\ \ - succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), \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 \For case analysis on whether a number is 0 or a successor.\ -lemma iszero_decidable: "a:N \ rec(a, inl(eq), \ka kb. inr()) : - Eq(N,a,0) + (\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 \Main Result. Holds when \b\ is 0 since \a mod 0 = a\ and \a div 0 = 0\.\ -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) - \ \case analysis on \succ(u mod b) |-| b\\ - 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) - \ \Replace one occurrence of \b\ by \succ(u mod b)\. Clumsy!\ - 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 diff -r ed18feb34c07 -r fae6051ec192 src/CTT/Bool.thy --- a/src/CTT/Bool.thy Sun Apr 09 19:03:55 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,73 +0,0 @@ -(* Title: CTT/Bool.thy - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1991 University of Cambridge -*) - -section \The two-element type (booleans and conditionals)\ - -theory Bool - imports CTT -begin - -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 - -end diff -r ed18feb34c07 -r fae6051ec192 src/CTT/CTT.thy --- a/src/CTT/CTT.thy Sun Apr 09 19:03:55 2017 +0200 +++ b/src/CTT/CTT.thy Sun Apr 09 19:56:52 2017 +0200 @@ -3,12 +3,12 @@ Copyright 1993 University of Cambridge *) -section \Constructive Type Theory\ - theory CTT imports Pure begin +section \Constructive Type Theory: axiomatic basis\ + ML_file "~~/src/Provers/typedsimp.ML" setup Pure_Thy.old_appl_syntax_setup @@ -482,4 +482,473 @@ 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 + apply (NE b) + apply hyp_rew + done + +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" + apply (NE a) + apply hyp_arith_rew + done + +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 + \<^item> \a - b = 0\ iff \a \ b\ + \<^item> \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 + apply (rule add_commute) + apply (typechk diff_typing) + done + +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)" + apply (unfold 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 \Computation for quotient: 0 and successor cases.\ + +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), \x y. a div b) : N" + unfolding div_def by (rew mod_typing) + + +text \Version of above with same condition as the \mod\ one.\ +lemma divC_succ2: "\a:N; b:N\ \ + succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), \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 \For case analysis on whether a number is 0 or a successor.\ +lemma iszero_decidable: "a:N \ rec(a, inl(eq), \ka kb. inr()) : + Eq(N,a,0) + (\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 \Main Result. Holds when \b\ is 0 since \a mod 0 = a\ and \a div 0 = 0\.\ +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) + \ \case analysis on \succ(u mod b) |-| b\\ + 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) + \ \Replace one occurrence of \b\ by \succ(u mod b)\. Clumsy!\ + 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 diff -r ed18feb34c07 -r fae6051ec192 src/CTT/Main.thy --- a/src/CTT/Main.thy Sun Apr 09 19:03:55 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,6 +0,0 @@ -section \Main includes everything\ - -theory Main - imports CTT Bool Arith -begin -end diff -r ed18feb34c07 -r fae6051ec192 src/CTT/ROOT --- a/src/CTT/ROOT Sun Apr 09 19:03:55 2017 +0200 +++ b/src/CTT/ROOT Sun Apr 09 19:56:52 2017 +0200 @@ -18,7 +18,7 @@ *} options [thy_output_source] theories - Main + CTT "ex/Typechecking" "ex/Elimination" "ex/Equality" diff -r ed18feb34c07 -r fae6051ec192 src/CTT/ex/Synthesis.thy --- a/src/CTT/ex/Synthesis.thy Sun Apr 09 19:03:55 2017 +0200 +++ b/src/CTT/ex/Synthesis.thy Sun Apr 09 19:56:52 2017 +0200 @@ -6,7 +6,7 @@ section "Synthesis examples, using a crude form of narrowing" theory Synthesis -imports "../Arith" +imports "../CTT" begin text "discovery of predecessor function"