<commit_before>(*  Title:      HOL/Statespace/state_fun.ML
    Author:     <NAME>, <NAME>
*)

signature STATE_FUN =
sig
  val lookupN : string
  val updateN : string

  val mk_constr : theory -> typ -> term
  val mk_destr : theory -> typ -> term

  val lookup_simproc : simproc
  val update_simproc : simproc
  val ex_lookup_eq_simproc : simproc
  val ex_lookup_ss : simpset
  val lazy_conj_simproc : simproc
  val string_eq_simp_tac : int -> tactic

  val setup : theory -> theory
end;

structure StateFun: STATE_FUN = 
struct

val lookupN = "StateFun.lookup";
val updateN = "StateFun.update";

val sel_name = HOLogic.dest_string;

fun mk_name i t =
  (case try sel_name t of
     SOME name => name
   | NONE => (case t of 
               Free (x,_) => x
              |Const (x,_) => x
              |_ => "x"^string_of_int i))
               
local
val conj1_False = thm "conj1_False";
val conj2_False = thm "conj2_False";
val conj_True = thm "conj_True";
val conj_cong = thm "conj_cong";
fun isFalse (Const ("False",_)) = true
  | isFalse _ = false;
fun isTrue (Const ("True",_)) = true
  | isTrue _ = false;

