equal
deleted
inserted
replaced
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 ML {* val _ = cheat_fv_rsp := true *} |
|
10 ML {* val _ = cheat_equivp := true *} |
|
11 ML {* val _ = cheat_alpha_bn_rsp := true *} |
|
12 |
|
13 nominal_datatype exp = |
9 nominal_datatype exp = |
14 EVar name |
10 EVar name |
15 | EUnit |
11 | EUnit |
16 | EPair exp exp |
12 | EPair exp exp |
17 | ELetRec l::lrbs e::exp bind_set "b_lrbs l" in l e |
13 | ELetRec l::lrbs e::exp bind (set) "b_lrbs l" in l e |
18 and fnclause = |
14 and fnclause = |
19 K x::name p::pat f::exp bind_set "b_pat p" in f |
15 K x::name p::pat f::exp bind (set) "b_pat p" in f |
20 and fnclauses = |
16 and fnclauses = |
21 S fnclause |
17 S fnclause |
22 | ORs fnclause fnclauses |
18 | ORs fnclause fnclauses |
23 and lrb = |
19 and lrb = |
24 Clause fnclauses |
20 Clause fnclauses |
44 | "b_fnclauses (S fc) = (b_fnclause fc)" |
40 | "b_fnclauses (S fc) = (b_fnclause fc)" |
45 | "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)" |
41 | "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)" |
46 | "b_lrb (Clause fcs) = (b_fnclauses fcs)" |
42 | "b_lrb (Clause fcs) = (b_fnclauses fcs)" |
47 | "b_fnclause (K x pat exp) = {atom x}" |
43 | "b_fnclause (K x pat exp) = {atom x}" |
48 |
44 |
49 thm exp_fnclause_fnclauses_lrb_lrbs_pat.fv |
|
50 thm exp_fnclause_fnclauses_lrb_lrbs_pat.eq_iff |
|
51 |
45 |
52 end |
46 end |
53 |
47 |
54 |
48 |
55 |
49 |