src/HOL/BNF_Wellorder_Constructions.thy
changeset 63561 fba08009ff3e
parent 63092 a949b2a5f51d
child 67091 1393c2340eec
     1.1 --- a/src/HOL/BNF_Wellorder_Constructions.thy	Thu Jul 28 20:39:51 2016 +0200
     1.2 +++ b/src/HOL/BNF_Wellorder_Constructions.thy	Fri Jul 29 09:49:23 2016 +0200
     1.3 @@ -36,6 +36,10 @@
     1.4  lemma Refl_Restr: "Refl r \<Longrightarrow> Refl(Restr r A)"
     1.5  unfolding refl_on_def Field_def by auto
     1.6  
     1.7 +lemma linear_order_on_Restr:
     1.8 +  "linear_order_on A r \<Longrightarrow> linear_order_on (A \<inter> above r x) (Restr r (above r x))"
     1.9 +by(simp add: order_on_defs refl_on_def trans_def antisym_def total_on_def)(safe; blast)
    1.10 +
    1.11  lemma antisym_Restr:
    1.12  "antisym r \<Longrightarrow> antisym(Restr r A)"
    1.13  unfolding antisym_def Field_def by auto