equal
deleted
inserted
replaced
1 theory ExPS3 |
1 theory ExPS3 |
2 imports "../Parser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
5 (* example 3 from Peter Sewell's bestiary *) |
5 (* example 3 from Peter Sewell's bestiary *) |
6 |
6 |
7 atom_decl name |
7 atom_decl name |
8 |
8 |
9 ML {* val _ = recursive := false *} |
9 ML {* val _ = cheat_alpha_eqvt := true *} |
|
10 ML {* val _ = cheat_equivp := true *} |
|
11 ML {* val _ = cheat_alpha_bn_rsp := true *} |
|
12 |
10 nominal_datatype exp = |
13 nominal_datatype exp = |
11 VarP "name" |
14 VarP "name" |
12 | AppP "exp" "exp" |
15 | AppP "exp" "exp" |
13 | LamP x::"name" e::"exp" bind x in e |
16 | LamP x::"name" e::"exp" bind_set x in e |
14 | LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp p" in e1 |
17 | LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind_set x in e2, bind_set "bp p" in e1 |
15 and pat3 = |
18 and pat3 = |
16 PVar "name" |
19 PVar "name" |
17 | PUnit |
20 | PUnit |
18 | PPair "pat3" "pat3" |
21 | PPair "pat3" "pat3" |
19 binder |
22 binder |
28 thm exp_pat3.bn |
31 thm exp_pat3.bn |
29 thm exp_pat3.perm |
32 thm exp_pat3.perm |
30 thm exp_pat3.induct |
33 thm exp_pat3.induct |
31 thm exp_pat3.distinct |
34 thm exp_pat3.distinct |
32 thm exp_pat3.fv |
35 thm exp_pat3.fv |
33 thm exp_pat3.supp |
36 thm exp_pat3.supp(1-2) |
34 |
37 |
35 end |
38 end |
36 |
39 |
37 |
40 |
38 |
41 |