80 |
80 |
81 |
81 |
82 |
82 |
83 (* Construction Site code *) |
83 (* Construction Site code *) |
84 |
84 |
85 lemma perm_rsp: "op = ===> alpha ===> alpha op \<bullet> op \<bullet>" |
85 lemma perm_rsp: "(op = ===> alpha ===> alpha) op \<bullet> op \<bullet>" |
86 apply(auto) |
86 apply(auto) |
87 (* this is propably true if some type conditions are imposed ;o) *) |
87 (* this is propably true if some type conditions are imposed ;o) *) |
88 sorry |
88 sorry |
89 |
89 |
90 lemma fresh_rsp: "op = ===> (alpha ===> op =) fresh fresh" |
90 lemma fresh_rsp: "(op = ===> alpha ===> op =) fresh fresh" |
91 apply(auto) |
91 apply(auto) |
92 (* this is probably only true if some type conditions are imposed *) |
92 (* this is probably only true if some type conditions are imposed *) |
93 sorry |
93 sorry |
94 |
94 |
95 lemma rLam_rsp: "op = ===> (alpha ===> alpha) rLam rLam" |
95 lemma rVar_rsp: "(op = ===> alpha) rVar rVar" |
|
96 apply(auto) |
|
97 apply(rule a1) |
|
98 apply(simp) |
|
99 done |
|
100 |
|
101 lemma rApp_rsp: "(alpha ===> alpha ===> alpha) rApp rApp" |
|
102 apply(auto) |
|
103 apply(rule a2) |
|
104 apply (assumption) |
|
105 apply (assumption) |
|
106 done |
|
107 |
|
108 lemma rLam_rsp: "(op = ===> alpha ===> alpha) rLam rLam" |
96 apply(auto) |
109 apply(auto) |
97 apply(rule a3) |
110 apply(rule a3) |
98 apply(rule_tac t="[(x,x)]\<bullet>y" and s="y" in subst) |
111 apply(rule_tac t="[(x,x)]\<bullet>y" and s="y" in subst) |
99 apply(rule sym) |
112 apply(rule sym) |
100 apply(rule trans) |
113 apply(rule trans) |
103 apply(simp add: pt_name1) |
116 apply(simp add: pt_name1) |
104 apply(assumption) |
117 apply(assumption) |
105 apply(simp add: abs_fresh) |
118 apply(simp add: abs_fresh) |
106 done |
119 done |
107 |
120 |
108 ML {* val defs = @{thms Var_def App_def Lam_def} *} |
121 ML {* val defs = @{thms Var_def App_def Lam_def perm_lam_def} *} |
109 ML {* val consts = [@{const_name "rVar"}, @{const_name "rApp"}, @{const_name "rLam"}]; *} |
122 ML {* val consts = [@{const_name "rVar"}, @{const_name "rApp"}, @{const_name "rLam"}, @{const_name "perm"}]; *} |
110 |
123 |
111 ML {* val rty = @{typ "rlam"} *} |
124 ML {* val rty = @{typ "rlam"} *} |
112 ML {* val qty = @{typ "lam"} *} |
125 ML {* val qty = @{typ "lam"} *} |
113 ML {* val rel = @{term "alpha"} *} |
126 ML {* val rel = @{term "alpha"} *} |
114 ML {* val rel_eqv = (#equiv_thm o hd) (quotdata_lookup @{context}) *} |
127 ML {* val rel_eqv = (#equiv_thm o hd) (quotdata_lookup @{context}) *} |
115 ML {* val rel_refl = @{thm EQUIV_REFL} OF [rel_eqv] *} |
128 ML {* val rel_refl = @{thm EQUIV_REFL} OF [rel_eqv] *} |
116 ML {* val quot = @{thm QUOTIENT_lam} *} |
129 ML {* val quot = @{thm QUOTIENT_lam} *} |
117 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rLam_rsp} @ @{thms ho_all_prs ho_ex_prs} *} |
130 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp} @ @{thms ho_all_prs ho_ex_prs} *} |
118 ML {* val trans2 = @{thm QUOT_TYPE_I_lam.R_trans2} *} |
131 ML {* val trans2 = @{thm QUOT_TYPE_I_lam.R_trans2} *} |
119 ML {* val reps_same = @{thm QUOT_TYPE_I_lam.REPS_same} *} |
132 ML {* val reps_same = @{thm QUOT_TYPE_I_lam.REPS_same} *} |
120 |
133 |
121 ML {* |
134 ML {* add_lower_defs @{context} @{thms perm_lam_def} *} |
122 fun lift_thm_lam lthy t = |
135 ML {* val rr = @{thm eq_reflection} OF [hd (rev (add_lower_defs @{context} @{thms perm_lam_def}))] *} |
123 lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t |
|
124 *} |
|
125 ML {* lift_thm_lam @{context} @{thm a3} *} |
|
126 |
|
127 local_setup {* |
|
128 old_make_const_def @{binding lperm} @{term "perm :: ('a \<times> 'a) list \<Rightarrow> rlam \<Rightarrow> rlam"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd |
|
129 *} |
|
130 |
|
131 ML {* val consts = @{const_name perm} :: consts *} |
|
132 ML {* val defs = @{thms lperm_def} @ defs *} |
|
133 ML {* |
|
134 fun lift_thm_lam lthy t = |
|
135 lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t |
|
136 *} |
|
137 ML {* val t_b = lift_thm_lam @{context} @{thm a3} *} |
|
138 ML {* val rr = @{thm eq_reflection} OF [hd (rev (add_lower_defs @{context} @{thms lperm_def}))] *} |
|
139 lemma prod_fun_id: "prod_fun id id = id" |
136 lemma prod_fun_id: "prod_fun id id = id" |
140 apply (simp add: prod_fun_def) |
137 apply (simp add: prod_fun_def) |
141 done |
138 done |
142 lemma map_id: "map id x = x" |
139 lemma map_id: "map id x = x" |
143 apply (induct x) |
140 apply (induct x) |
144 apply (simp_all add: map.simps) |
141 apply (simp_all add: map.simps) |
145 done |
142 done |
|
143 ML {* val rrr = repeat_eqsubst_thm @{context} @{thms prod_fun_id map_id} rr *} |
|
144 ML {* |
|
145 fun lift_thm_lam lthy t = |
|
146 lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t |
|
147 *} |
|
148 ML {* val t1 = Toplevel.program (fn () => lift_thm_lam @{context} @{thm pi_var_com}) *} |
|
149 ML {* val t2 = eqsubst_thm @{context} [rrr] (atomize_thm t1) *} |
|
150 ML {* ObjectLogic.rulify t2 *} |
|
151 ML {* val t1 = Toplevel.program (fn () => lift_thm_lam @{context} @{thm pi_app_com}) *} |
|
152 ML {* val t2 = repeat_eqsubst_thm @{context} [rrr] (atomize_thm t1) *} |
|
153 ML {* ObjectLogic.rulify t2 *} |
|
154 ML {* val t1 = Toplevel.program (fn () => lift_thm_lam @{context} @{thm pi_lam_com}) *} |
|
155 ML {* val t2 = repeat_eqsubst_thm @{context} [rrr] (atomize_thm t1) *} |
|
156 ML {* ObjectLogic.rulify t2 *} |
146 |
157 |
147 ML {* val rrr = repeat_eqsubst_thm @{context} @{thms prod_fun_id map_id} rr *} |
|
148 ML {* val t_b' = eqsubst_thm @{context} [rrr] (atomize_thm t_b) *} |
|
149 ML {* ObjectLogic.rulify t_b' *} |
|
150 |
|
151 ML {* val t_u = MetaSimplifier.rewrite_rule @{thms fresh_def supp_def} @{thm a3} *} |
|
152 ML {* Toplevel.program (fn () => lift_thm_lam @{context} t_u) *} (* Is not ture *) |
|