tuned ML setup;
authorwenzelm
Tue Aug 07 23:24:10 2007 +0200 (2007-08-07)
changeset 241809f818139951b
parent 24179 c89d77d97f84
child 24181 102ebceaa495
tuned ML setup;
src/HOL/Hyperreal/MacLaurin.thy
src/HOL/TLA/Action.thy
src/HOL/TLA/Inc/Inc.thy
src/HOL/TLA/Intensional.thy
src/HOL/TLA/Memory/MIParameters.thy
src/HOL/TLA/Memory/MemoryImplementation.thy
     1.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Tue Aug 07 20:43:36 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Tue Aug 07 23:24:10 2007 +0200
     1.3 @@ -29,31 +29,30 @@
     1.4  by arith
     1.5  
     1.6  text{*A crude tactic to differentiate by proof.*}
     1.7 +
     1.8 +lemmas deriv_rulesI =
     1.9 +  DERIV_ident DERIV_const DERIV_cos DERIV_cmult
    1.10 +  DERIV_sin DERIV_exp DERIV_inverse DERIV_pow
    1.11 +  DERIV_add DERIV_diff DERIV_mult DERIV_minus
    1.12 +  DERIV_inverse_fun DERIV_quotient DERIV_fun_pow
    1.13 +  DERIV_fun_exp DERIV_fun_sin DERIV_fun_cos
    1.14 +  DERIV_ident DERIV_const DERIV_cos
    1.15 +
    1.16  ML
    1.17  {*
    1.18  local
    1.19 -val deriv_rulesI =
    1.20 -  [thm "DERIV_ident", thm "DERIV_const", thm "DERIV_cos", thm "DERIV_cmult",
    1.21 -  thm "DERIV_sin", thm "DERIV_exp", thm "DERIV_inverse", thm "DERIV_pow",
    1.22 -  thm "DERIV_add", thm "DERIV_diff", thm "DERIV_mult", thm "DERIV_minus",
    1.23 -  thm "DERIV_inverse_fun", thm "DERIV_quotient", thm "DERIV_fun_pow",
    1.24 -  thm "DERIV_fun_exp", thm "DERIV_fun_sin", thm "DERIV_fun_cos",
    1.25 -  thm "DERIV_ident", thm "DERIV_const", thm "DERIV_cos"];
    1.26 -
    1.27 -val DERIV_chain2 = thm "DERIV_chain2";
    1.28 -
    1.29 -in
    1.30 -
    1.31  exception DERIV_name;
    1.32  fun get_fun_name (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _)) = f
    1.33  |   get_fun_name (_ $ (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _))) = f
    1.34  |   get_fun_name _ = raise DERIV_name;
    1.35  
    1.36 +in
    1.37 +
    1.38  val deriv_tac =
    1.39    SUBGOAL (fn (prem,i) =>
    1.40 -   (resolve_tac deriv_rulesI i) ORELSE
    1.41 +   (resolve_tac @{thms deriv_rulesI} i) ORELSE
    1.42      ((rtac (read_instantiate [("f",get_fun_name prem)]
    1.43 -                     DERIV_chain2) i) handle DERIV_name => no_tac));;
    1.44 +                     @{thm DERIV_chain2}) i) handle DERIV_name => no_tac));;
    1.45  
    1.46  val DERIV_tac = ALLGOALS(fn i => REPEAT(deriv_tac i));
    1.47  
     2.1 --- a/src/HOL/TLA/Action.thy	Tue Aug 07 20:43:36 2007 +0200
     2.2 +++ b/src/HOL/TLA/Action.thy	Tue Aug 07 23:24:10 2007 +0200
     2.3 @@ -109,13 +109,9 @@
     2.4     functions defined in Intensional.ML in that they introduce a
     2.5     "world" parameter of the form (s,t) and apply additional rewrites.
     2.6  *)
     2.7 -local
     2.8 -  val action_rews = thms "action_rews";
     2.9 -  val actionD = thm "actionD";
    2.10 -in
    2.11  
    2.12  fun action_unlift th =
    2.13 -  (rewrite_rule action_rews (th RS actionD))
    2.14 +  (rewrite_rule @{thms action_rews} (th RS @{thm actionD}))
    2.15      handle THM _ => int_unlift th;
    2.16  
    2.17  (* Turn  |- A = B  into meta-level rewrite rule  A == B *)
    2.18 @@ -126,8 +122,6 @@
    2.19        Const _ $ (Const ("Intensional.Valid", _) $ _) =>
    2.20                (flatten (action_unlift th) handle THM _ => th)
    2.21      | _ => th;
    2.22 -
    2.23 -end
    2.24  *}
    2.25  
    2.26  setup {*
    2.27 @@ -269,22 +263,12 @@
    2.28     should plug in only "very safe" rules that can be applied blindly.
    2.29     Note that it applies whatever simplifications are currently active.
    2.30  *)
    2.31 -local
    2.32 -  val actionI = thm "actionI";
    2.33 -  val intI = thm "intI";
    2.34 -in
    2.35 -
    2.36  fun action_simp_tac ss intros elims =
    2.37      asm_full_simp_tac
    2.38           (ss setloop ((resolve_tac ((map action_use intros)
    2.39 -                                    @ [refl,impI,conjI,actionI,intI,allI]))
    2.40 +                                    @ [refl,impI,conjI,@{thm actionI},@{thm intI},allI]))
    2.41                        ORELSE' (eresolve_tac ((map action_use elims)
    2.42                                               @ [conjE,disjE,exE]))));
    2.43 -
    2.44 -(* default version without additional plug-in rules *)
    2.45 -val Action_simp_tac = action_simp_tac (simpset()) [] []
    2.46 -
    2.47 -end
    2.48  *}
    2.49  
    2.50  (* ---------------- enabled_tac: tactic to prove (Enabled A) -------------------- *)
    2.51 @@ -299,14 +283,9 @@
    2.52     - Solve for the unknowns using standard HOL reasoning.
    2.53     The following tactic combines these steps except the final one.
    2.54  *)
    2.55 -local
    2.56 -  val base_enabled = thm "base_enabled";
    2.57 -in
    2.58  
    2.59 -fun enabled_tac base_vars =
    2.60 -  clarsimp_tac (claset() addSIs [base_vars RS base_enabled], simpset());
    2.61 -
    2.62 -end
    2.63 +fun enabled_tac (cs, ss) base_vars =
    2.64 +  clarsimp_tac (cs addSIs [base_vars RS @{thm base_enabled}], ss);
    2.65  *}
    2.66  
    2.67  (* Example *)
    2.68 @@ -314,7 +293,7 @@
    2.69  lemma
    2.70    assumes "basevars (x,y,z)"
    2.71    shows "|- x --> Enabled ($x & (y$ = #False))"
    2.72 -  apply (tactic {* enabled_tac (thm "assms") 1 *})
    2.73 +  apply (tactic {* enabled_tac @{clasimpset} @{thm assms} 1 *})
    2.74    apply auto
    2.75    done
    2.76  
     3.1 --- a/src/HOL/TLA/Inc/Inc.thy	Tue Aug 07 20:43:36 2007 +0200
     3.2 +++ b/src/HOL/TLA/Inc/Inc.thy	Tue Aug 07 23:24:10 2007 +0200
     3.3 @@ -164,7 +164,7 @@
     3.4  lemma N1_enabled_at_g: "|- pc1 = #g --> Enabled (<N1>_(x,y,sem,pc1,pc2))"
     3.5    apply clarsimp
     3.6    apply (rule_tac F = gamma1 in enabled_mono)
     3.7 -   apply (tactic {* enabled_tac (thm "Inc_base") 1 *})
     3.8 +   apply (tactic {* enabled_tac @{clasimpset} @{thm Inc_base} 1 *})
     3.9    apply (force simp: gamma1_def)
    3.10    apply (force simp: angle_def gamma1_def N1_def)
    3.11    done
    3.12 @@ -186,7 +186,7 @@
    3.13  lemma N2_enabled_at_g: "|- pc2 = #g --> Enabled (<N2>_(x,y,sem,pc1,pc2))"
    3.14    apply clarsimp
    3.15    apply (rule_tac F = gamma2 in enabled_mono)
    3.16 -  apply (tactic {* enabled_tac (thm "Inc_base") 1 *})
    3.17 +  apply (tactic {* enabled_tac @{clasimpset} @{thm Inc_base} 1 *})
    3.18     apply (force simp: gamma2_def)
    3.19    apply (force simp: angle_def gamma2_def N2_def)
    3.20    done
    3.21 @@ -205,7 +205,7 @@
    3.22  lemma N2_enabled_at_b: "|- pc2 = #b --> Enabled (<N2>_(x,y,sem,pc1,pc2))"
    3.23    apply clarsimp
    3.24    apply (rule_tac F = beta2 in enabled_mono)
    3.25 -   apply (tactic {* enabled_tac (thm "Inc_base") 1 *})
    3.26 +   apply (tactic {* enabled_tac @{clasimpset} @{thm Inc_base} 1 *})
    3.27     apply (force simp: beta2_def)
    3.28    apply (force simp: angle_def beta2_def N2_def)
    3.29    done
    3.30 @@ -247,7 +247,7 @@
    3.31    "|- pc2 = #a & (PsiInv & pc1 = #a) --> Enabled (<N1>_(x,y,sem,pc1,pc2))"
    3.32    apply clarsimp
    3.33    apply (rule_tac F = alpha1 in enabled_mono)
    3.34 -  apply (tactic {* enabled_tac (thm "Inc_base") 1 *})
    3.35 +  apply (tactic {* enabled_tac @{clasimpset} @{thm Inc_base} 1 *})
    3.36     apply (force simp: alpha1_def PsiInv_defs)
    3.37    apply (force simp: angle_def alpha1_def N1_def)
    3.38    done
    3.39 @@ -288,7 +288,7 @@
    3.40  lemma N1_enabled_at_b: "|- pc1 = #b --> Enabled (<N1>_(x,y,sem,pc1,pc2))"
    3.41    apply clarsimp
    3.42    apply (rule_tac F = beta1 in enabled_mono)
    3.43 -   apply (tactic {* enabled_tac (thm "Inc_base") 1 *})
    3.44 +   apply (tactic {* enabled_tac @{clasimpset} @{thm Inc_base} 1 *})
    3.45     apply (force simp: beta1_def)
    3.46    apply (force simp: angle_def beta1_def N1_def)
    3.47    done
     4.1 --- a/src/HOL/TLA/Intensional.thy	Tue Aug 07 20:43:36 2007 +0200
     4.2 +++ b/src/HOL/TLA/Intensional.thy	Tue Aug 07 23:24:10 2007 +0200
     4.3 @@ -243,24 +243,17 @@
     4.4  (* ======== Functions to "unlift" intensional implications into HOL rules ====== *)
     4.5  
     4.6  ML {*
     4.7 -
     4.8 -local
     4.9 -  val intD = thm "intD";
    4.10 -  val inteq_reflection = thm "inteq_reflection";
    4.11 -  val intensional_rews = thms "intensional_rews";
    4.12 -in
    4.13 -
    4.14  (* Basic unlifting introduces a parameter "w" and applies basic rewrites, e.g.
    4.15     |- F = G    becomes   F w = G w
    4.16     |- F --> G  becomes   F w --> G w
    4.17  *)
    4.18  
    4.19  fun int_unlift th =
    4.20 -  rewrite_rule intensional_rews (th RS intD handle THM _ => th);
    4.21 +  rewrite_rule @{thms intensional_rews} (th RS @{thm intD} handle THM _ => th);
    4.22  
    4.23  (* Turn  |- F = G  into meta-level rewrite rule  F == G *)
    4.24  fun int_rewrite th =
    4.25 -  zero_var_indexes (rewrite_rule intensional_rews (th RS inteq_reflection))
    4.26 +  zero_var_indexes (rewrite_rule @{thms intensional_rews} (th RS @{thm inteq_reflection}))
    4.27  
    4.28  (* flattening turns "-->" into "==>" and eliminates conjunctions in the
    4.29     antecedent. For example,
    4.30 @@ -299,8 +292,6 @@
    4.31        Const _ $ (Const ("Intensional.Valid", _) $ _) =>
    4.32                (flatten (int_unlift th) handle THM _ => th)
    4.33      | _ => th
    4.34 -
    4.35 -end
    4.36  *}
    4.37  
    4.38  setup {*
     5.1 --- a/src/HOL/TLA/Memory/MIParameters.thy	Tue Aug 07 20:43:36 2007 +0200
     5.2 +++ b/src/HOL/TLA/Memory/MIParameters.thy	Tue Aug 07 23:24:10 2007 +0200
     5.3 @@ -14,6 +14,4 @@
     5.4  
     5.5  datatype  histState  =  histA | histB
     5.6  
     5.7 -ML {* use_legacy_bindings (the_context ()) *}
     5.8 -
     5.9  end
     6.1 --- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Tue Aug 07 20:43:36 2007 +0200
     6.2 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Tue Aug 07 23:24:10 2007 +0200
     6.3 @@ -115,7 +115,7 @@
     6.4       (one- or two-element) set.
     6.5       NB: The second conjunct of the definition in the paper is taken care of by
     6.6       the type definitions. The last conjunct is asserted separately as the memory
     6.7 -     invariant MemInv, proved in Memory.ML. *)
     6.8 +     invariant MemInv, proved in Memory.thy. *)
     6.9    S :: "histType => bool => bool => bool => mClkState => rpcState => histState => histState => PrIds => stpred"
    6.10        "S rmhist ecalling ccalling rcalling cs rs hs1 hs2 p == PRED
    6.11                  Calling memCh p = #ecalling
    6.12 @@ -177,8 +177,8 @@
    6.13  (*
    6.14      The main theorem is theorem "Implementation" at the end of this file,
    6.15      which shows that the composition of a reliable memory, an RPC component, and
    6.16 -    a memory clerk implements an unreliable memory. The files "MIsafe.ML" and
    6.17 -    "MIlive.ML" contain lower-level lemmas for the safety and liveness parts.
    6.18 +    a memory clerk implements an unreliable memory. The files "MIsafe.thy" and
    6.19 +    "MIlive.thy" contain lower-level lemmas for the safety and liveness parts.
    6.20  
    6.21      Steps are (roughly) numbered as in the hand proof.
    6.22  *)
    6.23 @@ -187,7 +187,7 @@
    6.24  
    6.25  declare if_weak_cong [cong del]
    6.26  
    6.27 -ML {* val MI_css = (claset(), simpset()) *}
    6.28 +ML {* val MI_css = (@{claset}, @{simpset}) *}
    6.29  
    6.30  (* A more aggressive variant that tries to solve subgoals by assumption
    6.31     or contradiction during the simplification.
    6.32 @@ -200,7 +200,7 @@
    6.33    let
    6.34      val (cs,ss) = MI_css
    6.35    in
    6.36 -    (cs addSEs [temp_use (thm "squareE")],
    6.37 +    (cs addSEs [temp_use @{thm squareE}],
    6.38        ss addSSolver (mk_solver "" (fn thms => assume_tac ORELSE' (etac notE))))
    6.39    end;
    6.40  
    6.41 @@ -762,19 +762,13 @@
    6.42     steps of the implementation, and try to solve the idling case by simplification
    6.43  *)
    6.44  ML {*
    6.45 -local
    6.46 -  val actionI = thm "actionI";
    6.47 -  val action_rews = thms "action_rews";
    6.48 -  val Step1_4_7 = thm "Step1_4_7";
    6.49 -in
    6.50 -fun split_idle_tac simps i =
    6.51 -    EVERY [TRY (rtac actionI i),
    6.52 +fun split_idle_tac ss simps i =
    6.53 +    EVERY [TRY (rtac @{thm actionI} i),
    6.54             case_tac "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" i,
    6.55 -           rewrite_goals_tac action_rews,
    6.56 -           forward_tac [temp_use Step1_4_7] i,
    6.57 -           asm_full_simp_tac (simpset() addsimps simps) i
    6.58 +           rewrite_goals_tac @{thms action_rews},
    6.59 +           forward_tac [temp_use @{thm Step1_4_7}] i,
    6.60 +           asm_full_simp_tac (ss addsimps simps) i
    6.61            ]
    6.62 -end
    6.63  *}
    6.64  (* ----------------------------------------------------------------------
    6.65     Combine steps 1.2 and 1.4 to prove that the implementation satisfies
    6.66 @@ -786,7 +780,7 @@
    6.67  lemma unchanged_safe: "|- (~unchanged (e p, c p, r p, m p, rmhist!p)
    6.68               --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p))
    6.69           --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
    6.70 -  apply (tactic {* split_idle_tac [thm "square_def"] 1 *})
    6.71 +  apply (tactic {* split_idle_tac @{simpset} [thm "square_def"] 1 *})
    6.72    apply force
    6.73    done
    6.74  (* turn into (unsafe, looping!) introduction rule *)
    6.75 @@ -858,7 +852,7 @@
    6.76  
    6.77  lemma S1_successors: "|- $S1 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
    6.78           --> (S1 rmhist p)$ | (S2 rmhist p)$"
    6.79 -  apply (tactic "split_idle_tac [] 1")
    6.80 +  apply (tactic "split_idle_tac @{simpset} [] 1")
    6.81    apply (auto dest!: Step1_2_1 [temp_use])
    6.82    done
    6.83  
    6.84 @@ -892,7 +886,7 @@
    6.85  
    6.86  lemma S2_successors: "|- $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
    6.87           --> (S2 rmhist p)$ | (S3 rmhist p)$"
    6.88 -  apply (tactic "split_idle_tac [] 1")
    6.89 +  apply (tactic "split_idle_tac @{simpset} [] 1")
    6.90    apply (auto dest!: Step1_2_2 [temp_use])
    6.91    done
    6.92  
    6.93 @@ -918,7 +912,7 @@
    6.94  
    6.95  lemma S3_successors: "|- $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
    6.96           --> (S3 rmhist p)$ | (S4 rmhist p | S6 rmhist p)$"
    6.97 -  apply (tactic "split_idle_tac [] 1")
    6.98 +  apply (tactic "split_idle_tac @{simpset} [] 1")
    6.99    apply (auto dest!: Step1_2_3 [temp_use])
   6.100    done
   6.101  
   6.102 @@ -946,7 +940,7 @@
   6.103  lemma S4_successors: "|- $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
   6.104          & (ALL l. $MemInv mm l)
   6.105          --> (S4 rmhist p)$ | (S5 rmhist p)$"
   6.106 -  apply (tactic "split_idle_tac [] 1")
   6.107 +  apply (tactic "split_idle_tac @{simpset} [] 1")
   6.108    apply (auto dest!: Step1_2_4 [temp_use])
   6.109    done
   6.110  
   6.111 @@ -956,7 +950,7 @@
   6.112           & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (ALL l. $MemInv mm l)
   6.113           --> (S4 rmhist p & ires!p = #NotAResult)$
   6.114               | ((S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)$"
   6.115 -  apply (tactic {* split_idle_tac [thm "m_def"] 1 *})
   6.116 +  apply (tactic {* split_idle_tac @{simpset} [thm "m_def"] 1 *})
   6.117    apply (auto dest!: Step1_2_4 [temp_use])
   6.118    done
   6.119  
   6.120 @@ -987,7 +981,7 @@
   6.121  lemma S4b_successors: "|- $(S4 rmhist p & ires!p ~= #NotAResult)
   6.122           & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (ALL l. $MemInv mm l)
   6.123           --> (S4 rmhist p & ires!p ~= #NotAResult)$ | (S5 rmhist p)$"
   6.124 -  apply (tactic {* split_idle_tac [thm "m_def"] 1 *})
   6.125 +  apply (tactic {* split_idle_tac @{simpset} [thm "m_def"] 1 *})
   6.126    apply (auto dest!: WriteResult [temp_use] Step1_2_4 [temp_use] ReadResult [temp_use])
   6.127    done
   6.128  
   6.129 @@ -1016,7 +1010,7 @@
   6.130  
   6.131  lemma S5_successors: "|- $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
   6.132           --> (S5 rmhist p)$ | (S6 rmhist p)$"
   6.133 -  apply (tactic "split_idle_tac [] 1")
   6.134 +  apply (tactic "split_idle_tac @{simpset} [] 1")
   6.135    apply (auto dest!: Step1_2_5 [temp_use])
   6.136    done
   6.137  
   6.138 @@ -1042,7 +1036,7 @@
   6.139  
   6.140  lemma S6_successors: "|- $S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
   6.141           --> (S1 rmhist p)$ | (S3 rmhist p)$ | (S6 rmhist p)$"
   6.142 -  apply (tactic "split_idle_tac [] 1")
   6.143 +  apply (tactic "split_idle_tac @{simpset} [] 1")
   6.144    apply (auto dest!: Step1_2_6 [temp_use])
   6.145    done
   6.146  
   6.147 @@ -1257,7 +1251,7 @@
   6.148    apply clarsimp
   6.149    apply (drule WriteS4 [action_use])
   6.150     apply assumption
   6.151 -  apply (tactic "split_idle_tac [] 1")
   6.152 +  apply (tactic "split_idle_tac @{simpset} [] 1")
   6.153    apply (auto simp: ImpNext_def dest!: S4EnvUnch [temp_use] S4ClerkUnch [temp_use]
   6.154      S4RPCUnch [temp_use])
   6.155       apply (auto simp: square_def dest: S4Write [temp_use])