equal
deleted
inserted
replaced
1 theory Test |
1 theory Test |
2 imports "Parser" "../Attic/Prove" |
2 imports "Parser" "../Attic/Prove" |
3 begin |
3 begin |
4 |
4 |
5 text {* example 1, equivalent to example 2 from Terms *} |
5 text {* example 1, equivalent to example 2 from Terms *} |
|
6 |
|
7 atom_decl name |
6 |
8 |
7 nominal_datatype lam = |
9 nominal_datatype lam = |
8 VAR "name" |
10 VAR "name" |
9 | APP "lam" "lam" |
11 | APP "lam" "lam" |
10 | LET bp::"bp" t::"lam" bind "bi bp" in t |
12 | LET bp::"bp" t::"lam" bind "bi bp" in t |
19 thm lam_bp_inject |
21 thm lam_bp_inject |
20 thm lam_bp_bn |
22 thm lam_bp_bn |
21 thm lam_bp_perm |
23 thm lam_bp_perm |
22 thm lam_bp_induct |
24 thm lam_bp_induct |
23 thm lam_bp_distinct |
25 thm lam_bp_distinct |
|
26 ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *} |
|
27 |
|
28 term "supp (x :: lam)" |
24 |
29 |
25 (* compat should be |
30 (* compat should be |
26 compat (BP x t) pi (BP x' t') |
31 compat (BP x t) pi (BP x' t') |
27 \<equiv> alpha_trm t t' \<and> pi o x = x' |
32 \<equiv> alpha_trm t t' \<and> pi o x = x' |
28 *) |
33 *) |