--- 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
--- 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}}}
--- 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}
--- 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
--- 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
--- 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
--- 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)"
--- 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 =
--- 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;
--- 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);
--- 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"