463 {hp, (Bool (v1 = v2) # os), lvars}" |
463 {hp, (Bool (v1 = v2) # os), lvars}" |
464 apply (case_tac "v1 = v2") |
464 apply (case_tac "v1 = v2") |
465 |
465 |
466 (* case v1 = v2 *) |
466 (* case v1 = v2 *) |
467 apply (rule_tac "instrs1.0" = "[LitPush (Bool True)]" in jump_fwd_progression) |
467 apply (rule_tac "instrs1.0" = "[LitPush (Bool True)]" in jump_fwd_progression) |
468 apply (auto simp: NatBin.nat_add_distrib) |
468 apply (auto simp: nat_add_distrib) |
469 apply (rule progression_one_step) apply simp |
469 apply (rule progression_one_step) apply simp |
470 |
470 |
471 (* case v1 \<noteq> v2 *) |
471 (* case v1 \<noteq> v2 *) |
472 apply (rule progression_one_step [THEN HOL.refl [THEN progression_transitive], simplified]) |
472 apply (rule progression_one_step [THEN HOL.refl [THEN progression_transitive], simplified]) |
473 apply auto |
473 apply auto |
474 apply (rule progression_one_step [THEN HOL.refl [THEN progression_transitive], simplified]) |
474 apply (rule progression_one_step [THEN HOL.refl [THEN progression_transitive], simplified]) |
475 apply auto |
475 apply auto |
476 apply (rule_tac "instrs1.0" = "[]" in jump_fwd_progression) |
476 apply (rule_tac "instrs1.0" = "[]" in jump_fwd_progression) |
477 apply (auto simp: NatBin.nat_add_distrib intro: progression_refl) |
477 apply (auto simp: nat_add_distrib intro: progression_refl) |
478 done |
478 done |
479 |
479 |
480 |
480 |
481 (**********************************************************************) |
481 (**********************************************************************) |
482 |
482 |
1006 apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl) |
1006 apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl) |
1007 apply (rule_tac "instrs0.0" = "(compStmt (gmb G CL S) c1)" in progression_transitive, simp) |
1007 apply (rule_tac "instrs0.0" = "(compStmt (gmb G CL S) c1)" in progression_transitive, simp) |
1008 apply fast |
1008 apply fast |
1009 apply (rule_tac "instrs1.0" = "[]" in jump_fwd_progression) |
1009 apply (rule_tac "instrs1.0" = "[]" in jump_fwd_progression) |
1010 apply (simp, rule conjI, (rule HOL.refl)+) |
1010 apply (simp, rule conjI, (rule HOL.refl)+) |
1011 apply simp apply (rule conjI, simp) apply (simp add: NatBin.nat_add_distrib) |
1011 apply simp apply (rule conjI, simp) apply (simp add: nat_add_distrib) |
1012 apply (rule progression_refl) |
1012 apply (rule progression_refl) |
1013 |
1013 |
1014 (* case b= False *) |
1014 (* case b= False *) |
1015 apply simp |
1015 apply simp |
1016 apply (rule_tac "instrs1.0" = "compStmt (gmb G CL S) c2" in jump_fwd_progression) |
1016 apply (rule_tac "instrs1.0" = "compStmt (gmb G CL S) c2" in jump_fwd_progression) |
1017 apply (simp, rule conjI, (rule HOL.refl)+) |
1017 apply (simp, rule conjI, (rule HOL.refl)+) |
1018 apply (simp, rule conjI, rule HOL.refl, simp add: NatBin.nat_add_distrib) |
1018 apply (simp, rule conjI, rule HOL.refl, simp add: nat_add_distrib) |
1019 apply fast |
1019 apply fast |
1020 |
1020 |
1021 (* case exit Loop *) |
1021 (* case exit Loop *) |
1022 apply (intro allI impI) |
1022 apply (intro allI impI) |
1023 apply (frule wtpd_stmt_loop, (erule conjE)+) |
1023 apply (frule wtpd_stmt_loop, (erule conjE)+) |
1041 |
1041 |
1042 apply (rule_tac "instrs0.0" = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl) |
1042 apply (rule_tac "instrs0.0" = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl) |
1043 apply fast |
1043 apply fast |
1044 apply (rule_tac "instrs1.0" = "[]" in jump_fwd_progression) |
1044 apply (rule_tac "instrs1.0" = "[]" in jump_fwd_progression) |
1045 apply (simp, rule conjI, rule HOL.refl, rule HOL.refl) |
1045 apply (simp, rule conjI, rule HOL.refl, rule HOL.refl) |
1046 apply (simp, rule conjI, rule HOL.refl, simp add: NatBin.nat_add_distrib) |
1046 apply (simp, rule conjI, rule HOL.refl, simp add: nat_add_distrib) |
1047 apply (rule progression_refl) |
1047 apply (rule progression_refl) |
1048 |
1048 |
1049 |
1049 |
1050 (* case continue Loop *) |
1050 (* case continue Loop *) |
1051 apply (intro allI impI) |
1051 apply (intro allI impI) |