1 theory ExPS8 |
|
2 imports "../Nominal2" |
|
3 begin |
|
4 |
|
5 (* example 8 from Peter Sewell's bestiary *) |
|
6 |
|
7 atom_decl name |
|
8 |
|
9 declare [[STEPS = 31]] |
|
10 |
|
11 nominal_datatype fun_pats: exp = |
|
12 EVar name |
|
13 | EUnit |
|
14 | EPair exp exp |
|
15 | ELetRec l::lrbs e::exp bind (set) "b_lrbs l" in l e |
|
16 and fnclause = |
|
17 K x::name p::pat f::exp bind (set) "b_pat p" in f |
|
18 and fnclauses = |
|
19 S fnclause |
|
20 | ORs fnclause fnclauses |
|
21 and lrb = |
|
22 Clause fnclauses |
|
23 and lrbs = |
|
24 Single lrb |
|
25 | More lrb lrbs |
|
26 and pat = |
|
27 PVar name |
|
28 | PUnit |
|
29 | PPair pat pat |
|
30 binder |
|
31 b_lrbs :: "lrbs \<Rightarrow> atom set" and |
|
32 b_pat :: "pat \<Rightarrow> atom set" and |
|
33 b_fnclauses :: "fnclauses \<Rightarrow> atom set" and |
|
34 b_fnclause :: "fnclause \<Rightarrow> atom set" and |
|
35 b_lrb :: "lrb \<Rightarrow> atom set" |
|
36 where |
|
37 "b_lrbs (Single l) = b_lrb l" |
|
38 | "b_lrbs (More l ls) = b_lrb l \<union> b_lrbs ls" |
|
39 | "b_pat (PVar x) = {atom x}" |
|
40 | "b_pat (PUnit) = {}" |
|
41 | "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2" |
|
42 | "b_fnclauses (S fc) = (b_fnclause fc)" |
|
43 | "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)" |
|
44 | "b_lrb (Clause fcs) = (b_fnclauses fcs)" |
|
45 | "b_fnclause (K x pat exp) = {atom x}" |
|
46 |
|
47 thm fun_pats.distinct |
|
48 thm fun_pats.induct |
|
49 thm fun_pats.inducts |
|
50 thm fun_pats.exhaust |
|
51 thm fun_pats.fv_defs |
|
52 thm fun_pats.bn_defs |
|
53 thm fun_pats.perm_simps |
|
54 thm fun_pats.eq_iff |
|
55 thm fun_pats.fv_bn_eqvt |
|
56 thm fun_pats.size_eqvt |
|
57 thm fun_pats.supports |
|
58 thm fun_pats.fsupp |
|
59 thm fun_pats.supp |
|
60 |
|
61 lemma |
|
62 "(fv_exp x = supp x) \<and> |
|
63 (fv_fnclause xa = supp xa \<and> fv_b_lrb xa = supp_rel alpha_b_lrb xa) \<and> |
|
64 (fv_fnclauses xb = supp xb \<and> fv_b_fnclauses xb = supp_rel alpha_b_fnclauses xb) \<and> |
|
65 (fv_lrb xc = supp xc \<and> fv_b_fnclause xc = supp_rel alpha_b_fnclause xc) \<and> |
|
66 (fv_lrbs xd = supp xd \<and> fv_b_lrbs xd = supp_rel alpha_b_lrbs xd) \<and> |
|
67 (fv_pat xe = supp xe \<and> fv_b_pat xe = supp_rel alpha_b_pat xe)" |
|
68 apply(rule fun_pats.induct) |
|
69 apply(tactic {* ALLGOALS (TRY o rtac @{thm conjI})*}) |
|
70 thm fun_pats.inducts |
|
71 oops |
|
72 |
|
73 |
|
74 lemma |
|
75 "fv_exp x = supp x" and |
|
76 "fv_fnclause y = supp y" and |
|
77 "fv_fnclauses xb = supp xb" and |
|
78 "fv_lrb xc = supp xc" and |
|
79 "fv_lrbs xd = supp xd" and |
|
80 "fv_pat xe = supp xe" and |
|
81 "fv_b_lrbs xd = supp_rel alpha_b_lrbs xd" and |
|
82 "fv_b_pat xe = supp_rel alpha_b_pat xe" and |
|
83 "fv_b_fnclauses xb = supp_rel alpha_b_fnclauses xb" and |
|
84 "fv_b_fnclause xc = supp_rel alpha_b_fnclause xc" and |
|
85 "fv_b_lrb y = supp_rel alpha_b_lrb y" |
|
86 thm fun_pats.inducts |
|
87 apply(induct rule: fun_pats.inducts(1)[where ?exp="x::exp"] |
|
88 fun_pats.inducts(2)[where ?fnclause="y"] |
|
89 fun_pats.inducts(3)[where ?fnclauses="xb"] |
|
90 fun_pats.inducts(4)[where ?lrb="xc"] |
|
91 fun_pats.inducts(5)[where ?lrbs="xd"] |
|
92 fun_pats.inducts(6)[where ?pat="xe"]) |
|
93 thm fun_pats.inducts |
|
94 oops |
|
95 |
|
96 end |
|
97 |
|
98 |
|
99 |
|