# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1596985790 -3600
# Node ID a0768f16bccdbc203be847caf0b9543024fdfaea
# Parent  5de9a5fbf2ec135565576c87ab6cf200062a48ae
one last lemma about Total and Restr

diff -r 5de9a5fbf2ec -r a0768f16bccd src/HOL/BNF_Wellorder_Constructions.thy
--- a/src/HOL/BNF_Wellorder_Constructions.thy	Sun Aug 09 15:18:19 2020 +0100
+++ b/src/HOL/BNF_Wellorder_Constructions.thy	Sun Aug 09 16:09:50 2020 +0100
@@ -24,74 +24,77 @@
 subsection \<open>Restriction to a set\<close>
 
 abbreviation Restr :: "'a rel \<Rightarrow> 'a set \<Rightarrow> 'a rel"
-where "Restr r A \<equiv> r Int (A \<times> A)"
+  where "Restr r A \<equiv> r Int (A \<times> A)"
 
 lemma Restr_subset:
-"A \<le> B \<Longrightarrow> Restr (Restr r B) A = Restr r A"
-by blast
+  "A \<le> B \<Longrightarrow> Restr (Restr r B) A = Restr r A"
+  by blast
 
 lemma Restr_Field: "Restr r (Field r) = r"
-unfolding Field_def by auto
+  unfolding Field_def by auto
 
 lemma Refl_Restr: "Refl r \<Longrightarrow> Refl(Restr r A)"
-unfolding refl_on_def Field_def by auto
+  unfolding refl_on_def Field_def by auto
 
 lemma linear_order_on_Restr:
   "linear_order_on A r \<Longrightarrow> linear_order_on (A \<inter> above r x) (Restr r (above r x))"
-by(simp add: order_on_defs refl_on_def trans_def antisym_def total_on_def)(safe; blast)
+  by(simp add: order_on_defs refl_on_def trans_def antisym_def total_on_def)(safe; blast)
 
 lemma antisym_Restr:
-"antisym r \<Longrightarrow> antisym(Restr r A)"
-unfolding antisym_def Field_def by auto
+  "antisym r \<Longrightarrow> antisym(Restr r A)"
+  unfolding antisym_def Field_def by auto
 
 lemma Total_Restr:
-"Total r \<Longrightarrow> Total(Restr r A)"
-unfolding total_on_def Field_def by auto
+  "Total r \<Longrightarrow> Total(Restr r A)"
+  unfolding total_on_def Field_def by auto
+
+lemma total_on_imp_Total_Restr: "total_on A r \<Longrightarrow> Total (Restr r A)"
+  by (auto simp: Field_def total_on_def)
 
 lemma trans_Restr:
-"trans r \<Longrightarrow> trans(Restr r A)"
-unfolding trans_def Field_def by blast
+  "trans r \<Longrightarrow> trans(Restr r A)"
+  unfolding trans_def Field_def by blast
 
 lemma Preorder_Restr:
-"Preorder r \<Longrightarrow> Preorder(Restr r A)"
-unfolding preorder_on_def by (simp add: Refl_Restr trans_Restr)
+  "Preorder r \<Longrightarrow> Preorder(Restr r A)"
+  unfolding preorder_on_def by (simp add: Refl_Restr trans_Restr)
 
 lemma Partial_order_Restr:
-"Partial_order r \<Longrightarrow> Partial_order(Restr r A)"
-unfolding partial_order_on_def by (simp add: Preorder_Restr antisym_Restr)
+  "Partial_order r \<Longrightarrow> Partial_order(Restr r A)"
+  unfolding partial_order_on_def by (simp add: Preorder_Restr antisym_Restr)
 
 lemma Linear_order_Restr:
-"Linear_order r \<Longrightarrow> Linear_order(Restr r A)"
-unfolding linear_order_on_def by (simp add: Partial_order_Restr Total_Restr)
+  "Linear_order r \<Longrightarrow> Linear_order(Restr r A)"
+  unfolding linear_order_on_def by (simp add: Partial_order_Restr Total_Restr)
 
 lemma Well_order_Restr:
-assumes "Well_order r"
-shows "Well_order(Restr r A)"
+  assumes "Well_order r"
+  shows "Well_order(Restr r A)"
 proof-
   have "Restr r A - Id \<le> r - Id" using Restr_subset by blast
   hence "wf(Restr r A - Id)" using assms
-  using well_order_on_def wf_subset by blast
+    using well_order_on_def wf_subset by blast
   thus ?thesis using assms unfolding well_order_on_def
-  by (simp add: Linear_order_Restr)
+    by (simp add: Linear_order_Restr)
 qed
 
 lemma Field_Restr_subset: "Field(Restr r A) \<le> A"
-by (auto simp add: Field_def)
+  by (auto simp add: Field_def)
 
 lemma Refl_Field_Restr:
-"Refl r \<Longrightarrow> Field(Restr r A) = (Field r) Int A"
-unfolding refl_on_def Field_def by blast
+  "Refl r \<Longrightarrow> Field(Restr r A) = (Field r) Int A"
+  unfolding refl_on_def Field_def by blast
 
 lemma Refl_Field_Restr2:
-"\<lbrakk>Refl r; A \<le> Field r\<rbrakk> \<Longrightarrow> Field(Restr r A) = A"
-by (auto simp add: Refl_Field_Restr)
+  "\<lbrakk>Refl r; A \<le> Field r\<rbrakk> \<Longrightarrow> Field(Restr r A) = A"
+  by (auto simp add: Refl_Field_Restr)
 
 lemma well_order_on_Restr:
-assumes WELL: "Well_order r" and SUB: "A \<le> Field r"
-shows "well_order_on A (Restr r A)"
-using assms
-using Well_order_Restr[of r A] Refl_Field_Restr2[of r A]
-     order_on_defs[of "Field r" r] by auto
+  assumes WELL: "Well_order r" and SUB: "A \<le> Field r"
+  shows "well_order_on A (Restr r A)"
+  using assms
+  using Well_order_Restr[of r A] Refl_Field_Restr2[of r A]
+    order_on_defs[of "Field r" r] by auto
 
 
 subsection \<open>Order filters versus restrictions and embeddings\<close>