2165 apply(generate_fresh "name") |
2165 apply(generate_fresh "name") |
2166 apply(subgoal_tac "NotR (x).M d = NotR (c).([(c,x)]\<bullet>M) d") |
2166 apply(subgoal_tac "NotR (x).M d = NotR (c).([(c,x)]\<bullet>M) d") |
2167 apply(auto simp add: fresh_left calc_atm forget) |
2167 apply(auto simp add: fresh_left calc_atm forget) |
2168 apply(generate_fresh "coname") |
2168 apply(generate_fresh "coname") |
2169 apply(rule_tac f="fresh_fun" in arg_cong) |
2169 apply(rule_tac f="fresh_fun" in arg_cong) |
2170 apply(simp add: ext_iff) |
2170 apply(simp add: fun_eq_iff) |
2171 apply(rule allI) |
2171 apply(rule allI) |
2172 apply(simp add: trm.inject alpha fresh_prod fresh_atm) |
2172 apply(simp add: trm.inject alpha fresh_prod fresh_atm) |
2173 apply(perm_simp add: trm.inject alpha fresh_prod fresh_atm fresh_left, auto) |
2173 apply(perm_simp add: trm.inject alpha fresh_prod fresh_atm fresh_left, auto) |
2174 done |
2174 done |
2175 |
2175 |
2181 apply(generate_fresh "coname") |
2181 apply(generate_fresh "coname") |
2182 apply(subgoal_tac "NotL <a>.M y = NotL <ca>.([(ca,a)]\<bullet>M) y") |
2182 apply(subgoal_tac "NotL <a>.M y = NotL <ca>.([(ca,a)]\<bullet>M) y") |
2183 apply(auto simp add: fresh_left calc_atm forget) |
2183 apply(auto simp add: fresh_left calc_atm forget) |
2184 apply(generate_fresh "name") |
2184 apply(generate_fresh "name") |
2185 apply(rule_tac f="fresh_fun" in arg_cong) |
2185 apply(rule_tac f="fresh_fun" in arg_cong) |
2186 apply(simp add: ext_iff) |
2186 apply(simp add: fun_eq_iff) |
2187 apply(rule allI) |
2187 apply(rule allI) |
2188 apply(simp add: trm.inject alpha fresh_prod fresh_atm) |
2188 apply(simp add: trm.inject alpha fresh_prod fresh_atm) |
2189 apply(perm_simp add: trm.inject alpha fresh_prod fresh_atm fresh_left, auto) |
2189 apply(perm_simp add: trm.inject alpha fresh_prod fresh_atm fresh_left, auto) |
2190 done |
2190 done |
2191 |
2191 |
2197 apply(generate_fresh "name") |
2197 apply(generate_fresh "name") |
2198 apply(subgoal_tac "AndL1 (x).M y = AndL1 (ca).([(ca,x)]\<bullet>M) y") |
2198 apply(subgoal_tac "AndL1 (x).M y = AndL1 (ca).([(ca,x)]\<bullet>M) y") |
2199 apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1] |
2199 apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1] |
2200 apply(generate_fresh "name") |
2200 apply(generate_fresh "name") |
2201 apply(rule_tac f="fresh_fun" in arg_cong) |
2201 apply(rule_tac f="fresh_fun" in arg_cong) |
2202 apply(simp add: ext_iff) |
2202 apply(simp add: fun_eq_iff) |
2203 apply(rule allI) |
2203 apply(rule allI) |
2204 apply(simp add: trm.inject alpha fresh_prod fresh_atm) |
2204 apply(simp add: trm.inject alpha fresh_prod fresh_atm) |
2205 apply(rule forget) |
2205 apply(rule forget) |
2206 apply(simp add: fresh_left calc_atm) |
2206 apply(simp add: fresh_left calc_atm) |
2207 apply(rule_tac f="fresh_fun" in arg_cong) |
2207 apply(rule_tac f="fresh_fun" in arg_cong) |
2208 apply(simp add: ext_iff) |
2208 apply(simp add: fun_eq_iff) |
2209 apply(rule allI) |
2209 apply(rule allI) |
2210 apply(simp add: trm.inject alpha fresh_prod fresh_atm) |
2210 apply(simp add: trm.inject alpha fresh_prod fresh_atm) |
2211 apply(rule forget) |
2211 apply(rule forget) |
2212 apply(simp add: fresh_left calc_atm) |
2212 apply(simp add: fresh_left calc_atm) |
2213 apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm) |
2213 apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm) |
2222 apply(generate_fresh "name") |
2222 apply(generate_fresh "name") |
2223 apply(subgoal_tac "AndL2 (x).M y = AndL2 (ca).([(ca,x)]\<bullet>M) y") |
2223 apply(subgoal_tac "AndL2 (x).M y = AndL2 (ca).([(ca,x)]\<bullet>M) y") |
2224 apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1] |
2224 apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1] |
2225 apply(generate_fresh "name") |
2225 apply(generate_fresh "name") |
2226 apply(rule_tac f="fresh_fun" in arg_cong) |
2226 apply(rule_tac f="fresh_fun" in arg_cong) |
2227 apply(simp add: ext_iff) |
2227 apply(simp add: fun_eq_iff) |
2228 apply(rule allI) |
2228 apply(rule allI) |
2229 apply(simp add: trm.inject alpha fresh_prod fresh_atm) |
2229 apply(simp add: trm.inject alpha fresh_prod fresh_atm) |
2230 apply(rule forget) |
2230 apply(rule forget) |
2231 apply(simp add: fresh_left calc_atm) |
2231 apply(simp add: fresh_left calc_atm) |
2232 apply(rule_tac f="fresh_fun" in arg_cong) |
2232 apply(rule_tac f="fresh_fun" in arg_cong) |
2233 apply(simp add: ext_iff) |
2233 apply(simp add: fun_eq_iff) |
2234 apply(rule allI) |
2234 apply(rule allI) |
2235 apply(simp add: trm.inject alpha fresh_prod fresh_atm) |
2235 apply(simp add: trm.inject alpha fresh_prod fresh_atm) |
2236 apply(rule forget) |
2236 apply(rule forget) |
2237 apply(simp add: fresh_left calc_atm) |
2237 apply(simp add: fresh_left calc_atm) |
2238 apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm) |
2238 apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm) |
2253 apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1] |
2253 apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1] |
2254 apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1] |
2254 apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1] |
2255 apply(auto simp add: fresh_prod fresh_atm)[1] |
2255 apply(auto simp add: fresh_prod fresh_atm)[1] |
2256 apply(simp) |
2256 apply(simp) |
2257 apply(rule_tac f="fresh_fun" in arg_cong) |
2257 apply(rule_tac f="fresh_fun" in arg_cong) |
2258 apply(simp add: ext_iff) |
2258 apply(simp add: fun_eq_iff) |
2259 apply(rule allI) |
2259 apply(rule allI) |
2260 apply(simp add: trm.inject alpha fresh_prod fresh_atm) |
2260 apply(simp add: trm.inject alpha fresh_prod fresh_atm) |
2261 apply(rule conjI) |
2261 apply(rule conjI) |
2262 apply(rule forget) |
2262 apply(rule forget) |
2263 apply(auto simp add: fresh_left calc_atm abs_fresh)[1] |
2263 apply(auto simp add: fresh_left calc_atm abs_fresh)[1] |
2281 apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1] |
2281 apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1] |
2282 apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1] |
2282 apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1] |
2283 apply(auto simp add: fresh_prod fresh_atm)[1] |
2283 apply(auto simp add: fresh_prod fresh_atm)[1] |
2284 apply(simp) |
2284 apply(simp) |
2285 apply(rule_tac f="fresh_fun" in arg_cong) |
2285 apply(rule_tac f="fresh_fun" in arg_cong) |
2286 apply(simp add: ext_iff) |
2286 apply(simp add: fun_eq_iff) |
2287 apply(rule allI) |
2287 apply(rule allI) |
2288 apply(simp add: trm.inject alpha fresh_prod fresh_atm) |
2288 apply(simp add: trm.inject alpha fresh_prod fresh_atm) |
2289 apply(rule conjI) |
2289 apply(rule conjI) |
2290 apply(rule forget) |
2290 apply(rule forget) |
2291 apply(auto simp add: fresh_left calc_atm abs_fresh)[1] |
2291 apply(auto simp add: fresh_left calc_atm abs_fresh)[1] |
2302 apply - |
2302 apply - |
2303 apply(generate_fresh "coname") |
2303 apply(generate_fresh "coname") |
2304 apply(subgoal_tac "OrR1 <a>.M d = OrR1 <c>.([(c,a)]\<bullet>M) d") |
2304 apply(subgoal_tac "OrR1 <a>.M d = OrR1 <c>.([(c,a)]\<bullet>M) d") |
2305 apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1] |
2305 apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1] |
2306 apply(rule_tac f="fresh_fun" in arg_cong) |
2306 apply(rule_tac f="fresh_fun" in arg_cong) |
2307 apply(simp add: ext_iff) |
2307 apply(simp add: fun_eq_iff) |
2308 apply(rule allI) |
2308 apply(rule allI) |
2309 apply(simp add: trm.inject alpha fresh_prod fresh_atm) |
2309 apply(simp add: trm.inject alpha fresh_prod fresh_atm) |
2310 apply(rule forget) |
2310 apply(rule forget) |
2311 apply(simp add: fresh_left calc_atm) |
2311 apply(simp add: fresh_left calc_atm) |
2312 apply(rule_tac f="fresh_fun" in arg_cong) |
2312 apply(rule_tac f="fresh_fun" in arg_cong) |
2313 apply(simp add: ext_iff) |
2313 apply(simp add: fun_eq_iff) |
2314 apply(rule allI) |
2314 apply(rule allI) |
2315 apply(simp add: trm.inject alpha fresh_prod fresh_atm) |
2315 apply(simp add: trm.inject alpha fresh_prod fresh_atm) |
2316 apply(rule forget) |
2316 apply(rule forget) |
2317 apply(simp add: fresh_left calc_atm) |
2317 apply(simp add: fresh_left calc_atm) |
2318 apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm) |
2318 apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm) |
2326 apply - |
2326 apply - |
2327 apply(generate_fresh "coname") |
2327 apply(generate_fresh "coname") |
2328 apply(subgoal_tac "OrR2 <a>.M d = OrR2 <c>.([(c,a)]\<bullet>M) d") |
2328 apply(subgoal_tac "OrR2 <a>.M d = OrR2 <c>.([(c,a)]\<bullet>M) d") |
2329 apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1] |
2329 apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1] |
2330 apply(rule_tac f="fresh_fun" in arg_cong) |
2330 apply(rule_tac f="fresh_fun" in arg_cong) |
2331 apply(simp add: ext_iff) |
2331 apply(simp add: fun_eq_iff) |
2332 apply(rule allI) |
2332 apply(rule allI) |
2333 apply(simp add: trm.inject alpha fresh_prod fresh_atm) |
2333 apply(simp add: trm.inject alpha fresh_prod fresh_atm) |
2334 apply(rule forget) |
2334 apply(rule forget) |
2335 apply(simp add: fresh_left calc_atm) |
2335 apply(simp add: fresh_left calc_atm) |
2336 apply(rule_tac f="fresh_fun" in arg_cong) |
2336 apply(rule_tac f="fresh_fun" in arg_cong) |
2337 apply(simp add: ext_iff) |
2337 apply(simp add: fun_eq_iff) |
2338 apply(rule allI) |
2338 apply(rule allI) |
2339 apply(simp add: trm.inject alpha fresh_prod fresh_atm) |
2339 apply(simp add: trm.inject alpha fresh_prod fresh_atm) |
2340 apply(rule forget) |
2340 apply(rule forget) |
2341 apply(simp add: fresh_left calc_atm) |
2341 apply(simp add: fresh_left calc_atm) |
2342 apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm) |
2342 apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm) |
2351 apply(generate_fresh "coname") |
2351 apply(generate_fresh "coname") |
2352 apply(generate_fresh "name") |
2352 apply(generate_fresh "name") |
2353 apply(subgoal_tac "ImpR (x).<a>.M d = ImpR (ca).<c>.([(c,a)]\<bullet>[(ca,x)]\<bullet>M) d") |
2353 apply(subgoal_tac "ImpR (x).<a>.M d = ImpR (ca).<c>.([(c,a)]\<bullet>[(ca,x)]\<bullet>M) d") |
2354 apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1] |
2354 apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1] |
2355 apply(rule_tac f="fresh_fun" in arg_cong) |
2355 apply(rule_tac f="fresh_fun" in arg_cong) |
2356 apply(simp add: ext_iff) |
2356 apply(simp add: fun_eq_iff) |
2357 apply(rule allI) |
2357 apply(rule allI) |
2358 apply(simp add: trm.inject alpha fresh_prod fresh_atm abs_perm abs_fresh fresh_left calc_atm) |
2358 apply(simp add: trm.inject alpha fresh_prod fresh_atm abs_perm abs_fresh fresh_left calc_atm) |
2359 apply(rule forget) |
2359 apply(rule forget) |
2360 apply(simp add: fresh_left calc_atm) |
2360 apply(simp add: fresh_left calc_atm) |
2361 apply(rule_tac f="fresh_fun" in arg_cong) |
2361 apply(rule_tac f="fresh_fun" in arg_cong) |
2362 apply(simp add: ext_iff) |
2362 apply(simp add: fun_eq_iff) |
2363 apply(rule allI) |
2363 apply(rule allI) |
2364 apply(simp add: trm.inject alpha fresh_prod fresh_atm abs_perm fresh_left calc_atm abs_fresh) |
2364 apply(simp add: trm.inject alpha fresh_prod fresh_atm abs_perm fresh_left calc_atm abs_fresh) |
2365 apply(rule forget) |
2365 apply(rule forget) |
2366 apply(simp add: fresh_left calc_atm) |
2366 apply(simp add: fresh_left calc_atm) |
2367 apply(rule sym) |
2367 apply(rule sym) |
2376 apply(generate_fresh "coname") |
2376 apply(generate_fresh "coname") |
2377 apply(generate_fresh "name") |
2377 apply(generate_fresh "name") |
2378 apply(subgoal_tac "ImpL <a>.M (x).N y = ImpL <ca>.([(ca,a)]\<bullet>M) (caa).([(caa,x)]\<bullet>N) y") |
2378 apply(subgoal_tac "ImpL <a>.M (x).N y = ImpL <ca>.([(ca,a)]\<bullet>M) (caa).([(caa,x)]\<bullet>N) y") |
2379 apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1] |
2379 apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1] |
2380 apply(rule_tac f="fresh_fun" in arg_cong) |
2380 apply(rule_tac f="fresh_fun" in arg_cong) |
2381 apply(simp add: ext_iff) |
2381 apply(simp add: fun_eq_iff) |
2382 apply(rule allI) |
2382 apply(rule allI) |
2383 apply(simp add: trm.inject alpha fresh_prod fresh_atm abs_perm abs_fresh fresh_left calc_atm) |
2383 apply(simp add: trm.inject alpha fresh_prod fresh_atm abs_perm abs_fresh fresh_left calc_atm) |
2384 apply(rule forget) |
2384 apply(rule forget) |
2385 apply(simp add: fresh_left calc_atm) |
2385 apply(simp add: fresh_left calc_atm) |
2386 apply(auto)[1] |
2386 apply(auto)[1] |