equal
deleted
inserted
replaced
87 apply simp |
87 apply simp |
88 apply blast |
88 apply blast |
89 done |
89 done |
90 |
90 |
91 lemma Cons_acc_step1I [intro!]: |
91 lemma Cons_acc_step1I [intro!]: |
92 "accp r x ==> accp (step1 r) xs \<Longrightarrow> accp (step1 r) (x # xs)" |
92 "Wellfounded.accp r x ==> Wellfounded.accp (step1 r) xs \<Longrightarrow> Wellfounded.accp (step1 r) (x # xs)" |
93 apply (induct arbitrary: xs set: accp) |
93 apply (induct arbitrary: xs set: Wellfounded.accp) |
94 apply (erule thin_rl) |
94 apply (erule thin_rl) |
95 apply (erule accp_induct) |
95 apply (erule accp_induct) |
96 apply (rule accp.accI) |
96 apply (rule accp.accI) |
97 apply blast |
97 apply blast |
98 done |
98 done |
99 |
99 |
100 lemma lists_accD: "listsp (accp r) xs ==> accp (step1 r) xs" |
100 lemma lists_accD: "listsp (Wellfounded.accp r) xs ==> Wellfounded.accp (step1 r) xs" |
101 apply (induct set: listsp) |
101 apply (induct set: listsp) |
102 apply (rule accp.accI) |
102 apply (rule accp.accI) |
103 apply simp |
103 apply simp |
104 apply (rule accp.accI) |
104 apply (rule accp.accI) |
105 apply (fast dest: accp_downward) |
105 apply (fast dest: accp_downward) |
111 apply (unfold step1_def) |
111 apply (unfold step1_def) |
112 apply (drule in_set_conv_decomp [THEN iffD1]) |
112 apply (drule in_set_conv_decomp [THEN iffD1]) |
113 apply force |
113 apply force |
114 done |
114 done |
115 |
115 |
116 lemma lists_accI: "accp (step1 r) xs ==> listsp (accp r) xs" |
116 lemma lists_accI: "Wellfounded.accp (step1 r) xs ==> listsp (Wellfounded.accp r) xs" |
117 apply (induct set: accp) |
117 apply (induct set: Wellfounded.accp) |
118 apply clarify |
118 apply clarify |
119 apply (rule accp.accI) |
119 apply (rule accp.accI) |
120 apply (drule_tac r=r in ex_step1I, assumption) |
120 apply (drule_tac r=r in ex_step1I, assumption) |
121 apply blast |
121 apply blast |
122 done |
122 done |