--- 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 \<Rightarrow> bool" where
-"even 0 = True" |
-"even (Suc 0) = False" |
-"even (Suc(Suc n)) = even n"
+fun evn :: "nat \<Rightarrow> bool" where
+"evn 0 = True" |
+"evn (Suc 0) = False" |
+"evn (Suc(Suc n)) = evn n"
-text{* We prove @{prop"ev m \<Longrightarrow> even m"}. That is, we
+text{* We prove @{prop"ev m \<Longrightarrow> 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"\<Longrightarrow>"} @{prop"m=(0::nat)"} @{text"\<Longrightarrow>"} @{text "even m = even 0 = True"}
+ @{text"\<Longrightarrow>"} @{prop"m=(0::nat)"} @{text"\<Longrightarrow>"} @{text "evn m = evn 0 = True"}
\item[Case @{thm[source]evSS}:]
@{prop"ev m"} was derived by rule @{prop "ev n \<Longrightarrow> ev(n+2)"}: \\
-@{text"\<Longrightarrow>"} @{prop"m=n+(2::nat)"} and by induction hypothesis @{prop"even n"}\\
-@{text"\<Longrightarrow>"} @{text"even m = even(n + 2) = even n = True"}
+@{text"\<Longrightarrow>"} @{prop"m=n+(2::nat)"} and by induction hypothesis @{prop"evn n"}\\
+@{text"\<Longrightarrow>"} @{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 \<Longrightarrow> even m"
+lemma "ev m \<Longrightarrow> 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 \<Longrightarrow> ev n"
-apply(induction n rule: even.induct)
+lemma "evn n \<Longrightarrow> 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 \<Longrightarrow> P n"}} because it only asks you
-to prove the positive cases. In the proof of @{prop"even n \<Longrightarrow> 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 \<Longrightarrow> 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
--- 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"
--- 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
--- 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 \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is Cons parametric Cons_transfer
+lift_definition fcons :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is Cons parametric list.ctr_transfer(2)
by simp
lift_definition fappend :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is append parametric append_transfer
by simp
-lift_definition fmap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" is map parametric map_transfer
+lift_definition fmap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" is map parametric list.map_transfer
by simp
lift_definition ffilter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is filter parametric filter_transfer
by simp
-lift_definition fset :: "'a fset \<Rightarrow> 'a set" is set parametric set_transfer
+lift_definition fset :: "'a fset \<Rightarrow> 'a set" is set parametric list.set_transfer
by simp
text {* Constants with nested types (like concat) yield a more