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 declare [[STEPS = 100]] |
9 declare [[STEPS = 31]] |
10 |
10 |
11 nominal_datatype exp = |
11 nominal_datatype fun_pats: exp = |
12 EVar name |
12 EVar name |
13 | EUnit |
13 | EUnit |
14 | EPair exp exp |
14 | EPair exp exp |
15 | ELetRec l::lrbs e::exp bind (set) "b_lrbs l" in l e |
15 | ELetRec l::lrbs e::exp bind (set) "b_lrbs l" in l e |
16 and fnclause = |
16 and fnclause = |
17 K x::name p::pat f::exp bind (set) "b_pat p" in f |
17 K x::name p::pat f::exp bind (set) "b_pat p" in f |
18 and fnclauses = |
18 and fnclauses = |
42 | "b_fnclauses (S fc) = (b_fnclause fc)" |
42 | "b_fnclauses (S fc) = (b_fnclause fc)" |
43 | "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)" |
43 | "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)" |
44 | "b_lrb (Clause fcs) = (b_fnclauses fcs)" |
44 | "b_lrb (Clause fcs) = (b_fnclauses fcs)" |
45 | "b_fnclause (K x pat exp) = {atom x}" |
45 | "b_fnclause (K x pat exp) = {atom x}" |
46 |
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 |
|
62 ML {* |
|
63 fun add_ss thms = |
|
64 HOL_basic_ss addsimps thms |
|
65 |
|
66 fun symmetric thms = |
|
67 map (fn thm => thm RS @{thm sym}) thms |
|
68 *} |
|
69 |
|
70 lemma |
|
71 "(fv_exp x = supp x) \<and> |
|
72 (fv_fnclause xa = supp xa \<and> fv_b_lrb xa = supp_rel alpha_b_lrb xa) \<and> |
|
73 (fv_fnclauses xb = supp xb \<and> fv_b_fnclauses xb = supp_rel alpha_b_fnclauses xb) \<and> |
|
74 (fv_lrb xc = supp xc \<and> fv_b_fnclause xc = supp_rel alpha_b_fnclause xc) \<and> |
|
75 (fv_lrbs xd = supp xd \<and> fv_b_lrbs xd = supp_rel alpha_b_lrbs xd) \<and> |
|
76 (fv_pat xe = supp xe \<and> fv_b_pat xe = supp_rel alpha_b_pat xe)" |
|
77 apply(rule fun_pats.induct) |
|
78 apply(tactic {* ALLGOALS (TRY o rtac @{thm conjI})*}) |
|
79 thm fun_pats.inducts |
|
80 oops |
|
81 |
|
82 |
|
83 lemma |
|
84 "fv_exp x = supp x" and |
|
85 "fv_fnclause y = supp y" and |
|
86 "fv_fnclauses xb = supp xb" and |
|
87 "fv_lrb xc = supp xc" and |
|
88 "fv_lrbs xd = supp xd" and |
|
89 "fv_pat xe = supp xe" and |
|
90 "fv_b_lrbs xd = supp_rel alpha_b_lrbs xd" and |
|
91 "fv_b_pat xe = supp_rel alpha_b_pat xe" and |
|
92 "fv_b_fnclauses xb = supp_rel alpha_b_fnclauses xb" and |
|
93 "fv_b_fnclause xc = supp_rel alpha_b_fnclause xc" and |
|
94 "fv_b_lrb y = supp_rel alpha_b_lrb y" |
|
95 apply(induct "x::exp" and "y::fnclause" and xb and xc and xd and xe rule: fun_pats.inducts) |
|
96 thm fun_pats.inducts |
|
97 oops |
47 |
98 |
48 end |
99 end |
49 |
100 |
50 |
101 |
51 |
102 |