9 (* One function is recursive and the other one is not, |
9 (* One function is recursive and the other one is not, |
10 and as the parser cannot handle this we cannot set |
10 and as the parser cannot handle this we cannot set |
11 the reference. *) |
11 the reference. *) |
12 ML {* val _ = recursive := false *} |
12 ML {* val _ = recursive := false *} |
13 |
13 |
14 nominal_datatype exp8 = |
14 nominal_datatype exp = |
15 EVar name |
15 EVar name |
16 | EUnit |
16 | EUnit |
17 | EPair exp8 exp8 |
17 | EPair exp exp |
18 | ELetRec l::lrbs8 e::exp8 bind "b_lrbs8 l" in e (* rec *) |
18 | ELetRec l::lrbs e::exp bind "b_lrbs l" in e (* rec *) |
19 and fnclause = |
19 and fnclause = |
20 K x::name p::pat8 f::exp8 bind "b_pat p" in f (* non-rec *) |
20 K x::name p::pat f::exp bind "b_pat p" in f (* non-rec *) |
21 and fnclauses = |
21 and fnclauses = |
22 S fnclause |
22 S fnclause |
23 | ORs fnclause fnclauses |
23 | ORs fnclause fnclauses |
24 and lrb8 = |
24 and lrb = |
25 Clause fnclauses |
25 Clause fnclauses |
26 and lrbs8 = |
26 and lrbs = |
27 Single lrb8 |
27 Single lrb |
28 | More lrb8 lrbs8 |
28 | More lrb lrbs |
29 and pat8 = |
29 and pat = |
30 PVar name |
30 PVar name |
31 | PUnit |
31 | PUnit |
32 | PPair pat8 pat8 |
32 | PPair pat pat |
33 binder |
33 binder |
34 b_lrbs8 :: "lrbs8 \<Rightarrow> atom set" and |
34 b_lrbs :: "lrbs \<Rightarrow> atom set" and |
35 b_pat :: "pat8 \<Rightarrow> atom set" and |
35 b_pat :: "pat \<Rightarrow> atom set" and |
36 b_fnclauses :: "fnclauses \<Rightarrow> atom set" and |
36 b_fnclauses :: "fnclauses \<Rightarrow> atom set" and |
37 b_fnclause :: "fnclause \<Rightarrow> atom set" and |
37 b_fnclause :: "fnclause \<Rightarrow> atom set" and |
38 b_lrb8 :: "lrb8 \<Rightarrow> atom set" |
38 b_lrb :: "lrb \<Rightarrow> atom set" |
39 where |
39 where |
40 "b_lrbs8 (Single l) = b_lrb8 l" |
40 "b_lrbs (Single l) = b_lrb l" |
41 | "b_lrbs8 (More l ls) = b_lrb8 l \<union> b_lrbs8 ls" |
41 | "b_lrbs (More l ls) = b_lrb l \<union> b_lrbs ls" |
42 | "b_pat (PVar x) = {atom x}" |
42 | "b_pat (PVar x) = {atom x}" |
43 | "b_pat (PUnit) = {}" |
43 | "b_pat (PUnit) = {}" |
44 | "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2" |
44 | "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2" |
45 | "b_fnclauses (S fc) = (b_fnclause fc)" |
45 | "b_fnclauses (S fc) = (b_fnclause fc)" |
46 | "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)" |
46 | "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)" |
47 | "b_lrb8 (Clause fcs) = (b_fnclauses fcs)" |
47 | "b_lrb (Clause fcs) = (b_fnclauses fcs)" |
48 | "b_fnclause (K x pat exp8) = {atom x}" |
48 | "b_fnclause (K x pat exp) = {atom x}" |
49 |
49 |
50 thm exp7_lrb_lrbs.eq_iff |
50 thm exp7_lrb_lrbs.eq_iff |
51 thm exp7_lrb_lrbs.supp |
51 thm exp7_lrb_lrbs.supp |
52 |
52 |
53 end |
53 end |