# HG changeset patch
# User wenzelm
# Date 1363609122 -3600
# Node ID d2bc229e1f37cf60b6ac8dfe505fbebbd0ecc287
# Parent  b041137f7fe54fea16b20855f379a016be500011# Parent  14e6d761ba1c1caf8f11bce3cfb31758ea8b89c4
merged

diff -r 14e6d761ba1c -r d2bc229e1f37 src/Doc/ProgProve/Isar.thy
--- a/src/Doc/ProgProve/Isar.thy	Mon Mar 18 11:29:50 2013 +0100
+++ b/src/Doc/ProgProve/Isar.thy	Mon Mar 18 13:18:42 2013 +0100
@@ -894,6 +894,7 @@
 going through rule @{text i} from left to right.
 
 \subsection{Assumption naming}
+\label{sec:assm-naming}
 
 In any induction, \isacom{case}~@{text name} sets up a list of assumptions
 also called @{text name}, which is subdivided into three parts:
@@ -978,8 +979,75 @@
 
 text{* Normally not all cases will be impossible. As a simple exercise,
 prove that \mbox{@{prop"\<not> ev(Suc(Suc(Suc 0)))"}.}
+
+\subsection{Advanced rule induction}
+\label{sec:advanced-rule-induction}
+
+So far, rule induction was always applied to goals of the form @{text"I x y z \<Longrightarrow> \<dots>"}
+where @{text I} is some inductively defined predicate and @{text x}, @{text y}, @{text z}
+are variables. In some rare situations one needs to deal with an assumption where
+not all arguments @{text r}, @{text s}, @{text t} are variables:
+\begin{isabelle}
+\isacom{lemma} @{text[source]"I r s t \<Longrightarrow> \<dots>"}
+\end{isabelle}
+Applying the standard form of
+rule induction in such a situation will lead to strange and typically unproveable goals.
+We can easily reduce this situation to the standard one by introducing
+new variables @{text x}, @{text y}, @{text z} and reformulating the goal like this:
+\begin{isabelle}
+\isacom{lemma} @{text[source]"I x y z \<Longrightarrow> x = r \<Longrightarrow> y = s \<Longrightarrow> z = t \<Longrightarrow> \<dots>"}
+\end{isabelle}
+Standard rule induction will worke fine now, provided the free variables in
+@{text r}, @{text s}, @{text t} are generalized via @{text"arbitrary"}.
+
+However, induction can do the above transformation for us, behind the curtains, so we never
+need to see the expanded version of the lemma. This is what we need to write:
+\begin{isabelle}
+\isacom{lemma} @{text[source]"I r s t \<Longrightarrow> \<dots>"}\isanewline
+\isacom{proof}@{text"(induction \"r\" \"s\" \"t\" arbitrary: \<dots> rule: I.induct)"}
+\end{isabelle}
+Just like for rule inversion, cases that are impossible because of constructor clashes
+will not show up at all. Here is a concrete example: *}
+
+lemma "ev (Suc m) \<Longrightarrow> \<not> ev m"
+proof(induction "Suc m" arbitrary: m rule: ev.induct)
+  fix n assume IH: "\<And>m. n = Suc m \<Longrightarrow> \<not> ev m"
+  show "\<not> ev (Suc n)"
+  proof --"contradition"
+    assume "ev(Suc n)"
+    thus False
+    proof cases --"rule inversion"
+      fix k assume "n = Suc k" "ev k"
+      thus False using IH by auto
+    qed
+  qed
+qed
+
+text{*
+Remarks:
+\begin{itemize}
+\item 
+Instead of the \isacom{case} and @{text ?case} magic we have spelled all formulas out.
+This is merely for greater clarity.
+\item
+We only need to deal with one case because the @{thm[source] ev0} case is impossible.
+\item
+The form of the @{text IH} shows us that internally the lemma was expanded as explained
+above: \noquotes{@{prop[source]"ev x \<Longrightarrow> x = Suc m \<Longrightarrow> \<not> ev m"}}.
+\item
+The goal @{prop"\<not> ev (Suc n)"} may suprise. The expanded version of the lemma
+would suggest that we have a \isacom{fix} @{text m} \isacom{assume} @{prop"Suc(Suc n) = Suc m"}
+and need to show @{prop"\<not> ev m"}. What happened is that Isabelle immediately
+simplified @{prop"Suc(Suc n) = Suc m"} to @{prop"Suc n = m"} and could then eliminate
+@{text m}. Beware of such nice surprises with this advanced form of induction.
+\end{itemize}
+\begin{warn}
+This advanced form of induction does not support the @{text IH}
+naming schema explained in \autoref{sec:assm-naming}:
+the induction hypotheses are instead found under the name @{text hyps}, like for the simpler
+@{text induct} method.
+\end{warn}
 *}
