src/HOL/Bali/AxExample.thy
changeset 13688 a0b16d42d489
parent 12925 99131847fb93
child 14030 cd928c0ac225
--- a/src/HOL/Bali/AxExample.thy	Wed Oct 30 12:44:18 2002 +0100
+++ b/src/HOL/Bali/AxExample.thy	Thu Oct 31 18:27:10 2002 +0100
@@ -52,10 +52,13 @@
 
 theorem ax_test: "tprg,({}::'a triple set)\<turnstile> 
   {Normal (\<lambda>Y s Z::'a. heap_free four s \<and> \<not>initd Base s \<and> \<not> initd Ext s)} 
-  .test [Class Base]. {\<lambda>Y s Z. abrupt s = Some (Xcpt (Std IndOutBound))}"
+  .test [Class Base]. 
+  {\<lambda>Y s Z. abrupt s = Some (Xcpt (Std IndOutBound))}"
 apply (unfold test_def arr_viewed_from_def)
 apply (tactic "ax_tac 1" (*;;*))
-defer
+defer (* We begin with the last assertion, to synthesise the intermediate
+         assertions, like in the fashion of the weakest
+         precondition. *)
 apply  (tactic "ax_tac 1" (* Try *))
 defer
 apply    (tactic {* inst1_tac "Q1" 
@@ -108,11 +111,18 @@
 (* apply       (rule_tac [2] ax_derivs.Abrupt) *)
 defer
 apply      (simp (no_asm))
-apply      (tactic "ax_tac 1")
+apply      (tactic "ax_tac 1") (* Comp *)
+            (* The first statement in the  composition 
+                 ((Ext)z).vee = 1; Return Null 
+                will throw an exception (since z is null). So we can handle
+                Return Null with the Abrupt rule *)
+apply       (rule_tac [2] ax_derivs.Abrupt)
+             
+apply      (rule ax_derivs.Expr) (* Expr *)
 apply      (tactic "ax_tac 1") (* Ass *)
 prefer 2
 apply       (rule ax_subst_Var_allI)
-apply       (tactic {* inst1_tac "P'27" "\<lambda>a vs l vf. ?PP a vs l vf\<leftarrow>?x \<and>. ?p" *})
+apply       (tactic {* inst1_tac "P'29" "\<lambda>a vs l vf. ?PP a vs l vf\<leftarrow>?x \<and>. ?p" *})
 apply       (rule allI)
 apply       (tactic {* simp_tac (simpset() delloop "split_all_tac" delsimps [thm "peek_and_def2"]) 1 *})
 apply       (rule ax_derivs.Abrupt)
@@ -120,11 +130,10 @@
 apply      (tactic "ax_tac 1" (* FVar *))
 apply       (tactic "ax_tac 2", tactic "ax_tac 2", tactic "ax_tac 2")
 apply      (tactic "ax_tac 1")
-apply     clarsimp
 apply     (tactic {* inst1_tac "R14" "\<lambda>a'. Normal ((\<lambda>Vals:vs (x, s) Z. arr_inv s \<and> inited Ext (globs s) \<and> a' \<noteq> Null \<and> hd vs = Null) \<and>. heap_free two)" *})
-prefer 5
-apply     (rule ax_derivs.Done [THEN conseq1], force)
-apply    force
+apply     fastsimp
+prefer 4
+apply    (rule ax_derivs.Done [THEN conseq1],force)
 apply   (rule ax_subst_Val_allI)
 apply   (tactic {* inst1_tac "P'33" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})
 apply   (simp (no_asm) del: peek_and_def2)