prefer Proof.context over old-style clasimpset;
authorwenzelm
Thu May 12 18:18:06 2011 +0200 (2011-05-12)
changeset 42767e6d920bea7a6
parent 42766 92173262cfe9
child 42768 4db4a8b164c1
prefer Proof.context over old-style clasimpset;
src/HOL/UNITY/Comp/Alloc.thy
src/HOL/UNITY/Simple/NSP_Bad.thy
src/HOL/UNITY/UNITY_Main.thy
src/HOL/UNITY/UNITY_tactics.ML
     1.1 --- a/src/HOL/UNITY/Comp/Alloc.thy	Thu May 12 18:17:32 2011 +0200
     1.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy	Thu May 12 18:18:06 2011 +0200
     1.3 @@ -330,15 +330,15 @@
     1.4  
     1.5  (*** bijectivity of sysOfAlloc [MUST BE AUTOMATED] ***)
     1.6  ML {*
     1.7 -fun record_auto_tac (cs, ss) =
     1.8 -  auto_tac (cs addIs [ext] addSWrapper Record.split_wrapper,
     1.9 -    ss addsimps [@{thm sysOfAlloc_def}, @{thm sysOfClient_def},
    1.10 +fun record_auto_tac ctxt =
    1.11 +  auto_tac (claset_of ctxt addIs [ext] addSWrapper Record.split_wrapper,
    1.12 +    simpset_of ctxt addsimps [@{thm sysOfAlloc_def}, @{thm sysOfClient_def},
    1.13        @{thm client_map_def}, @{thm non_dummy_def}, @{thm funPair_def},
    1.14        @{thm o_apply}, @{thm Let_def}])
    1.15  *}
    1.16  
    1.17  method_setup record_auto = {*
    1.18 -  Scan.succeed (fn ctxt => SIMPLE_METHOD (record_auto_tac (clasimpset_of ctxt)))
    1.19 +  Scan.succeed (SIMPLE_METHOD o record_auto_tac)
    1.20  *} ""
    1.21  
    1.22  lemma inj_sysOfAlloc [iff]: "inj sysOfAlloc"
     2.1 --- a/src/HOL/UNITY/Simple/NSP_Bad.thy	Thu May 12 18:17:32 2011 +0200
     2.2 +++ b/src/HOL/UNITY/Simple/NSP_Bad.thy	Thu May 12 18:18:06 2011 +0200
     2.3 @@ -101,7 +101,11 @@
     2.4  
     2.5  text{*This ML code does the inductions directly.*}
     2.6  ML{*
     2.7 -fun ns_constrains_tac(cs,ss) i =
     2.8 +fun ns_constrains_tac ctxt i =
     2.9 +  let
    2.10 +    val cs = claset_of ctxt;
    2.11 +    val ss = simpset_of ctxt;
    2.12 +  in
    2.13     SELECT_GOAL
    2.14        (EVERY [REPEAT (etac @{thm Always_ConstrainsI} 1),
    2.15                REPEAT (resolve_tac [@{thm StableI}, @{thm stableI},
    2.16 @@ -111,21 +115,26 @@
    2.17                REPEAT (FIRSTGOAL (etac disjE)),
    2.18                ALLGOALS (clarify_tac (cs delrules [impI, @{thm impCE}])),
    2.19                REPEAT (FIRSTGOAL analz_mono_contra_tac),
    2.20 -              ALLGOALS (asm_simp_tac ss)]) i;
    2.21 +              ALLGOALS (asm_simp_tac ss)]) i
    2.22 +  end;
    2.23  
    2.24  (*Tactic for proving secrecy theorems*)
    2.25 -fun ns_induct_tac(cs,ss) =
    2.26 -  (SELECT_GOAL o EVERY)
    2.27 -     [rtac @{thm AlwaysI} 1,
    2.28 -      force_tac (cs,ss) 1,
    2.29 -      (*"reachable" gets in here*)
    2.30 -      rtac (@{thm Always_reachable} RS @{thm Always_ConstrainsI} RS @{thm StableI}) 1,
    2.31 -      ns_constrains_tac(cs,ss) 1];
    2.32 +fun ns_induct_tac ctxt =
    2.33 +  let
    2.34 +    val cs = claset_of ctxt;
    2.35 +    val ss = simpset_of ctxt;
    2.36 +  in
    2.37 +    (SELECT_GOAL o EVERY)
    2.38 +       [rtac @{thm AlwaysI} 1,
    2.39 +        force_tac (cs,ss) 1,
    2.40 +        (*"reachable" gets in here*)
    2.41 +        rtac (@{thm Always_reachable} RS @{thm Always_ConstrainsI} RS @{thm StableI}) 1,
    2.42 +        ns_constrains_tac ctxt 1]
    2.43 +  end;
    2.44  *}
    2.45  
    2.46  method_setup ns_induct = {*
    2.47 -    Scan.succeed (fn ctxt =>
    2.48 -        SIMPLE_METHOD' (ns_induct_tac (clasimpset_of ctxt))) *}
    2.49 +    Scan.succeed (SIMPLE_METHOD' o ns_induct_tac) *}
    2.50      "for inductive reasoning about the Needham-Schroeder protocol"
    2.51  
    2.52  text{*Converts invariants into statements about reachable states*}
     3.1 --- a/src/HOL/UNITY/UNITY_Main.thy	Thu May 12 18:17:32 2011 +0200
     3.2 +++ b/src/HOL/UNITY/UNITY_Main.thy	Thu May 12 18:18:06 2011 +0200
     3.3 @@ -11,13 +11,12 @@
     3.4  begin
     3.5  
     3.6  method_setup safety = {*
     3.7 -    Scan.succeed (fn ctxt =>
     3.8 -        SIMPLE_METHOD' (constrains_tac (clasimpset_of ctxt))) *}
     3.9 +    Scan.succeed (SIMPLE_METHOD' o constrains_tac) *}
    3.10      "for proving safety properties"
    3.11  
    3.12  method_setup ensures_tac = {*
    3.13    Args.goal_spec -- Scan.lift Args.name_source >>
    3.14 -  (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac (clasimpset_of ctxt) s))
    3.15 +  (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
    3.16  *} "for proving progress properties"
    3.17  
    3.18  end
     4.1 --- a/src/HOL/UNITY/UNITY_tactics.ML	Thu May 12 18:17:32 2011 +0200
     4.2 +++ b/src/HOL/UNITY/UNITY_tactics.ML	Thu May 12 18:18:06 2011 +0200
     4.3 @@ -13,7 +13,11 @@
     4.4  
     4.5  (*Proves "co" properties when the program is specified.  Any use of invariants
     4.6    (from weak constrains) must have been done already.*)
     4.7 -fun constrains_tac(cs,ss) i =
     4.8 +fun constrains_tac ctxt i =
     4.9 +  let
    4.10 +    val cs = claset_of ctxt;
    4.11 +    val ss = simpset_of ctxt;
    4.12 +  in
    4.13     SELECT_GOAL
    4.14        (EVERY [REPEAT (Always_Int_tac 1),
    4.15                (*reduce the fancy safety properties to "constrains"*)
    4.16 @@ -28,10 +32,15 @@
    4.17                full_simp_tac ss 1,
    4.18                REPEAT (FIRSTGOAL (etac disjE)),
    4.19                ALLGOALS (clarify_tac cs),
    4.20 -              ALLGOALS (asm_full_simp_tac ss)]) i;
    4.21 +              ALLGOALS (asm_full_simp_tac ss)]) i
    4.22 +  end;
    4.23  
    4.24  (*proves "ensures/leadsTo" properties when the program is specified*)
    4.25 -fun ensures_tac(cs,ss) sact =
    4.26 +fun ensures_tac ctxt sact =
    4.27 +  let
    4.28 +    val cs = claset_of ctxt;
    4.29 +    val ss = simpset_of ctxt;
    4.30 +  in
    4.31      SELECT_GOAL
    4.32        (EVERY [REPEAT (Always_Int_tac 1),
    4.33                etac @{thm Always_LeadsTo_Basis} 1
    4.34 @@ -46,9 +55,10 @@
    4.35                  [(("act", 0), sact)] @{thm transientI} 2,
    4.36                   (*simplify the command's domain*)
    4.37                simp_tac (ss addsimps [@{thm Domain_def}]) 3,
    4.38 -              constrains_tac (cs,ss) 1,
    4.39 +              constrains_tac ctxt 1,
    4.40                ALLGOALS (clarify_tac cs),
    4.41 -              ALLGOALS (asm_lr_simp_tac ss)]);
    4.42 +              ALLGOALS (asm_lr_simp_tac ss)])
    4.43 +  end;
    4.44  
    4.45  
    4.46  (*Composition equivalences, from Lift_prog*)