equal
deleted
inserted
replaced
280 "[| lift_prog i (F i): X guarantees[v] Y; i : I; \ |
280 "[| lift_prog i (F i): X guarantees[v] Y; i : I; \ |
281 \ ALL j:I. i~=j --> lift_prog j (F j) : preserves v |] \ |
281 \ ALL j:I. i~=j --> lift_prog j (F j) : preserves v |] \ |
282 \ ==> (PLam I F) : X guarantees[v] Y"; |
282 \ ==> (PLam I F) : X guarantees[v] Y"; |
283 by (asm_simp_tac (simpset() addsimps [guarantees_JN_I]) 1); |
283 by (asm_simp_tac (simpset() addsimps [guarantees_JN_I]) 1); |
284 qed "guarantees_PLam_I"; |
284 qed "guarantees_PLam_I"; |
|
285 |
|
286 Goal "(PLam I F : preserves (v o sub j)) = \ |
|
287 \ (if j: I then F j : preserves v else True)"; |
|
288 by (asm_simp_tac (simpset() addsimps [PLam_def, lift_prog_preserves_sub]) 1); |
|
289 by (Blast_tac 1); |
|
290 qed "PLam_preserves"; |
|
291 |
|
292 AddIffs [PLam_preserves]; |