equal
deleted
inserted
replaced
2396 qed |
2396 qed |
2397 |
2397 |
2398 lemma list_renaming_perm: |
2398 lemma list_renaming_perm: |
2399 shows "\<exists>q. (\<forall>b \<in> set bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" |
2399 shows "\<exists>q. (\<forall>b \<in> set bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" |
2400 proof (induct bs) |
2400 proof (induct bs) |
2401 case Nil |
|
2402 have "(\<forall>b \<in> set []. 0 \<bullet> b = p \<bullet> b) \<and> supp (0::perm) \<subseteq> set [] \<union> p \<bullet> set []" |
|
2403 by (simp add: supp_zero_perm) |
|
2404 then show "\<exists>q. (\<forall>b \<in> set []. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set [] \<union> p \<bullet> (set [])" by blast |
|
2405 next |
|
2406 case (Cons a bs) |
2401 case (Cons a bs) |
2407 then have " \<exists>q. (\<forall>b \<in> set bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set bs \<union> p \<bullet> (set bs)" by simp |
2402 then have " \<exists>q. (\<forall>b \<in> set bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set bs \<union> p \<bullet> (set bs)" by simp |
2408 then obtain q where *: "\<forall>b \<in> set bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> set bs \<union> p \<bullet> (set bs)" |
2403 then obtain q where *: "\<forall>b \<in> set bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> set bs \<union> p \<bullet> (set bs)" |
2409 by (blast) |
2404 by (blast) |
2410 { assume 1: "a \<in> set bs" |
2405 { assume 1: "a \<in> set bs" |
2441 ultimately |
2436 ultimately |
2442 have "\<exists>q. (\<forall>b \<in> set (a # bs). q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" by blast |
2437 have "\<exists>q. (\<forall>b \<in> set (a # bs). q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" by blast |
2443 } |
2438 } |
2444 ultimately show "\<exists>q. (\<forall>b \<in> set (a # bs). q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" |
2439 ultimately show "\<exists>q. (\<forall>b \<in> set (a # bs). q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" |
2445 by blast |
2440 by blast |
|
2441 next |
|
2442 case Nil |
|
2443 have "(\<forall>b \<in> set []. 0 \<bullet> b = p \<bullet> b) \<and> supp (0::perm) \<subseteq> set [] \<union> p \<bullet> set []" |
|
2444 by (simp add: supp_zero_perm) |
|
2445 then show "\<exists>q. (\<forall>b \<in> set []. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set [] \<union> p \<bullet> (set [])" by blast |
2446 qed |
2446 qed |
2447 |
2447 |
2448 |
2448 |
2449 section {* Concrete Atoms Types *} |
2449 section {* Concrete Atoms Types *} |
2450 |
2450 |