proper ML structure with signature;
authorwenzelm
Fri Feb 21 20:37:13 2014 +0100 (2014-02-21)
changeset 55660f0f895716a8b
parent 55659 4089f6e98ab9
child 55661 ec14796cd140
proper ML structure with signature;
src/HOL/Hoare/Hoare_Logic.thy
src/HOL/Hoare/Hoare_Logic_Abort.thy
src/HOL/Hoare/hoare_tac.ML
src/HOL/Isar_Examples/Hoare.thy
     1.1 --- a/src/HOL/Hoare/Hoare_Logic.thy	Fri Feb 21 20:29:33 2014 +0100
     1.2 +++ b/src/HOL/Hoare/Hoare_Logic.thy	Fri Feb 21 20:37:13 2014 +0100
     1.3 @@ -96,12 +96,12 @@
     1.4  ML_file "hoare_tac.ML"
     1.5  
     1.6  method_setup vcg = {*
     1.7 -  Scan.succeed (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
     1.8 +  Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tac ctxt (K all_tac))) *}
     1.9    "verification condition generator"
    1.10  
    1.11  method_setup vcg_simp = {*
    1.12    Scan.succeed (fn ctxt =>
    1.13 -    SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac ctxt))) *}
    1.14 +    SIMPLE_METHOD' (Hoare.hoare_tac ctxt (asm_full_simp_tac ctxt))) *}
    1.15    "verification condition generator plus simplification"
    1.16  
    1.17  end
     2.1 --- a/src/HOL/Hoare/Hoare_Logic_Abort.thy	Fri Feb 21 20:29:33 2014 +0100
     2.2 +++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy	Fri Feb 21 20:37:13 2014 +0100
     2.3 @@ -107,12 +107,12 @@
     2.4  ML_file "hoare_tac.ML"
     2.5  
     2.6  method_setup vcg = {*
     2.7 -  Scan.succeed (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
     2.8 +  Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tac ctxt (K all_tac))) *}
     2.9    "verification condition generator"
    2.10  
    2.11  method_setup vcg_simp = {*
    2.12    Scan.succeed (fn ctxt =>
    2.13 -    SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac ctxt))) *}
    2.14 +    SIMPLE_METHOD' (Hoare.hoare_tac ctxt (asm_full_simp_tac ctxt))) *}
    2.15    "verification condition generator plus simplification"
    2.16  
    2.17  (* Special syntax for guarded statements and guarded array updates: *)
     3.1 --- a/src/HOL/Hoare/hoare_tac.ML	Fri Feb 21 20:29:33 2014 +0100
     3.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Fri Feb 21 20:37:13 2014 +0100
     3.3 @@ -4,7 +4,14 @@
     3.4  Derivation of the proof rules and, most importantly, the VCG tactic.
     3.5  *)
     3.6  
     3.7 -(* FIXME structure Hoare: HOARE *)
     3.8 +signature HOARE =
     3.9 +sig
    3.10 +  val hoare_rule_tac: Proof.context -> term list * thm -> (int -> tactic) -> bool -> int -> tactic
    3.11 +  val hoare_tac: Proof.context -> (int -> tactic) -> int -> tactic
    3.12 +end;
    3.13 +
    3.14 +structure Hoare: HOARE =
    3.15 +struct
    3.16  
    3.17  (*** The tactics ***)
    3.18  
    3.19 @@ -178,3 +185,5 @@
    3.20  fun hoare_tac ctxt tac = SUBGOAL (fn (goal, i) =>
    3.21    SELECT_GOAL (hoare_rule_tac ctxt (Mset ctxt goal) tac true 1) i);
    3.22  
    3.23 +end;
    3.24 +
     4.1 --- a/src/HOL/Isar_Examples/Hoare.thy	Fri Feb 21 20:29:33 2014 +0100
     4.2 +++ b/src/HOL/Isar_Examples/Hoare.thy	Fri Feb 21 20:37:13 2014 +0100
     4.3 @@ -400,7 +400,7 @@
     4.4  method_setup hoare = {*
     4.5    Scan.succeed (fn ctxt =>
     4.6      (SIMPLE_METHOD'
     4.7 -       (hoare_tac ctxt
     4.8 +       (Hoare.hoare_tac ctxt
     4.9          (simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm "Record.K_record_comp"}] ))))) *}
    4.10    "verification condition generator for Hoare logic"
    4.11