58 ML {* val quot = @{thm QUOTIENT_lam} *} |
58 ML {* val quot = @{thm QUOTIENT_lam} *} |
59 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rLam_rsp} @ @{thms ho_all_prs ho_ex_prs} *} |
59 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rLam_rsp} @ @{thms ho_all_prs ho_ex_prs} *} |
60 ML {* val trans2 = @{thm QUOT_TYPE_I_lam.R_trans2} *} |
60 ML {* val trans2 = @{thm QUOT_TYPE_I_lam.R_trans2} *} |
61 ML {* val reps_same = @{thm QUOT_TYPE_I_lam.REPS_same} *} |
61 ML {* val reps_same = @{thm QUOT_TYPE_I_lam.REPS_same} *} |
62 |
62 |
63 thm a3 |
63 ML {* |
64 ML {* val t_a = atomize_thm @{thm a3} *} |
64 fun lift_thm_lam lthy t = |
65 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *} |
65 lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t |
66 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} |
66 *} |
67 ML {* val abs = findabs rty (prop_of t_a) *} |
67 ML {* lift_thm_lam @{context} @{thm a3} *} |
68 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} |
|
69 ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *} |
|
70 ML {* val t_c = simp_allex_prs @{context} quot t_l *} |
|
71 ML {* val t_defs_sym = add_lower_defs @{context} defs *} |
|
72 ML {* val t_d = repeat_eqsubst_thm @{context} t_defs_sym t_c *} |
|
73 ML {* val t_b = MetaSimplifier.rewrite_rule [reps_same] t_d *} |
|
74 ML {* ObjectLogic.rulify t_b *} |
|
75 |
|
76 thm fresh_def |
|
77 thm supp_def |
|
78 |
68 |
79 local_setup {* |
69 local_setup {* |
80 old_make_const_def @{binding lperm} @{term "perm :: ('a \<times> 'a) list \<Rightarrow> rlam \<Rightarrow> rlam"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd |
70 old_make_const_def @{binding lperm} @{term "perm :: ('a \<times> 'a) list \<Rightarrow> rlam \<Rightarrow> rlam"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd |
81 *} |
71 *} |
82 |
72 |
83 ML {* val consts = @{const_name perm} :: consts *} |
73 ML {* val consts = @{const_name perm} :: consts *} |
84 ML {* val defs = @{thms lperm_def} @ defs *} |
74 ML {* val defs = @{thms lperm_def} @ defs *} |
85 ML {* val t_u = MetaSimplifier.rewrite_rule @{thms fresh_def supp_def} @{thm a3} *} |
75 ML {* |
86 ML {* val t_a = atomize_thm @{thm a3} *} |
76 fun lift_thm_lam lthy t = |
87 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *} |
77 lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t |
88 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} |
78 *} |
89 ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *} |
79 ML {* val t_b = lift_thm_lam @{context} @{thm a3} *} |
90 ML {* val t_c = simp_allex_prs @{context} quot t_l *} |
80 ML {* val rr = @{thm eq_reflection} OF [hd (rev (add_lower_defs @{context} @{thms lperm_def}))] *} |
91 ML {* val t_defs_sym = add_lower_defs @{context} defs *} |
|
92 ML {* val t_d = repeat_eqsubst_thm @{context} t_defs_sym t_c *} |
|
93 ML {* val t_b = MetaSimplifier.rewrite_rule [reps_same] t_d *} |
|
94 ML {* val rr = (add_lower_defs @{context} @{thms lperm_def}) *} |
|
95 ML {* val rrr = @{thm eq_reflection} OF [hd (rev rr)] *} |
|
96 lemma prod_fun_id: "prod_fun id id = id" |
81 lemma prod_fun_id: "prod_fun id id = id" |
97 apply (simp add: prod_fun_def) |
82 apply (simp add: prod_fun_def) |
98 done |
83 done |
99 lemma map_id: "map id x = x" |
84 lemma map_id: "map id x = x" |
100 apply (induct x) |
85 apply (induct x) |
101 apply (simp_all add: map.simps) |
86 apply (simp_all add: map.simps) |
102 done |
87 done |
103 |
88 |
104 ML {* val rrrr = repeat_eqsubst_thm @{context} @{thms prod_fun_id map_id} rrr *} |
89 ML {* val rrr = repeat_eqsubst_thm @{context} @{thms prod_fun_id map_id} rr *} |
105 ML {* val t_b' = eqsubst_thm @{context} [rrrr] t_b *} |
90 ML {* val t_b' = eqsubst_thm @{context} [rrr] (atomize_thm t_b) *} |
106 ML {* ObjectLogic.rulify t_b' *} |
91 ML {* ObjectLogic.rulify t_b' *} |
107 |
92 |
|
93 ML {* val t_u = MetaSimplifier.rewrite_rule @{thms fresh_def supp_def} @{thm a3} *} |
|
94 lemma "alpha ===> (alpha ===> op =) op = op =" |
|
95 sorry |
108 |
96 |
109 |
97 ML {* Toplevel.program (fn () => lift_thm_lam @{context} t_u) *} (* Is not ture *) |
110 local_setup {* |
|
111 make_const_def @{binding lfresh} @{term "fresh :: 'a \<Rightarrow> rlam \<Rightarrow> bool"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #> |
|
112 *} |
|
113 @{const_name fresh} :: |
|
114 lfresh_def |
|
115 ML {* |
|
116 fun lift_thm_lam lthy t = |
|
117 lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t |
|
118 *} |
|
119 |
|
120 ML {* Toplevel.program (fn () => lift_thm_lam @{context} @{thm a3}) *} |
|
121 |
|