equal
deleted
inserted
replaced
41 |
41 |
42 |
42 |
43 |
43 |
44 (* Construction Site code *) |
44 (* Construction Site code *) |
45 |
45 |
46 lemma perm_rsp: "op = ===> alpha ===> alpha op \<bullet> op \<bullet>" sorry |
46 lemma perm_rsp: "(op = ===> alpha ===> alpha) op \<bullet> op \<bullet>" sorry |
47 lemma fresh_rsp: "op = ===> (alpha ===> op =) fresh fresh" sorry |
47 lemma fresh_rsp: "(op = ===> (alpha ===> op =)) fresh fresh" sorry |
48 lemma rLam_rsp: "op = ===> (alpha ===> alpha) rLam rLam" sorry |
48 lemma rLam_rsp: "(op = ===> (alpha ===> alpha)) rLam rLam" sorry |
49 |
49 |
50 ML {* val defs = @{thms Var_def App_def Lam_def} *} |
50 ML {* val defs = @{thms Var_def App_def Lam_def} *} |
51 ML {* val consts = [@{const_name "rVar"}, @{const_name "rApp"}, @{const_name "rLam"}]; *} |
51 ML {* val consts = [@{const_name "rVar"}, @{const_name "rApp"}, @{const_name "rLam"}]; *} |
52 |
52 |
53 ML {* val rty = @{typ "rlam"} *} |
53 ML {* val rty = @{typ "rlam"} *} |
89 ML {* val rrr = repeat_eqsubst_thm @{context} @{thms prod_fun_id map_id} rr *} |
89 ML {* val rrr = repeat_eqsubst_thm @{context} @{thms prod_fun_id map_id} rr *} |
90 ML {* val t_b' = eqsubst_thm @{context} [rrr] (atomize_thm t_b) *} |
90 ML {* val t_b' = eqsubst_thm @{context} [rrr] (atomize_thm t_b) *} |
91 ML {* ObjectLogic.rulify t_b' *} |
91 ML {* ObjectLogic.rulify t_b' *} |
92 |
92 |
93 ML {* val t_u = MetaSimplifier.rewrite_rule @{thms fresh_def supp_def} @{thm a3} *} |
93 ML {* val t_u = MetaSimplifier.rewrite_rule @{thms fresh_def supp_def} @{thm a3} *} |
94 lemma "alpha ===> (alpha ===> op =) op = op =" |
|
95 sorry |
|
96 |
|
97 ML {* Toplevel.program (fn () => lift_thm_lam @{context} t_u) *} (* Is not ture *) |
94 ML {* Toplevel.program (fn () => lift_thm_lam @{context} t_u) *} (* Is not ture *) |