--- a/src/HOL/Hoare/Hoare_Logic.thy Tue Mar 29 21:11:02 2011 +0200
+++ b/src/HOL/Hoare/Hoare_Logic.thy Tue Mar 29 21:48:01 2011 +0200
@@ -10,7 +10,7 @@
theory Hoare_Logic
imports Main
-uses ("hoare_tac.ML")
+uses ("hoare_syntax.ML") ("hoare_tac.ML")
begin
types
@@ -45,9 +45,6 @@
where "Valid p c q \<longleftrightarrow> (!s s'. Sem c s s' --> s : p --> s' : q)"
-
-(** parse translations **)
-
syntax
"_assign" :: "idt => 'b => 'a com" ("(2_ :=/ _)" [70, 65] 61)
@@ -58,126 +55,10 @@
"_hoare" :: "['a assn,'a com,'a assn] => bool"
("{_} // _ // {_}" [0,55,0] 50)
-parse_translation {*
- let
- fun mk_abstuple [x] body = Syntax.abs_tr [x, body]
- | mk_abstuple (x :: xs) body =
- Syntax.const @{const_syntax prod_case} $ Syntax.abs_tr [x, mk_abstuple xs body];
-
- fun mk_fbody x e [y] = if Syntax.eq_idt (x, y) then e else y
- | mk_fbody x e (y :: xs) =
- Syntax.const @{const_syntax Pair} $
- (if Syntax.eq_idt (x, y) then e else y) $ mk_fbody x e xs;
-
- fun mk_fexp x e xs = mk_abstuple xs (mk_fbody x e xs);
-
- (* bexp_tr & assn_tr *)
- (*all meta-variables for bexp except for TRUE are translated as if they
- were boolean expressions*)
-
- fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE" (* FIXME !? *)
- | bexp_tr b xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs b;
-
- fun assn_tr r xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs r;
-
- (* com_tr *)
-
- fun com_tr (Const (@{syntax_const "_assign"}, _) $ x $ e) xs =
- Syntax.const @{const_syntax Basic} $ mk_fexp x e xs
- | com_tr (Const (@{const_syntax Basic},_) $ f) xs = Syntax.const @{const_syntax Basic} $ f
- | com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs =
- Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs
- | com_tr (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) xs =
- Syntax.const @{const_syntax Cond} $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
- | com_tr (Const (@{const_syntax While},_) $ b $ I $ c) xs =
- Syntax.const @{const_syntax While} $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs
- | com_tr t _ = t;
-
- fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) = idt :: vars_tr vars
- | vars_tr t = [t];
-
- fun hoare_vars_tr [vars, pre, prg, post] =
- let val xs = vars_tr vars
- in Syntax.const @{const_syntax Valid} $
- assn_tr pre xs $ com_tr prg xs $ assn_tr post xs
- end
- | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts);
-
- in [(@{syntax_const "_hoare_vars"}, hoare_vars_tr)] end
-*}
-
-
-(*****************************************************************************)
-
-(*** print translations ***)
-ML{*
-fun dest_abstuple (Const (@{const_syntax prod_case},_) $ (Abs(v,_, body))) =
- subst_bound (Syntax.free v, dest_abstuple body)
- | dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body)
- | dest_abstuple trm = trm;
+use "hoare_syntax.ML"
+parse_translation {* [(@{syntax_const "_hoare_vars"}, Hoare_Syntax.hoare_vars_tr)] *}
+print_translation {* [(@{const_syntax Valid}, Hoare_Syntax.spec_tr' @{syntax_const "_hoare"})] *}
-fun abs2list (Const (@{const_syntax prod_case},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
- | abs2list (Abs(x,T,t)) = [Free (x, T)]
- | abs2list _ = [];
-
-fun mk_ts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = mk_ts t
- | mk_ts (Abs(x,_,t)) = mk_ts t
- | mk_ts (Const (@{const_syntax Pair},_) $ a $ b) = a::(mk_ts b)
- | mk_ts t = [t];
-
-fun mk_vts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) =
- ((Syntax.free x)::(abs2list t), mk_ts t)
- | mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t])
- | mk_vts t = raise Match;
-
-fun find_ch [] i xs = (false, (Syntax.free "not_ch", Syntax.free "not_ch"))
- | find_ch ((v,t)::vts) i xs =
- if t = Bound i then find_ch vts (i-1) xs
- else (true, (v, subst_bounds (xs, t)));
-
-fun is_f (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = true
- | is_f (Abs(x,_,t)) = true
- | is_f t = false;
-*}
-
-(* assn_tr' & bexp_tr'*)
-ML{*
-fun assn_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T
- | assn_tr' (Const (@{const_syntax inter}, _) $
- (Const (@{const_syntax Collect},_) $ T1) $ (Const (@{const_syntax Collect},_) $ T2)) =
- Syntax.const @{const_syntax inter} $ dest_abstuple T1 $ dest_abstuple T2
- | assn_tr' t = t;
-
-fun bexp_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T
- | bexp_tr' t = t;
-*}
-
-(*com_tr' *)
-ML{*
-fun mk_assign f =
- let val (vs, ts) = mk_vts f;
- val (ch, which) = find_ch (vs~~ts) ((length vs)-1) (rev vs)
- in
- if ch then Syntax.const @{syntax_const "_assign"} $ fst which $ snd which
- else Syntax.const @{const_syntax annskip}
- end;
-
-fun com_tr' (Const (@{const_syntax Basic},_) $ f) =
- if is_f f then mk_assign f
- else Syntax.const @{const_syntax Basic} $ f
- | com_tr' (Const (@{const_syntax Seq},_) $ c1 $ c2) =
- Syntax.const @{const_syntax Seq} $ com_tr' c1 $ com_tr' c2
- | com_tr' (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) =
- Syntax.const @{const_syntax Cond} $ bexp_tr' b $ com_tr' c1 $ com_tr' c2
- | com_tr' (Const (@{const_syntax While},_) $ b $ I $ c) =
- Syntax.const @{const_syntax While} $ bexp_tr' b $ assn_tr' I $ com_tr' c
- | com_tr' t = t;
-
-fun spec_tr' [p, c, q] =
- Syntax.const @{syntax_const "_hoare"} $ assn_tr' p $ com_tr' c $ assn_tr' q
-*}
-
-print_translation {* [(@{const_syntax Valid}, spec_tr')] *}
lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
by (auto simp:Valid_def)