src/HOL/TLA/TLA.thy
changeset 60592 c9bd1d902f04
parent 60591 e0b77517f9a9
child 60754 02924903a6fd
     1.1 --- a/src/HOL/TLA/TLA.thy	Fri Jun 26 15:55:44 2015 +0200
     1.2 +++ b/src/HOL/TLA/TLA.thy	Fri Jun 26 18:51:19 2015 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4      Copyright:  1998 University of Munich
     1.5  *)
     1.6  
     1.7 -section {* The temporal level of TLA *}
     1.8 +section \<open>The temporal level of TLA\<close>
     1.9  
    1.10  theory TLA
    1.11  imports Init
    1.12 @@ -102,7 +102,7 @@
    1.13  
    1.14  (* ======== Functions to "unlift" temporal theorems ====== *)
    1.15  
    1.16 -ML {*
    1.17 +ML \<open>
    1.18  (* The following functions are specialized versions of the corresponding
    1.19     functions defined in theory Intensional in that they introduce a
    1.20     "world" parameter of type "behavior".
    1.21 @@ -121,16 +121,16 @@
    1.22    | _ => th;
    1.23  
    1.24  fun try_rewrite ctxt th = temp_rewrite ctxt th handle THM _ => temp_use ctxt th;
    1.25 -*}
    1.26 +\<close>
    1.27  
    1.28  attribute_setup temp_unlift =
    1.29 -  {* Scan.succeed (Thm.rule_attribute (temp_unlift o Context.proof_of)) *}
    1.30 +  \<open>Scan.succeed (Thm.rule_attribute (temp_unlift o Context.proof_of))\<close>
    1.31  attribute_setup temp_rewrite =
    1.32 -  {* Scan.succeed (Thm.rule_attribute (temp_rewrite o Context.proof_of)) *}
    1.33 +  \<open>Scan.succeed (Thm.rule_attribute (temp_rewrite o Context.proof_of))\<close>
    1.34  attribute_setup temp_use =
    1.35 -  {* Scan.succeed (Thm.rule_attribute (temp_use o Context.proof_of)) *}
    1.36 +  \<open>Scan.succeed (Thm.rule_attribute (temp_use o Context.proof_of))\<close>
    1.37  attribute_setup try_rewrite =
    1.38 -  {* Scan.succeed (Thm.rule_attribute (try_rewrite o Context.proof_of)) *}
    1.39 +  \<open>Scan.succeed (Thm.rule_attribute (try_rewrite o Context.proof_of))\<close>
    1.40  
    1.41  
    1.42  (* ------------------------------------------------------------------------- *)
    1.43 @@ -283,7 +283,7 @@
    1.44  
    1.45  lemma box_thin: "\<lbrakk> sigma \<Turnstile> \<box>F; PROP W \<rbrakk> \<Longrightarrow> PROP W" .
    1.46  
    1.47 -ML {*
    1.48 +ML \<open>
    1.49  fun merge_box_tac i =
    1.50     REPEAT_DETERM (EVERY [etac @{thm box_conjE} i, atac i, etac @{thm box_thin} i])
    1.51  
    1.52 @@ -298,12 +298,12 @@
    1.53  fun merge_act_box_tac ctxt i =
    1.54    REPEAT_DETERM (EVERY [etac @{thm box_conjE_act} i, atac i,
    1.55      Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "state * state")] [] @{thm box_thin} i])
    1.56 -*}
    1.57 +\<close>
    1.58  
    1.59 -method_setup merge_box = {* Scan.succeed (K (SIMPLE_METHOD' merge_box_tac)) *}
    1.60 -method_setup merge_temp_box = {* Scan.succeed (SIMPLE_METHOD' o merge_temp_box_tac) *}
    1.61 -method_setup merge_stp_box = {* Scan.succeed (SIMPLE_METHOD' o merge_stp_box_tac) *}
    1.62 -method_setup merge_act_box = {* Scan.succeed (SIMPLE_METHOD' o merge_act_box_tac) *}
    1.63 +method_setup merge_box = \<open>Scan.succeed (K (SIMPLE_METHOD' merge_box_tac))\<close>
    1.64 +method_setup merge_temp_box = \<open>Scan.succeed (SIMPLE_METHOD' o merge_temp_box_tac)\<close>
    1.65 +method_setup merge_stp_box = \<open>Scan.succeed (SIMPLE_METHOD' o merge_stp_box_tac)\<close>
    1.66 +method_setup merge_act_box = \<open>Scan.succeed (SIMPLE_METHOD' o merge_act_box_tac)\<close>
    1.67  
    1.68  (* rewrite rule to push universal quantification through box:
    1.69        (sigma \<Turnstile> \<box>(\<forall>x. F x)) = (\<forall>x. (sigma \<Turnstile> \<box>F x))
    1.70 @@ -571,7 +571,7 @@
    1.71  
    1.72  (* ---------------- (Semi-)automatic invariant tactics ---------------------- *)
    1.73  
    1.74 -ML {*
    1.75 +ML \<open>
    1.76  (* inv_tac reduces goals of the form ... \<Longrightarrow> sigma \<Turnstile> \<box>P *)
    1.77  fun inv_tac ctxt =
    1.78    SELECT_GOAL
    1.79 @@ -592,15 +592,15 @@
    1.80      (inv_tac ctxt 1 THEN
    1.81        (TRYALL (action_simp_tac
    1.82          (ctxt addsimps [@{thm Init_stp}, @{thm Init_act}]) [] [@{thm squareE}])));
    1.83 -*}
    1.84 +\<close>
    1.85  
    1.86 -method_setup invariant = {*
    1.87 +method_setup invariant = \<open>
    1.88    Method.sections Clasimp.clasimp_modifiers >> (K (SIMPLE_METHOD' o inv_tac))
    1.89 -*}
    1.90 +\<close>
    1.91  
    1.92 -method_setup auto_invariant = {*
    1.93 +method_setup auto_invariant = \<open>
    1.94    Method.sections Clasimp.clasimp_modifiers >> (K (SIMPLE_METHOD' o auto_inv_tac))
    1.95 -*}
    1.96 +\<close>
    1.97  
    1.98  lemma unless: "\<turnstile> \<box>($P \<longrightarrow> P` \<or> Q`) \<longrightarrow> (stable P) \<or> \<diamond>Q"
    1.99    apply (unfold dmd_def)
   1.100 @@ -685,10 +685,10 @@
   1.101    done
   1.102  
   1.103  (* A tactic that "boxes" all fairness conditions. Apply more_temp_simps to "unbox". *)
   1.104 -ML {*
   1.105 +ML \<open>
   1.106  fun box_fair_tac ctxt =
   1.107    SELECT_GOAL (REPEAT (dresolve_tac ctxt [@{thm BoxWFI}, @{thm BoxSFI}] 1))
   1.108 -*}
   1.109 +\<close>
   1.110  
   1.111  
   1.112  (* ------------------------------ leads-to ------------------------------ *)