equal
deleted
inserted
replaced
847 qed |
847 qed |
848 then show "P z" |
848 then show "P z" |
849 by (simp add: zeq) |
849 by (simp add: zeq) |
850 qed auto |
850 qed auto |
851 |
851 |
|
852 lemma refl_lex_prod[simp]: "refl r\<^sub>B \<Longrightarrow> refl (r\<^sub>A <*lex*> r\<^sub>B)" |
|
853 by (auto intro!: reflI dest: refl_onD) |
|
854 |
852 lemma irrefl_on_lex_prod[simp]: |
855 lemma irrefl_on_lex_prod[simp]: |
853 "irrefl_on A r\<^sub>A \<Longrightarrow> irrefl_on B r\<^sub>B \<Longrightarrow> irrefl_on (A \<times> B) (r\<^sub>A <*lex*> r\<^sub>B)" |
856 "irrefl_on A r\<^sub>A \<Longrightarrow> irrefl_on B r\<^sub>B \<Longrightarrow> irrefl_on (A \<times> B) (r\<^sub>A <*lex*> r\<^sub>B)" |
854 by (auto intro!: irrefl_onI dest: irrefl_onD) |
857 by (auto intro!: irrefl_onI dest: irrefl_onD) |
855 |
858 |
856 lemma irrefl_lex_prod[simp]: "irrefl r\<^sub>A \<Longrightarrow> irrefl r\<^sub>B \<Longrightarrow> irrefl (r\<^sub>A <*lex*> r\<^sub>B)" |
859 lemma irrefl_lex_prod[simp]: "irrefl r\<^sub>A \<Longrightarrow> irrefl r\<^sub>B \<Longrightarrow> irrefl (r\<^sub>A <*lex*> r\<^sub>B)" |