-
 (*
 lemma "\<not> ev(Suc(Suc(Suc 0)))"
 proof
diff -r 14e6d761ba1c -r d2bc229e1f37 src/Doc/ProgProve/document/prelude.tex
--- a/src/Doc/ProgProve/document/prelude.tex	Mon Mar 18 11:29:50 2013 +0100
+++ b/src/Doc/ProgProve/document/prelude.tex	Mon Mar 18 13:18:42 2013 +0100
@@ -48,6 +48,7 @@
 % section commands
 \renewcommand{\chapterautorefname}{Chapter}
 \renewcommand{\sectionautorefname}{Section}
+\renewcommand{\subsectionautorefname}{Section}
 
 \renewcommand{\isamarkupheader}[1]{{\rmfamily\subsection{#1}}}
 \renewcommand{\isamarkupsection}[1]{{\rmfamily\subsection{#1}}}
diff -r 14e6d761ba1c -r d2bc229e1f37 src/Doc/ProgProve/document/root.tex
--- a/src/Doc/ProgProve/document/root.tex	Mon Mar 18 11:29:50 2013 +0100
+++ b/src/Doc/ProgProve/document/root.tex	Mon Mar 18 13:18:42 2013 +0100
@@ -34,7 +34,7 @@
 %\label{sec:CaseStudyExp}
 %\input{../generated/Expressions}
 
-\chapter{Logic and proof beyond equality}
+\chapter{Logic and Proof Beyond Equality}
 \label{ch:Logic}
 \input{Logic}
 
diff -r 14e6d761ba1c -r d2bc229e1f37 src/HOL/BNF/BNF.thy
--- a/src/HOL/BNF/BNF.thy	Mon Mar 18 11:29:50 2013 +0100
+++ b/src/HOL/BNF/BNF.thy	Mon Mar 18 13:18:42 2013 +0100
@@ -13,4 +13,8 @@
 imports More_BNFs
 begin
 
+hide_const (open) Gr collect fsts snds setl setr 
+  convol thePull pick_middle fstO sndO csquare inver
+  image2 relImage relInvImage prefCl PrefCl Succ Shift shift
+
 end
diff -r 14e6d761ba1c -r d2bc229e1f37 src/HOL/BNF/BNF_GFP.thy
--- a/src/HOL/BNF/BNF_GFP.thy	Mon Mar 18 11:29:50 2013 +0100
+++ b/src/HOL/BNF/BNF_GFP.thy	Mon Mar 18 13:18:42 2013 +0100
@@ -44,35 +44,29 @@
 qed
 
 (* Operators: *)
-definition diag where "diag A \<equiv> {(a,a) | a. a \<in> A}"
 definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}"
 
-lemma diagI: "x \<in> A \<Longrightarrow> (x, x) \<in> diag A"
-unfolding diag_def by simp
 
-lemma diagE: "(a, b) \<in> diag A \<Longrightarrow> a = b"
-unfolding diag_def by simp
+lemma Id_onD: "(a, b) \<in> Id_on A \<Longrightarrow> a = b"
+unfolding Id_on_def by simp
 
-lemma diagE': "x \<in> diag A \<Longrightarrow> fst x = snd x"
-unfolding diag_def by auto
+lemma Id_onD': "x \<in> Id_on A \<Longrightarrow> fst x = snd x"
+unfolding Id_on_def by auto
 
-lemma diag_fst: "x \<in> diag A \<Longrightarrow> fst x \<in> A"
-unfolding diag_def by auto
+lemma Id_on_fst: "x \<in> Id_on A \<Longrightarrow> fst x \<in> A"
+unfolding Id_on_def by auto
 
-lemma diag_UNIV: "diag UNIV = Id"
-unfolding diag_def by auto
+lemma Id_on_UNIV: "Id_on UNIV = Id"
+unfolding Id_on_def by auto
 
-lemma diag_converse: "diag A = (diag A) ^-1"
-unfolding diag_def by auto
+lemma Id_on_Comp: "Id_on A = Id_on A O Id_on A"
+unfolding Id_on_def by auto
 
-lemma diag_Comp: "diag A = diag A O diag A"
-unfolding diag_def by auto
+lemma Id_on_Gr: "Id_on A = Gr A id"
+unfolding Id_on_def Gr_def by auto
 
-lemma diag_Gr: "diag A = Gr A id"
-unfolding diag_def Gr_def by simp
-
-lemma diag_UNIV_I: "x = y \<Longrightarrow> (x, y) \<in> diag UNIV"
-unfolding diag_def by auto
+lemma Id_on_UNIV_I: "x = y \<Longrightarrow> (x, y) \<in> Id_on UNIV"
+unfolding Id_on_def by auto
 
 lemma image2_eqI: "\<lbrakk>b = f x; c = g x; x \<in> A\<rbrakk> \<Longrightarrow> (b, c) \<in> image2 A f g"
 unfolding image2_def by auto
@@ -122,9 +116,9 @@
 "R1 \<subseteq> R2 \<Longrightarrow> relInvImage A R1 f \<subseteq> relInvImage A R2 f"
 unfolding relInvImage_def by auto
 
-lemma relInvImage_diag:
-"(\<And>a1 a2. f a1 = f a2 \<longleftrightarrow> a1 = a2) \<Longrightarrow> relInvImage A (diag B) f \<subseteq> Id"
-unfolding relInvImage_def diag_def by auto
+lemma relInvImage_Id_on:
+"(\<And>a1 a2. f a1 = f a2 \<longleftrightarrow> a1 = a2) \<Longrightarrow> relInvImage A (Id_on B) f \<subseteq> Id"
+unfolding relInvImage_def Id_on_def by auto
 
 lemma relInvImage_UNIV_relImage:
 "R \<subseteq> relInvImage UNIV (relImage R f) f"
@@ -135,10 +129,10 @@
 
 lemma relImage_proj:
 assumes "equiv A R"
-shows "relImage R (proj R) \<subseteq> diag (A//R)"
-unfolding relImage_def diag_def apply safe
-using proj_iff[OF assms]
-by (metis assms equiv_Image proj_def proj_preserves)
+shows "relImage R (proj R) \<subseteq> Id_on (A//R)"
+unfolding relImage_def Id_on_def
+using proj_iff[OF assms] equiv_class_eq_iff[OF assms]
+by (auto simp: proj_preserves)
 
 lemma relImage_relInvImage:
 assumes "R \<subseteq> f ` A <*> f ` A"
@@ -276,23 +270,14 @@
 unfolding fromCard_def by (rule some_equality) (auto simp add: toCard_inj)
 
 (* pick according to the weak pullback *)
-definition pickWP_pred where
-"pickWP_pred A p1 p2 b1 b2 a \<equiv> a \<in> A \<and> p1 a = b1 \<and> p2 a = b2"
-
 definition pickWP where
-"pickWP A p1 p2 b1 b2 \<equiv> SOME a. pickWP_pred A p1 p2 b1 b2 a"
+"pickWP A p1 p2 b1 b2 \<equiv> SOME a. a \<in> A \<and> p1 a = b1 \<and> p2 a = b2"
 
 lemma pickWP_pred:
 assumes "wpull A B1 B2 f1 f2 p1 p2" and
 "b1 \<in> B1" and "b2 \<in> B2" and "f1 b1 = f2 b2"
-shows "\<exists> a. pickWP_pred A p1 p2 b1 b2 a"
-using assms unfolding wpull_def pickWP_pred_def by blast
-
-lemma pickWP_pred_pickWP:
-assumes "wpull A B1 B2 f1 f2 p1 p2" and
-"b1 \<in> B1" and "b2 \<in> B2" and "f1 b1 = f2 b2"
-shows "pickWP_pred A p1 p2 b1 b2 (pickWP A p1 p2 b1 b2)"
-unfolding pickWP_def using assms by(rule someI_ex[OF pickWP_pred])
+shows "\<exists> a. a \<in> A \<and> p1 a = b1 \<and> p2 a = b2"
+using assms unfolding wpull_def by blast
 
 lemma pickWP:
 assumes "wpull A B1 B2 f1 f2 p1 p2" and
@@ -300,7 +285,7 @@
 shows "pickWP A p1 p2 b1 b2 \<in> A"
       "p1 (pickWP A p1 p2 b1 b2) = b1"
       "p2 (pickWP A p1 p2 b1 b2) = b2"
-using assms pickWP_pred_pickWP unfolding pickWP_pred_def by fastforce+
+unfolding pickWP_def using assms someI_ex[OF pickWP_pred] by fastforce+
 
 lemma Inl_Field_csum: "a \<in> Field r \<Longrightarrow> Inl a \<in> Field (r +c s)"
 unfolding Field_card_of csum_def by auto
diff -r 14e6d761ba1c -r d2bc229e1f37 src/HOL/BNF/Basic_BNFs.thy
--- a/src/HOL/BNF/Basic_BNFs.thy	Mon Mar 18 11:29:50 2013 +0100
+++ b/src/HOL/BNF/Basic_BNFs.thy	Mon Mar 18 13:18:42 2013 +0100
@@ -24,11 +24,12 @@
 lemma natLeq_cinfinite: "cinfinite natLeq"
 unfolding cinfinite_def Field_natLeq by (rule nat_infinite)
 
+lemma wpull_Gr_def: "wpull A B1 B2 f1 f2 p1 p2 \<longleftrightarrow> Gr B1 f1 O (Gr B2 f2)\<inverse> \<subseteq> (Gr A p1)\<inverse> O Gr A p2"
+  unfolding wpull_def Gr_def relcomp_unfold converse_unfold by auto
+
 bnf_def ID: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" ["\<lambda>x. {x}"] "\<lambda>_:: 'a. natLeq" ["id :: 'a \<Rightarrow> 'a"]
   "\<lambda>x :: 'a \<Rightarrow> 'b \<Rightarrow> bool. x"
-apply auto
-apply (rule natLeq_card_order)
-apply (rule natLeq_cinfinite)
+apply (auto simp: Gr_def fun_eq_iff natLeq_card_order natLeq_cinfinite)
 apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
 apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3]
 apply (rule ordLeq_transitive)
@@ -48,18 +49,13 @@
 apply (rule ordLeq_csum2)
 apply (rule Card_order_ctwo)
 apply (rule natLeq_Card_order)
-apply (auto simp: Gr_def fun_eq_iff)
 done
 
 bnf_def DEADID: "id :: 'a \<Rightarrow> 'a" [] "\<lambda>_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"]
   "op =::'a \<Rightarrow> 'a \<Rightarrow> bool"
-apply (auto simp add: wpull_id)
-apply (rule card_order_csum)
-apply (rule natLeq_card_order)
-apply (rule card_of_card_order_on)
-apply (rule cinfinite_csum)
-apply (rule disjI1)
-apply (rule natLeq_cinfinite)
+apply (auto simp add: wpull_Gr_def Gr_def
+  card_order_csum natLeq_card_order card_of_card_order_on
+  cinfinite_csum natLeq_cinfinite)
 apply (rule ordLess_imp_ordLeq)
 apply (rule ordLess_ordLeq_trans)
 apply (rule ordLess_ctwo_cexp)
@@ -69,7 +65,6 @@
 apply (rule card_of_Card_order)
 apply (rule ctwo_Cnotzero)
 apply (rule card_of_Card_order)
-apply (auto simp: Id_def Gr_def fun_eq_iff)
 done
 
 definition setl :: "'a + 'b \<Rightarrow> 'a set" where
@@ -344,11 +339,8 @@
   ultimately show ?thesis using card_of_ordLeq by fast
 qed
 
-definition fun_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> ('c \<Rightarrow> 'b) \<Rightarrow> bool" where
-"fun_rel \<phi> f g = (\<forall>x. \<phi> (f x) (g x))"
-
 bnf_def "op \<circ>" [range] "\<lambda>_:: 'a \<Rightarrow> 'b. natLeq +c |UNIV :: 'a set|" ["%c x::'b::type. c::'a::type"]
-  fun_rel
+  "fun_rel op ="
 proof
   fix f show "id \<circ> f = id f" by simp
 next
@@ -408,10 +400,10 @@
   qed
 next
   fix R
-  show "{p. fun_rel (\<lambda>x y. (x, y) \<in> R) (fst p) (snd p)} =
+  show "{p. fun_rel op = (\<lambda>x y. (x, y) \<in> R) (fst p) (snd p)} =
         (Gr {x. range x \<subseteq> R} (op \<circ> fst))\<inverse> O Gr {x. range x \<subseteq> R} (op \<circ> snd)"
   unfolding fun_rel_def Gr_def relcomp_unfold converse_unfold
-  by (auto intro!: exI dest!: in_mono)
+  by force
 qed auto
 
 end
diff -r 14e6d761ba1c -r d2bc229e1f37 src/HOL/BNF/More_BNFs.thy
--- a/src/HOL/BNF/More_BNFs.thy	Mon Mar 18 11:29:50 2013 +0100
+++ b/src/HOL/BNF/More_BNFs.thy	Mon Mar 18 13:18:42 2013 +0100
@@ -22,13 +22,6 @@
 lemma option_rec_conv_option_case: "option_rec = option_case"
 by (simp add: fun_eq_iff split: option.split)
 
-definition option_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> bool" where
-"option_rel R x_opt y_opt =
-  (case (x_opt, y_opt) of
-    (None, None) \<Rightarrow> True
-  | (Some x, Some y) \<Rightarrow> R x y
-  | _ \<Rightarrow> False)"
-
 bnf_def Option.map [Option.set] "\<lambda>_::'a option. natLeq" ["None"] option_rel
 proof -
   show "Option.map id = id" by (simp add: fun_eq_iff Option.map_def split: option.split)
@@ -92,7 +85,7 @@
   fix R
   show "{p. option_rel (\<lambda>x y. (x, y) \<in> R) (fst p) (snd p)} =
         (Gr {x. Option.set x \<subseteq> R} (Option.map fst))\<inverse> O Gr {x. Option.set x \<subseteq> R} (Option.map snd)"
-  unfolding option_rel_def Gr_def relcomp_unfold converse_unfold
+  unfolding option_rel_unfold Gr_def relcomp_unfold converse_unfold
   by (auto simp: trans[OF eq_commute option_map_is_None] trans[OF eq_commute option_map_eq_Some]
            split: option.splits) blast
 qed
@@ -286,9 +279,6 @@
 lemma abs_fset_rep_fset[simp]: "abs_fset (rep_fset x) = x"
   by (rule Quotient_fset[unfolded Quotient_def, THEN conjunct1, rule_format])
 
-lemma wpull_Gr_def: "wpull A B1 B2 f1 f2 p1 p2 \<longleftrightarrow> Gr B1 f1 O (Gr B2 f2)\<inverse> \<subseteq> (Gr A p1)\<inverse> O Gr A p2"
-  unfolding wpull_def Gr_def relcomp_unfold converse_unfold by auto
-
 lemma wpull_image:
   assumes "wpull A B1 B2 f1 f2 p1 p2"
   shows "wpull (Pow A) (Pow B1) (Pow B2) (image f1) (image f2) (image p1) (image p2)"
diff -r 14e6d761ba1c -r d2bc229e1f37 src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Mon Mar 18 11:29:50 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Mon Mar 18 13:18:42 2013 +0100
@@ -198,7 +198,7 @@
       ||>> mk_Freess "K" (map (fn AT => map (fn T => T --> AT) activeAs) ATs);
 
     val passive_UNIVs = map HOLogic.mk_UNIV passiveAs;
-    val passive_diags = map mk_diag As;
+    val passive_Id_ons = map mk_Id_on As;
     val active_UNIVs = map HOLogic.mk_UNIV activeAs;
     val sum_UNIVs = map HOLogic.mk_UNIV sumBsAs;
     val passive_ids = map HOLogic.id_const passiveAs;
@@ -854,7 +854,7 @@
           list_all_free [b1, b2] (HOLogic.mk_imp
             (HOLogic.mk_mem (HOLogic.mk_prod (b1, b2), R),
             HOLogic.mk_mem (HOLogic.mk_prod (s $ b1, s' $ b2),
-              Term.list_comb (srel, passive_diags @ Rs))));
+              Term.list_comb (srel, passive_Id_ons @ Rs))));
 
         val rhs = HOLogic.mk_conj
           (bis_le, Library.foldr1 HOLogic.mk_conj
@@ -907,8 +907,8 @@
       ((bis_O_thm OF [bis_Gr_thm RS bis_converse_thm, bis_Gr_thm]) ::
       replicate n @{thm image2_Gr});
 
-    val bis_diag_thm = bis_cong_thm OF ((mor_id_thm RSN (2, bis_Gr_thm)) ::
-      replicate n @{thm diag_Gr});
+    val bis_Id_on_thm = bis_cong_thm OF ((mor_id_thm RSN (2, bis_Gr_thm)) ::
+      replicate n @{thm Id_on_Gr});
 
     val bis_Union_thm =
       let
@@ -1004,7 +1004,7 @@
         map3 (fn goal => fn l_incl => fn incl_l =>
           Skip_Proof.prove lthy [] [] goal
             (K (mk_equiv_lsbis_tac sbis_lsbis_thm l_incl incl_l
-              bis_diag_thm bis_converse_thm bis_O_thm))
+              bis_Id_on_thm bis_converse_thm bis_O_thm))
           |> Thm.close_derivation)
         goals lsbis_incl_thms incl_lsbis_thms
       end;
@@ -2187,7 +2187,7 @@
         val zs = Jzs1 @ Jzs2;
         val frees = phis @ zs;
 
-        fun mk_Ids Id = if Id then map Id_const passiveAs else map mk_diag passive_UNIVs;
+        fun mk_Ids Id = if Id then map Id_const passiveAs else map mk_Id_on passive_UNIVs;
 
         fun mk_phi strong_eq phi z1 z2 = if strong_eq
           then Term.absfree (dest_Free z1) (Term.absfree (dest_Free z2)
@@ -2220,7 +2220,7 @@
           fold_rev Logic.all frees (Logic.list_implies (srel_prems, concl));
         val coinduct_params = rev (Term.add_tfrees dtor_srel_coinduct_goal []);
 
-        val dtor_srel_coinduct = unfold_thms lthy @{thms diag_UNIV}
+        val dtor_srel_coinduct = unfold_thms lthy @{thms Id_on_UNIV}
           (Skip_Proof.prove lthy [] [] dtor_srel_coinduct_goal
             (K (mk_dtor_srel_coinduct_tac ks raw_coind_thm bis_srel_thm))
           |> Thm.close_derivation);
@@ -2270,7 +2270,7 @@
           (Skip_Proof.prove lthy [] []
             (fold_rev Logic.all zs (Logic.list_implies (strong_prems, concl)))
             (K (mk_dtor_map_strong_coinduct_tac ks cTs cts dtor_map_coinduct bis_def
-              (tcoalg_thm RS bis_diag_thm))))
+              (tcoalg_thm RS bis_Id_on_thm))))
           |> Thm.close_derivation;
 
         val rel_of_srel_thms =
