--- a/src/HOL/IMP/Abs_Int0.thy Tue Sep 15 11:18:25 2015 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy Tue Sep 15 17:09:13 2015 +0200
@@ -31,14 +31,15 @@
lemma Some_le[simp]: "(Some x \<le> u) = (\<exists>y. u = Some y \<and> x \<le> y)"
by (cases u) auto
-instance proof
- case goal1 show ?case by(rule less_option_def)
+instance
+proof (standard, goal_cases)
+ case 1 show ?case by(rule less_option_def)
next
- case goal2 show ?case by(cases x, simp_all)
+ case (2 x) show ?case by(cases x, simp_all)
next
- case goal3 thus ?case by(cases z, simp, cases y, simp, cases x, auto)
+ case (3 x y z) thus ?case by(cases z, simp, cases y, simp, cases x, auto)
next
- case goal4 thus ?case by(cases y, simp, cases x, auto)
+ case (4 x y) thus ?case by(cases y, simp, cases x, auto)
qed
end
@@ -63,14 +64,15 @@
definition top_option where "\<top> = Some \<top>"
-instance proof
- case goal4 show ?case by(cases a, simp_all add: top_option_def)
+instance
+proof (standard, goal_cases)
+ case (4 a) show ?case by(cases a, simp_all add: top_option_def)
next
- case goal1 thus ?case by(cases x, simp, cases y, simp_all)
+ case (1 x y) thus ?case by(cases x, simp, cases y, simp_all)
next
- case goal2 thus ?case by(cases y, simp, cases x, simp_all)
+ case (2 x y) thus ?case by(cases y, simp, cases x, simp_all)
next
- case goal3 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
+ case (3 x y z) thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
qed
end
@@ -85,8 +87,8 @@
"\<bottom> = None"
instance
-proof
- case goal1 thus ?case by(auto simp: bot_option_def)
+proof (standard, goal_cases)
+ case 1 thus ?case by(auto simp: bot_option_def)
qed
end
--- a/src/HOL/IMP/Abs_Int1_const.thy Tue Sep 15 11:18:25 2015 +0200
+++ b/src/HOL/IMP/Abs_Int1_const.thy Tue Sep 15 17:09:13 2015 +0200
@@ -32,22 +32,22 @@
definition "\<top> = Any"
instance
-proof
- case goal1 thus ?case by (rule less_const_def)
+proof (standard, goal_cases)
+ case 1 thus ?case by (rule less_const_def)
next
- case goal2 show ?case by (cases x) simp_all
+ case (2 x) show ?case by (cases x) simp_all
next
- case goal3 thus ?case by(cases z, cases y, cases x, simp_all)
+ case (3 x y z) thus ?case by(cases z, cases y, cases x, simp_all)
next
- case goal4 thus ?case by(cases x, cases y, simp_all, cases y, simp_all)
+ case (4 x y) thus ?case by(cases x, cases y, simp_all, cases y, simp_all)
next
- case goal6 thus ?case by(cases x, cases y, simp_all)
+ case (6 x y) thus ?case by(cases x, cases y, simp_all)
next
- case goal5 thus ?case by(cases y, cases x, simp_all)
+ case (5 x y) thus ?case by(cases y, cases x, simp_all)
next
- case goal7 thus ?case by(cases z, cases y, cases x, simp_all)
+ case (7 x y z) thus ?case by(cases z, cases y, cases x, simp_all)
next
- case goal8 thus ?case by(simp add: top_const_def)
+ case 8 thus ?case by(simp add: top_const_def)
qed
end
@@ -55,16 +55,15 @@
permanent_interpretation Val_semilattice
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
-proof
- case goal1 thus ?case
+proof (standard, goal_cases)
+ case (1 a b) thus ?case
by(cases a, cases b, simp, simp, cases b, simp, simp)
next
- case goal2 show ?case by(simp add: top_const_def)
+ case 2 show ?case by(simp add: top_const_def)
next
- case goal3 show ?case by simp
+ case 3 show ?case by simp
next
- case goal4 thus ?case
- by(auto simp: plus_const_cases split: const.split)
+ case 4 thus ?case by(auto simp: plus_const_cases split: const.split)
qed
permanent_interpretation Abs_Int
@@ -123,9 +122,8 @@
permanent_interpretation Abs_Int_mono
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
-proof
- case goal1 thus ?case
- by(auto simp: plus_const_cases split: const.split)
+proof (standard, goal_cases)
+ case 1 thus ?case by(auto simp: plus_const_cases split: const.split)
qed
text{* Termination: *}
@@ -136,10 +134,10 @@
permanent_interpretation Abs_Int_measure
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
and m = m_const and h = "1"
-proof
- case goal1 thus ?case by(auto simp: m_const_def split: const.splits)
+proof (standard, goal_cases)
+ case 1 thus ?case by(auto simp: m_const_def split: const.splits)
next
- case goal2 thus ?case by(auto simp: m_const_def less_const_def split: const.splits)
+ case 2 thus ?case by(auto simp: m_const_def less_const_def split: const.splits)
qed
thm AI_Some_measure
--- a/src/HOL/IMP/Abs_Int1_parity.thy Tue Sep 15 11:18:25 2015 +0200
+++ b/src/HOL/IMP/Abs_Int1_parity.thy Tue Sep 15 17:09:13 2015 +0200
@@ -58,21 +58,21 @@
definition top_parity where
"\<top> = Either"
-text{* Now the instance proof. This time we take a lazy shortcut: we do not
-write out the proof obligations but use the @{text goali} primitive to refer
-to the assumptions of subgoal i and @{text "case?"} to refer to the
-conclusion of subgoal i. The class axioms are presented in the same order as
-in the class definition. Warning: this is brittle! *}
+text{* Now the instance proof. This time we take a shortcut with the help of
+proof method @{text goal_cases}: it creates cases 1 ... n for the subgoals
+1 ... n; in case i, i is also the name of the assumptions of subgoal i and
+@{text "case?"} refers to the conclusion of subgoal i.
+The class axioms are presented in the same order as in the class definition. *}
instance
-proof
- case goal1 (*sup1*) show ?case by(auto simp: less_eq_parity_def sup_parity_def)
+proof (standard, goal_cases)
+ case 1 (*sup1*) show ?case by(auto simp: less_eq_parity_def sup_parity_def)
next
- case goal2 (*sup2*) show ?case by(auto simp: less_eq_parity_def sup_parity_def)
+ case 2 (*sup2*) show ?case by(auto simp: less_eq_parity_def sup_parity_def)
next
- case goal3 (*sup least*) thus ?case by(auto simp: less_eq_parity_def sup_parity_def)
+ case 3 (*sup least*) thus ?case by(auto simp: less_eq_parity_def sup_parity_def)
next
- case goal4 (*top*) show ?case by(auto simp: less_eq_parity_def top_parity_def)
+ case 4 (*top*) show ?case by(auto simp: less_eq_parity_def top_parity_def)
qed
end
@@ -104,21 +104,22 @@
permanent_interpretation Val_semilattice
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
-proof txt{* of the locale axioms *}
- fix a b :: parity
- assume "a \<le> b" thus "\<gamma>_parity a \<subseteq> \<gamma>_parity b"
- by(auto simp: less_eq_parity_def)
-next txt{* The rest in the lazy, implicit way *}
- case goal2 show ?case by(auto simp: top_parity_def)
+proof (standard, goal_cases) txt{* subgoals are the locale axioms *}
+ case 1 thus ?case by(auto simp: less_eq_parity_def)
next
- case goal3 show ?case by auto
+ case 2 show ?case by(auto simp: top_parity_def)
next
- txt{* Warning: this subproof refers to the names @{text a1} and @{text a2}
- from the statement of the axiom. *}
- case goal4 thus ?case
+ case 3 show ?case by auto
+next
+ case (4 _ a1 _ a2) thus ?case
by (induction a1 a2 rule: plus_parity.induct) (auto simp add:mod_add_eq)
qed
+text{* In case 4 we needed to refer to particular variables.
+Writing (i x y z) fixes the names of the variables in case i to be x, y and z
+in the left-to-right order in which the variables occur in the subgoal.
+Underscores are anonymous placeholders for variable names we don't care to fix. *}
+
text{* Instantiating the abstract interpretation locale requires no more
proofs (they happened in the instatiation above) but delivers the
instantiated abstract interpreter which we call @{text AI_parity}: *}
@@ -156,8 +157,8 @@
permanent_interpretation Abs_Int_mono
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
-proof
- case goal1 thus ?case
+proof (standard, goal_cases)
+ case (1 _ a1 _ a2) thus ?case
by(induction a1 a2 rule: plus_parity.induct)
(auto simp add:less_eq_parity_def)
qed
@@ -168,10 +169,10 @@
permanent_interpretation Abs_Int_measure
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
and m = m_parity and h = "1"
-proof
- case goal1 thus ?case by(auto simp add: m_parity_def less_eq_parity_def)
+proof (standard, goal_cases)
+ case 1 thus ?case by(auto simp add: m_parity_def less_eq_parity_def)
next
- case goal2 thus ?case by(auto simp add: m_parity_def less_eq_parity_def less_parity_def)
+ case 2 thus ?case by(auto simp add: m_parity_def less_eq_parity_def less_parity_def)
qed
thm AI_Some_measure
--- a/src/HOL/IMP/Abs_Int2.thy Tue Sep 15 11:18:25 2015 +0200
+++ b/src/HOL/IMP/Abs_Int2.thy Tue Sep 15 17:09:13 2015 +0200
@@ -11,14 +11,14 @@
definition "less_prod p1 p2 = (p1 \<le> p2 \<and> \<not> p2 \<le> (p1::'a*'b))"
instance
-proof
- case goal1 show ?case by(rule less_prod_def)
+proof (standard, goal_cases)
+ case 1 show ?case by(rule less_prod_def)
next
- case goal2 show ?case by(simp add: less_eq_prod_def)
+ case 2 show ?case by(simp add: less_eq_prod_def)
next
- case goal3 thus ?case unfolding less_eq_prod_def by(metis order_trans)
+ case 3 thus ?case unfolding less_eq_prod_def by(metis order_trans)
next
- case goal4 thus ?case by(simp add: less_eq_prod_def)(metis eq_iff surjective_pairing)
+ case 4 thus ?case by(simp add: less_eq_prod_def)(metis eq_iff surjective_pairing)
qed
end
--- a/src/HOL/IMP/Abs_Int2_ivl.thy Tue Sep 15 11:18:25 2015 +0200
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy Tue Sep 15 17:09:13 2015 +0200
@@ -104,22 +104,22 @@
by(auto simp add: is_empty_rep_def max_def min_def split: if_splits)
instance
-proof
- case goal1 show ?case by (rule less_ivl_def)
+proof (standard, goal_cases)
+ case 1 show ?case by (rule less_ivl_def)
next
- case goal2 show ?case by transfer (simp add: le_rep_def split: prod.splits)
+ case 2 show ?case by transfer (simp add: le_rep_def split: prod.splits)
next
- case goal3 thus ?case by transfer (auto simp: le_rep_def split: if_splits)
+ case 3 thus ?case by transfer (auto simp: le_rep_def split: if_splits)
next
- case goal4 thus ?case by transfer (auto simp: le_rep_def eq_ivl_iff split: if_splits)
+ case 4 thus ?case by transfer (auto simp: le_rep_def eq_ivl_iff split: if_splits)
next
- case goal5 thus ?case by transfer (auto simp add: le_rep_def sup_rep_def is_empty_min_max)
+ case 5 thus ?case by transfer (auto simp add: le_rep_def sup_rep_def is_empty_min_max)
next
- case goal6 thus ?case by transfer (auto simp add: le_rep_def sup_rep_def is_empty_min_max)
+ case 6 thus ?case by transfer (auto simp add: le_rep_def sup_rep_def is_empty_min_max)
next
- case goal7 thus ?case by transfer (auto simp add: le_rep_def sup_rep_def)
+ case 7 thus ?case by transfer (auto simp add: le_rep_def sup_rep_def)
next
- case goal8 show ?case by transfer (simp add: le_rep_def is_empty_rep_def)
+ case 8 show ?case by transfer (simp add: le_rep_def is_empty_rep_def)
qed
end
@@ -132,8 +132,8 @@
"equal_ivl i1 (i2::ivl) = (i1\<le>i2 \<and> i2 \<le> i1)"
instance
-proof
- case goal1 show ?case by(simp add: equal_ivl_def eq_iff)
+proof (standard, goal_cases)
+ case 1 show ?case by(simp add: equal_ivl_def eq_iff)
qed
end
@@ -161,14 +161,14 @@
definition "\<bottom> = empty_ivl"
instance
-proof
- case goal1 thus ?case by (simp add: \<gamma>_inf le_ivl_iff_subset)
+proof (standard, goal_cases)
+ case 1 thus ?case by (simp add: \<gamma>_inf le_ivl_iff_subset)
next
- case goal2 thus ?case by (simp add: \<gamma>_inf le_ivl_iff_subset)
+ case 2 thus ?case by (simp add: \<gamma>_inf le_ivl_iff_subset)
next
- case goal3 thus ?case by (simp add: \<gamma>_inf le_ivl_iff_subset)
+ case 3 thus ?case by (simp add: \<gamma>_inf le_ivl_iff_subset)
next
- case goal4 show ?case
+ case 4 show ?case
unfolding bot_ivl_def by transfer (auto simp: le_iff_subset)
qed
@@ -304,14 +304,14 @@
permanent_interpretation Val_semilattice
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
-proof
- case goal1 thus ?case by transfer (simp add: le_iff_subset)
+proof (standard, goal_cases)
+ case 1 thus ?case by transfer (simp add: le_iff_subset)
next
- case goal2 show ?case by transfer (simp add: \<gamma>_rep_def)
+ case 2 show ?case by transfer (simp add: \<gamma>_rep_def)
next
- case goal3 show ?case by transfer (simp add: \<gamma>_rep_def)
+ case 3 show ?case by transfer (simp add: \<gamma>_rep_def)
next
- case goal4 thus ?case
+ case 4 thus ?case
apply transfer
apply(auto simp: \<gamma>_rep_def plus_rep_def add_mono_le_Fin add_mono_Fin_le)
by(auto simp: empty_rep_def is_empty_rep_def)
@@ -321,26 +321,26 @@
permanent_interpretation Val_lattice_gamma
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
defining aval_ivl = aval'
-proof
- case goal1 show ?case by(simp add: \<gamma>_inf)
+proof (standard, goal_cases)
+ case 1 show ?case by(simp add: \<gamma>_inf)
next
- case goal2 show ?case unfolding bot_ivl_def by transfer simp
+ case 2 show ?case unfolding bot_ivl_def by transfer simp
qed
permanent_interpretation Val_inv
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
and test_num' = in_ivl
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
-proof
- case goal1 thus ?case by transfer (auto simp: \<gamma>_rep_def)
+proof (standard, goal_cases)
+ case 1 thus ?case by transfer (auto simp: \<gamma>_rep_def)
next
- case goal2 thus ?case
+ case (2 _ _ _ _ _ i1 i2) thus ?case
unfolding inv_plus_ivl_def minus_ivl_def
apply(clarsimp simp add: \<gamma>_inf)
using gamma_plus'[of "i1+i2" _ "-i1"] gamma_plus'[of "i1+i2" _ "-i2"]
by(simp add: \<gamma>_uminus)
next
- case goal3 thus ?case
+ case (3 i1 i2) thus ?case
unfolding inv_less_ivl_def minus_ivl_def one_extended_def
apply(clarsimp simp add: \<gamma>_inf split: if_splits)
using gamma_plus'[of "i1+1" _ "-1"] gamma_plus'[of "i2 - 1" _ "1"]
@@ -388,14 +388,14 @@
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
and test_num' = in_ivl
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
-proof
- case goal1 thus ?case by (rule mono_plus_ivl)
+proof (standard, goal_cases)
+ case 1 thus ?case by (rule mono_plus_ivl)
next
- case goal2 thus ?case
+ case 2 thus ?case
unfolding inv_plus_ivl_def minus_ivl_def less_eq_prod_def
by (auto simp: le_infI1 le_infI2 mono_plus_ivl mono_minus_ivl)
next
- case goal3 thus ?case
+ case 3 thus ?case
unfolding less_eq_prod_def inv_less_ivl_def minus_ivl_def
by (auto simp: le_infI1 le_infI2 mono_plus_ivl mono_above mono_below)
qed
--- a/src/HOL/IMP/Abs_Int3.thy Tue Sep 15 11:18:25 2015 +0200
+++ b/src/HOL/IMP/Abs_Int3.thy Tue Sep 15 17:09:13 2015 +0200
@@ -63,18 +63,14 @@
by(auto simp: eq_st_def)
instance
-proof
- case goal1 thus ?case
- by transfer (simp add: less_eq_st_rep_iff widen1)
+proof (standard, goal_cases)
+ case 1 thus ?case by transfer (simp add: less_eq_st_rep_iff widen1)
next
- case goal2 thus ?case
- by transfer (simp add: less_eq_st_rep_iff widen2)
+ case 2 thus ?case by transfer (simp add: less_eq_st_rep_iff widen2)
next
- case goal3 thus ?case
- by transfer (simp add: less_eq_st_rep_iff narrow1)
+ case 3 thus ?case by transfer (simp add: less_eq_st_rep_iff narrow1)
next
- case goal4 thus ?case
- by transfer (simp add: less_eq_st_rep_iff narrow2)
+ case 4 thus ?case by transfer (simp add: less_eq_st_rep_iff narrow2)
qed
end
@@ -94,17 +90,17 @@
"(Some x) \<triangle> (Some y) = Some(x \<triangle> y)"
instance
-proof
- case goal1 thus ?case
+proof (standard, goal_cases)
+ case (1 x y) thus ?case
by(induct x y rule: widen_option.induct)(simp_all add: widen1)
next
- case goal2 thus ?case
+ case (2 x y) thus ?case
by(induct x y rule: widen_option.induct)(simp_all add: widen2)
next
- case goal3 thus ?case
+ case (3 x y) thus ?case
by(induct x y rule: narrow_option.induct) (simp_all add: narrow1)
next
- case goal4 thus ?case
+ case (4 y x) thus ?case
by(induct x y rule: narrow_option.induct) (simp_all add: narrow2)
qed
@@ -550,14 +546,14 @@
and test_num' = in_ivl
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
and m = m_ivl and n = n_ivl and h = 3
-proof
- case goal2 thus ?case by(rule m_ivl_anti_mono)
+proof (standard, goal_cases)
+ case 2 thus ?case by(rule m_ivl_anti_mono)
next
- case goal1 thus ?case by(rule m_ivl_height)
+ case 1 thus ?case by(rule m_ivl_height)
next
- case goal3 thus ?case by(rule m_ivl_widen)
+ case 3 thus ?case by(rule m_ivl_widen)
next
- case goal4 from goal4(2) show ?case by(rule n_ivl_narrow)
+ case 4 from 4(2) show ?case by(rule n_ivl_narrow)
-- "note that the first assms is unnecessary for intervals"
qed
--- a/src/HOL/IMP/Abs_State.thy Tue Sep 15 11:18:25 2015 +0200
+++ b/src/HOL/IMP/Abs_State.thy Tue Sep 15 17:09:13 2015 +0200
@@ -66,15 +66,14 @@
definition less_st where "F < (G::'a st) = (F \<le> G \<and> \<not> G \<le> F)"
instance
-proof
- case goal1 show ?case by(rule less_st_def)
-next
- case goal2 show ?case by transfer (auto simp: less_eq_st_rep_def)
+proof (standard, goal_cases)
+ case 1 show ?case by(rule less_st_def)
next
- case goal3 thus ?case
- by transfer (metis less_eq_st_rep_iff order_trans)
+ case 2 show ?case by transfer (auto simp: less_eq_st_rep_def)
next
- case goal4 thus ?case
+ case 3 thus ?case by transfer (metis less_eq_st_rep_iff order_trans)
+next
+ case 4 thus ?case
by transfer (metis less_eq_st_rep_iff eq_st_def fun_eq_iff antisym)
qed
@@ -105,15 +104,14 @@
lift_definition top_st :: "'a st" is "[]" .
instance
-proof
- case goal1 show ?case by transfer (simp add:less_eq_st_rep_iff)
-next
- case goal2 show ?case by transfer (simp add:less_eq_st_rep_iff)
+proof (standard, goal_cases)
+ case 1 show ?case by transfer (simp add:less_eq_st_rep_iff)
next
- case goal3 thus ?case by transfer (simp add:less_eq_st_rep_iff)
+ case 2 show ?case by transfer (simp add:less_eq_st_rep_iff)
next
- case goal4 show ?case
- by transfer (simp add:less_eq_st_rep_iff fun_rep_map_of)
+ case 3 thus ?case by transfer (simp add:less_eq_st_rep_iff)
+next
+ case 4 show ?case by transfer (simp add:less_eq_st_rep_iff fun_rep_map_of)
qed
end
--- a/src/HOL/IMP/Collecting.thy Tue Sep 15 11:18:25 2015 +0200
+++ b/src/HOL/IMP/Collecting.thy Tue Sep 15 17:09:13 2015 +0200
@@ -45,14 +45,14 @@
"less_acom x y = (x \<le> y \<and> \<not> y \<le> x)"
instance
-proof
- case goal1 show ?case by(simp add: less_acom_def)
+proof (standard, goal_cases)
+ case 1 show ?case by(simp add: less_acom_def)
next
- case goal2 thus ?case by(auto simp: less_eq_acom_def)
+ case 2 thus ?case by(auto simp: less_eq_acom_def)
next
- case goal3 thus ?case by(fastforce simp: less_eq_acom_def size_annos)
+ case 3 thus ?case by(fastforce simp: less_eq_acom_def size_annos)
next
- case goal4 thus ?case
+ case 4 thus ?case
by(fastforce simp: le_antisym less_eq_acom_def size_annos
eq_acom_iff_strip_anno)
qed
@@ -97,14 +97,14 @@
permanent_interpretation
Complete_Lattice "{C. strip C = c}" "Inf_acom c" for c
-proof
- case goal1 thus ?case
+proof (standard, goal_cases)
+ case 1 thus ?case
by(auto simp: Inf_acom_def less_eq_acom_def size_annos intro:INF_lower)
next
- case goal2 thus ?case
+ case 2 thus ?case
by(auto simp: Inf_acom_def less_eq_acom_def size_annos intro:INF_greatest)
next
- case goal3 thus ?case by(auto simp: Inf_acom_def)
+ case 3 thus ?case by(auto simp: Inf_acom_def)
qed