<commit_before>(*  Title:      HOL/Subst/subst.ML
    ID:         $Id$
    Author:     <NAME>, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge

For subst.thy.  
*)

open Subst;

(***********)

val subst_defs = [subst_def,comp_def,sdom_def];

val raw_subst_ss = simpset_of "UTLemmas" addsimps al_rews;

local fun mk_thm s = prove_goalw Subst.thy subst_defs s 
                                 (fn _ => [simp_tac raw_subst_ss 1])
in val subst_rews = map mk_thm 
["Const(c) <| al = Const(c)",
 "Comb t u <| al = Comb (t <| al) (u <| al)",
 "[] <> bl = bl",
 "((a,b)#al) <> bl = (a,b <| bl) # (al <> bl)",
 "sdom([]) = {}",
 "sdom((a,b)#al) = (if Var(a)=b then (sdom al) Int Compl({a}) \
\                               else (sdom al) Un {a})"
];
   (* This rewrite isn't always desired *)
   val Var_subst = mk_thm "Var(x) <| al = assoc x (Var x) al";
end;

val subst_ss = raw_subst_ss addsimps subst_rews;
<commit_msg>Simpset removes the de Morgan laws<commit_after>(*  Title:      HOL/Subst/subst.ML
    ID:         $Id$
    Author:     <NAME>, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge

For subst.thy.  
*)

open Subst;

(***********)

val subst_defs = [subst_def,comp_def,sdom_def];

val raw_subst_ss = simpset_of "UTLemmas" addsimps al_rews;

local fun mk_thm s = prove_goalw Subst.thy subst_defs s 
                                 (fn _ => [simp_tac raw_subst_ss 1])
in val subst_rews = map mk_thm 
["Const(c) <| al = Const(c)",
 "Comb t u <| al = Comb (t <| al) (u <| al)",
 "[] <> bl = bl",
 "((a,b)#al) <> bl = (a,b <| bl) # (al <> bl)",
 "sdom([]) = {}",
 "sdom((a,b)#al) = (if Var(a)=b then (sdom al) Int Compl({a}) \
\                               else (sdom al) Un {a})"
];
   (* This rewrite isn't always desired *)
   val Var_subst = mk_thm "Var(x) <| al = assoc x (Var x) al";
end;

val subst_ss = raw_subst_ss addsimps subst_rews 
                            delsimps [de_Morgan_conj, de_Morgan_disj];

{'fraction_non_alphanumeric': 0.16633366633366634, 'fraction_numerical': 0.004995004995004995, 'mean_word_length': 2.5767857142857142, 'pattern_counts': {'":': 0, '<': 23, '<?xml version=': 0, '>': 13, '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': '1035674', 'n_tokens_mistral': 806, 'n_tokens_neox': 789, 'n_words': 210}