--- a/src/HOL/HOLCF/Compact_Basis.thy Tue Dec 17 15:35:46 2024 +0100
+++ b/src/HOL/HOLCF/Compact_Basis.thy Tue Dec 17 23:07:13 2024 +0100
@@ -68,7 +68,7 @@
lemma PDPlus_absorb: "PDPlus t t = t"
unfolding Rep_pd_basis_inject [symmetric] Rep_PDPlus by (rule Un_absorb)
-lemma pd_basis_induct1:
+lemma pd_basis_induct1 [case_names PDUnit PDPlus]:
assumes PDUnit: "\<And>a. P (PDUnit a)"
assumes PDPlus: "\<And>a t. P t \<Longrightarrow> P (PDPlus (PDUnit a) t)"
shows "P x"
@@ -87,7 +87,7 @@
qed
qed
-lemma pd_basis_induct:
+lemma pd_basis_induct [case_names PDUnit PDPlus]:
assumes PDUnit: "\<And>a. P (PDUnit a)"
assumes PDPlus: "\<And>t u. \<lbrakk>P t; P u\<rbrakk> \<Longrightarrow> P (PDPlus t u)"
shows "P x"
--- a/src/HOL/HOLCF/ConvexPD.thy Tue Dec 17 15:35:46 2024 +0100
+++ b/src/HOL/HOLCF/ConvexPD.thy Tue Dec 17 23:07:13 2024 +0100
@@ -92,10 +92,7 @@
apply fast
done
show "t \<le>\<natural> ?v" "u \<le>\<natural> ?w"
- apply (insert z)
- apply (simp_all add: convex_le_def upper_le_def lower_le_def Rep_PDPlus Rep_v Rep_w)
- apply fast+
- done
+ using z by (simp_all add: convex_le_def upper_le_def lower_le_def Rep_PDPlus Rep_v Rep_w) fast+
qed
lemma convex_le_induct [induct set: convex_le]:
@@ -104,17 +101,24 @@
assumes 3: "\<And>a b. a \<sqsubseteq> b \<Longrightarrow> P (PDUnit a) (PDUnit b)"
assumes 4: "\<And>t u v w. \<lbrakk>P t v; P u w\<rbrakk> \<Longrightarrow> P (PDPlus t u) (PDPlus v w)"
shows "P t u"
-using le apply (induct t arbitrary: u rule: pd_basis_induct)
-apply (erule rev_mp)
-apply (induct_tac u rule: pd_basis_induct1)
-apply (simp add: 3)
-apply (simp, clarify, rename_tac a b t)
-apply (subgoal_tac "P (PDPlus (PDUnit a) (PDUnit a)) (PDPlus (PDUnit b) t)")
-apply (simp add: PDPlus_absorb)
-apply (erule (1) 4 [OF 3])
-apply (drule convex_le_PDPlus_lemma, clarify)
-apply (simp add: 4)
-done
+ using le
+proof (induct t arbitrary: u rule: pd_basis_induct)
+ case (PDUnit a)
+ then show ?case
+ proof (induct u rule: pd_basis_induct1)
+ case (PDUnit b)
+ then show ?case by (simp add: 3)
+ next
+ case (PDPlus b t)
+ have "P (PDPlus (PDUnit a) (PDUnit a)) (PDPlus (PDUnit b) t)"
+ by (rule 4 [OF 3]) (use PDPlus in simp_all)
+ then show ?case by (simp add: PDPlus_absorb)
+ qed
+next
+ case PDPlus
+ from PDPlus(1,2) show ?case
+ using convex_le_PDPlus_lemma [OF PDPlus(3)] by (auto simp add: 4)
+qed
subsection \<open>Type definition\<close>
@@ -281,26 +285,34 @@
assumes unit: "\<And>x. P {x}\<natural>"
assumes insert: "\<And>x ys. \<lbrakk>P {x}\<natural>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<natural> \<union>\<natural> ys)"
shows "P (xs::'a::bifinite convex_pd)"
-apply (induct xs rule: convex_pd.principal_induct, rule P)
-apply (induct_tac a rule: pd_basis_induct1)
-apply (simp only: convex_unit_Rep_compact_basis [symmetric])
-apply (rule unit)
-apply (simp only: convex_unit_Rep_compact_basis [symmetric]
- convex_plus_principal [symmetric])
-apply (erule insert [OF unit])
-done
+proof (induct xs rule: convex_pd.principal_induct)
+ show "P (convex_principal a)" for a
+ proof (induct a rule: pd_basis_induct1)
+ case PDUnit
+ show ?case by (simp only: convex_unit_Rep_compact_basis [symmetric]) (rule unit)
+ next
+ case PDPlus
+ show ?case
+ by (simp only: convex_unit_Rep_compact_basis [symmetric] convex_plus_principal [symmetric])
+ (rule insert [OF unit PDPlus])
+ qed
+qed (rule P)
-lemma convex_pd_induct
- [case_names adm convex_unit convex_plus, induct type: convex_pd]:
+lemma convex_pd_induct [case_names adm convex_unit convex_plus, induct type: convex_pd]:
assumes P: "adm P"
assumes unit: "\<And>x. P {x}\<natural>"
assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs \<union>\<natural> ys)"
shows "P (xs::'a::bifinite convex_pd)"
-apply (induct xs rule: convex_pd.principal_induct, rule P)
-apply (induct_tac a rule: pd_basis_induct)
-apply (simp only: convex_unit_Rep_compact_basis [symmetric] unit)
-apply (simp only: convex_plus_principal [symmetric] plus)
-done
+proof (induct xs rule: convex_pd.principal_induct)
+ show "P (convex_principal a)" for a
+ proof (induct a rule: pd_basis_induct)
+ case PDUnit
+ then show ?case by (simp only: convex_unit_Rep_compact_basis [symmetric] unit)
+ next
+ case PDPlus
+ then show ?case by (simp only: convex_plus_principal [symmetric] plus)
+ qed
+qed (rule P)
subsection \<open>Monadic bind\<close>
--- a/src/HOL/HOLCF/LowerPD.thy Tue Dec 17 15:35:46 2024 +0100
+++ b/src/HOL/HOLCF/LowerPD.thy Tue Dec 17 23:07:13 2024 +0100
@@ -59,17 +59,33 @@
assumes 2: "\<And>t u a. P (PDUnit a) t \<Longrightarrow> P (PDUnit a) (PDPlus t u)"
assumes 3: "\<And>t u v. \<lbrakk>P t v; P u v\<rbrakk> \<Longrightarrow> P (PDPlus t u) v"
shows "P t u"
-using le
-apply (induct t arbitrary: u rule: pd_basis_induct)
-apply (erule rev_mp)
-apply (induct_tac u rule: pd_basis_induct)
-apply (simp add: 1)
-apply (simp add: lower_le_PDUnit_PDPlus_iff)
-apply (simp add: 2)
-apply (subst PDPlus_commute)
-apply (simp add: 2)
-apply (simp add: lower_le_PDPlus_iff 3)
-done
+ using le
+proof (induct t arbitrary: u rule: pd_basis_induct)
+ case (PDUnit a)
+ then show ?case
+ proof (induct u rule: pd_basis_induct)
+ case PDUnit
+ then show ?case by (simp add: 1)
+ next
+ case (PDPlus t u)
+ from PDPlus(3) consider (t) "PDUnit a \<le>\<flat> t" | (u) "PDUnit a \<le>\<flat> u"
+ by (auto simp: lower_le_PDUnit_PDPlus_iff)
+ then show ?case
+ proof cases
+ case t
+ then have "P (PDUnit a) t" by (rule PDPlus(1))
+ then show ?thesis by (rule 2)
+ next
+ case u
+ then have "P (PDUnit a) u" by (rule PDPlus(2))
+ then have "P (PDUnit a) (PDPlus u t)" by (rule 2)
+ then show ?thesis by (simp only: PDPlus_commute)
+ qed
+ qed
+next
+ case (PDPlus t t')
+ then show ?case by (simp add: lower_le_PDPlus_iff 3)
+qed
subsection \<open>Type definition\<close>
@@ -271,29 +287,42 @@
lemma lower_pd_induct1:
assumes P: "adm P"
assumes unit: "\<And>x. P {x}\<flat>"
- assumes insert:
- "\<And>x ys. \<lbrakk>P {x}\<flat>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<flat> \<union>\<flat> ys)"
+ assumes insert: "\<And>x ys. \<lbrakk>P {x}\<flat>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<flat> \<union>\<flat> ys)"
shows "P (xs::'a::bifinite lower_pd)"
-apply (induct xs rule: lower_pd.principal_induct, rule P)
-apply (induct_tac a rule: pd_basis_induct1)
-apply (simp only: lower_unit_Rep_compact_basis [symmetric])
-apply (rule unit)
-apply (simp only: lower_unit_Rep_compact_basis [symmetric]
- lower_plus_principal [symmetric])
-apply (erule insert [OF unit])
-done
+proof (induct xs rule: lower_pd.principal_induct)
+ have *: "P {Rep_compact_basis a}\<flat>" for a
+ by (rule unit)
+ show "P (lower_principal a)" for a
+ proof (induct a rule: pd_basis_induct1)
+ case PDUnit
+ from * show ?case
+ by (simp only: lower_unit_Rep_compact_basis [symmetric])
+ next
+ case (PDPlus a t)
+ with * have "P ({Rep_compact_basis a}\<flat> \<union>\<flat> lower_principal t)"
+ by (rule insert)
+ then show ?case
+ by (simp only: lower_unit_Rep_compact_basis [symmetric] lower_plus_principal [symmetric])
+ qed
+qed (rule P)
-lemma lower_pd_induct
- [case_names adm lower_unit lower_plus, induct type: lower_pd]:
+lemma lower_pd_induct [case_names adm lower_unit lower_plus, induct type: lower_pd]:
assumes P: "adm P"
assumes unit: "\<And>x. P {x}\<flat>"
assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs \<union>\<flat> ys)"
shows "P (xs::'a::bifinite lower_pd)"
-apply (induct xs rule: lower_pd.principal_induct, rule P)
-apply (induct_tac a rule: pd_basis_induct)
-apply (simp only: lower_unit_Rep_compact_basis [symmetric] unit)
-apply (simp only: lower_plus_principal [symmetric] plus)
-done
+proof (induct xs rule: lower_pd.principal_induct)
+ show "P (lower_principal a)" for a
+ proof (induct a rule: pd_basis_induct)
+ case PDUnit
+ then show ?case
+ by (simp only: lower_unit_Rep_compact_basis [symmetric] unit)
+ next
+ case PDPlus
+ then show ?case
+ by (simp only: lower_plus_principal [symmetric] plus)
+ qed
+qed (rule P)
subsection \<open>Monadic bind\<close>
--- a/src/HOL/HOLCF/UpperPD.thy Tue Dec 17 15:35:46 2024 +0100
+++ b/src/HOL/HOLCF/UpperPD.thy Tue Dec 17 23:07:13 2024 +0100
@@ -58,16 +58,33 @@
assumes 2: "\<And>t u a. P t (PDUnit a) \<Longrightarrow> P (PDPlus t u) (PDUnit a)"
assumes 3: "\<And>t u v. \<lbrakk>P t u; P t v\<rbrakk> \<Longrightarrow> P t (PDPlus u v)"
shows "P t u"
-using le apply (induct u arbitrary: t rule: pd_basis_induct)
-apply (erule rev_mp)
-apply (induct_tac t rule: pd_basis_induct)
-apply (simp add: 1)
-apply (simp add: upper_le_PDPlus_PDUnit_iff)
-apply (simp add: 2)
-apply (subst PDPlus_commute)
-apply (simp add: 2)
-apply (simp add: upper_le_PDPlus_iff 3)
-done
+ using le
+proof (induct u arbitrary: t rule: pd_basis_induct)
+ case (PDUnit a)
+ then show ?case
+ proof (induct t rule: pd_basis_induct)
+ case PDUnit
+ then show ?case by (simp add: 1)
+ next
+ case (PDPlus t u)
+ from PDPlus(3) consider (t) "t \<le>\<sharp> PDUnit a" | (u) "u \<le>\<sharp> PDUnit a"
+ by (auto simp: upper_le_PDPlus_PDUnit_iff)
+ then show ?case
+ proof cases
+ case t
+ then have "P t (PDUnit a)" by (rule PDPlus(1))
+ then show ?thesis by (rule 2)
+ next
+ case u
+ then have "P u (PDUnit a)" by (rule PDPlus(2))
+ then have "P (PDPlus u t) (PDUnit a)" by (rule 2)
+ then show ?thesis by (simp only: PDPlus_commute)
+ qed
+ qed
+next
+ case (PDPlus t t' u)
+ then show ?case by (simp add: upper_le_PDPlus_iff 3)
+qed
subsection \<open>Type definition\<close>
@@ -267,26 +284,41 @@
assumes unit: "\<And>x. P {x}\<sharp>"
assumes insert: "\<And>x ys. \<lbrakk>P {x}\<sharp>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<sharp> \<union>\<sharp> ys)"
shows "P (xs::'a::bifinite upper_pd)"
-apply (induct xs rule: upper_pd.principal_induct, rule P)
-apply (induct_tac a rule: pd_basis_induct1)
-apply (simp only: upper_unit_Rep_compact_basis [symmetric])
-apply (rule unit)
-apply (simp only: upper_unit_Rep_compact_basis [symmetric]
- upper_plus_principal [symmetric])
-apply (erule insert [OF unit])
-done
+proof (induct xs rule: upper_pd.principal_induct)
+ have *: "P {Rep_compact_basis a}\<sharp>" for a
+ by (rule unit)
+ show "P (upper_principal a)" for a
+ proof (induct a rule: pd_basis_induct1)
+ case (PDUnit a)
+ with * show ?case
+ by (simp only: upper_unit_Rep_compact_basis [symmetric])
+ next
+ case (PDPlus a t)
+ with * have "P ({Rep_compact_basis a}\<sharp> \<union>\<sharp> upper_principal t)"
+ by (rule insert)
+ then show ?case
+ by (simp only: upper_unit_Rep_compact_basis [symmetric]
+ upper_plus_principal [symmetric])
+ qed
+qed (rule P)
-lemma upper_pd_induct
- [case_names adm upper_unit upper_plus, induct type: upper_pd]:
+lemma upper_pd_induct [case_names adm upper_unit upper_plus, induct type: upper_pd]:
assumes P: "adm P"
assumes unit: "\<And>x. P {x}\<sharp>"
assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs \<union>\<sharp> ys)"
shows "P (xs::'a::bifinite upper_pd)"
-apply (induct xs rule: upper_pd.principal_induct, rule P)
-apply (induct_tac a rule: pd_basis_induct)
-apply (simp only: upper_unit_Rep_compact_basis [symmetric] unit)
-apply (simp only: upper_plus_principal [symmetric] plus)
-done
+proof (induct xs rule: upper_pd.principal_induct)
+ show "P (upper_principal a)" for a
+ proof (induct a rule: pd_basis_induct)
+ case PDUnit
+ then show ?case
+ by (simp only: upper_unit_Rep_compact_basis [symmetric] unit)
+ next
+ case PDPlus
+ then show ?case
+ by (simp only: upper_plus_principal [symmetric] plus)
+ qed
+qed (rule P)
subsection \<open>Monadic bind\<close>