equal
deleted
inserted
replaced
4 |
4 |
5 text {* example 1, equivalent to example 2 from Terms *} |
5 text {* example 1, equivalent to example 2 from Terms *} |
6 |
6 |
7 atom_decl name |
7 atom_decl name |
8 |
8 |
9 ML {* val cheat_alpha_eqvt = ref false *} |
9 ML {* val _ = cheat_alpha_eqvt := false *} |
10 ML {* val cheat_fv_eqvt = ref false *} |
10 ML {* val _ = cheat_fv_eqvt := false *} |
|
11 ML {* val _ = recursive := false *} |
11 |
12 |
12 (* |
13 (* |
13 nominal_datatype lam = |
14 nominal_datatype lam = |
14 VAR "name" |
15 VAR "name" |
15 | APP "lam" "lam" |
16 | APP "lam" "lam" |
58 term alpha_bi |
59 term alpha_bi |
59 |
60 |
60 lemma alpha_bi: |
61 lemma alpha_bi: |
61 shows "alpha_bi pi b b' = True" |
62 shows "alpha_bi pi b b' = True" |
62 apply(induct b rule: lam_bp_inducts(2)) |
63 apply(induct b rule: lam_bp_inducts(2)) |
63 sorry |
64 apply(simp_all) |
|
65 apply(induct b' rule: lam_bp_inducts(2)) |
|
66 apply (simp_all add: lam_bp_inject) |
|
67 done |
64 |
68 |
65 lemma fv_bi: |
69 lemma fv_bi: |
66 shows "fv_bi b = {}" |
70 shows "fv_bi b = {}" |
67 apply(induct b rule: lam_bp_inducts(2)) |
71 apply(induct b rule: lam_bp_inducts(2)) |
68 apply(auto)[1] |
72 apply(auto)[1] |