equal
deleted
inserted
replaced
45 apply simp |
45 apply simp |
46 apply blast |
46 apply blast |
47 done |
47 done |
48 |
48 |
49 lemma acc_le_prodI [intro!]: |
49 lemma acc_le_prodI [intro!]: |
50 "\<lbrakk> acc r\<^isub>A; acc r\<^isub>B \<rbrakk> \<Longrightarrow> acc(Product.le r\<^isub>A r\<^isub>B)" |
50 "\<lbrakk> acc r\<^sub>A; acc r\<^sub>B \<rbrakk> \<Longrightarrow> acc(Product.le r\<^sub>A r\<^sub>B)" |
51 apply (unfold acc_def) |
51 apply (unfold acc_def) |
52 apply (rule wf_subset) |
52 apply (rule wf_subset) |
53 apply (erule wf_lex_prod) |
53 apply (erule wf_lex_prod) |
54 apply assumption |
54 apply assumption |
55 apply (auto simp add: lesssub_def less_prod_Pair_conv lex_prod_def) |
55 apply (auto simp add: lesssub_def less_prod_Pair_conv lex_prod_def) |