Changed semantics, so that the given precondition is the only guard, …

…rather than having the guard be calculated via weakest preconditions. For most models, this makes no practical difference.

Z_Machine.ML

@@ -103,6 +103,12 @@ fun mk_zinit (Init {name = n, state = s, update = upd}) ctx =
            , check_term ctx (Type.constraint (st --> st) (parse_term ctx upd)))) ctx)
   end;
 
+fun gen n ty term ctx = snd (Local_Theory.define 
+  ((Binding.name n, NoSyn)
+  , ((Binding.name (n ^ "_def")
+  , @{attributes [code_unfold, z_defs]})
+  , Syntax.check_term ctx (Type.constraint ty term))) ctx);
+
 fun mk_zop (Operation {name = n, state = s, body = OperDefn {params = ps, pre = pre, update = upd, guard = g, output = ot}}) ctx =
   let open Syntax; open Library; open Logic; open HOLogic; open Lift_Expr
       val pss = (map (fn (p, t) => (p, lift_expr ctx ((parse_term ctx t)))) ps)
@@ -128,8 +134,8 @@ fun mk_zop (Operation {name = n, state = s, body = OperDefn {params = ps, pre =
                 $ tupled_lambda ppat (SEXP $ pguard)
                 $ tupled_lambda ppat (SEXP $ poutput)
                 )
-
-  in def_zop n set st body ctx
+  in def_zop n set st body ctx 
+     |> gen (zop_pre n) (parm --> st --> dummyT) (tupled_lambda ppat (SEXP $ ppre))
   end |
      (*
      (* Generate the precondition *)
@@ -147,7 +153,7 @@ mk_zop (Operation {name = n, state = s, body = OperProm {promop = opr, plens = l
   let open Syntax; open Lift_Expr
       val opr' = read_term ctx opr; 
       val pn = fst (dest_Const opr');
-      val opr_type = const (pn ^ "_type"); 
+      val opr_type = const (zop_type pn); 
       val lens' = parse_term ctx lens 
       val st = read_typ ctx s
       val set = check_term ctx (const @{const_name "promoted_type"} $ lens' $ const @{const_name collection_lens} $ opr_type)
@@ -168,8 +174,11 @@ mk_zop (Operation {name = n, state = s, body = OperEmit {emit = e}}) ctx =
   let open Syntax; open HOLogic; open Lift_Expr
   val set = mk_lift_expr ctx (mk_set dummyT [parse_term ctx e])
   val st = read_typ ctx s
+  val parm = dest_setT (range_type (Term.type_of (check_term ctx set)))
   val body = const @{const_abbrev emit_op}
-  in def_zop n set st body ctx
+  in def_zop n set st body ctx 
+     (* Generate precondition *)
+     |> gen (zop_pre n) (parm --> st --> dummyT) (Abs ("p", parm, SEXP $ lambda (free state_id) @{term True}))
   end;
 
 fun get_zop_ptype n ctx =
@@ -196,7 +205,12 @@ fun zmachine_body_sem n st init inve ops ends ctx =
   let open Syntax; open HOLogic; open Proof_Context
       val oplist = 
             mk_list dummyT 
-              (map (fn n => const @{const_name zop_event} $ read_const {proper = false, strict = false} ctx (firstLower n) $ const (read_const_name ctx (zop_type n)) $ read_const {proper = false, strict = false} ctx (firstLower n ^ "_Out") $  const (read_const_name ctx n)) ops)
+              (map (fn n => const @{const_name zop_event} 
+                            $ read_const {proper = false, strict = false} ctx (firstLower n) 
+                            $ const (read_const_name ctx (zop_type n))
+                            $ const (read_const_name ctx (zop_pre n)) 
+                            $ read_const {proper = false, strict = false} ctx (firstLower n ^ "_Out") 
+                            $ const (read_const_name ctx n)) ops)
   in snd (Local_Theory.define 
            ((Binding.name n, NoSyn)
          , ((Binding.name (n ^ "_def")

Z_Machine.thy

@@ -31,14 +31,14 @@ definition zop_event ::
 *)
 
 definition zop_event :: 
-  "('a \<Longrightarrow>\<^sub>\<triangle> 'e) \<Rightarrow> ('s \<Rightarrow> 'a set) \<Rightarrow> ('b \<Longrightarrow>\<^sub>\<triangle> 'e) \<Rightarrow> 
+  "('a \<Longrightarrow>\<^sub>\<triangle> 'e) \<Rightarrow> ('s \<Rightarrow> 'a set) \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('b \<Longrightarrow>\<^sub>\<triangle> 'e) \<Rightarrow> 
    ('a \<Rightarrow> 's \<Rightarrow> ('e, 'b \<times> 's) itree) \<Rightarrow> 
    ('e, 's) htree" where
 [code_unfold]: 
-  "zop_event c A d zop = (c?(x):A | pre (zop x) \<rightarrow> output_return (zop x) d)"
+  "zop_event c A P d zop = (c?(x):A | @(P x) \<rightarrow> output_return (zop x) d)"
 
 lemma hl_zop_event_full: 
-  "\<lbrakk> wb_prism c; \<And> p. H{P \<and> \<guillemotleft>p\<guillemotright> \<in> A \<and> pre (zop p)} zop p {ret. Q} \<rbrakk> \<Longrightarrow> \<^bold>{P\<^bold>} zop_event c A d zop \<^bold>{Q\<^bold>}"
+  "\<lbrakk> wb_prism c; \<And> p. H{P \<and> \<guillemotleft>p\<guillemotright> \<in> A \<and> @(Pre p)} zop p {ret. Q} \<rbrakk> \<Longrightarrow> \<^bold>{P\<^bold>} zop_event c A Pre d zop \<^bold>{Q\<^bold>}"
   apply (simp add: zop_event_def)
   apply (rule hoare_safe)
    apply (simp)
@@ -47,7 +47,7 @@ lemma hl_zop_event_full:
   done
 
 lemma hl_zop_event: 
-  "\<lbrakk> wb_prism c; \<And> p. H{P} zop p {ret. Q} \<rbrakk> \<Longrightarrow> \<^bold>{P\<^bold>} zop_event c A d zop \<^bold>{Q\<^bold>}"
+  "\<lbrakk> wb_prism c; \<And> p. H{P} zop p {ret. Q} \<rbrakk> \<Longrightarrow> \<^bold>{P\<^bold>} zop_event c A Pre d zop \<^bold>{Q\<^bold>}"
   by (simp add: hl_proc_conj_pre hl_zop_event_full)
 
 (*

examples/BirthdayBook.thy

@@ -35,7 +35,7 @@ lemma FindBirthday_inv: "FindBirthday n preserves BirthdayBook_inv"
 zoperation Remind =
   over BirthdayBook
   params today\<in>DATE cards\<in>"\<bbbP> NAME"
-  where "cards = {n \<in> known. birthday(n) = today}"
+  pre "cards = {n \<in> known. birthday(n) = today}"
 
 lemma Remind_inv: "Remind (n, d) preserves BirthdayBook_inv"
   by zpog_full

examples/Buffer_Z.thy

@@ -40,6 +40,8 @@ zmachine Buffer =
   invariant "Buffer_state_inv"
   operations Input Output State
 
+thm Buffer_def
+
 lemma Buffer_deadlock_free: "VAL \<noteq> {} \<Longrightarrow> deadlock_free Buffer"
   by deadlock_free