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 |
8 |
|
9 |
|
10 (* Atomize infrastructure *) |
|
11 (* FIXME/TODO: is this really needed? *) |
|
12 (* |
|
13 lemma atomize_eqv: |
|
14 shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)" |
|
15 proof |
|
16 assume "A \<equiv> B" |
|
17 then show "Trueprop A \<equiv> Trueprop B" by unfold |
|
18 next |
|
19 assume *: "Trueprop A \<equiv> Trueprop B" |
|
20 have "A = B" |
|
21 proof (cases A) |
|
22 case True |
|
23 have "A" by fact |
|
24 then show "A = B" using * by simp |
|
25 next |
|
26 case False |
|
27 have "\<not>A" by fact |
|
28 then show "A = B" using * by auto |
|
29 qed |
|
30 then show "A \<equiv> B" by (rule eq_reflection) |
|
31 qed |
|
32 *) |
9 |
33 |
10 |
34 |
11 ML {* |
35 ML {* |
12 fun dest_cbinop t = |
36 fun dest_cbinop t = |
13 let |
37 let |