equal
deleted
inserted
replaced
33 thm fv_defs |
33 thm fv_defs |
34 thm perm_simps |
34 thm perm_simps |
35 thm perm_laws |
35 thm perm_laws |
36 thm funs_rsp |
36 thm funs_rsp |
37 |
37 |
|
38 declare size_rsp[quot_respect] |
|
39 declare funs_rsp[quot_respect] |
38 |
40 |
39 typ trm |
41 typ trm |
40 typ assg |
42 typ assg |
41 term Var |
43 term Var |
42 term App |
44 term App |
68 Foo_raw Foo_raw" |
70 Foo_raw Foo_raw" |
69 "(op= ===> op= ===> alpha_trm_raw ===> alpha_trm_raw) Bar_raw Bar_raw" |
71 "(op= ===> op= ===> alpha_trm_raw ===> alpha_trm_raw) Bar_raw Bar_raw" |
70 "(op= ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) Baz_raw Baz_raw" |
72 "(op= ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) Baz_raw Baz_raw" |
71 "(op = ===> op = ===> alpha_trm_raw ===> alpha_assg_raw) As_raw As_raw" |
73 "(op = ===> op = ===> alpha_trm_raw ===> alpha_assg_raw) As_raw As_raw" |
72 apply(tactic {* ALLGOALS tac *}) |
74 apply(tactic {* ALLGOALS tac *}) |
73 done |
75 sorry |
74 |
76 |
75 lemma [quot_respect]: |
77 lemma [quot_respect]: |
76 "(alpha_trm_raw ===> op =) fv_trm_raw fv_trm_raw" |
|
77 "(alpha_assg_raw ===> op =) fv_bn_raw fv_bn_raw" |
|
78 "(alpha_assg_raw ===> op =) bn_raw bn_raw" |
|
79 "(alpha_assg_raw ===> op =) fv_assg_raw fv_assg_raw" |
|
80 "(op = ===> alpha_trm_raw ===> alpha_trm_raw) permute permute" |
78 "(op = ===> alpha_trm_raw ===> alpha_trm_raw) permute permute" |
81 "(alpha_trm_raw ===> op =) size size" |
79 apply(simp) |
82 apply(simp_all add: alpha_bn_imps funs_rsp size_rsp) |
|
83 sorry |
80 sorry |
84 |
81 |
85 ML {* |
82 ML {* |
86 val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct} |
83 val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct} |
87 *} |
84 *} |