diff -r 14e6d761ba1c -r d2bc229e1f37 src/HOL/BNF/Tools/bnf_gfp_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Mon Mar 18 11:29:50 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Mon Mar 18 13:18:42 2013 +0100
@@ -270,7 +270,7 @@
             CONJ_WRAP' (fn (i, thm) =>
               if i <= m
               then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans,
-                etac @{thm image_mono}, rtac @{thm image_subsetI}, etac @{thm diagI}]
+                etac @{thm image_mono}, rtac @{thm image_subsetI}, etac @{thm Id_onI}]
               else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
                 rtac trans_fun_cong_image_id_id_apply, atac])
             (1 upto (m + n) ~~ set_naturals),
@@ -295,13 +295,13 @@
         REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
         REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
         rtac trans, rtac map_cong,
-        REPEAT_DETERM_N m o EVERY' [rtac @{thm diagE'}, etac set_mp, atac],
+        REPEAT_DETERM_N m o EVERY' [rtac @{thm Id_onD'}, etac set_mp, atac],
         REPEAT_DETERM_N n o rtac refl,
         etac sym, rtac CollectI,
         CONJ_WRAP' (fn (i, thm) =>
           if i <= m
           then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm image_subsetI},
-            rtac @{thm diag_fst}, etac set_mp, atac]
+            rtac @{thm Id_on_fst}, etac set_mp, atac]
           else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
             rtac trans_fun_cong_image_id_id_apply, atac])
         (1 upto (m + n) ~~ set_naturals)];
