equal
deleted
inserted
replaced
19 |
19 |
20 lemma Br_neq_left: "l \<in> bt(A) ==> Br(x, l, r) \<noteq> l" |
20 lemma Br_neq_left: "l \<in> bt(A) ==> Br(x, l, r) \<noteq> l" |
21 by (induct arbitrary: x r set: bt) auto |
21 by (induct arbitrary: x r set: bt) auto |
22 |
22 |
23 lemma Br_iff: "Br(a, l, r) = Br(a', l', r') \<longleftrightarrow> a = a' & l = l' & r = r'" |
23 lemma Br_iff: "Br(a, l, r) = Br(a', l', r') \<longleftrightarrow> a = a' & l = l' & r = r'" |
24 -- "Proving a freeness theorem." |
24 \<comment> "Proving a freeness theorem." |
25 by (fast elim!: bt.free_elims) |
25 by (fast elim!: bt.free_elims) |
26 |
26 |
27 inductive_cases BrE: "Br(a, l, r) \<in> bt(A)" |
27 inductive_cases BrE: "Br(a, l, r) \<in> bt(A)" |
28 -- "An elimination rule, for type-checking." |
28 \<comment> "An elimination rule, for type-checking." |
29 |
29 |
30 text \<open> |
30 text \<open> |
31 \medskip Lemmas to justify using @{term bt} in other recursive type |
31 \medskip Lemmas to justify using @{term bt} in other recursive type |
32 definitions. |
32 definitions. |
33 \<close> |
33 \<close> |
56 "[| t \<in> bt(A); |
56 "[| t \<in> bt(A); |
57 c \<in> C(Lf); |
57 c \<in> C(Lf); |
58 !!x y z r s. [| x \<in> A; y \<in> bt(A); z \<in> bt(A); r \<in> C(y); s \<in> C(z) |] ==> |
58 !!x y z r s. [| x \<in> A; y \<in> bt(A); z \<in> bt(A); r \<in> C(y); s \<in> C(z) |] ==> |
59 h(x, y, z, r, s) \<in> C(Br(x, y, z)) |
59 h(x, y, z, r, s) \<in> C(Br(x, y, z)) |
60 |] ==> bt_rec(c, h, t) \<in> C(t)" |
60 |] ==> bt_rec(c, h, t) \<in> C(t)" |
61 -- \<open>Type checking for recursor -- example only; not really needed.\<close> |
61 \<comment> \<open>Type checking for recursor -- example only; not really needed.\<close> |
62 apply (induct_tac t) |
62 apply (induct_tac t) |
63 apply simp_all |
63 apply simp_all |
64 done |
64 done |
65 |
65 |
66 |
66 |