15 induction principles. *} |
15 induction principles. *} |
16 |
16 |
17 definition |
17 definition |
18 fresh_star :: "atom set \<Rightarrow> 'a::pt \<Rightarrow> bool" ("_ \<sharp>* _" [80,80] 80) |
18 fresh_star :: "atom set \<Rightarrow> 'a::pt \<Rightarrow> bool" ("_ \<sharp>* _" [80,80] 80) |
19 where |
19 where |
20 "xs \<sharp>* c \<equiv> \<forall>x \<in> xs. x \<sharp> c" |
20 "as \<sharp>* x \<equiv> \<forall>a \<in> as. a \<sharp> x" |
21 |
21 |
22 lemma fresh_star_prod: |
22 lemma fresh_star_prod: |
23 fixes xs::"atom set" |
23 fixes as::"atom set" |
24 shows "xs \<sharp>* (a, b) = (xs \<sharp>* a \<and> xs \<sharp>* b)" |
24 shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)" |
25 by (auto simp add: fresh_star_def fresh_Pair) |
25 by (auto simp add: fresh_star_def fresh_Pair) |
26 |
26 |
27 lemma fresh_star_union: |
27 lemma fresh_star_union: |
28 shows "(xs \<union> ys) \<sharp>* c = (xs \<sharp>* c \<and> ys \<sharp>* c)" |
28 shows "(as \<union> bs) \<sharp>* x = (as \<sharp>* x \<and> bs \<sharp>* x)" |
29 by (auto simp add: fresh_star_def) |
29 by (auto simp add: fresh_star_def) |
30 |
30 |
31 lemma fresh_star_insert: |
31 lemma fresh_star_insert: |
32 shows "(insert x ys) \<sharp>* c = (x \<sharp> c \<and> ys \<sharp>* c)" |
32 shows "(insert a as) \<sharp>* x = (a \<sharp> x \<and> as \<sharp>* x)" |
33 by (auto simp add: fresh_star_def) |
33 by (auto simp add: fresh_star_def) |
34 |
34 |
35 lemma fresh_star_Un_elim: |
35 lemma fresh_star_Un_elim: |
36 "((S \<union> T) \<sharp>* c \<Longrightarrow> PROP C) \<equiv> (S \<sharp>* c \<Longrightarrow> T \<sharp>* c \<Longrightarrow> PROP C)" |
36 "((as \<union> bs) \<sharp>* x \<Longrightarrow> PROP C) \<equiv> (as \<sharp>* x \<Longrightarrow> bs \<sharp>* x \<Longrightarrow> PROP C)" |
37 unfolding fresh_star_def |
37 unfolding fresh_star_def |
38 apply(rule) |
38 apply(rule) |
39 apply(erule meta_mp) |
39 apply(erule meta_mp) |
40 apply(auto) |
40 apply(auto) |
41 done |
41 done |
42 |
42 |
43 lemma fresh_star_insert_elim: |
43 lemma fresh_star_insert_elim: |
44 "(insert x S \<sharp>* c \<Longrightarrow> PROP C) \<equiv> (x \<sharp> c \<Longrightarrow> S \<sharp>* c \<Longrightarrow> PROP C)" |
44 "(insert a as \<sharp>* x \<Longrightarrow> PROP C) \<equiv> (a \<sharp> x \<Longrightarrow> as \<sharp>* x \<Longrightarrow> PROP C)" |
45 unfolding fresh_star_def |
45 unfolding fresh_star_def |
46 by rule (simp_all add: fresh_star_def) |
46 by rule (simp_all add: fresh_star_def) |
47 |
47 |
48 lemma fresh_star_empty_elim: |
48 lemma fresh_star_empty_elim: |
49 "({} \<sharp>* c \<Longrightarrow> PROP C) \<equiv> PROP C" |
49 "({} \<sharp>* x \<Longrightarrow> PROP C) \<equiv> PROP C" |
50 by (simp add: fresh_star_def) |
50 by (simp add: fresh_star_def) |
51 |
51 |
52 lemma fresh_star_unit_elim: |
52 lemma fresh_star_unit_elim: |
53 shows "(a \<sharp>* () \<Longrightarrow> PROP C) \<equiv> PROP C" |
53 shows "(a \<sharp>* () \<Longrightarrow> PROP C) \<equiv> PROP C" |
54 by (simp add: fresh_star_def fresh_unit) |
54 by (simp add: fresh_star_def fresh_unit) |