@@ -319,7 +319,7 @@
     CONJ_WRAP' (fn (srel_cong, srel_converse) =>
       EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm set_mp[OF equalityD2]},
         rtac (srel_cong RS trans),
-        REPEAT_DETERM_N m o rtac @{thm diag_converse},
+        REPEAT_DETERM_N m o rtac (@{thm converse_Id_on} RS sym),
         REPEAT_DETERM_N (length srel_congs) o rtac refl,
         rtac srel_converse,
         REPEAT_DETERM o etac allE,
@@ -332,7 +332,7 @@
     CONJ_WRAP' (fn (srel_cong, srel_O) =>
       EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm set_mp[OF equalityD2]},
         rtac (srel_cong RS trans),
-        REPEAT_DETERM_N m o rtac @{thm diag_Comp},
+        REPEAT_DETERM_N m o rtac @{thm Id_on_Comp},
         REPEAT_DETERM_N (length srel_congs) o rtac refl,
         rtac srel_O,
         etac @{thm relcompE},
@@ -343,7 +343,7 @@
 
 fun mk_bis_Gr_tac bis_srel srel_Grs mor_images morEs coalg_ins
   {context = ctxt, prems = _} =
-  unfold_thms_tac ctxt (bis_srel :: @{thm diag_Gr} :: srel_Grs) THEN
+  unfold_thms_tac ctxt (bis_srel :: @{thm Id_on_Gr} :: srel_Grs) THEN
   EVERY' [rtac conjI,
     CONJ_WRAP' (fn thm => rtac (@{thm Gr_incl} RS ssubst) THEN' etac thm) mor_images,
     CONJ_WRAP' (fn (coalg_in, morE) =>