in
val lazy_conj_simproc =
  Simplifier.simproc @{theory HOL} "lazy_conj_simp" ["P & Q"]
    (fn thy => fn ss => fn t =>
      (case t of (Const ("op &",_)$P$Q) => 
         let
            val P_P' = Simplifier.rewrite ss (cterm_of thy P);
            val P' = P_P' |> prop_of |> Logic.dest_equals |> #2 
         in if isFalse P'
            then SOME (conj1_False OF [P_P'])
            else 
              let
                val Q_Q' = Simplifier.rewrite ss (cterm_of thy Q);
                val Q' = Q_Q' |> prop_of |> Logic.dest_equals |> #2 
              in if isFalse Q'
                 then SOME (conj2_False OF [Q_Q'])
                 else if isTrue P' andalso isTrue Q'
                      then SOME (conj_True OF [P_P', Q_Q'])
                      else if P aconv P' andalso Q aconv Q' then NONE
                           else SOME (conj_cong OF [P_P', Q_Q'])
              end 
         end
        
      | _ => NONE));

val string_eq_simp_tac =
     simp_tac (HOL_basic_ss 
                 addsimps (thms "list.inject"@thms "char.inject"@simp_thms)
                 addsimprocs [Datatype.distinct_simproc,lazy_conj_simproc]
                 addcongs [thm "block_conj_cong"])
end;



local
val rules = 
 [thm "StateFun.lookup_update_id_same",
  thm "StateFun.id_id_cancel",
  thm "StateFun.lookup_update_same",thm "StateFun.lookup_update_other"
  ]
in
val lookup_ss = (HOL_basic_ss 
                 addsimps (thms "list.inject"@thms "char.inject"@simp_thms@rules)
                 addsimprocs [Datatype.distinct_simproc,lazy_conj_simproc]
                 addcongs [thm "block_conj_cong"]
                 addSolver StateSpace.distinctNameSolver) 
end;

val ex_lookup_ss = HOL_ss addsimps [thm "StateFun.ex_id"];

structure StateFunArgs =
struct
  type T = (simpset * simpset * bool); 
           (* lookup simpset, ex_lookup simpset, are simprocs installed *)
  val empty = (empty_ss, empty_ss, false);
  val extend = I;
  fun merge pp ((ss1,ex_ss1,b1),(ss2,ex_ss2,b2)) = 
               (merge_ss (ss1,ss2)
               ,merge_ss (ex_ss1,ex_ss2)
               ,b1 orelse b2);
end;


structure StateFunData = GenericDataFun(StateFunArgs);

val init_state_fun_data =
  Context.theory_map (StateFunData.put (lookup_ss,ex_lookup_ss,false));

val lookup_simproc =
  Simplifier.simproc @{theory} "lookup_simp" ["lookup d n (update d' c m v s)"]
    (fn thy => fn ss => fn t =>
      (case t of (Const ("StateFun.lookup",lT)$destr$n$
                   (s as Const ("StateFun.update",uT)$_$_$_$_$_)) =>
        (let
          val (_::_::_::_::sT::_) = binder_types uT;
          val mi = maxidx_of_term t;
          fun mk_upds (Const ("StateFun.update",uT)$d'$c$m$v$s) =
               let
                 val (_::_::_::fT::_::_) = binder_types uT;
                 val vT = domain_type fT;
                 val (s',cnt) = mk_upds s;
                 val (v',cnt') = 
                      (case v of
                        Const ("StateFun.K_statefun",KT)$v''
                         => (case v'' of 
                             (Const ("StateFun.lookup",_)$(d as (Const ("Fun.id",_)))$n'$_)
                              => if d aconv c andalso n aconv m andalso m aconv n' 
                                 then (v,cnt) (* Keep value so that 
                                                 lookup_update_id_same can fire *)
                                 else (Const ("StateFun.K_statefun",KT)$Var (("v",cnt),vT),
                                       cnt+1)
                              | _ => (Const ("StateFun.K_statefun",KT)$Var (("v",cnt),vT),
                                       cnt+1))
                       | _ => (v,cnt));
               in (Const ("StateFun.update",uT)$d'$c$m$v'$s',cnt')
               end
            | mk_upds s = (Var (("s",mi+1),sT),mi+2);
          
          val ct = cterm_of thy 
                    (Const ("StateFun.lookup",lT)$destr$n$(fst (mk_upds s)));
          val ctxt = Simplifier.the_context ss;
          val basic_ss = #1 (StateFunData.get (Context.Proof ctxt));
          val ss' = Simplifier.context 
                     (Config.map MetaSimplifier.simp_depth_limit (K 100) ctxt) basic_ss;
          val thm = Simplifier.rewrite ss' ct;
        in if (op aconv) (Logic.dest_equals (prop_of thm))
           then NONE
           else SOME thm
        end
        handle Option => NONE)
         
      | _ => NONE ));


fun foldl1 f (x::xs) = foldl f x xs;

local
val update_apply = thm "StateFun.update_apply";
val meta_ext = thm "StateFun.meta_ext";
val o_apply = thm "Fun.o_apply";
val ss' = (HOL_ss addsimps (update_apply::o_apply::thms "list.inject"@thms "char.inject")
                 addsimprocs [Datatype.distinct_simproc,lazy_conj_simproc,StateSpace.distinct_simproc]
                 addcongs [thm "block_conj_cong"]);
in
val update_simproc =
  Simplifier.simproc @{theory} "update_simp" ["update d c n v s"]
    (fn thy => fn ss => fn t =>
      (case t of ((upd as Const ("StateFun.update", uT)) $ d $ c $ n $ v $ s) =>
         let 
            
             val (_::_::_::_::sT::_) = binder_types uT;
                (*"('v => 'a1) => ('a2 => 'v) => 'n => ('a1 => 'a2) => ('n => 'v) => ('n => 'v)"*)
             fun init_seed s = (Bound 0,Bound 0, [("s",sT)],[], false);

             fun mk_comp f fT g gT =
               let val T = (domain_type fT --> range_type gT) 
               in (Const ("Fun.comp",gT --> fT --> T)$g$f,T) end

             fun mk_comps fs = 
                   foldl1 (fn ((f,fT),(g,gT)) => mk_comp f fT g gT) fs;

             fun append n c cT f fT d dT comps =
               (case AList.lookup (op aconv) comps n of<commit_msg>dropped Datatype.distinct_simproc; tuned<commit_after>(*  Title:      HOL/Statespace/state_fun.ML
    Author:     <NAME>, <NAME>
*)

signature STATE_FUN =
sig
  val lookupN : string
  val updateN : string

  val mk_constr : theory -> typ -> term
  val mk_destr : theory -> typ -> term

  val lookup_simproc : simproc
  val update_simproc : simproc
  val ex_lookup_eq_simproc : simproc
  val ex_lookup_ss : simpset
  val lazy_conj_simproc : simproc
  val string_eq_simp_tac : int -> tactic

  val setup : theory -> theory
end;

structure StateFun: STATE_FUN = 
struct

val lookupN = "StateFun.lookup";
val updateN = "StateFun.update";

val sel_name = HOLogic.dest_string;

fun mk_name i t =
  (case try sel_name t of
     SOME name => name
   | NONE => (case t of 
               Free (x,_) => x
              |Const (x,_) => x
              |_ => "x"^string_of_int i))
               
local

val conj1_False = thm "conj1_False";
val conj2_False = thm "conj2_False";
val conj_True = thm "conj_True";
val conj_cong = thm "conj_cong";

fun isFalse (Const ("False",_)) = true
  | isFalse _ = false;
fun isTrue (Const ("True",_)) = true
  | isTrue _ = false;

in

val lazy_conj_simproc =
  Simplifier.simproc @{theory HOL} "lazy_conj_simp" ["P & Q"]
    (fn thy => fn ss => fn t =>
      (case t of (Const ("op &",_)$P$Q) => 
         let
            val P_P' = Simplifier.rewrite ss (cterm_of thy P);
            val P' = P_P' |> prop_of |> Logic.dest_equals |> #2 
         in if isFalse P'
            then SOME (conj1_False OF [P_P'])
            else 
              let
                val Q_Q' = Simplifier.rewrite ss (cterm_of thy Q);
                val Q' = Q_Q' |> prop_of |> Logic.dest_equals |> #2 
              in if isFalse Q'
                 then SOME (conj2_False OF [Q_Q'])
                 else if isTrue P' andalso isTrue Q'
                      then SOME (conj_True OF [P_P', Q_Q'])
                      else if P aconv P' andalso Q aconv Q' then NONE
                           else SOME (conj_cong OF [P_P', Q_Q'])
              end 
         end
        
      | _ => NONE));

val string_eq_simp_tac = simp_tac (HOL_basic_ss 
  addsimps (@{thms list.inject} @ @{thms char.inject}
    @ @{thms list.distinct} @ @{thms char.distinct} @ simp_thms)
  addsimprocs [lazy_conj_simproc]
  addcongs [@{thm block_conj_cong}])

end;

val lookup_ss = (HOL_basic_ss 
  addsimps (@{thms list.inject} @ @{thms char.inject}
    @ @{thms list.distinct} @ @{thms char.distinct} @ simp_thms
    @ [@{thm StateFun.lookup_update_id_same}, @{thm StateFun.id_id_cancel},
      @{thm StateFun.lookup_update_same}, @{thm StateFun.lookup_update_other}])
  addsimprocs [lazy_conj_simproc]
  addcongs @{thms block_conj_cong}
  addSolver StateSpace.distinctNameSolver);

val ex_lookup_ss = HOL_ss addsimps @{thms StateFun.ex_id};

structure StateFunArgs =
struct
  type T = (simpset * simpset * bool); 
           (* lookup simpset, ex_lookup simpset, are simprocs installed *)
  val empty = (empty_ss, empty_ss, false);
  val extend = I;
  fun merge pp ((ss1,ex_ss1,b1),(ss2,ex_ss2,b2)) = 
               (merge_ss (ss1,ss2)
               ,merge_ss (ex_ss1,ex_ss2)
               ,b1 orelse b2);
end;


structure StateFunData = GenericDataFun(StateFunArgs);

val init_state_fun_data =
  Context.theory_map (StateFunData.put (lookup_ss,ex_lookup_ss,false));

val lookup_simproc =
  Simplifier.simproc @{theory} "lookup_simp" ["lookup d n (update d' c m v s)"]
    (fn thy => fn ss => fn t =>
      (case t of (Const ("StateFun.lookup",lT)$destr$n$
                   (s as Const ("StateFun.update",uT)$_$_$_$_$_)) =>
        (let
          val (_::_::_::_::sT::_) = binder_types uT;
          val mi = maxidx_of_term t;
          fun mk_upds (Const ("StateFun.update",uT)$d'$c$m$v$s) =
               let
                 val (_::_::_::fT::_::_) = binder_types uT;
                 val vT = domain_type fT;
                 val (s',cnt) = mk_upds s;
                 val (v',cnt') = 
                      (case v of
                        Const ("StateFun.K_statefun",KT)$v''
                         => (case v'' of 
                             (Const ("StateFun.lookup",_)$(d as (Const ("Fun.id",_)))$n'$_)
                              => if d aconv c andalso n aconv m andalso m aconv n' 
                                 then (v,cnt) (* Keep value so that 
                                                 lookup_update_id_same can fire *)
                                 else (Const ("StateFun.K_statefun",KT)$Var (("v",cnt),vT),
                                       cnt+1)
                              | _ => (Const ("StateFun.K_statefun",KT)$Var (("v",cnt),vT),
                                       cnt+1))
                       | _ => (v,cnt));
               in (Const ("StateFun.update",uT)$d'$c$m$v'$s',cnt')
               end
            | mk_upds s = (Var (("s",mi+1),sT),mi+2);
          
          val ct = cterm_of thy 
                    (Const ("StateFun.lookup",lT)$destr$n$(fst (mk_upds s)));
          val ctxt = Simplifier.the_context ss;
          val basic_ss = #1 (StateFunData.get (Context.Proof ctxt));
          val ss' = Simplifier.context 
                     (Config.map MetaSimplifier.simp_depth_limit (K 100) ctxt) basic_ss;
          val thm = Simplifier.rewrite ss' ct;
        in if (op aconv) (Logic.dest_equals (prop_of thm))
           then NONE
           else SOME thm
        end
        handle Option => NONE)
         
      | _ => NONE ));


fun foldl1 f (x::xs) = foldl f x xs;

local
val meta_ext = @{thm StateFun.meta_ext};
val ss' = (HOL_ss addsimps
  (@{thm StateFun.update_apply} :: @{thm Fun.o_apply} :: @{thms list.inject} @ @{thms char.inject}
    @ @{thms list.distinct} @ @{thms char.distinct})
  addsimprocs [lazy_conj_simproc, StateSpace.distinct_simproc]
  addcongs @{thms block_conj_cong});
in
val update_simproc =
  Simplifier.simproc @{theory} "update_simp" ["update d c n v s"]
    (fn thy => fn ss => fn t =>
      (case t of ((upd as Const ("StateFun.update", uT)) $ d $ c $ n $ v $ s) =>
         let 
            
             val (_::_::_::_::sT::_) = binder_types uT;
                (*"('v => 'a1) => ('a2 => 'v) => 'n => ('a1 => 'a2) => ('n => 'v) => ('n => 'v)"*)
             fun init_seed s = (Bound 0,Bound 0, [("s",sT)],[], false);

             fun mk_comp f fT g gT =
               let val T = (domain_type fT --> range_type gT) 
               in (Const ("Fun.comp",gT --> fT --> T)$g$f,T) end

             fun mk_comps fs = 
                   foldl1 (fn ((f,fT),(g,gT)) => mk_comp f fT g gT) fs;

             fun append n c cT f fT d dT comps =
               (case AList.lookup (op aconv) comps n of
{'fraction_non_alphanumeric': 0.12991833704528583, 'fraction_numerical': 0.005345211581291759, 'mean_word_length': 1.8698338304218152, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 107, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 18, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2739842', 'n_tokens_mistral': 4803, 'n_tokens_neox': 4671, 'n_words': 1213}