--- a/src/HOL/IMP/Abs_Int2_ivl.thy Fri Sep 06 10:56:40 2013 +0200
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy Fri Sep 06 10:56:40 2013 +0200
@@ -55,7 +55,7 @@
lift_definition is_empty_ivl :: "ivl \<Rightarrow> bool" is is_empty_rep
apply(auto simp: eq_ivl_def \<gamma>_rep_cases is_empty_rep_def)
-apply(auto simp: not_less less_eq_extended_cases split: extended.splits)
+apply(auto simp: not_less less_eq_extended_case split: extended.splits)
done
lemma eq_ivl_iff: "eq_ivl p1 p2 = (is_empty_rep p1 & is_empty_rep p2 | p1 = p2)"
--- a/src/HOL/Library/Extended.thy Fri Sep 06 10:56:40 2013 +0200
+++ b/src/HOL/Library/Extended.thy Fri Sep 06 10:56:40 2013 +0200
@@ -5,14 +5,13 @@
*)
theory Extended
-imports Main
+imports
+ Main
+ "~~/src/HOL/Library/Simps_Case_Conv"
begin
datatype 'a extended = Fin 'a | Pinf ("\<infinity>") | Minf ("-\<infinity>")
-lemmas extended_cases2 = extended.exhaust[case_product extended.exhaust]
-lemmas extended_cases3 = extended.exhaust[case_product extended_cases2]
-
instantiation extended :: (order)order
begin
@@ -23,31 +22,18 @@
"Minf \<le> _ = True" |
"(_::'a extended) \<le> _ = False"
-lemma less_eq_extended_cases:
- "x \<le> y = (case x of Fin x \<Rightarrow> (case y of Fin y \<Rightarrow> x \<le> y | Pinf \<Rightarrow> True | Minf \<Rightarrow> False)
- | Pinf \<Rightarrow> y=Pinf | Minf \<Rightarrow> True)"
-by(induct x y rule: less_eq_extended.induct)(auto split: extended.split)
+case_of_simps less_eq_extended_case: less_eq_extended.simps
definition less_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> bool" where
"((x::'a extended) < y) = (x \<le> y & \<not> x \<ge> y)"
instance
-proof
- case goal1 show ?case by(rule less_extended_def)
-next
- case goal2 show ?case by(cases x) auto
-next
- case goal3 thus ?case by(auto simp: less_eq_extended_cases split:extended.splits)
-next
- case goal4 thus ?case by(auto simp: less_eq_extended_cases split:extended.splits)
-qed
+ by intro_classes (auto simp: less_extended_def less_eq_extended_case split: extended.splits)
end
instance extended :: (linorder)linorder
-proof
- case goal1 thus ?case by(auto simp: less_eq_extended_cases split:extended.splits)
-qed
+ by intro_classes (auto simp: less_eq_extended_case split:extended.splits)
lemma Minf_le[simp]: "Minf \<le> y"
by(cases y) auto
@@ -114,26 +100,19 @@
"Minf + Pinf = Pinf" |
"Pinf + Minf = Pinf"
+case_of_simps plus_case: plus_extended.simps
+
instance ..
end
+
instance extended :: (ab_semigroup_add)ab_semigroup_add
-proof
- fix a b c :: "'a extended"
- show "a + b = b + a"
- by (induct a b rule: plus_extended.induct) (simp_all add: ac_simps)
- show "a + b + c = a + (b + c)"
- by (cases rule: extended_cases3[of a b c]) (simp_all add: ac_simps)
-qed
+ by intro_classes (simp_all add: ac_simps plus_case split: extended.splits)
instance extended :: (ordered_ab_semigroup_add)ordered_ab_semigroup_add
-proof
- fix a b c :: "'a extended"
- assume "a \<le> b" then show "c + a \<le> c + b"
- by (cases rule: extended_cases3[of a b c]) (auto simp: add_left_mono)
-qed
+ by intro_classes (auto simp: add_left_mono plus_case split: extended.splits)
instance extended :: (comm_monoid_add)comm_monoid_add
proof
@@ -206,16 +185,12 @@
"sup_extended Minf a = a" |
"sup_extended a Minf = a"
+case_of_simps inf_extended_case: inf_extended.simps
+case_of_simps sup_extended_case: sup_extended.simps
+
instance
-proof
- fix x y z ::"'a extended"
- show "inf x y \<le> x" "inf x y \<le> y" "\<lbrakk>x \<le> y; x \<le> z\<rbrakk> \<Longrightarrow> x \<le> inf y z"
- "x \<le> sup x y" "y \<le> sup x y" "\<lbrakk>y \<le> x; z \<le> x\<rbrakk> \<Longrightarrow> sup y z \<le> x" "bot \<le> x" "x \<le> top"
- apply (atomize (full))
- apply (cases rule: extended_cases3[of x y z])
- apply (auto simp: bot_extended_def top_extended_def)
- done
-qed
+ by (intro_classes) (auto simp: inf_extended_case sup_extended_case less_eq_extended_case
+ bot_extended_def top_extended_def split: extended.splits)
end
end