<commit_before>(*  Title:      HOL/UNITY/UNITY_tactics.ML
    ID:         $Id$
    Author:     <NAME>, Cambridge University Computer Laboratory
    Copyright   2003  University of Cambridge

Specialized UNITY tactics.
*)

(*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
val Always_Int_tac = dtac @{thm Always_Int_I} THEN' assume_tac THEN' etac @{thm Always_thin}

(*Combines a list of invariance THEOREMS into one.*)
val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I})

(*Proves "co" properties when the program is specified.  Any use of invariants
  (from weak constrains) must have been done already.*)
fun constrains_tac(cs,ss) i =
   SELECT_GOAL
      (EVERY [REPEAT (Always_Int_tac 1),
              (*reduce the fancy safety properties to "constrains"*)
              REPEAT (etac @{thm Always_ConstrainsI} 1
                      ORELSE
                      resolve_tac [@{thm StableI}, @{thm stableI},
                                   @{thm constrains_imp_Constrains}] 1),
              (*for safety, the totalize operator can be ignored*)
              simp_tac (HOL_ss addsimps
                         [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1,
              rtac @{thm constrainsI} 1,
              full_simp_tac ss 1,
              REPEAT (FIRSTGOAL (etac disjE)),
              ALLGOALS (clarify_tac cs),
              ALLGOALS (asm_lr_simp_tac ss)]) i;

(*proves "ensures/leadsTo" properties when the program is specified*)
fun ensures_tac(cs,ss) sact =
    SELECT_GOAL
      (EVERY [REPEAT (Always_Int_tac 1),
              etac @{thm Always_LeadsTo_Basis} 1
                  ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
                  REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
                                    @{thm EnsuresI}, @{thm ensuresI}] 1),
              (*now there are two subgoals: co & transient*)
              simp_tac (ss addsimps [@{thm mk_total_program_def}]) 2,
              res_inst_tac (Simplifier.the_context ss)
                [(("act", 0), sact)] @{thm totalize_transientI} 2
              ORELSE res_inst_tac (Simplifier.the_context ss)
                [(("act", 0), sact)] @{thm transientI} 2,
                 (*simplify the command's domain*)
              simp_tac (ss addsimps [@{thm Domain_def}]) 3,
              constrains_tac (cs,ss) 1,
              ALLGOALS (clarify_tac cs),
              ALLGOALS (asm_lr_simp_tac ss)]);


(*Composition equivalences, from Lift_prog*)

fun make_o_equivs th =
    [th,
     th RS @{thm o_equiv_assoc} |> simplify (HOL_ss addsimps [@{thm o_assoc}]),
     th RS @{thm o_equiv_apply} |> simplify (HOL_ss addsimps [@{thm o_def}, @{thm sub_def}])];

Addsimps (make_o_equivs @{thm fst_o_funPair} @ make_o_equivs @{thm snd_o_funPair});

Addsimps (make_o_equivs @{thm fst_o_lift_map} @ make_o_equivs @{thm snd_o_lift_map});<commit_msg>eliminated old Addsimps;<commit_after>(*  Title:      HOL/UNITY/UNITY_tactics.ML
    ID:         $Id$
    Author:     <NAME>, Cambridge University Computer Laboratory
    Copyright   2003  University of Cambridge

Specialized UNITY tactics.
*)

(*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
val Always_Int_tac = dtac @{thm Always_Int_I} THEN' assume_tac THEN' etac @{thm Always_thin}

(*Combines a list of invariance THEOREMS into one.*)
val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I})

(*Proves "co" properties when the program is specified.  Any use of invariants
  (from weak constrains) must have been done already.*)
fun constrains_tac(cs,ss) i =
   SELECT_GOAL
      (EVERY [REPEAT (Always_Int_tac 1),
              (*reduce the fancy safety properties to "constrains"*)
              REPEAT (etac @{thm Always_ConstrainsI} 1
                      ORELSE
                      resolve_tac [@{thm StableI}, @{thm stableI},
                                   @{thm constrains_imp_Constrains}] 1),
              (*for safety, the totalize operator can be ignored*)
              simp_tac (HOL_ss addsimps
                         [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1,
              rtac @{thm constrainsI} 1,
              full_simp_tac ss 1,
              REPEAT (FIRSTGOAL (etac disjE)),
              ALLGOALS (clarify_tac cs),
              ALLGOALS (asm_lr_simp_tac ss)]) i;

(*proves "ensures/leadsTo" properties when the program is specified*)
fun ensures_tac(cs,ss) sact =
    SELECT_GOAL
      (EVERY [REPEAT (Always_Int_tac 1),
              etac @{thm Always_LeadsTo_Basis} 1
                  ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
                  REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
                                    @{thm EnsuresI}, @{thm ensuresI}] 1),
              (*now there are two subgoals: co & transient*)
              simp_tac (ss addsimps [@{thm mk_total_program_def}]) 2,
              res_inst_tac (Simplifier.the_context ss)
                [(("act", 0), sact)] @{thm totalize_transientI} 2
              ORELSE res_inst_tac (Simplifier.the_context ss)
                [(("act", 0), sact)] @{thm transientI} 2,
                 (*simplify the command's domain*)
              simp_tac (ss addsimps [@{thm Domain_def}]) 3,
              constrains_tac (cs,ss) 1,
              ALLGOALS (clarify_tac cs),
              ALLGOALS (asm_lr_simp_tac ss)]);


(*Composition equivalences, from Lift_prog*)

fun make_o_equivs th =
    [th,
     th RS @{thm o_equiv_assoc} |> simplify (HOL_ss addsimps [@{thm o_assoc}]),
     th RS @{thm o_equiv_apply} |> simplify (HOL_ss addsimps [@{thm o_def}, @{thm sub_def}])];

Simplifier.change_simpset (fn ss => ss
  addsimps (make_o_equivs @{thm fst_o_funPair} @ make_o_equivs @{thm snd_o_funPair})
  addsimps (make_o_equivs @{thm fst_o_lift_map} @ make_o_equivs @{thm snd_o_lift_map}));
{'fraction_non_alphanumeric': 0.10523640061006609, 'fraction_numerical': 0.00847314014573801, 'mean_word_length': 2.447429906542056, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 12, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 4, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5300372', 'n_tokens_mistral': 2127, 'n_tokens_neox': 1987, 'n_words': 543}