@@ -383,12 +383,12 @@
     REPEAT_DETERM_N n o rtac exI, rtac conjI, rtac refl, atac, rtac equalityD2,
     rtac (mk_nth_conv n i)] 1;
 
-fun mk_equiv_lsbis_tac sbis_lsbis lsbis_incl incl_lsbis bis_diag bis_converse bis_O =
+fun mk_equiv_lsbis_tac sbis_lsbis lsbis_incl incl_lsbis bis_Id_on bis_converse bis_O =
   EVERY' [rtac (@{thm equiv_def} RS iffD2),
 
     rtac conjI, rtac (@{thm refl_on_def} RS iffD2),
     rtac conjI, rtac lsbis_incl, rtac ballI, rtac set_mp,
-    rtac incl_lsbis, rtac bis_diag, atac, etac @{thm diagI},
+    rtac incl_lsbis, rtac bis_Id_on, atac, etac @{thm Id_onI},
 
     rtac conjI, rtac (@{thm sym_def} RS iffD2),
     rtac allI, rtac allI, rtac impI, rtac set_mp,
@@ -1090,7 +1090,7 @@
           rtac @{thm xt1(3)}, rtac @{thm Sigma_cong},
           rtac @{thm proj_image}, rtac @{thm proj_image}, rtac lsbis_incl,
           rtac subset_trans, rtac @{thm relImage_mono}, rtac incl_lsbis, atac,
