# HG changeset patch # User wenzelm # Date 1415661071 -3600 # Node ID a93d114eaa5d96fbd15c94a1f065b3a6ab5bd54a # Parent e3491acee50f71cd6e875c3280418a158ec9d1ea# Parent 26bf09b95dda6ae5935309154a99fe135dd442d5 merged diff -r 26bf09b95dda -r a93d114eaa5d src/Doc/Prog_Prove/Logic.thy --- a/src/Doc/Prog_Prove/Logic.thy Mon Nov 10 21:49:48 2014 +0100 +++ b/src/Doc/Prog_Prove/Logic.thy Tue Nov 11 00:11:11 2014 +0100 @@ -537,23 +537,23 @@ example, let us prove that the inductive definition of even numbers agrees with the following recursive one:*} -fun even :: "nat \ bool" where -"even 0 = True" | -"even (Suc 0) = False" | -"even (Suc(Suc n)) = even n" +fun evn :: "nat \ bool" where +"evn 0 = True" | +"evn (Suc 0) = False" | +"evn (Suc(Suc n)) = evn n" -text{* We prove @{prop"ev m \ even m"}. That is, we +text{* We prove @{prop"ev m \ evn m"}. That is, we assume @{prop"ev m"} and by induction on the form of its derivation -prove @{prop"even m"}. There are two cases corresponding to the two rules +prove @{prop"evn m"}. There are two cases corresponding to the two rules for @{const ev}: \begin{description} \item[Case @{thm[source]ev0}:] @{prop"ev m"} was derived by rule @{prop "ev 0"}: \\ - @{text"\"} @{prop"m=(0::nat)"} @{text"\"} @{text "even m = even 0 = True"} + @{text"\"} @{prop"m=(0::nat)"} @{text"\"} @{text "evn m = evn 0 = True"} \item[Case @{thm[source]evSS}:] @{prop"ev m"} was derived by rule @{prop "ev n \ ev(n+2)"}: \\ -@{text"\"} @{prop"m=n+(2::nat)"} and by induction hypothesis @{prop"even n"}\\ -@{text"\"} @{text"even m = even(n + 2) = even n = True"} +@{text"\"} @{prop"m=n+(2::nat)"} and by induction hypothesis @{prop"evn n"}\\ +@{text"\"} @{text"evn m = evn(n + 2) = evn n = True"} \end{description} What we have just seen is a special case of \concept{rule induction}. @@ -627,7 +627,7 @@ Rule induction is applied by giving the induction rule explicitly via the @{text"rule:"} modifier:\index{inductionrule@@{text"induction ... rule:"}}*} -lemma "ev m \ even m" +lemma "ev m \ evn m" apply(induction rule: ev.induct) by(simp_all) @@ -636,17 +636,17 @@ one. As a bonus, we also prove the remaining direction of the equivalence of -@{const ev} and @{const even}: +@{const ev} and @{const evn}: *} -lemma "even n \ ev n" -apply(induction n rule: even.induct) +lemma "evn n \ ev n" +apply(induction n rule: evn.induct) txt{* This is a proof by computation induction on @{text n} (see \autoref{sec:recursive-funs}) that sets up three subgoals corresponding to -the three equations for @{const even}: +the three equations for @{const evn}: @{subgoals[display,indent=0]} -The first and third subgoals follow with @{thm[source]ev0} and @{thm[source]evSS}, and the second subgoal is trivially true because @{prop"even(Suc 0)"} is @{const False}: +The first and third subgoals follow with @{thm[source]ev0} and @{thm[source]evSS}, and the second subgoal is trivially true because @{prop"evn(Suc 0)"} is @{const False}: *} by (simp_all add: ev0 evSS) @@ -674,8 +674,8 @@ information, for example, that @{text 1} is not even, has to be proved from it (by induction or rule inversion). On the other hand, rule induction is tailor-made for proving \mbox{@{prop"ev n \ P n"}} because it only asks you -to prove the positive cases. In the proof of @{prop"even n \ P n"} by -computation induction via @{thm[source]even.induct}, we are also presented +to prove the positive cases. In the proof of @{prop"evn n \ P n"} by +computation induction via @{thm[source]evn.induct}, we are also presented with the trivial negative cases. If you want the convenience of both rewriting and rule induction, you can make two definitions and show their equivalence (as above) or make one definition and prove additional properties diff -r 26bf09b95dda -r a93d114eaa5d src/HOL/Library/Quotient_List.thy --- a/src/HOL/Library/Quotient_List.thy Mon Nov 10 21:49:48 2014 +0100 +++ b/src/HOL/Library/Quotient_List.thy Tue Nov 11 00:11:11 2014 +0100 @@ -117,7 +117,7 @@ and q2: "Quotient3 R2 Abs2 Rep2" shows "((R1 ===> R2) ===> (list_all2 R1) ===> list_all2 R2) map map" and "((R1 ===> op =) ===> (list_all2 R1) ===> op =) map map" - unfolding list_all2_eq [symmetric] by (rule map_transfer)+ + unfolding list_all2_eq [symmetric] by (rule list.map_transfer)+ lemma foldr_prs_aux: assumes a: "Quotient3 R1 abs1 rep1" @@ -169,7 +169,7 @@ lemma [quot_respect]: "((R ===> R ===> op =) ===> list_all2 R ===> list_all2 R ===> op =) list_all2 list_all2" - by (rule list_all2_transfer) + by (rule list.rel_transfer) lemma [quot_preserve]: assumes a: "Quotient3 R abs1 rep1" diff -r 26bf09b95dda -r a93d114eaa5d src/HOL/List.thy --- a/src/HOL/List.thy Mon Nov 10 21:49:48 2014 +0100 +++ b/src/HOL/List.thy Tue Nov 11 00:11:11 2014 +0100 @@ -6449,23 +6449,6 @@ begin interpretation lifting_syntax . -lemma Nil_transfer [transfer_rule]: "(list_all2 A) [] []" - by simp - -lemma Cons_transfer [transfer_rule]: - "(A ===> list_all2 A ===> list_all2 A) Cons Cons" - unfolding rel_fun_def by simp - -lemma case_list_transfer [transfer_rule]: - "(B ===> (A ===> list_all2 A ===> B) ===> list_all2 A ===> B) - case_list case_list" - unfolding rel_fun_def by (simp split: list.split) - -lemma rec_list_transfer [transfer_rule]: - "(B ===> (A ===> list_all2 A ===> B ===> B) ===> list_all2 A ===> B) - rec_list rec_list" - unfolding rel_fun_def by (clarify, erule list_all2_induct, simp_all) - lemma tl_transfer [transfer_rule]: "(list_all2 A ===> list_all2 A) tl tl" unfolding tl_def[abs_def] by transfer_prover @@ -6474,17 +6457,9 @@ "(list_all2 A ===> list_all2 A) butlast butlast" by (rule rel_funI, erule list_all2_induct, auto) -lemma set_transfer [transfer_rule]: - "(list_all2 A ===> rel_set A) set set" - unfolding set_rec[abs_def] by transfer_prover - lemma map_rec: "map f xs = rec_list Nil (%x _ y. Cons (f x) y) xs" by (induct xs) auto -lemma map_transfer [transfer_rule]: - "((A ===> B) ===> list_all2 A ===> list_all2 B) map map" - unfolding map_rec[abs_def] by transfer_prover - lemma append_transfer [transfer_rule]: "(list_all2 A ===> list_all2 A ===> list_all2 A) append append" unfolding List.append_def by transfer_prover @@ -6596,14 +6571,6 @@ "(op = ===> list_all2 A ===> list_all2 A) rotate rotate" unfolding rotate_def [abs_def] by transfer_prover -lemma list_all2_transfer [transfer_rule]: - "((A ===> B ===> op =) ===> list_all2 A ===> list_all2 B ===> op =) - list_all2 list_all2" - apply (subst (4) list_all2_iff [abs_def]) - apply (subst (3) list_all2_iff [abs_def]) - apply transfer_prover - done - lemma sublist_transfer [transfer_rule]: "(list_all2 A ===> rel_set (op =) ===> list_all2 A) sublist sublist" unfolding sublist_def [abs_def] by transfer_prover diff -r 26bf09b95dda -r a93d114eaa5d src/HOL/Quotient_Examples/Lift_FSet.thy --- a/src/HOL/Quotient_Examples/Lift_FSet.thy Mon Nov 10 21:49:48 2014 +0100 +++ b/src/HOL/Quotient_Examples/Lift_FSet.thy Tue Nov 11 00:11:11 2014 +0100 @@ -39,21 +39,21 @@ subsection {* Lifted constant definitions *} -lift_definition fnil :: "'a fset" ("{||}") is "[]" parametric Nil_transfer . +lift_definition fnil :: "'a fset" ("{||}") is "[]" parametric list.ctr_transfer(1) . -lift_definition fcons :: "'a \ 'a fset \ 'a fset" is Cons parametric Cons_transfer +lift_definition fcons :: "'a \ 'a fset \ 'a fset" is Cons parametric list.ctr_transfer(2) by simp lift_definition fappend :: "'a fset \ 'a fset \ 'a fset" is append parametric append_transfer by simp -lift_definition fmap :: "('a \ 'b) \ 'a fset \ 'b fset" is map parametric map_transfer +lift_definition fmap :: "('a \ 'b) \ 'a fset \ 'b fset" is map parametric list.map_transfer by simp lift_definition ffilter :: "('a \ bool) \ 'a fset \ 'a fset" is filter parametric filter_transfer by simp -lift_definition fset :: "'a fset \ 'a set" is set parametric set_transfer +lift_definition fset :: "'a fset \ 'a set" is set parametric list.set_transfer by simp text {* Constants with nested types (like concat) yield a more