<commit_before>theory Collecting_Examples
imports Collecting
begin

text{* Tweak code generation to work with sets of non-equality types: *}
declare insert_code[code del] union_coset_filter[code del]
lemma insert_code [code]:  "insert x (set xs) = set (x#xs)"
by simp

text{* The example: *}
definition "c = WHILE Less (V ''x'') (N 3)
                DO ''x'' ::= Plus (V ''x'') (N 2)"
definition c0 :: "state set acom" where "c0 = anno {} c"

definition "show_acom xs = map_acom (\<lambda>S. show_state xs ` S)"

text{* Collecting semantics: *}
value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 1) c0)"
value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 2) c0)"
value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 3) c0)"
value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 4) c0)"
value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 5) c0)"
value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 6) c0)"
value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 7) c0)"
value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 8) c0)"

text{* Small-step semantics: *}
value "show_acom [''x''] (((step {}) ^^ 0) (step {\<lambda>x. 0} c0))"
value "show_acom [''x''] (((step {}) ^^ 1) (step {\<lambda>x. 0} c0))"
value "show_acom [''x''] (((step {}) ^^ 2) (step {\<lambda>x. 0} c0))"
value "show_acom [''x''] (((step {}) ^^ 3) (step {\<lambda>x. 0} c0))"
value "show_acom [''x''] (((step {}) ^^ 4) (step {\<lambda>x. 0} c0))"
value "show_acom [''x''] (((step {}) ^^ 5) (step {\<lambda>x. 0} c0))"
value "show_acom [''x''] (((step {}) ^^ 6) (step {\<lambda>x. 0} c0))"
value "show_acom [''x''] (((step {}) ^^ 7) (step {\<lambda>x. 0} c0))"
value "show_acom [''x''] (((step {}) ^^ 8) (step {\<lambda>x. 0} c0))"

<commit_msg>tuned names<commit_after>theory Collecting_Examples
imports Collecting
begin

text{* Tweak code generation to work with sets of non-equality types: *}
declare insert_code[code del] union_coset_filter[code del]
lemma insert_code [code]:  "insert x (set xs) = set (x#xs)"
by simp

text{* The example: *}
definition "c = WHILE Less (V ''x'') (N 3)
                DO ''x'' ::= Plus (V ''x'') (N 2)"
definition C0 :: "state set acom" where "C0 = anno {} c"

definition "show_acom xs = map_acom (\<lambda>S. show_state xs ` S)"

text{* Collecting semantics: *}
value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 1) C0)"
value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 2) C0)"
value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 3) C0)"
value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 4) C0)"
value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 5) C0)"
value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 6) C0)"
value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 7) C0)"
value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 8) C0)"

text{* Small-step semantics: *}
value "show_acom [''x''] (((step {}) ^^ 0) (step {\<lambda>x. 0} C0))"
value "show_acom [''x''] (((step {}) ^^ 1) (step {\<lambda>x. 0} C0))"
value "show_acom [''x''] (((step {}) ^^ 2) (step {\<lambda>x. 0} C0))"
value "show_acom [''x''] (((step {}) ^^ 3) (step {\<lambda>x. 0} C0))"
value "show_acom [''x''] (((step {}) ^^ 4) (step {\<lambda>x. 0} C0))"
value "show_acom [''x''] (((step {}) ^^ 5) (step {\<lambda>x. 0} C0))"
value "show_acom [''x''] (((step {}) ^^ 6) (step {\<lambda>x. 0} C0))"
value "show_acom [''x''] (((step {}) ^^ 7) (step {\<lambda>x. 0} C0))"
value "show_acom [''x''] (((step {}) ^^ 8) (step {\<lambda>x. 0} C0))"


{'fraction_non_alphanumeric': 0.2881257275902212, 'fraction_numerical': 0.0320139697322468, 'mean_word_length': 4.404088050314465, 'pattern_counts': {'":': 0, '<': 39, '<?xml version=': 0, '>': 39, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4210549', 'n_tokens_mistral': 1534, 'n_tokens_neox': 1491, 'n_words': 437}