-          rtac @{thm relImage_proj}, rtac equiv_LSBIS, rtac @{thm relInvImage_diag},
+          rtac @{thm relImage_proj}, rtac equiv_LSBIS, rtac @{thm relInvImage_Id_on},
           rtac Rep_inject])
       (Rep_injects ~~ (equiv_LSBISs ~~ (incl_lsbiss ~~ lsbis_incls)))] 1
   end;
@@ -1163,16 +1163,16 @@
         rtac CollectI, etac (refl RSN (2, @{thm subst_Pair}))]) ks] 1
   end;
 
-fun mk_dtor_map_strong_coinduct_tac ks cTs cts dtor_map_coinduct bis_def bis_diag =
+fun mk_dtor_map_strong_coinduct_tac ks cTs cts dtor_map_coinduct bis_def bis_Id_on =
   EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts dtor_map_coinduct),
     EVERY' (map (fn i =>
       EVERY' [etac disjE, REPEAT_DETERM o dtac @{thm meta_spec}, etac meta_mp,
-        atac, rtac rev_mp, rtac subst, rtac bis_def, rtac bis_diag,
+        atac, rtac rev_mp, rtac subst, rtac bis_def, rtac bis_Id_on,
         rtac impI, dtac conjunct2, dtac (mk_conjunctN (length ks) i), REPEAT_DETERM o etac allE,
