equal
deleted
inserted
replaced
7 |
7 |
8 lemma permute_rsp_fset[quot_respect]: |
8 lemma permute_rsp_fset[quot_respect]: |
9 shows "(op = ===> list_eq ===> list_eq) permute permute" |
9 shows "(op = ===> list_eq ===> list_eq) permute permute" |
10 apply(simp) |
10 apply(simp) |
11 apply(clarify) |
11 apply(clarify) |
12 apply(simp add: eqvts[symmetric]) |
12 apply(rule_tac p="-x" in permute_boolE) |
13 apply(subst permute_minus_cancel(1)[symmetric, of "xb"]) |
13 apply(perm_simp add: permute_minus_cancel) |
14 apply(subst mem_eqvt[symmetric]) |
|
15 apply(subst (2) permute_minus_cancel(1)[symmetric, of "xb"]) |
|
16 apply(subst mem_eqvt[symmetric]) |
|
17 apply(simp) |
14 apply(simp) |
18 done |
15 done |
19 |
16 |
20 instantiation fset :: (pt) pt |
17 instantiation fset :: (pt) pt |
21 begin |
18 begin |