src/ZF/UNITY/Constrains.thy
changeset 24893 b8ef7afe3a6b
parent 24051 896fb015079c
child 30510 4120fc59dd85
     1.1 --- a/src/ZF/UNITY/Constrains.thy	Sun Oct 07 15:49:25 2007 +0200
     1.2 +++ b/src/ZF/UNITY/Constrains.thy	Sun Oct 07 21:19:31 2007 +0200
     1.3 @@ -7,8 +7,8 @@
     1.4  
     1.5  theory Constrains
     1.6  imports UNITY
     1.7 +begin
     1.8  
     1.9 -begin
    1.10  consts traces :: "[i, i] => i"
    1.11    (* Initial states and program => (final state, reversed trace to it)... 
    1.12        the domain may also be state*list(state) *)
    1.13 @@ -39,23 +39,22 @@
    1.14    type_intros UnI1 UnI2 fieldI2 UN_I
    1.15  
    1.16    
    1.17 -consts
    1.18 -  Constrains :: "[i,i] => i"  (infixl "Co"     60)
    1.19 -  op_Unless  :: "[i, i] => i"  (infixl "Unless" 60)
    1.20 +definition
    1.21 +  Constrains :: "[i,i] => i"  (infixl "Co" 60)  where
    1.22 +  "A Co B == {F:program. F:(reachable(F) Int A) co B}"
    1.23  
    1.24 -defs
    1.25 -  Constrains_def:
    1.26 -    "A Co B == {F:program. F:(reachable(F) Int A) co B}"
    1.27 +definition
    1.28 +  op_Unless  :: "[i, i] => i"  (infixl "Unless" 60)  where
    1.29 +  "A Unless B == (A-B) Co (A Un B)"
    1.30  
    1.31 -  Unless_def:
    1.32 -    "A Unless B == (A-B) Co (A Un B)"
    1.33 +definition
    1.34 +  Stable     :: "i => i"  where
    1.35 +  "Stable(A) == A Co A"
    1.36  
    1.37 -constdefs
    1.38 -  Stable     :: "i => i"
    1.39 -    "Stable(A) == A Co A"
    1.40 +definition
    1.41    (*Always is the weak form of "invariant"*)
    1.42 -  Always :: "i => i"
    1.43 -    "Always(A) == initially(A) Int Stable(A)"
    1.44 +  Always :: "i => i"  where
    1.45 +  "Always(A) == initially(A) Int Stable(A)"
    1.46  
    1.47  
    1.48  (*** traces and reachable ***)
    1.49 @@ -330,8 +329,7 @@
    1.50  (** Unless **)
    1.51  
    1.52  lemma Unless_type: "A Unless B <=program"
    1.53 -
    1.54 -apply (unfold Unless_def)
    1.55 +apply (unfold op_Unless_def)
    1.56  apply (rule Constrains_type)
    1.57  done
    1.58  
    1.59 @@ -457,80 +455,11 @@
    1.60  
    1.61  ML
    1.62  {*
    1.63 -val reachable_type = thm "reachable_type";
    1.64 -val st_set_reachable = thm "st_set_reachable";
    1.65 -val reachable_Int_state = thm "reachable_Int_state";
    1.66 -val state_Int_reachable = thm "state_Int_reachable";
    1.67 -val reachable_equiv_traces = thm "reachable_equiv_traces";
    1.68 -val Init_into_reachable = thm "Init_into_reachable";
    1.69 -val stable_reachable = thm "stable_reachable";
    1.70 -val invariant_reachable = thm "invariant_reachable";
    1.71 -val invariant_includes_reachable = thm "invariant_includes_reachable";
    1.72 -val constrains_reachable_Int = thm "constrains_reachable_Int";
    1.73 -val Constrains_eq_constrains = thm "Constrains_eq_constrains";
    1.74 -val Constrains_def2 = thm "Constrains_def2";
    1.75 -val constrains_imp_Constrains = thm "constrains_imp_Constrains";
    1.76 -val ConstrainsI = thm "ConstrainsI";
    1.77 -val Constrains_type = thm "Constrains_type";
    1.78 -val Constrains_empty = thm "Constrains_empty";
    1.79 -val Constrains_state = thm "Constrains_state";
    1.80 -val Constrains_weaken_R = thm "Constrains_weaken_R";
    1.81 -val Constrains_weaken_L = thm "Constrains_weaken_L";
    1.82 -val Constrains_weaken = thm "Constrains_weaken";
    1.83 -val Constrains_Un = thm "Constrains_Un";
    1.84 -val Constrains_UN = thm "Constrains_UN";
    1.85 -val Constrains_Int = thm "Constrains_Int";
    1.86 -val Constrains_INT = thm "Constrains_INT";
    1.87 -val Constrains_imp_subset = thm "Constrains_imp_subset";
    1.88 -val Constrains_trans = thm "Constrains_trans";
    1.89 -val Constrains_cancel = thm "Constrains_cancel";
    1.90 -val stable_imp_Stable = thm "stable_imp_Stable";
    1.91 -val Stable_eq = thm "Stable_eq";
    1.92 -val Stable_eq_stable = thm "Stable_eq_stable";
    1.93 -val StableI = thm "StableI";
    1.94 -val StableD = thm "StableD";
    1.95 -val Stable_Un = thm "Stable_Un";
    1.96 -val Stable_Int = thm "Stable_Int";
    1.97 -val Stable_Constrains_Un = thm "Stable_Constrains_Un";
    1.98 -val Stable_Constrains_Int = thm "Stable_Constrains_Int";
    1.99 -val Stable_UN = thm "Stable_UN";
   1.100 -val Stable_INT = thm "Stable_INT";
   1.101 -val Stable_reachable = thm "Stable_reachable";
   1.102 -val Stable_type = thm "Stable_type";
   1.103 -val Elimination = thm "Elimination";
   1.104 -val Elimination2 = thm "Elimination2";
   1.105 -val Unless_type = thm "Unless_type";
   1.106 -val AlwaysI = thm "AlwaysI";
   1.107 -val AlwaysD = thm "AlwaysD";
   1.108 -val AlwaysE = thm "AlwaysE";
   1.109 -val Always_imp_Stable = thm "Always_imp_Stable";
   1.110 -val Always_includes_reachable = thm "Always_includes_reachable";
   1.111 -val invariant_imp_Always = thm "invariant_imp_Always";
   1.112 -val Always_reachable = thm "Always_reachable";
   1.113 -val Always_eq_invariant_reachable = thm "Always_eq_invariant_reachable";
   1.114 -val Always_eq_includes_reachable = thm "Always_eq_includes_reachable";
   1.115 -val Always_type = thm "Always_type";
   1.116 -val Always_state_eq = thm "Always_state_eq";
   1.117 -val state_AlwaysI = thm "state_AlwaysI";
   1.118 -val Always_eq_UN_invariant = thm "Always_eq_UN_invariant";
   1.119 -val Always_weaken = thm "Always_weaken";
   1.120 -val Int_absorb2 = thm "Int_absorb2";
   1.121 -val Always_Constrains_pre = thm "Always_Constrains_pre";
   1.122 -val Always_Constrains_post = thm "Always_Constrains_post";
   1.123 -val Always_ConstrainsI = thm "Always_ConstrainsI";
   1.124 -val Always_ConstrainsD = thm "Always_ConstrainsD";
   1.125 -val Always_Constrains_weaken = thm "Always_Constrains_weaken";
   1.126 -val Always_Int_distrib = thm "Always_Int_distrib";
   1.127 -val Always_INT_distrib = thm "Always_INT_distrib";
   1.128 -val Always_Int_I = thm "Always_Int_I";
   1.129 -val Always_Diff_Un_eq = thm "Always_Diff_Un_eq";
   1.130 -val Always_thin = thm "Always_thin";
   1.131 -
   1.132  (*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
   1.133 -val Always_Int_tac = dtac Always_Int_I THEN' assume_tac THEN' etac Always_thin;
   1.134 +val Always_Int_tac = dtac @{thm Always_Int_I} THEN' assume_tac THEN' etac @{thm Always_thin};
   1.135  
   1.136  (*Combines a list of invariance THEOREMS into one.*)
   1.137 -val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Always_Int_I);
   1.138 +val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I});
   1.139  
   1.140  (*To allow expansion of the program's definition when appropriate*)
   1.141  structure ProgramDefs = NamedThmsFun(val name = "program" val description = "program definitions");
   1.142 @@ -541,13 +470,13 @@
   1.143    let val css as (cs, ss) = local_clasimpset_of ctxt in
   1.144     SELECT_GOAL
   1.145        (EVERY [REPEAT (Always_Int_tac 1),
   1.146 -              REPEAT (etac Always_ConstrainsI 1
   1.147 +              REPEAT (etac @{thm Always_ConstrainsI} 1
   1.148                        ORELSE
   1.149 -                      resolve_tac [StableI, stableI,
   1.150 -                                   constrains_imp_Constrains] 1),
   1.151 -              rtac constrainsI 1,
   1.152 +                      resolve_tac [@{thm StableI}, @{thm stableI},
   1.153 +                                   @{thm constrains_imp_Constrains}] 1),
   1.154 +              rtac @{thm constrainsI} 1,
   1.155                (* Three subgoals *)
   1.156 -              rewrite_goal_tac [st_set_def] 3,
   1.157 +              rewrite_goal_tac [@{thm st_set_def}] 3,
   1.158                REPEAT (force_tac css 2),
   1.159                full_simp_tac (ss addsimps (ProgramDefs.get ctxt)) 1,
   1.160                ALLGOALS (clarify_tac cs),
   1.161 @@ -561,7 +490,7 @@
   1.162  
   1.163  (*For proving invariants*)
   1.164  fun always_tac ctxt i = 
   1.165 -    rtac AlwaysI i THEN force_tac (local_clasimpset_of ctxt) i THEN constrains_tac ctxt i;
   1.166 +    rtac @{thm AlwaysI} i THEN force_tac (local_clasimpset_of ctxt) i THEN constrains_tac ctxt i;
   1.167  *}
   1.168  
   1.169  setup ProgramDefs.setup