-        etac impE, etac @{thm diag_UNIV_I}, REPEAT_DETERM o eresolve_tac [bexE, conjE, CollectE],
+        etac impE, etac @{thm Id_on_UNIV_I}, REPEAT_DETERM o eresolve_tac [bexE, conjE, CollectE],
         rtac exI, rtac conjI, etac conjI, atac,
         CONJ_WRAP' (K (EVERY' [REPEAT_DETERM o resolve_tac [allI, impI],
-          rtac disjI2, rtac @{thm diagE}, etac set_mp, atac])) ks])
+          rtac disjI2, rtac @{thm Id_onD}, etac set_mp, atac])) ks])
     ks),
     rtac impI, REPEAT_DETERM o etac conjE,
     CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) ks] 1;
diff -r 14e6d761ba1c -r d2bc229e1f37 src/HOL/BNF/Tools/bnf_gfp_util.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_util.ML	Mon Mar 18 11:29:50 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_util.ML	Mon Mar 18 13:18:42 2013 +0100
@@ -18,7 +18,7 @@
   val mk_append: term * term -> term
   val mk_congruent: term -> term -> term
   val mk_clists: term -> term
-  val mk_diag: term -> term
+  val mk_Id_on: term -> term
   val mk_equiv: term -> term -> term
   val mk_fromCard: term -> term -> term
   val mk_list_rec: term -> term -> term
