# HG changeset patch # User wenzelm # Date 1608753991 -3600 # Node ID b1be35908165959e4b25e3e3382589a49ddbdd8d # Parent d231d71d27b4621e141a39447eb12ae5888b2b54 clarified modules: avoid multiple uses of the same ML file; clarified concrete vs. abstract syntax; diff -r d231d71d27b4 -r b1be35908165 NEWS --- a/NEWS Wed Dec 23 20:49:05 2020 +0100 +++ b/NEWS Wed Dec 23 21:06:31 2020 +0100 @@ -103,8 +103,6 @@ *** HOL *** -* Session "Hoare" now provides a total correctness logic as well. - * An updated version of the veriT solver is now included as Isabelle component. It can be used in the "smt" proof method via "smt (verit)" or via "declare [[smt_solver = verit]]" in the context; see also session @@ -213,6 +211,11 @@ * Syntax for reflected term syntax is organized in bundle term_syntax, discontinuing previous locale term_syntax. Minor INCOMPATIBILITY. +* Session "HOL-Hoare": concrete syntax only for Hoare triples, not +abstract language constructors. + +* Session "HOL-Hoare": now provides a total correctness logic as well. + *** FOL *** diff -r d231d71d27b4 -r b1be35908165 src/HOL/Hoare/Hoare_Logic.thy --- a/src/HOL/Hoare/Hoare_Logic.thy Wed Dec 23 20:49:05 2020 +0100 +++ b/src/HOL/Hoare/Hoare_Logic.thy Wed Dec 23 21:06:31 2020 +0100 @@ -2,15 +2,18 @@ Author: Leonor Prensa Nieto & Tobias Nipkow Copyright 1998 TUM Author: Walter Guttmann (extension to total-correctness proofs) - -Sugared semantic embedding of Hoare logic. -Strictly speaking a shallow embedding (as implemented by Norbert Galm -following Mike Gordon) would suffice. Maybe the datatype com comes in useful -later. *) +section \Sugared semantic embedding of Hoare logic\ + +text \ + Strictly speaking a shallow embedding (as implemented by Norbert Galm + following Mike Gordon) would suffice. Maybe the datatype com comes in useful + later. +\ + theory Hoare_Logic -imports Hoare_Tac +imports Hoare_Syntax Hoare_Tac begin type_synonym 'a bexp = "'a set" @@ -19,14 +22,9 @@ datatype 'a com = Basic "'a \ 'a" -| Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60) -| Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61) -| While "'a bexp" "'a assn" "'a var" "'a com" ("(1WHILE _/ INV {_} / VAR {_} //DO _ /OD)" [0,0,0,0] 61) - -syntax - "_whilePC" :: "'a bexp \ 'a assn \ 'a com \ 'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61) -translations - "WHILE b INV {x} DO c OD" \ "WHILE b INV {x} VAR {0} DO c OD" +| Seq "'a com" "'a com" +| Cond "'a bexp" "'a com" "'a com" +| While "'a bexp" "'a assn" "'a var" "'a com" abbreviation annskip ("SKIP") where "SKIP == Basic id" @@ -35,16 +33,22 @@ inductive Sem :: "'a com \ 'a sem" where "Sem (Basic f) s (f s)" -| "Sem c1 s s'' \ Sem c2 s'' s' \ Sem (c1;c2) s s'" -| "s \ b \ Sem c1 s s' \ Sem (IF b THEN c1 ELSE c2 FI) s s'" -| "s \ b \ Sem c2 s s' \ Sem (IF b THEN c1 ELSE c2 FI) s s'" +| "Sem c1 s s'' \ Sem c2 s'' s' \ Sem (Seq c1 c2) s s'" +| "s \ b \ Sem c1 s s' \ Sem (Cond b c1 c2) s s'" +| "s \ b \ Sem c2 s s' \ Sem (Cond b c1 c2) s s'" | "s \ b \ Sem (While b x y c) s s" | "s \ b \ Sem c s s'' \ Sem (While b x y c) s'' s' \ Sem (While b x y c) s s'" +definition Valid :: "'a bexp \ 'a com \ 'a bexp \ bool" + where "Valid p c q \ \s s'. Sem c s s' \ s \ p \ s' \ q" + +definition ValidTC :: "'a bexp \ 'a com \ 'a bexp \ bool" + where "ValidTC p c q \ \s. s \ p \ (\t. Sem c s t \ t \ q)" + inductive_cases [elim!]: - "Sem (Basic f) s s'" "Sem (c1;c2) s s'" - "Sem (IF b THEN c1 ELSE c2 FI) s s'" + "Sem (Basic f) s s'" "Sem (Seq c1 c2) s s'" + "Sem (Cond b c1 c2) s s'" lemma Sem_deterministic: assumes "Sem c s s1" @@ -57,12 +61,6 @@ using assms by simp qed -definition Valid :: "'a bexp \ 'a com \ 'a bexp \ bool" - where "Valid p c q \ \s s'. Sem c s s' \ s \ p \ s' \ q" - -definition ValidTC :: "'a bexp \ 'a com \ 'a bexp \ bool" - where "ValidTC p c q \ \s . s \ p \ (\t . Sem c s t \ t \ q)" - lemma tc_implies_pc: "ValidTC p c q \ Valid p c q" by (metis Sem_deterministic Valid_def ValidTC_def) @@ -71,30 +69,6 @@ "ValidTC p c q \ \f . \s . s \ p \ f s \ q" by (metis ValidTC_def) -syntax - "_assign" :: "idt => 'b => 'a com" ("(2_ :=/ _)" [70, 65] 61) - -syntax - "_hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool" - ("VARS _// {_} // _ // {_}" [0,0,55,0] 50) -syntax (output) - "_hoare" :: "['a assn,'a com,'a assn] => bool" - ("{_} // _ // {_}" [0,55,0] 50) - -ML_file \hoare_syntax.ML\ -parse_translation \[(\<^syntax_const>\_hoare_vars\, K Hoare_Syntax.hoare_vars_tr)]\ -print_translation \[(\<^const_syntax>\Valid\, K (Hoare_Syntax.spec_tr' \<^syntax_const>\_hoare\))]\ - -syntax - "_hoare_tc_vars" :: "[idts, 'a assn,'a com,'a assn] => bool" - ("VARS _// [_] // _ // [_]" [0,0,55,0] 50) -syntax (output) - "_hoare_tc" :: "['a assn,'a com,'a assn] => bool" - ("[_] // _ // [_]" [0,55,0] 50) - -parse_translation \[(\<^syntax_const>\_hoare_tc_vars\, K Hoare_Syntax.hoare_tc_vars_tr)]\ -print_translation \[(\<^const_syntax>\ValidTC\, K (Hoare_Syntax.spec_tr' \<^syntax_const>\_hoare_tc\))]\ - lemma SkipRule: "p \ q \ Valid p (Basic id) q" by (auto simp:Valid_def) @@ -102,7 +76,7 @@ lemma BasicRule: "p \ {s. f s \ q} \ Valid p (Basic f) q" by (auto simp:Valid_def) -lemma SeqRule: "Valid P c1 Q \ Valid Q c2 R \ Valid P (c1;c2) R" +lemma SeqRule: "Valid P c1 Q \ Valid Q c2 R \ Valid P (Seq c1 c2) R" by (auto simp:Valid_def) lemma CondRule: @@ -111,11 +85,11 @@ by (auto simp:Valid_def) lemma While_aux: - assumes "Sem (WHILE b INV {i} VAR {v} DO c OD) s s'" + assumes "Sem (While b i v c) s s'" shows "\s s'. Sem c s s' \ s \ I \ s \ b \ s' \ I \ s \ I \ s' \ I \ s' \ b" using assms - by (induct "WHILE b INV {i} VAR {v} DO c OD" s s') auto + by (induct "While b i v c" s s') auto lemma WhileRule: "p \ i \ Valid (i \ b) c i \ i \ (-b) \ q \ Valid p (While b i v c) q" @@ -139,7 +113,7 @@ lemma SeqRuleTC: assumes "ValidTC p c1 q" and "ValidTC q c2 r" - shows "ValidTC p (c1;c2) r" + shows "ValidTC p (Seq c1 c2) r" by (meson assms Sem.intros(2) ValidTC_def) lemma CondRuleTC: @@ -193,6 +167,22 @@ qed +subsection \Concrete syntax\ + +setup \ + Hoare_Syntax.setup + {Basic = \<^const_syntax>\Basic\, + Skip = \<^const_syntax>\annskip\, + Seq = \<^const_syntax>\Seq\, + Cond = \<^const_syntax>\Cond\, + While = \<^const_syntax>\While\, + Valid = \<^const_syntax>\Valid\, + ValidTC = \<^const_syntax>\ValidTC\} +\ + + +subsection \Proof methods: VCG\ + declare BasicRule [Hoare_Tac.BasicRule] and SkipRule [Hoare_Tac.SkipRule] and SeqRule [Hoare_Tac.SeqRule] diff -r d231d71d27b4 -r b1be35908165 src/HOL/Hoare/Hoare_Logic_Abort.thy --- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Wed Dec 23 20:49:05 2020 +0100 +++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Wed Dec 23 21:06:31 2020 +0100 @@ -2,12 +2,12 @@ Author: Leonor Prensa Nieto & Tobias Nipkow Copyright 2003 TUM Author: Walter Guttmann (extension to total-correctness proofs) - -Like Hoare_Logic.thy, but with an Abort statement for modelling run time errors. *) +section \Hoare Logic with an Abort statement for modelling run time errors\ + theory Hoare_Logic_Abort -imports Hoare_Tac +imports Hoare_Syntax Hoare_Tac begin type_synonym 'a bexp = "'a set" @@ -17,14 +17,9 @@ datatype 'a com = Basic "'a \ 'a" | Abort -| Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60) -| Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61) -| While "'a bexp" "'a assn" "'a var" "'a com" ("(1WHILE _/ INV {_} / VAR {_} //DO _ /OD)" [0,0,0,0] 61) - -syntax - "_whilePC" :: "'a bexp \ 'a assn \ 'a com \ 'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61) -translations - "WHILE b INV {x} DO c OD" \ "WHILE b INV {x} VAR {0} DO c OD" +| Seq "'a com" "'a com" +| Cond "'a bexp" "'a com" "'a com" +| While "'a bexp" "'a assn" "'a var" "'a com" abbreviation annskip ("SKIP") where "SKIP == Basic id" @@ -35,18 +30,18 @@ "Sem (Basic f) None None" | "Sem (Basic f) (Some s) (Some (f s))" | "Sem Abort s None" -| "Sem c1 s s'' \ Sem c2 s'' s' \ Sem (c1;c2) s s'" -| "Sem (IF b THEN c1 ELSE c2 FI) None None" -| "s \ b \ Sem c1 (Some s) s' \ Sem (IF b THEN c1 ELSE c2 FI) (Some s) s'" -| "s \ b \ Sem c2 (Some s) s' \ Sem (IF b THEN c1 ELSE c2 FI) (Some s) s'" +| "Sem c1 s s'' \ Sem c2 s'' s' \ Sem (Seq c1 c2) s s'" +| "Sem (Cond b c1 c2) None None" +| "s \ b \ Sem c1 (Some s) s' \ Sem (Cond b c1 c2) (Some s) s'" +| "s \ b \ Sem c2 (Some s) s' \ Sem (Cond b c1 c2) (Some s) s'" | "Sem (While b x y c) None None" | "s \ b \ Sem (While b x y c) (Some s) (Some s)" | "s \ b \ Sem c (Some s) s'' \ Sem (While b x y c) s'' s' \ Sem (While b x y c) (Some s) s'" inductive_cases [elim!]: - "Sem (Basic f) s s'" "Sem (c1;c2) s s'" - "Sem (IF b THEN c1 ELSE c2 FI) s s'" + "Sem (Basic f) s s'" "Sem (Seq c1 c2) s s'" + "Sem (Cond b c1 c2) s s'" lemma Sem_deterministic: assumes "Sem c s s1" @@ -73,30 +68,6 @@ "ValidTC p c q \ \f . \s . s \ p \ f s \ q" by (meson ValidTC_def) -syntax - "_assign" :: "idt => 'b => 'a com" ("(2_ :=/ _)" [70, 65] 61) - -syntax - "_hoare_abort_vars" :: "[idts, 'a assn,'a com,'a assn] => bool" - ("VARS _// {_} // _ // {_}" [0,0,55,0] 50) -syntax (output) - "_hoare_abort" :: "['a assn,'a com,'a assn] => bool" - ("{_} // _ // {_}" [0,55,0] 50) - -ML_file \hoare_syntax.ML\ -parse_translation \[(\<^syntax_const>\_hoare_abort_vars\, K Hoare_Syntax.hoare_vars_tr)]\ -print_translation \[(\<^const_syntax>\Valid\, K (Hoare_Syntax.spec_tr' \<^syntax_const>\_hoare_abort\))]\ - -syntax - "_hoare_abort_tc_vars" :: "[idts, 'a assn,'a com,'a assn] => bool" - ("VARS _// [_] // _ // [_]" [0,0,55,0] 50) -syntax (output) - "_hoare_abort_tc" :: "['a assn,'a com,'a assn] => bool" - ("[_] // _ // [_]" [0,55,0] 50) - -parse_translation \[(\<^syntax_const>\_hoare_abort_tc_vars\, K Hoare_Syntax.hoare_tc_vars_tr)]\ -print_translation \[(\<^const_syntax>\ValidTC\, K (Hoare_Syntax.spec_tr' \<^syntax_const>\_hoare_abort_tc\))]\ - text \The proof rules for partial correctness\ lemma SkipRule: "p \ q \ Valid p (Basic id) q" @@ -105,7 +76,7 @@ lemma BasicRule: "p \ {s. f s \ q} \ Valid p (Basic f) q" by (auto simp:Valid_def) -lemma SeqRule: "Valid P c1 Q \ Valid Q c2 R \ Valid P (c1;c2) R" +lemma SeqRule: "Valid P c1 Q \ Valid Q c2 R \ Valid P (Seq c1 c2) R" by (auto simp:Valid_def) lemma CondRule: @@ -114,11 +85,11 @@ by (fastforce simp:Valid_def image_def) lemma While_aux: - assumes "Sem (WHILE b INV {i} VAR {v} DO c OD) s s'" + assumes "Sem (While b i v c) s s'" shows "\s s'. Sem c s s' \ s \ Some ` (I \ b) \ s' \ Some ` I \ s \ Some ` I \ s' \ Some ` (I \ -b)" using assms - by (induct "WHILE b INV {i} VAR {v} DO c OD" s s') auto + by (induct "While b i v c" s s') auto lemma WhileRule: "p \ i \ Valid (i \ b) c i \ i \ (-b) \ q \ Valid p (While b i v c) q" @@ -147,7 +118,7 @@ lemma SeqRuleTC: assumes "ValidTC p c1 q" and "ValidTC q c2 r" - shows "ValidTC p (c1;c2) r" + shows "ValidTC p (Seq c1 c2) r" by (meson assms Sem.intros(4) ValidTC_def) lemma CondRuleTC: @@ -201,7 +172,35 @@ qed -subsection \Derivation of the proof rules and, most importantly, the VCG tactic\ +subsection \Concrete syntax\ + +setup \ + Hoare_Syntax.setup + {Basic = \<^const_syntax>\Basic\, + Skip = \<^const_syntax>\annskip\, + Seq = \<^const_syntax>\Seq\, + Cond = \<^const_syntax>\Cond\, + While = \<^const_syntax>\While\, + Valid = \<^const_syntax>\Valid\, + ValidTC = \<^const_syntax>\ValidTC\} +\ + +\ \Special syntax for guarded statements and guarded array updates:\ +syntax + "_guarded_com" :: "bool \ 'a com \ 'a com" ("(2_ \/ _)" 71) + "_array_update" :: "'a list \ nat \ 'a \ 'a com" ("(2_[_] :=/ _)" [70, 65] 61) +translations + "P \ c" \ "IF P THEN c ELSE CONST Abort FI" + "a[i] := v" \ "(i < CONST length a) \ (a := CONST list_update a i v)" + \ \reverse translation not possible because of duplicate \a\\ + +text \ + Note: there is no special syntax for guarded array access. Thus + you must write \j < length a \ a[i] := a!j\. +\ + + +subsection \Proof methods: VCG\ declare BasicRule [Hoare_Tac.BasicRule] and SkipRule [Hoare_Tac.SkipRule] @@ -234,18 +233,4 @@ SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))\ "verification condition generator plus simplification" -\ \Special syntax for guarded statements and guarded array updates:\ -syntax - "_guarded_com" :: "bool \ 'a com \ 'a com" ("(2_ \/ _)" 71) - "_array_update" :: "'a list \ nat \ 'a \ 'a com" ("(2_[_] :=/ _)" [70, 65] 61) -translations - "P \ c" == "IF P THEN c ELSE CONST Abort FI" - "a[i] := v" => "(i < CONST length a) \ (a := CONST list_update a i v)" - \ \reverse translation not possible because of duplicate \a\\ - -text \ - Note: there is no special syntax for guarded array access. Thus - you must write \j < length a \ a[i] := a!j\. -\ - end diff -r d231d71d27b4 -r b1be35908165 src/HOL/Hoare/Hoare_Syntax.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Hoare/Hoare_Syntax.thy Wed Dec 23 21:06:31 2020 +0100 @@ -0,0 +1,32 @@ +(* Title: HOL/Hoare/Hoare_Syntax.thy + Author: Leonor Prensa Nieto & Tobias Nipkow + Author: Walter Guttmann (extension to total-correctness proofs) + +Concrete syntax for Hoare logic, with translations for variables. +*) + +theory Hoare_Syntax + imports Main +begin + +syntax + "_assign" :: "idt \ 'b \ 'com" ("(2_ :=/ _)" [70, 65] 61) + "_Seq" :: "'com \ 'com \ 'com" ("(_;/ _)" [61,60] 60) + "_Cond" :: "'bexp \ 'com \ 'com \ 'com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61) + "_While" :: "'bexp \ 'assn \ 'var \ 'com \ 'com" ("(1WHILE _/ INV {_} / VAR {_} //DO _ /OD)" [0,0,0,0] 61) + +syntax + "_While0" :: "'bexp \ 'assn \ 'com \ 'com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61) +translations + "WHILE b INV {x} DO c OD" \ "WHILE b INV {x} VAR {0} DO c OD" + +syntax + "_hoare_vars" :: "[idts, 'assn,'com, 'assn] \ bool" ("VARS _// {_} // _ // {_}" [0,0,55,0] 50) + "_hoare_vars_tc" :: "[idts, 'assn, 'com, 'assn] \ bool" ("VARS _// [_] // _ // [_]" [0,0,55,0] 50) +syntax (output) + "_hoare" :: "['assn, 'com, 'assn] \ bool" ("{_} // _ // {_}" [0,55,0] 50) + "_hoare_tc" :: "['assn, 'com, 'assn] \ bool" ("[_] // _ // [_]" [0,55,0] 50) + +ML_file \hoare_syntax.ML\ + +end diff -r d231d71d27b4 -r b1be35908165 src/HOL/Hoare/hoare_syntax.ML --- a/src/HOL/Hoare/hoare_syntax.ML Wed Dec 23 20:49:05 2020 +0100 +++ b/src/HOL/Hoare/hoare_syntax.ML Wed Dec 23 21:06:31 2020 +0100 @@ -7,14 +7,41 @@ signature HOARE_SYNTAX = sig - val hoare_vars_tr: term list -> term - val hoare_tc_vars_tr: term list -> term - val spec_tr': string -> term list -> term + val hoare_vars_tr: Proof.context -> term list -> term + val hoare_tc_vars_tr: Proof.context -> term list -> term + val spec_tr': string -> Proof.context -> term list -> term + val setup: + {Basic: string, Skip: string, Seq: string, Cond: string, While: string, + Valid: string, ValidTC: string} -> theory -> theory end; structure Hoare_Syntax: HOARE_SYNTAX = struct +(** theory data **) + +structure Data = Theory_Data +( + type T = + {Basic: string, Skip: string, Seq: string, Cond: string, While: string, + Valid: string, ValidTC: string} option; + val empty: T = NONE; + val extend = I; + fun merge (data1, data2) = + if is_some data1 andalso is_some data2 andalso data1 <> data2 then + error "Cannot merge syntax from different Hoare Logics" + else merge_options (data1, data2); +); + +fun const_syntax ctxt which = + (case Data.get (Proof_Context.theory_of ctxt) of + SOME consts => which consts + | NONE => error "Undefined Hoare syntax consts"); + +val syntax_const = Syntax.const oo const_syntax; + + + (** parse translation **) local @@ -54,35 +81,33 @@ (* 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) _ = 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 $ V $ c) xs = - Syntax.const \<^const_syntax>\While\ $ bexp_tr b xs $ assn_tr I xs $ var_tr V xs $ com_tr c xs - | com_tr t _ = t; +fun com_tr ctxt = + let + fun tr (Const (\<^syntax_const>\_assign\, _) $ x $ e) xs = + syntax_const ctxt #Basic $ mk_fexp x e xs + | tr (Const (\<^syntax_const>\_Seq\,_) $ c1 $ c2) xs = + syntax_const ctxt #Seq $ tr c1 xs $ tr c2 xs + | tr (Const (\<^syntax_const>\_Cond\,_) $ b $ c1 $ c2) xs = + syntax_const ctxt #Cond $ bexp_tr b xs $ tr c1 xs $ tr c2 xs + | tr (Const (\<^syntax_const>\_While\,_) $ b $ I $ V $ c) xs = + syntax_const ctxt #While $ bexp_tr b xs $ assn_tr I xs $ var_tr V xs $ tr c xs + | tr t _ = t; + in tr end; fun vars_tr (Const (\<^syntax_const>\_idts\, _) $ idt $ vars) = idt :: vars_tr vars | vars_tr t = [t]; in -fun hoare_vars_tr [vars, pre, prg, post] = +fun hoare_vars_tr ctxt [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 ctxt #Valid $ assn_tr pre xs $ com_tr ctxt prg xs $ assn_tr post xs end + | hoare_vars_tr _ ts = raise TERM ("hoare_vars_tr", ts); -fun hoare_tc_vars_tr [vars, pre, prg, post] = +fun hoare_tc_vars_tr ctxt [vars, pre, prg, post] = let val xs = vars_tr vars - in Syntax.const \<^const_syntax>\ValidTC\ $ - assn_tr pre xs $ com_tr prg xs $ assn_tr post xs - end - | hoare_tc_vars_tr ts = raise TERM ("hoare_tc_vars_tr", ts); + in syntax_const ctxt #ValidTC $ assn_tr pre xs $ com_tr ctxt prg xs $ assn_tr post xs end + | hoare_tc_vars_tr _ ts = raise TERM ("hoare_tc_vars_tr", ts); end; @@ -139,32 +164,55 @@ (* com_tr' *) -fun mk_assign f = +fun mk_assign ctxt f = let val (vs, ts) = mk_vts f; - val (ch, which) = find_ch (vs ~~ ts) (length vs - 1) (rev vs); + val (ch, (a, b)) = 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\ + then Syntax.const \<^syntax_const>\_assign\ $ a $ b + else syntax_const ctxt #Skip 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 $ V $ c) = - Syntax.const \<^const_syntax>\While\ $ bexp_tr' b $ assn_tr' I $ var_tr' V $ com_tr' c - | com_tr' t = t; +fun com_tr' ctxt t = + let + val (head, args) = apfst (try (#1 o Term.dest_Const)) (Term.strip_comb t); + fun arg k = nth args (k - 1); + val n = length args; + in + (case head of + NONE => t + | SOME c => + if c = const_syntax ctxt #Basic andalso n = 1 andalso is_f (arg 1) then + mk_assign ctxt (arg 1) + else if c = const_syntax ctxt #Seq andalso n = 2 then + Syntax.const \<^syntax_const>\_Seq\ $ com_tr' ctxt (arg 1) $ com_tr' ctxt (arg 2) + else if c = const_syntax ctxt #Cond andalso n = 3 then + Syntax.const \<^syntax_const>\_Cond\ $ + bexp_tr' (arg 1) $ com_tr' ctxt (arg 2) $ com_tr' ctxt (arg 3) + else if c = const_syntax ctxt #While andalso n = 4 then + Syntax.const \<^syntax_const>\_While\ $ + bexp_tr' (arg 1) $ assn_tr' (arg 2) $ var_tr' (arg 3) $ com_tr' ctxt (arg 4) + else t) + end; in -fun spec_tr' syn [p, c, q] = Syntax.const syn $ assn_tr' p $ com_tr' c $ assn_tr' q; +fun spec_tr' syn ctxt [p, c, q] = + Syntax.const syn $ assn_tr' p $ com_tr' ctxt c $ assn_tr' q; end; + +(** setup **) + +fun setup consts = + Data.put (SOME consts) #> + Sign.parse_translation + [(\<^syntax_const>\_hoare_vars\, hoare_vars_tr), + (\<^syntax_const>\_hoare_vars_tc\, hoare_tc_vars_tr)] #> + Sign.print_translation + [(#Valid consts, spec_tr' \<^syntax_const>\_hoare\), + (#ValidTC consts, spec_tr' \<^syntax_const>\_hoare_tc\)]; + end; -