36 (fn _ => [ auto_tac (Inc_css addsimps2 gamma2_def::PsiInv_defs) ]); |
36 (fn _ => [ auto_tac (Inc_css addsimps2 gamma2_def::PsiInv_defs) ]); |
37 |
37 |
38 qed_goal "PsiInv_stutter" Inc.thy "unchanged <x,y,sem,pc1,pc2> .& PsiInv .-> PsiInv`" |
38 qed_goal "PsiInv_stutter" Inc.thy "unchanged <x,y,sem,pc1,pc2> .& PsiInv .-> PsiInv`" |
39 (fn _ => [ auto_tac (Inc_css addsimps2 PsiInv_defs) ]); |
39 (fn _ => [ auto_tac (Inc_css addsimps2 PsiInv_defs) ]); |
40 |
40 |
41 qed_goal "PsiInv" Inc.thy "Psi .-> []PsiInv" |
41 qed_goal "PsiInv" Inc.thy "Psi .-> []PsiInv" (K [ |
42 (fn _ => [inv_tac (Inc_css addsimps2 [Psi_def]) 1, |
42 inv_tac (Inc_css addsimps2 [Psi_def]) 1, |
43 SELECT_GOAL (auto_tac (Inc_css addSIs2 [action_mp PsiInv_Init] |
43 SELECT_GOAL (auto_tac (Inc_css addSIs2 [action_mp PsiInv_Init] |
44 addsimps2 [Init_def])) 1, |
44 addsimps2 [Init_def])) 1, |
45 auto_tac (Inc_css addSEs2 (map action_conjimpE |
45 force_tac (Inc_css addSEs2 (map action_conjimpE |
46 [PsiInv_alpha1,PsiInv_alpha2,PsiInv_beta1, |
46 [PsiInv_alpha1,PsiInv_alpha2,PsiInv_beta1, |
47 PsiInv_beta2,PsiInv_gamma1,PsiInv_gamma2]) |
47 PsiInv_beta2,PsiInv_gamma1,PsiInv_gamma2]) |
48 addIs2 [action_mp PsiInv_stutter] |
48 addIs2 [action_mp PsiInv_stutter] |
49 addsimps2 [square_def,N1_def, N2_def]) |
49 addsimps2 [square_def,N1_def, N2_def]) 1]); |
50 ]); |
|
51 |
50 |
52 |
51 |
53 |
52 |
54 (* Automatic proof works too, but it make take a while on a slow machine. |
53 (* Automatic proof works too, but it make take a while on a slow machine. |
55 More substantial examples require manual guidance anyway. |
54 More substantial examples require manual guidance anyway. |