equal
deleted
inserted
replaced
1 theory Classical |
1 theory Classical |
2 imports "../Parser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
5 (* example from my Urban's PhD *) |
5 (* example from my Urban's PhD *) |
6 |
6 |
7 (* |
7 (* |
8 alpha_trm_raw is incorrectly defined, therefore the equivalence proof |
8 alpha_trm_raw is incorrectly defined, therefore the equivalence proof |
9 does not go through; below the correct definition is given |
9 does not go through; below the correct definition is given |
10 *) |
10 *) |
11 ML {* val _ = cheat_equivp := true *} |
|
12 |
11 |
13 atom_decl name |
12 atom_decl name |
14 atom_decl coname |
13 atom_decl coname |
15 |
14 |
16 nominal_datatype trm = |
15 nominal_datatype trm = |
18 | Cut n::"coname" t1::"trm" c::"coname" t2::"trm" bind n in t1, bind c in t2 |
17 | Cut n::"coname" t1::"trm" c::"coname" t2::"trm" bind n in t1, bind c in t2 |
19 | AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" bind c1 in t1, bind c2 in t2 |
18 | AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" bind c1 in t1, bind c2 in t2 |
20 | AndL1 n::"name" t::"trm" "name" bind n in t |
19 | AndL1 n::"name" t::"trm" "name" bind n in t |
21 | AndL2 n::"name" t::"trm" "name" bind n in t |
20 | AndL2 n::"name" t::"trm" "name" bind n in t |
22 | ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name" bind c in t1, bind n in t2 |
21 | ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name" bind c in t1, bind n in t2 |
23 | ImpR c::"coname" n::"name" t::"trm" "coname" bind n in t, bind c in t |
22 | ImpR c::"coname" n::"name" t::"trm" "coname" bind n c in t |
24 |
23 |
25 |
24 |
26 thm trm.fv |
25 thm trm.fv |
27 thm trm.eq_iff |
26 thm trm.eq_iff |
28 thm trm.bn |
27 thm trm.bn |