equal
deleted
inserted
replaced
1 theory ExPS8 |
1 theory ExPS8 |
2 imports "../Parser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
5 (* example 8 from Peter Sewell's bestiary *) |
5 (* example 8 from Peter Sewell's bestiary *) |
6 |
6 |
7 atom_decl name |
7 atom_decl name |
8 |
8 |
9 (* One function is recursive and the other one is not, |
9 ML {* val _ = cheat_fv_rsp := true *} |
10 and as the parser cannot handle this we cannot set |
10 ML {* val _ = cheat_alpha_bn_rsp := true *} |
11 the reference. *) |
|
12 ML {* val _ = recursive := false *} |
|
13 |
11 |
14 nominal_datatype exp = |
12 nominal_datatype exp = |
15 EVar name |
13 EVar name |
16 | EUnit |
14 | EUnit |
17 | EPair exp exp |
15 | EPair exp exp |
18 | ELetRec l::lrbs e::exp bind "b_lrbs l" in e (* rec *) |
16 | ELetRec l::lrbs e::exp bind_set "b_lrbs l" in l e |
19 and fnclause = |
17 and fnclause = |
20 K x::name p::pat f::exp bind "b_pat p" in f (* non-rec *) |
18 K x::name p::pat f::exp bind_set "b_pat p" in f |
21 and fnclauses = |
19 and fnclauses = |
22 S fnclause |
20 S fnclause |
23 | ORs fnclause fnclauses |
21 | ORs fnclause fnclauses |
24 and lrb = |
22 and lrb = |
25 Clause fnclauses |
23 Clause fnclauses |
45 | "b_fnclauses (S fc) = (b_fnclause fc)" |
43 | "b_fnclauses (S fc) = (b_fnclause fc)" |
46 | "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)" |
44 | "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)" |
47 | "b_lrb (Clause fcs) = (b_fnclauses fcs)" |
45 | "b_lrb (Clause fcs) = (b_fnclauses fcs)" |
48 | "b_fnclause (K x pat exp) = {atom x}" |
46 | "b_fnclause (K x pat exp) = {atom x}" |
49 |
47 |
50 thm exp7_lrb_lrbs.eq_iff |
48 thm exp_fnclause_fnclauses_lrb_lrbs_pat.fv |
51 thm exp7_lrb_lrbs.supp |
49 thm exp_fnclause_fnclauses_lrb_lrbs_pat.eq_iff |
52 |
50 |
53 end |
51 end |
54 |
52 |
55 |
53 |
56 |
54 |