@@ -59,11 +59,11 @@
     val ABT = mk_relT (HOLogic.dest_setT AT, HOLogic.dest_setT (range_type BT));
   in Const (@{const_name Sigma}, AT --> BT --> ABT) $ A $ B end;
 
-fun mk_diag A =
+fun mk_Id_on A =
   let
     val AT = fastype_of A;
     val AAT = mk_relT (HOLogic.dest_setT AT, HOLogic.dest_setT AT);
-  in Const (@{const_name diag}, AT --> AAT) $ A end;
+  in Const (@{const_name Id_on}, AT --> AAT) $ A end;
 
 fun mk_Times (A, B) =
   let val AT = HOLogic.dest_setT (fastype_of A);
diff -r 14e6d761ba1c -r d2bc229e1f37 src/HOL/IMP/Live.thy
--- a/src/HOL/IMP/Live.thy	Mon Mar 18 11:29:50 2013 +0100
+++ b/src/HOL/IMP/Live.thy	Mon Mar 18 13:18:42 2013 +0100
@@ -9,7 +9,7 @@
 
 fun L :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where
 "L SKIP X = X" |
-"L (x ::= a) X = (X - {x}) \<union> vars a" |
+"L (x ::= a) X = vars a \<union> (X - {x})" |
 "L (c\<^isub>1; c\<^isub>2) X = L c\<^isub>1 (L c\<^isub>2 X)" |
 "L (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = vars b \<union> L c\<^isub>1 X \<union> L c\<^isub>2 X" |
 "L (WHILE b DO c) X = vars b \<union> X \<union> L c X"