equal
deleted
inserted
replaced
92 let |
92 let |
93 val ty = fastype_of arg |
93 val ty = fastype_of arg |
94 in |
94 in |
95 Const (@{const_name permute}, @{typ perm} --> ty --> ty) |
95 Const (@{const_name permute}, @{typ perm} --> ty --> ty) |
96 end |
96 end |
97 |
|
98 val perm_at = @{term "permute :: perm \<Rightarrow> atom set \<Rightarrow> atom set"} |
|
99 *} |
97 *} |
100 |
98 |
101 lemma exi: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (pi \<bullet> p)) \<Longrightarrow> \<exists>pi. Q pi" |
99 lemma exi: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (pi \<bullet> p)) \<Longrightarrow> \<exists>pi. Q pi" |
102 apply (erule exE) |
100 apply (erule exE) |
103 apply (rule_tac x="pi \<bullet> pia" in exI) |
101 apply (rule_tac x="pi \<bullet> pia" in exI) |