equal
deleted
inserted
replaced
4 lemma regularize_to_injection: |
4 lemma regularize_to_injection: |
5 shows "(QUOT_TRUE l \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y" |
5 shows "(QUOT_TRUE l \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y" |
6 by(auto simp add: QUOT_TRUE_def) |
6 by(auto simp add: QUOT_TRUE_def) |
7 |
7 |
8 syntax |
8 syntax |
9 "Bexeq" :: "id \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" ("(3\<exists>!!_\<in>_./ _)" [0, 0, 10] 10) |
9 "Bex1_rel" :: "id \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" ("(3\<exists>!!_\<in>_./ _)" [0, 0, 10] 10) |
10 translations |
10 translations |
11 "\<exists>!!x\<in>A. P" == "Bexeq A (%x. P)" |
11 "\<exists>!!x\<in>A. P" == "Bex1_rel A (%x. P)" |
12 |
12 |
13 |
13 |
14 (* Atomize infrastructure *) |
14 (* Atomize infrastructure *) |
15 (* FIXME/TODO: is this really needed? *) |
15 (* FIXME/TODO: is this really needed? *) |
16 (* |
16 (* |