# HG changeset patch # Parent efd58f8b16591ddd7c201bb7473cf1ba14946723 proper datatype for 8-bit characters diff -r efd58f8b1659 thys/Affine_Arithmetic/Print.thy --- a/thys/Affine_Arithmetic/Print.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/Affine_Arithmetic/Print.thy Tue Apr 24 11:35:45 2018 +0200 @@ -5,7 +5,6 @@ Affine_Code Show.Show_Instances "HOL-Library.Monad_Syntax" - "HOL-Library.Code_Char" Optimize_Float begin diff -r efd58f8b1659 thys/CAVA_Automata/CAVA_Base/Code_String.thy --- a/thys/CAVA_Automata/CAVA_Base/Code_String.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/CAVA_Automata/CAVA_Base/Code_String.thy Tue Apr 24 11:35:45 2018 +0200 @@ -6,41 +6,6 @@ imports (*"HOL-Library.List_lexord"*) Collections.Refine_Dflt - "HOL-Library.Code_Char" begin -(* TODO: Move to Collections *) -instantiation String.literal :: hashable -begin - definition hashcode_literal :: "String.literal \ uint32" - where "hashcode_literal s = hashcode (String.explode s)" - - definition def_hashmap_size_literal - :: "String.literal itself \ nat" where - "def_hashmap_size_literal _ = 10" - - instance proof - qed (simp_all only: def_hashmap_size_literal_def) end - -(* Append on literal strings -- allows for easier written exceptions *) - -context - includes literal.lifting -begin - -lift_definition literal_append - :: "String.literal \ String.literal \ String.literal" (infixr "@@" 65) - is "(@)" . - -end - -lifting_update literal.lifting -lifting_forget literal.lifting - -code_printing - constant literal_append \ - (SML) infixr 5 "^" - and (Haskell) infixr 5 "++" - and (OCaml) infixr 5 "^" -end diff -r efd58f8b1659 thys/CAVA_LTL_Modelchecker/BoolProgs/BoolProgs_LTL_Conv.thy --- a/thys/CAVA_LTL_Modelchecker/BoolProgs/BoolProgs_LTL_Conv.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/CAVA_LTL_Modelchecker/BoolProgs/BoolProgs_LTL_Conv.thy Tue Apr 24 11:35:45 2018 +0200 @@ -22,10 +22,10 @@ | "ltl_conv _ _ False_ltlc = Inl False_ltlc" | "ltl_conv C _ (Prop_ltlc (CProp s)) = (case Mapping.lookup C s of Some c \ Inl (b2l c) - | None \ Inr (STR ''Unknown constant: '' @@ s))" + | None \ Inr (STR ''Unknown constant: '' + s))" | "ltl_conv _ M (Prop_ltlc (FProp (s, argm))) = (case Mapping.lookup M s of Some f \ (Inl \ b2l \ f \ nat_of_integer) argm - | None \ Inr (STR ''Unknown function: '' @@ s))" + | None \ Inr (STR ''Unknown function: '' + s))" | "ltl_conv C M (Not_ltlc x) = (case ltl_conv C M x of Inl l \ Inl (Not_ltlc l) | Inr s \ Inr s)" | "ltl_conv C M (Next_ltlc x) = (case ltl_conv C M x of Inl l \ Inl (Next_ltlc l) | Inr s \ Inr s)" | "ltl_conv C M (Final_ltlc x) = (case ltl_conv C M x of Inl l \ Inl (Final_ltlc l) | Inr s \ Inr s)" diff -r efd58f8b1659 thys/CAVA_LTL_Modelchecker/BoolProgs/Programs/BoolProgs_Programs.thy --- a/thys/CAVA_LTL_Modelchecker/BoolProgs/Programs/BoolProgs_Programs.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/CAVA_LTL_Modelchecker/BoolProgs/Programs/BoolProgs_Programs.thy Tue Apr 24 11:35:45 2018 +0200 @@ -26,7 +26,7 @@ where "chose_prog P n = (case Mapping.lookup progs P of Some (descr, ndescr, p) \ (descr, ndescr, p n) | None \ let (descr, ndescr, p) = the (Mapping.lookup progs default_prog) - in (descr@@(STR '' (fallback)''), ndescr, p n))" + in (descr + STR '' (fallback)'', ndescr, p n))" definition list_progs :: "(String.literal \ String.literal \ String.literal) list" where "list_progs \ let keys = keys_of_map progs in diff -r efd58f8b1659 thys/CAVA_LTL_Modelchecker/CAVA_Impl.thy --- a/thys/CAVA_LTL_Modelchecker/CAVA_Impl.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/CAVA_LTL_Modelchecker/CAVA_Impl.thy Tue Apr 24 11:35:45 2018 +0200 @@ -876,6 +876,7 @@ nat_of_integer int_of_integer integer_of_nat integer_of_int in SML + module_name CAVA file "code/CAVA_Export.sml" end diff -r efd58f8b1659 thys/CakeML/generated/CakeML/PrimTypes.thy --- a/thys/CakeML/generated/CakeML/PrimTypes.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/CakeML/generated/CakeML/PrimTypes.thy Tue Apr 24 11:35:45 2018 +0200 @@ -30,8 +30,8 @@ Tdec (Dexn undefined (''Div'') []), Tdec (Dexn undefined (''Subscript'') []), Tdec (Dtype undefined [([], (''bool''), [((''false''), []), ((''true''), [])])]), - Tdec (Dtype undefined [([([(char_of_nat 39), (CHR ''a'')])], (''list''), [((''nil''), []), ((''::''), [Tvar ([(char_of_nat 39), (CHR ''a'')]), Tapp [Tvar ([(char_of_nat 39), (CHR ''a'')])] (TC_name (Short (''list'')))]) ])]), - Tdec (Dtype undefined [([([(char_of_nat 39), (CHR ''a'')])], (''option''), [((''NONE''), []),((''SOME''), [Tvar ([(char_of_nat 39), (CHR ''a'')])]) ])]) ])" + Tdec (Dtype undefined [([([CHR 0x27, CHR ''a''])], (''list''), [((''nil''), []), ((''::''), [Tvar ([CHR 0x27, CHR ''a'']), Tapp [Tvar ([CHR 0x27, CHR ''a''])] (TC_name (Short (''list'')))]) ])]), + Tdec (Dtype undefined [([([CHR 0x27, CHR ''a''])], (''option''), [((''NONE''), []),((''SOME''), [Tvar ([CHR 0x27, CHR ''a''])]) ])]) ])" (*val add_to_sem_env : diff -r efd58f8b1659 thys/CakeML/generated/CakeML/SemanticPrimitives.thy --- a/thys/CakeML/generated/CakeML/SemanticPrimitives.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/CakeML/generated/CakeML/SemanticPrimitives.thy Tue Apr 24 11:35:45 2018 +0200 @@ -452,12 +452,12 @@ (*val ws_to_chars : list word8 -> list char*) definition ws_to_chars :: "(8 word)list \(char)list " where - " ws_to_chars ws = ( List.map (\ w . char_of_nat(unat w)) ws )" + " ws_to_chars ws = ( List.map (\ w . char_of (unat w)) ws )" (*val chars_to_ws : list char -> list word8*) definition chars_to_ws :: "(char)list \(8 word)list " where - " chars_to_ws cs = ( List.map (\ c2 . word_of_int(int(nat_of_char c2))) cs )" + " chars_to_ws cs = ( List.map (\ c2 . word_of_int(of_char c2)) cs )" (*val opn_lookup : opn -> integer -> integer -> integer*) @@ -663,15 +663,15 @@ | _ => None ) | (Ord, [Litv (Char c2)]) => - Some ((s,t1), Rval (Litv(IntLit(int(nat_of_char c2))))) + Some ((s,t1), Rval (Litv(IntLit(of_char c2)))) | (Chr, [Litv (IntLit i)]) => Some ((s,t1), (if (i <( 0 :: int)) \ (i >( 255 :: int)) then Rerr (Rraise (prim_exn (''Chr''))) else - Rval (Litv(Char(char_of_nat(nat (abs ( i)))))))) + Rval (Litv(Char(char_of(nat (abs ( i)))))))) | (Chopb op1, [Litv (Char c1), Litv (Char c2)]) => - Some ((s,t1), Rval (Boolv (opb_lookup op1 (int(nat_of_char c1)) (int(nat_of_char c2))))) + Some ((s,t1), Rval (Boolv (opb_lookup op1 (of_char c1) (of_char c2)))) | (Implode, [v2]) => (case v_to_char_list v2 of Some ls => @@ -767,7 +767,7 @@ | (FFI n, [Litv(StrLit conf), Loc lnum]) => (case store_lookup lnum s of Some (W8array ws) => - (case call_FFI t1 n (List.map (\ c2 . of_nat(nat_of_char c2)) ( conf)) ws of + (case call_FFI t1 n (List.map (\ c2 . of_char c2) ( conf)) ws of (t', ws') => (case store_assign lnum (W8array ws') s of Some s' => Some ((s', t'), Rval (Conv None [])) diff -r efd58f8b1659 thys/CakeML/generated/LemExtraDefs.thy --- a/thys/CakeML/generated/LemExtraDefs.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/CakeML/generated/LemExtraDefs.thy Tue Apr 24 11:35:45 2018 +0200 @@ -850,16 +850,12 @@ subsection \Strings\ -lemma explode_str_simp [simp] : - "String.explode (STR l) = l" -by (metis STR_inverse UNIV_I) - declare String.literal.explode_inverse [simp] subsection \num to string conversions\ definition nat_list_to_string :: "nat list \ string" where - "nat_list_to_string nl = map char_of_nat nl" + "nat_list_to_string nl = map char_of nl" definition is_digit where "is_digit (n::nat) = (n < 10)" diff -r efd58f8b1659 thys/CakeML/generated/Lem_show.thy --- a/thys/CakeML/generated/Lem_show.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/CakeML/generated/Lem_show.thy Tue Apr 24 11:35:45 2018 +0200 @@ -26,7 +26,7 @@ definition instance_Show_Show_string_dict :: "(string)Show_class " where " instance_Show_Show_string_dict = ((| - show_method = (\ s. ([(char_of_nat 34)]) @ (s @ ([(char_of_nat 34)])))|) )" + show_method = (\ s. ([(char_of (34 :: nat))]) @ (s @ ([(char_of (34 :: nat))])))|) )" (*val stringFromMaybe : forall 'a. ('a -> string) -> maybe 'a -> string*) diff -r efd58f8b1659 thys/CakeML/generated/Lem_string_extra.thy --- a/thys/CakeML/generated/Lem_string_extra.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/CakeML/generated/Lem_string_extra.thy Tue Apr 24 11:35:45 2018 +0200 @@ -43,7 +43,7 @@ if n =( 0 :: nat) then acc1 else - stringFromNatHelper (n div( 10 :: nat)) (char_of_nat ((n mod( 10 :: nat)) +( 48 :: nat)) # acc1))" + stringFromNatHelper (n div( 10 :: nat)) (char_of ((n mod( 10 :: nat)) +( 48 :: nat)) # acc1))" by pat_completeness auto @@ -59,7 +59,7 @@ if n =( 0 :: nat) then acc1 else - stringFromNaturalHelper (n div( 10 :: nat)) (char_of_nat ( ((n mod( 10 :: nat)) +( 48 :: nat))) # acc1))" + stringFromNaturalHelper (n div( 10 :: nat)) (char_of ( ((n mod( 10 :: nat)) +( 48 :: nat))) # acc1))" by pat_completeness auto diff -r efd58f8b1659 thys/Collections/Lib/HashCode.thy --- a/thys/Collections/Lib/HashCode.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/Collections/Lib/HashCode.thy Tue Apr 24 11:35:45 2018 +0200 @@ -84,7 +84,7 @@ instantiation char :: hashable begin - definition [simp]: "hashcode (c :: char) == uint32_of_int (int (nat_of_char c))" + definition [simp]: "hashcode (c :: char) == uint32_of_int (of_char c)" definition "def_hashmap_size = (\_ :: char itself. 32)" instance by(intro_classes)(simp_all add: def_hashmap_size_char_def) end @@ -145,6 +145,21 @@ apply (simp_all add: algebra_simps mod_add_right_eq) *) +instantiation String.literal :: hashable +begin + +definition hashcode_literal :: "String.literal \ uint32" + where "hashcode_literal s = hashcode (String.explode s)" + +definition def_hashmap_size_literal :: "String.literal itself \ nat" + where "def_hashmap_size_literal _ = 10" + +instance + by standard (simp_all only: def_hashmap_size_literal_def) + +end + + hide_type (open) word end diff -r efd58f8b1659 thys/ConcurrentGC/Tactics.thy --- a/thys/ConcurrentGC/Tactics.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/ConcurrentGC/Tactics.thy Tue Apr 24 11:35:45 2018 +0200 @@ -193,7 +193,7 @@ lemmas loc_simps = bex_simps append.simps list.simps rev.simps (* evaluate string equality *) - Char_eq_Char_iff cong_exp_iff_simps (* evaluate character equality *) + char.inject cong_exp_iff_simps (* evaluate character equality *) prefix_code suffix_to_prefix mem_Collect_eq Un_iff UNION_eq Compl_iff insertI1 insertI2 singleton_iff Diff_iff UNIV_I if_True if_False diff -r efd58f8b1659 thys/Containers/Collection_Order.thy --- a/thys/Containers/Collection_Order.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/Containers/Collection_Order.thy Tue Apr 24 11:35:45 2018 +0200 @@ -311,11 +311,9 @@ instance by(intro_classes)(simp add: infinite_UNIV_listI) end -lemma UNIV_literal_eq_range_STR: "UNIV = range STR" -by(auto intro: explode_inverse[symmetric]) - -lemma infinite_UNIV_literal: "\ finite (UNIV :: String.literal set)" -by(auto simp add: UNIV_literal_eq_range_STR infinite_UNIV_listI dest!: finite_imageD intro: inj_onI) +lemma infinite_UNIV_literal: + "infinite (UNIV :: String.literal set)" + by (fact infinite_literal) instantiation String.literal :: cproper_interval begin definition cproper_interval_literal :: "String.literal proper_interval" diff -r efd58f8b1659 thys/Containers/Set_Linorder.thy --- a/thys/Containers/Set_Linorder.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/Containers/Set_Linorder.thy Tue Apr 24 11:35:45 2018 +0200 @@ -2150,32 +2150,42 @@ "proper_interval (Some x) (Some y) \ y - x > 1" by(transfer, simp)+ -lemma char_less_iff_nat_of_char: "x < y \ nat_of_char x < nat_of_char y" +lemma char_less_iff_nat_of_char: "x < y \ of_char x < (of_char y :: nat)" by (fact less_char_def) -lemma nat_of_char_inject [simp]: "nat_of_char x = nat_of_char y \ x = y" - by (fact nat_of_char_eq_iff) +lemma nat_of_char_inject [simp]: "of_char x = (of_char y :: nat) \ x = y" + by (fact of_char_eq_iff) -lemma char_le_iff_nat_of_char: "x \ y \ nat_of_char x \ nat_of_char y" +lemma char_le_iff_nat_of_char: "x \ y \ of_char x \ (of_char y :: nat)" by (fact less_eq_char_def) -instantiation char :: proper_interval begin +instantiation char :: proper_interval +begin + fun proper_interval_char :: "char proper_interval" where "proper_interval_char None None \ True" -| "proper_interval_char None (Some x) \ x \ 0" +| "proper_interval_char None (Some x) \ x \ CHR 0x00" | "proper_interval_char (Some x) None \ x \ CHR 0xFF" -| "proper_interval_char (Some x) (Some y) \ nat_of_char y - nat_of_char x > 1" -instance -proof intro_classes +| "proper_interval_char (Some x) (Some y) \ of_char y - of_char x > (1 :: nat)" + +instance proof fix y :: char - { assume "y \ 0" - hence "0 < y" - by (simp add: char_less_iff_nat_of_char nat_of_char_eq_iff [symmetric]) } + { assume "y \ CHR 0x00" + have "CHR 0x00 < y" + proof (rule ccontr) + assume "\ CHR 0x00 < y" + then have "of_char y = (of_char CHR 0x00 :: nat)" + by (simp add: not_less char_le_iff_nat_of_char) + then have "y = CHR 0x00" + using nat_of_char_inject [of y "CHR 0x00"] by simp + with \y \ CHR 0x00\ show False + by simp + qed } moreover { fix z :: char - assume "z < 0" + assume "z < CHR 0x00" hence False - by (simp add: char_less_iff_nat_of_char nat_of_char_eq_iff [symmetric]) } + by (simp add: char_less_iff_nat_of_char of_char_eq_iff [symmetric]) } ultimately show "proper_interval None (Some y) = (\z. z < y)" by auto @@ -2193,19 +2203,22 @@ (insert nat_of_char_less_256 [of z], simp) } ultimately show "proper_interval (Some x) None = (\z. x < z)" by auto - { assume gt: "nat_of_char y - nat_of_char x > 1" - let ?z = "char_of_nat (nat_of_char x + 1)" - from gt nat_of_char_less_256[of y] - have 255: "nat_of_char x < 255" by arith + { assume gt: "of_char y - of_char x > (1 :: nat)" + let ?z = "char_of (of_char x + (1 :: nat))" + from gt nat_of_char_less_256 [of y] + have 255: "of_char x < (255 :: nat)" by arith with gt have "x < ?z" "?z < y" by (simp_all add: char_less_iff_nat_of_char) hence "\z. x < z \ z < y" by blast } moreover { fix z assume "x < z" "z < y" - hence "1 < nat_of_char y - nat_of_char x" by(simp add: char_less_iff_nat_of_char) } - ultimately show "proper_interval (Some x) (Some y) = (\z>x. z < y)" by auto + hence "(1 :: nat) < of_char y - of_char x" + by (simp add: char_less_iff_nat_of_char) } + ultimately show "proper_interval (Some x) (Some y) = (\z>x. z < y)" + by auto qed simp + end instantiation Enum.finite_1 :: proper_interval begin diff -r efd58f8b1659 thys/FOL_Harrison/FOL_Harrison.thy --- a/thys/FOL_Harrison/FOL_Harrison.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/FOL_Harrison/FOL_Harrison.thy Tue Apr 24 11:35:45 2018 +0200 @@ -11,7 +11,7 @@ theory FOL_Harrison imports - "HOL-Library.Code_Char" + Main begin section \Module Proven\ diff -r efd58f8b1659 thys/Formal_SSA/Disjoin_Transform.thy --- a/thys/Formal_SSA/Disjoin_Transform.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/Formal_SSA/Disjoin_Transform.thy Tue Apr 24 11:35:45 2018 +0200 @@ -43,7 +43,7 @@ by (induction c) (auto intro:newname.intros dest:maxVnameLen_aux_newname) lemma tempname_newname[intro]: "newname c (tempName c)" -by (rule maxVnameLen_newname) (auto simp:tempName_def String.literal.STR_inverse implode_def) + by (rule maxVnameLen_newname) (simp add: tempName_def) fun transform_aux :: "vname \ cmd \ cmd" where "transform_aux _ Skip = Skip" diff -r efd58f8b1659 thys/Formula_Derivatives/WS1S_Nameful.thy --- a/thys/Formula_Derivatives/WS1S_Nameful.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/Formula_Derivatives/WS1S_Nameful.thy Tue Apr 24 11:35:45 2018 +0200 @@ -6,8 +6,8 @@ begin (*>*) -declare nat_of_char_Char[simp] - [[coercion nat_of_char, coercion_enabled]] +declare [[coercion "of_char :: char \ nat", coercion_enabled]] + definition is_upper :: "char \ bool" where [simp]: "is_upper c = (c \ {65..90 :: nat})" definition is_lower :: "char \ bool" where [simp]: "is_lower c = (c \ {97..122 :: nat})" diff -r efd58f8b1659 thys/HereditarilyFinite/Finitary.thy --- a/thys/HereditarilyFinite/Finitary.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/HereditarilyFinite/Finitary.thy Tue Apr 24 11:35:45 2018 +0200 @@ -43,9 +43,9 @@ instantiation char :: finitary begin definition hf_of_char_def: - "hf_of x \ hf_of (nat_of_char x)" + "hf_of x \ hf_of (of_char x :: nat)" instance - by intro_classes (auto simp: inj_on_def hf_of_char_def nat_of_char_eq_iff) + by standard (auto simp: inj_on_def hf_of_char_def) end instantiation prod :: (finitary,finitary) finitary diff -r efd58f8b1659 thys/IP_Addresses/Lib_Numbers_toString.thy --- a/thys/IP_Addresses/Lib_Numbers_toString.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/IP_Addresses/Lib_Numbers_toString.thy Tue Apr 24 11:35:45 2018 +0200 @@ -6,8 +6,8 @@ (*http://stackoverflow.com/questions/23864965/string-of-nat-in-isabelle*) fun string_of_nat :: "nat \ string" where - "string_of_nat n = (if n < 10 then [char_of_nat (48 + n)] else - string_of_nat (n div 10) @ [char_of_nat (48 + (n mod 10))])" + "string_of_nat n = (if n < 10 then [char_of (48 + n)] else + string_of_nat (n div 10) @ [char_of (48 + (n mod 10))])" definition string_of_int :: "int \ string" where "string_of_int i = (if i < 0 then ''-'' @ string_of_nat (nat (- i)) else string_of_nat (nat i))" diff -r efd58f8b1659 thys/IP_Addresses/Lib_Word_toString.thy --- a/thys/IP_Addresses/Lib_Word_toString.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/IP_Addresses/Lib_Word_toString.thy Tue Apr 24 11:35:45 2018 +0200 @@ -14,11 +14,11 @@ (if w < 10 then - [char_of_nat (48 + unat w)] + [char_of (48 + unat w)] else if w < 36 then - [char_of_nat ((if lc then 87 else 55) + unat w)] + [char_of ((if lc then 87 else 55) + unat w)] else undefined)" @@ -86,7 +86,7 @@ lemma "dec_string_of_word0 (-1::8 word) = ''255''" by eval lemma string_of_word_single_atoi: - "n < 10 \ string_of_word_single True n = [char_of_nat (48 + unat n)]" + "n < 10 \ string_of_word_single True n = [char_of (48 + unat n)]" by(simp add: string_of_word_single_def) (*TODO: move!*) diff -r efd58f8b1659 thys/Iptables_Semantics/Primitive_Matchers/Code_Interface.thy --- a/thys/Iptables_Semantics/Primitive_Matchers/Code_Interface.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/Iptables_Semantics/Primitive_Matchers/Code_Interface.thy Tue Apr 24 11:35:45 2018 +0200 @@ -13,7 +13,6 @@ Native_Word.Code_Target_Bits_Int "HOL-Library.Code_Target_Nat" "HOL-Library.Code_Target_Int" - "HOL-Library.Code_Char" begin (*Note: common_primitive_match_expr_ipv4_toString can be really slow*) diff -r efd58f8b1659 thys/Iptables_Semantics/ROOT --- a/thys/Iptables_Semantics/ROOT Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/Iptables_Semantics/ROOT Tue Apr 24 11:35:45 2018 +0200 @@ -11,7 +11,6 @@ Native_Word.Code_Target_Bits_Int "HOL-Library.Code_Target_Nat" "HOL-Library.Code_Target_Int" - "HOL-Library.Code_Char" Automatic_Refinement.Misc (* mergesort *) "Common/List_Misc" "Common/WordInterval_Lists" diff -r efd58f8b1659 thys/Isabelle_Meta_Model/Init.thy --- a/thys/Isabelle_Meta_Model/Init.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/Isabelle_Meta_Model/Init.thy Tue Apr 24 11:35:45 2018 +0200 @@ -36,9 +36,8 @@ ******************************************************************************) theory Init -imports "HOL-Library.Code_Char" - "isabelle_home/src/HOL/Isabelle_Main0" - +imports + "isabelle_home/src/HOL/Isabelle_Main0" begin section\Optimization on the String Datatype\ diff -r efd58f8b1659 thys/JinjaThreads/Basic/Auxiliary.thy --- a/thys/JinjaThreads/Basic/Auxiliary.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/JinjaThreads/Basic/Auxiliary.thy Tue Apr 24 11:35:45 2018 +0200 @@ -11,7 +11,6 @@ Complex_Main "HOL-Library.Transitive_Closure_Table" "HOL-Library.Predicate_Compile_Alternative_Defs" - "HOL-Library.Code_Char" "HOL-Library.Monad_Syntax" "HOL-Library.Infinite_Set" FinFun.FinFun diff -r efd58f8b1659 thys/JinjaThreads/Basic/Basic_Main.thy --- a/thys/JinjaThreads/Basic/Basic_Main.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/JinjaThreads/Basic/Basic_Main.thy Tue Apr 24 11:35:45 2018 +0200 @@ -2,7 +2,6 @@ imports Main "HOL-Library.Sublist" "HOL-Library.Transitive_Closure_Table" - "HOL-Library.Code_Char" "HOL-Library.Predicate_Compile_Alternative_Defs" "HOL-Library.Dlist" Set_without_equal diff -r efd58f8b1659 thys/JinjaThreads/Compiler/Compiler1.thy --- a/thys/JinjaThreads/Compiler/Compiler1.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/JinjaThreads/Compiler/Compiler1.thy Tue Apr 24 11:35:45 2018 +0200 @@ -13,13 +13,14 @@ begin definition fresh_var :: "vname list \ vname" -where "fresh_var Vs \ sum_list (STR ''V'' # Vs)" + where "fresh_var Vs = sum_list (STR ''V'' # Vs)" lemma fresh_var_fresh: "fresh_var Vs \ set Vs" proof - - have "\V \ set Vs. length (String.explode V) < length (String.explode (fresh_var Vs))" - by (induct Vs) (auto simp add: fresh_var_def STR_inverse implode_def) - thus ?thesis by auto + have "V \ set Vs \ length (String.explode V) < length (String.explode (fresh_var Vs))" for V + by (induction Vs) (auto simp add: fresh_var_def Literal.rep_eq) + then show ?thesis + by auto qed text{* Replacing variable names by indices. *} diff -r efd58f8b1659 thys/JinjaThreads/Examples/ApprenticeChallenge.thy --- a/thys/JinjaThreads/Examples/ApprenticeChallenge.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/JinjaThreads/Examples/ApprenticeChallenge.thy Tue Apr 24 11:35:45 2018 +0200 @@ -45,7 +45,7 @@ (Job, Thread, [(STR ''objref'', Class Container, \volatile=False\)], [(STR ''incr'', [], Class Job, $[], sync(Var (STR ''objref'')) - ((Var (STR ''objref''))\STR ''counter''{STR []} := ((Var (STR ''objref''))\STR ''counter''{STR []} \Add\ Val (Intg 1)));; + ((Var (STR ''objref''))\STR ''counter''{STR ''''} := ((Var (STR ''objref''))\STR ''counter''{STR ''''} \Add\ Val (Intg 1)));; Var this)$, (STR ''setref'', [Class Container], Void, $[STR ''o''], LAss (STR ''objref'') (Var (STR ''o'')))$, diff -r efd58f8b1659 thys/JinjaThreads/Examples/BufferExample.thy --- a/thys/JinjaThreads/Examples/BufferExample.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/JinjaThreads/Examples/BufferExample.thy Tue Apr 24 11:35:45 2018 +0200 @@ -36,7 +36,7 @@ (STR ''buffer'' := newA (Class Object)\Var (STR ''size'')\);; (STR ''front'' := Val (Intg 0));; (STR ''back'' := Val (Intg (- 1)));; - (Var this$STR ''size''){STR []} := Val (Intg 0)))$, + (Var this$STR ''size''){STR ''''} := Val (Intg 0)))$, (STR ''empty'', [], Boolean, $[], sync(Var this) (Var (STR ''size'') \Eq\ Val (Intg 0)))$, (STR ''full'', [], Boolean, $[], sync(Var this) (Var (STR ''size'') \Eq\ ((Var (STR ''buffer''))\length)))$, @@ -79,7 +79,7 @@ [(run, [], Void, $[], {STR ''i'':Integer=\Intg 0\; while (Var (STR ''i'') \NotEq\ Val (Intg (word_of_int n))) ( - (Var (STR ''buffer''))\STR ''put''([{STR ''temp'':Class (STR ''Integer'')=None; (STR ''temp'' := new (STR ''Integer'');; ((FAss (Var (STR ''temp'')) (STR ''value'') (STR []) (Var (STR ''i'')));; Var (STR ''temp'')))} ]);; + (Var (STR ''buffer''))\STR ''put''([{STR ''temp'':Class (STR ''Integer'')=None; (STR ''temp'' := new (STR ''Integer'');; ((FAss (Var (STR ''temp'')) (STR ''value'') (STR '''') (Var (STR ''i'')));; Var (STR ''temp'')))} ]);; STR ''i'' := (Var (STR ''i'') \Add\ (Val (Intg 1)))) })$])" @@ -118,8 +118,8 @@ {STR ''p'':Class Producer=None; STR ''p'' := new Producer;; {STR ''c'':Class Consumer=None; (STR ''c'' := new Consumer);; - (Var (STR ''c'')\STR ''buffer''{STR []} := Var (STR ''b''));; - (Var (STR ''p'')\STR ''buffer''{STR []} := Var (STR ''b''));; + (Var (STR ''c'')\STR ''buffer''{STR ''''} := Var (STR ''b''));; + (Var (STR ''p'')\STR ''buffer''{STR ''''} := Var (STR ''b''));; (Var (STR ''c'')\Type.start([]));;(Var (STR ''p'')\Type.start([])) } } diff -r efd58f8b1659 thys/JinjaThreads/Execute/Code_Generation.thy --- a/thys/JinjaThreads/Execute/Code_Generation.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/JinjaThreads/Execute/Code_Generation.thy Tue Apr 24 11:35:45 2018 +0200 @@ -13,7 +13,6 @@ "../Compiler/Compiler" Coinductive.Lazy_TLList "HOL-Library.Code_Target_Int" - "HOL-Library.Code_Char" "HOL-Library.Code_Target_Numeral" begin diff -r efd58f8b1659 thys/JinjaThreads/Execute/ToString.thy --- a/thys/JinjaThreads/Execute/ToString.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/JinjaThreads/Execute/ToString.thy Tue Apr 24 11:35:45 2018 +0200 @@ -261,7 +261,7 @@ instantiation rbt :: ("{toString,linorder}", toString) toString begin definition [code]: "toString (t :: ('a, 'b) rbt) = - sum_list (list_toString (STR [CHR 0x2C, CHR 0x0A]) (rm_to_list t))" + sum_list (list_toString (STR '',\'') (rm_to_list t))" instance proof qed end diff -r efd58f8b1659 thys/JinjaThreads/J/Annotate.thy --- a/thys/JinjaThreads/J/Annotate.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/JinjaThreads/J/Annotate.thy Tue Apr 24 11:35:45 2018 +0200 @@ -12,12 +12,12 @@ abbreviation (output) unanFAcc :: "'addr expr \ vname \ 'addr expr" ("(_\_)" [10,10] 90) where - "unanFAcc e F \ FAcc e F (STR [])" + "unanFAcc e F \ FAcc e F (STR '''')" abbreviation (output) unanFAss :: "'addr expr \ vname \ 'addr expr \ 'addr expr" ("(_\_ := _)" [10,0,90] 90) where - "unanFAss e F e' \ FAss e F (STR []) e'" + "unanFAss e F e' \ FAss e F (STR '''') e'" definition array_length_field_name :: vname where "array_length_field_name = STR ''length''" @@ -68,24 +68,24 @@ AnnoFAcc: "\ is_lub,P,E \ e \ e'; is_lub,P,E \ e' :: U; class_type_of' U = \C\; P \ C sees F:T (fm) in D; is_Array U \ F \ array_length_field_name \ - \ is_lub,P,E \ e\F{STR []} \ e'\F{D}" + \ is_lub,P,E \ e\F{STR ''''} \ e'\F{D}" | AnnoFAccALength: "\ is_lub,P,E \ e \ e'; is_lub,P,E \ e' :: T\\ \ - \ is_lub,P,E \ e\array_length_field_name{STR []} \ e'\length" + \ is_lub,P,E \ e\array_length_field_name{STR ''''} \ e'\length" | AnnoFAccSuper: \ \In class C with super class D, "super" is syntactic sugar for "((D) this)" (cf. JLS, 15.11.2)\ "\ E this = \Class C\; C \ Object; class P C = \(D, fs, ms)\; P \ D sees F:T (fm) in D' \ - \ is_lub,P,E \ Var super\F{STR []} \ (Cast (Class D) (Var this))\F{D'}" + \ is_lub,P,E \ Var super\F{STR ''''} \ (Cast (Class D) (Var this))\F{D'}" | AnnoFAss: "\ is_lub,P,E \ e1 \ e1'; is_lub,P,E \ e2 \ e2'; is_lub,P,E \ e1' :: U; class_type_of' U = \C\; P \ C sees F:T (fm) in D; is_Array U \ F \ array_length_field_name \ - \ is_lub,P,E \ e1\F{STR []} := e2 \ e1'\F{D} := e2'" + \ is_lub,P,E \ e1\F{STR ''''} := e2 \ e1'\F{D} := e2'" | AnnoFAssSuper: "\ E this = \Class C\; C \ Object; class P C = \(D, fs, ms)\; P \ D sees F:T (fm) in D'; is_lub,P,E \ e \ e' \ - \ is_lub,P,E \ Var super\F{STR []} := e \ (Cast (Class D) (Var this))\F{D'} := e'" + \ is_lub,P,E \ Var super\F{STR ''''} := e \ (Cast (Class D) (Var this))\F{D'} := e'" | AnnoCAS: "\ is_lub,P,E \ e1 \ e1'; is_lub,P,E \ e2 \ e2'; is_lub,P,E \ e3 \ e3' \ \ is_lub,P,E \ e1\compareAndSwap(D\F, e2, e3) \ e1'\compareAndSwap(D\F, e2', e3')" @@ -161,7 +161,7 @@ and Annos_fun: "\ is_lub,P,E \ es [\] es'; is_lub,P,E \ es [\] es'' \ \ es' = es''" proof(induct arbitrary: e'' and es'' rule: Anno_Annos.inducts) case (AnnoFAcc E e e' U C F T fm D) - from `is_lub,P,E \ e\F{STR []} \ e''` show ?case + from `is_lub,P,E \ e\F{STR ''''} \ e''` show ?case proof(rule Anno_cases) fix e''' U' C' T' fm' D' assume "is_lub,P,E \ e \ e'''" "is_lub,P,E \ e''' :: U'" @@ -198,7 +198,7 @@ case AnnoFAccALength thus ?case by(fastforce intro: WT_unique[OF is_lub_unique]) next case (AnnoFAss E e1 e1' e2 e2' U C F T fm D) - from `is_lub,P,E \ e1\F{STR []} := e2 \ e''` + from `is_lub,P,E \ e1\F{STR ''''} := e2 \ e''` show ?case proof(rule Anno_cases) fix e1'' e2'' U' C' T' fm' D' diff -r efd58f8b1659 thys/JinjaThreads/MM/SC_Collections.thy --- a/thys/JinjaThreads/MM/SC_Collections.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/JinjaThreads/MM/SC_Collections.thy Tue Apr 24 11:35:45 2018 +0200 @@ -305,7 +305,7 @@ assumes "map_of FDTs (F, D) = \(T, fm)\" shows "\fs' v. tm_\ (init_fields (map (\(FD, (T, fm)). (FD, T)) FDTs)) (String.explode F) = \fs'\ \ lm_\ fs' D = \v\ \ sc.conf P h v T" using assms -by(induct FDTs)(auto simp add: tm.lookup_correct tm.update_correct lm.update_correct init_fields_def explode_inject) + by(induct FDTs)(auto simp add: tm.lookup_correct tm.update_correct lm.update_correct init_fields_def String.explode_inject) lemma sc_oconf_init_fields: assumes "P \ C has_fields FDTs" @@ -349,7 +349,7 @@ fs' = (case tm_lookup (String.explode F) fs of None \ lm_empty () | Some fs' \ fs') \ \ P,h \sc (Obj C (tm_update (String.explode F) (lm_update D v fs') fs)) \" unfolding sc_oconf_def has_field_def -apply(auto dest: has_fields_fun simp add: lm.update_correct tm.update_correct tm.lookup_correct explode_inject) +apply(auto dest: has_fields_fun simp add: lm.update_correct tm.update_correct tm.lookup_correct String.explode_inject) apply(drule (1) has_fields_fun, fastforce) apply(drule (1) has_fields_fun, fastforce) done diff -r efd58f8b1659 thys/Knuth_Morris_Pratt/KMP.thy --- a/thys/Knuth_Morris_Pratt/KMP.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/Knuth_Morris_Pratt/KMP.thy Tue Apr 24 11:35:45 2018 +0200 @@ -1,7 +1,6 @@ theory KMP imports Refine_Imperative_HOL.IICF "HOL-Library.Sublist" - "HOL-Library.Code_Char" begin declare len_greater_imp_nonempty[simp del] min_absorb2[simp] @@ -927,8 +926,8 @@ section \Tests of Generated ML-Code\ ML_val \ - fun str2arl s = (Array.fromList (String.explode s), @{code nat_of_integer} (String.size s)) - fun kmp s t = map_option (@{code integer_of_nat}) (@{code kmp_string_impl} (str2arl s) (str2arl t) ()) + fun str2arl s = (Array.fromList (@{code String.explode} s), @{code nat_of_integer} (String.size s)) + fun kmp s t = map_option @{code integer_of_nat} (@{code kmp_string_impl} (str2arl s) (str2arl t) ()) val test1 = kmp "anas" "bananas" val test2 = kmp "" "bananas" diff -r efd58f8b1659 thys/LLL_Factorization/Modern_Computer_Algebra_Problem.thy --- a/thys/LLL_Factorization/Modern_Computer_Algebra_Problem.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/LLL_Factorization/Modern_Computer_Algebra_Problem.thy Tue Apr 24 11:35:45 2018 +0200 @@ -10,7 +10,6 @@ theory Modern_Computer_Algebra_Problem imports Factorization_Algorithm_16_22 - "HOL-Library.Code_Char" begin fun max_degree_poly :: "int poly \ int poly \ int poly" diff -r efd58f8b1659 thys/LOFT/OpenFlow_Matches.thy --- a/thys/LOFT/OpenFlow_Matches.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/LOFT/OpenFlow_Matches.thy Tue Apr 24 11:35:45 2018 +0200 @@ -3,6 +3,7 @@ Simple_Firewall.Simple_Packet "HOL-Library.Monad_Syntax" (*"../Iptables_Semantics/Primitive_Matchers/Simple_Packet" (* I just want those TCP,UDP,\ defs *)*) + "HOL-Library.List_lexord" "HOL-Library.Char_ord" (* For a linorder on strings. See below. *) begin @@ -101,8 +102,9 @@ termination prerequisites by(relation "measure (match_sorter \ fst)", simp_all) -definition "less_eq_of_match_field1 (a::of_match_field) (b::of_match_field) \ (case (a, b) of - (IngressPort a, IngressPort b) \ String.implode a \ String.implode b | +definition less_eq_of_match_field1 :: "of_match_field \ of_match_field \ bool" + where "less_eq_of_match_field1 (a::of_match_field) (b::of_match_field) \ (case (a, b) of + (IngressPort a, IngressPort b) \ a \ b | (VlanId a, VlanId b) \ a \ b | (EtherDst a, EtherDst b) \ a \ b | (EtherSrc a, EtherSrc b) \ a \ b | @@ -114,12 +116,20 @@ (L4Src a1 a2, L4Src b1 b2) \ if a2 = b2 then a1 \ b1 else a2 \ b2 | (L4Dst a1 a2, L4Dst b1 b2) \ if a2 = b2 then a1 \ b1 else a2 \ b2 | (a, b) \ match_sorter a < match_sorter b)" + (* feel free to move this to OpenFlowSerialize if it gets in the way. *) instantiation of_match_field :: linorder begin - definition "less_eq_of_match_field (a::of_match_field) (b::of_match_field) \ less_eq_of_match_field1 a b" - definition "less_of_match_field (a::of_match_field) (b::of_match_field) \ (a \ b \ less_eq_of_match_field1 a b)" -instance by standard (auto simp: less_eq_of_match_field_def less_eq_of_match_field1_def less_of_match_field_def implode_def split: prod.splits of_match_field.splits if_splits) + +definition + "less_eq_of_match_field (a::of_match_field) (b::of_match_field) \ less_eq_of_match_field1 a b" + +definition + "less_of_match_field (a::of_match_field) (b::of_match_field) \ a \ b \ less_eq_of_match_field1 a b" + +instance + by standard (auto simp add: less_eq_of_match_field_def less_of_match_field_def less_eq_of_match_field1_def split: prod.splits of_match_field.splits if_splits) + end fun match_no_prereq :: "of_match_field \ (32, 'a) simple_packet_ext_scheme \ bool" where diff -r efd58f8b1659 thys/LOFT/OpenFlow_Serialize.thy --- a/thys/LOFT/OpenFlow_Serialize.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/LOFT/OpenFlow_Serialize.thy Tue Apr 24 11:35:45 2018 +0200 @@ -4,7 +4,6 @@ Semantics_OpenFlow Simple_Firewall.Primitives_toString IP_Addresses.Lib_Word_toString - "HOL-Library.Code_Char" begin definition "serialization_test_entry \ OFEntry 7 {EtherDst 0x1, IPv4Dst (PrefixMatch 0xA000201 32), IngressPort ''s1-lan'', L4Dst 0x50 0, L4Src 0x400 0x3FF, IPv4Proto 6, EtherType 0x800} [ModifyField_l2dst 0xA641F185E862, Forward ''s1-wan'']" diff -r efd58f8b1659 thys/LTL/example/LTL_Example.thy --- a/thys/LTL/example/LTL_Example.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/LTL/example/LTL_Example.thy Tue Apr 24 11:35:45 2018 +0200 @@ -6,7 +6,7 @@ section \Example\ theory LTL_Example - imports Main "../LTL" "../LTL_Rewrite" "HOL-Library.Code_Target_Numeral" "HOL-Library.Code_Char" + imports Main "../LTL" "../LTL_Rewrite" "HOL-Library.Code_Target_Numeral" begin \ \The included parser always returns a @{typ "String.literal ltlc"}. If a different labelling is diff -r efd58f8b1659 thys/LTL/example/rewrite_example.sml --- a/thys/LTL/example/rewrite_example.sml Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/LTL/example/rewrite_example.sml Tue Apr 24 11:35:45 2018 +0200 @@ -19,6 +19,22 @@ end; (*struct HOL*) +structure Product_Type : sig + val equal_unit : unit HOL.equal + val fst : 'a * 'b -> 'a + val snd : 'a * 'b -> 'b +end = struct + +fun equal_unita u v = true; + +val equal_unit = {equal = equal_unita} : unit HOL.equal; + +fun fst (x1, x2) = x1; + +fun snd (x1, x2) = x2; + +end; (*struct Product_Type*) + structure Orderings : sig type 'a ord val less_eq : 'a ord -> 'a -> 'a -> bool @@ -49,6 +65,7 @@ val zero_nat : nat val funpow : nat -> ('a -> 'a) -> 'a -> 'a val less_nat : nat -> nat -> bool + val bit_cut_integer : IntInf.int -> IntInf.int * bool val less_eq_nat : nat -> nat -> bool end = struct @@ -85,6 +102,17 @@ fun less_nat m n = IntInf.< (integer_of_nat m, integer_of_nat n); +fun bit_cut_integer k = + (if ((k : IntInf.int) = (0 : IntInf.int)) then ((0 : IntInf.int), false) + else let + val (r, s) = + IntInf.divMod (IntInf.abs k, IntInf.abs (2 : IntInf.int)); + in + ((if IntInf.< ((0 : IntInf.int), k) then r + else IntInf.- (IntInf.~ r, s)), + ((s : IntInf.int) = (1 : IntInf.int))) + end); + fun less_eq_nat m n = IntInf.<= (integer_of_nat m, integer_of_nat n); end; (*struct Arith*) @@ -296,29 +324,51 @@ end; (*struct LTL*) -structure Stringa : sig +structure List : sig + val map : ('a -> 'b) -> 'a list -> 'b list + val size_list : 'a list -> Arith.nat +end = struct + +fun map f [] = [] + | map f (x21 :: x22) = f x21 :: map f x22; + +fun gen_length n (x :: xs) = gen_length (Arith.suc n) xs + | gen_length n [] = n; + +fun size_list x = gen_length Arith.zero_nat x; + +end; (*struct List*) + +structure String : sig + type char val size_literal : string -> Arith.nat end = struct -fun size_literal s = Arith.zero_nat; +datatype char = Chara of bool * bool * bool * bool * bool * bool * bool * bool; -end; (*struct Stringa*) +fun char_of_integer k = let + val (q0, b0) = Arith.bit_cut_integer k; + val (q1, b1) = Arith.bit_cut_integer q0; + val (q2, b2) = Arith.bit_cut_integer q1; + val (q3, b3) = Arith.bit_cut_integer q2; + val (q4, b4) = Arith.bit_cut_integer q3; + val (q5, b5) = Arith.bit_cut_integer q4; + val (q6, b6) = Arith.bit_cut_integer q5; + val a = Arith.bit_cut_integer q6; + val (_, aa) = a; + in + Chara (b0, b1, b2, b3, b4, b5, b6, aa) + end; -structure Product_Type : sig - val equal_unit : unit HOL.equal - val fst : 'a * 'b -> 'a - val snd : 'a * 'b -> 'b -end = struct +fun explode s = + List.map char_of_integer + ((map (fn c => let val k = Char.ord c in if k < 128 then IntInf.fromInt k else raise Fail "Non-ASCII character in literal" end) + o String.explode) + s); -fun equal_unita u v = true; +fun size_literal xa = List.size_list (explode xa); -val equal_unit = {equal = equal_unita} : unit HOL.equal; - -fun fst (x1, x2) = x1; - -fun snd (x1, x2) = x2; - -end; (*struct Product_Type*) +end; (*struct String*) structure Predicate : sig type 'a seq @@ -1285,7 +1335,7 @@ fun rewrite x = (LTL_Rewrite.rewrite_iter_slow Arith.equal_nat o LTL.ltlc_to_ltln o - LTL.map_ltlc Stringa.size_literal) + LTL.map_ltlc String.size_literal) x; end; (*struct LTL_Example*) diff -r efd58f8b1659 thys/LTL_to_DRA/Impl/Export_Code.thy --- a/thys/LTL_to_DRA/Impl/Export_Code.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/LTL_to_DRA/Impl/Export_Code.thy Tue Apr 24 11:35:45 2018 +0200 @@ -10,7 +10,6 @@ "HOL-Library.AList_Mapping" (* Future, Performance: Replace by LC *) LTL.LTL_Rewrite "HOL-Library.Code_Target_Numeral" - "HOL-Library.Code_Char" begin subsection \External Interface\ diff -r efd58f8b1659 thys/Native_Word/Native_Cast.thy --- a/thys/Native_Word/Native_Cast.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/Native_Word/Native_Cast.thy Tue Apr 24 11:35:45 2018 +0200 @@ -2,39 +2,25 @@ Author: Andreas Lochbihler, ETH Zurich *) -chapter {* Conversions between unsigned words and between char *} +chapter \Conversions between unsigned words and between char\ -theory Native_Cast imports - "HOL-Library.Code_Char" +theory Native_Cast + imports Uint8 Uint16 Uint32 Uint64 begin -text {* Auxiliary stuff *} - -context includes lifting_syntax -begin - -lemma char_of_integer_transfer [transfer_rule]: - "(pcr_integer ===> (=)) (\n. char_of_nat (nat n)) char_of_integer" -by(simp add: integer.pcr_cr_eq cr_integer_def rel_fun_def char_of_integer_def nat_of_integer_def) - -lemma integer_of_char_transfer [transfer_rule]: - "((=) ===> pcr_integer) (\n. int (nat_of_char n)) integer_of_char" -by(simp add: integer.pcr_cr_eq cr_integer_def rel_fun_def integer_of_char_def) - -end +text \Auxiliary stuff\ lemma integer_of_char_char_of_integer [simp]: - "0 \ x \ integer_of_char (char_of_integer x) = x mod 256" -unfolding integer_of_char_def char_of_integer_def o_apply nat_of_char_of_nat -including integer.lifting by transfer(auto dest: nat_mod_distrib[of _ 256, symmetric]) + "integer_of_char (char_of_integer x) = x mod 256" + by (simp add: integer_of_char_def char_of_integer_def) lemma char_of_integer_integer_of_char [simp]: "char_of_integer (integer_of_char x) = x" -by(simp add: integer_of_char_def char_of_integer_def) + by (simp add: integer_of_char_def char_of_integer_def) lemma int_lt_numeral [simp]: "int x < numeral n \ x < numeral n" by (metis nat_numeral zless_nat_eq_int_zless) @@ -43,58 +29,11 @@ including integer.lifting by transfer simp lemma integer_of_char_ge_0 [simp]: "0 \ integer_of_char x" -including integer.lifting by transfer simp + including integer.lifting unfolding integer_of_char_def + by transfer (simp add: of_char_def) -section {* Conversions between @{typ uint8} and @{typ char} *} - -definition uint8_of_char :: "char \ uint8" -where "uint8_of_char = Uint8 \ integer_of_char" - -definition char_of_uint8 :: "uint8 \ char" -where "char_of_uint8 = char_of_integer \ integer_of_int \ uint \ Rep_uint8'" - -lemma uint8_of_char_char_of_uint8 [simp]: - "uint8_of_char (char_of_uint8 x) = x" -apply(simp add: uint8_of_char_def char_of_uint8_def) -including integer.lifting apply transfer -apply(simp add: mod_pos_pos_trivial uint_bounded[where ?'a=8, simplified]) -done - -lemma char_of_uint8_uint8_of_char [simp]: - "char_of_uint8 (uint8_of_char x) = x" -proof - - have "char_of_uint8 (uint8_of_char x) = - char_of_integer (of_int (int_of_integer (integer_of_char x) mod 256))" - by(simp add: uint8_of_char_def char_of_uint8_def Uint8.rep_eq uint_word_of_int) - also { have "int_of_integer (integer_of_char x) < 256" - including integer.lifting by transfer(simp add: nat_of_char_less_256) } - hence "\ = x" - by(simp add: mod_pos_pos_trivial int_of_integer_ge_0) - finally show ?thesis . -qed - -code_printing code_module Native_Casts \ (Haskell) -{*import qualified Data.Char; - -ord :: Char -> Int; -ord = Data.Char.ord; - -chr :: Int -> Char; -chr = Data.Char.chr; -*} -code_reserved Haskell Native_Casts - -code_printing constant uint8_of_char \ - (SML) "Word8.fromInt (Char.ord _)" and - (Haskell) "(Prelude.fromIntegral (Native'_Casts.ord _) :: Uint8.Word8)" and - (Scala) "_.toByte" -| constant char_of_uint8 \ - (SML) "Char.chr (Word8.toInt _)" and - (Haskell) "Native'_Casts.chr (Prelude.fromIntegral _)" and - (Scala) "((_).toInt & 0xFF).toChar" - -section {* Conversion between native words *} +section \Conversion between native words\ lift_definition uint8_of_uint16 :: "uint16 \ uint8" is ucast . lift_definition uint8_of_uint32 :: "uint32 \ uint8" is ucast . @@ -167,11 +106,11 @@ (Scala) "((_).toLong & 0xFFFFFFFFL)" and (OCaml) "Int64.logand (Int64.of'_int32 _) (Int64.of'_string \"4294967295\")" -text {* +text \ Use @{const Abs_uint8'} etc. instead of @{const Rep_uint8} in code equations for conversion functions to avoid exceptions during code generation when the target language provides only some of the uint types. -*} +\ lemma uint8_of_uint16_code [code]: "uint8_of_uint16 x = Abs_uint8' (ucast (Rep_uint16' x))" diff -r efd58f8b1659 thys/Native_Word/Native_Word_Test.thy --- a/thys/Native_Word/Native_Word_Test.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/Native_Word/Native_Word_Test.thy Tue Apr 24 11:35:45 2018 +0200 @@ -421,8 +421,6 @@ definition test_casts :: bool where "test_casts \ - map uint8_of_char [CHR ''a'', 0, char_of_nat 255] = [97, 0, 255] \ - map char_of_uint8 [65, 0, 255] = [CHR ''A'', 0, char_of_nat 255] \ map uint8_of_uint32 [10, 0, 0xFE, 0xFFFFFFFF] = [10, 0, 0xFE, 0xFF] \ map uint8_of_uint64 [10, 0, 0xFE, 0xFFFFFFFFFFFFFFFF] = [10, 0, 0xFE, 0xFF] \ map uint32_of_uint8 [10, 0, 0xFF] = [10, 0, 0xFF] \ diff -r efd58f8b1659 thys/Ordinary_Differential_Equations/Numerics/Refine_Reachability_Analysis.thy --- a/thys/Ordinary_Differential_Equations/Numerics/Refine_Reachability_Analysis.thy Sat Apr 21 08:42:02 2018 +0200 +++ b/thys/Ordinary_Differential_Equations/Numerics/Refine_Reachability_Analysis.thy Tue Apr 24 11:35:45 2018 +0200 @@ -1172,7 +1172,7 @@ shows "(nres_of ?f, mk_safe $ (R::'a::executable_euclidean_space set)) \ \appr_rel\nres_rel" unfolding autoref_tag_defs unfolding mk_safe_def - by (autoref_monadic) + by autoref_monadic concrete_definition mk_safe_impl for Ri uses mk_safe_impl lemma sappr_rel_nres_relI: @@ -1218,7 +1218,7 @@ shows "(nres_of (?f::?'c dres), mk_safe_coll IS)\?R" unfolding mk_safe_coll_def by (subst rel_ANNOT_eq[of "sets_of_coll X" "\\appr_rel\list_wset_rel\nres_rel" for X]) - (autoref_monadic) + autoref_monadic concrete_definition mk_safe_coll_impl for ISi uses mk_safe_coll_impl lemma mk_safe_coll_impl_refine[autoref_rules]: @@ -1482,7 +1482,7 @@ unfolding autoref_tag_defs unfolding Picard_step_ivl_def including art - by (autoref_monadic) + by autoref_monadic concrete_definition Picard_step_ivl_impl for X0i t0i hi PHIi uses Picard_step_ivl_impl lemmas [autoref_rules] = Picard_step_ivl_impl.refine @@ -1541,7 +1541,7 @@ shows "(nres_of (?f::?'r dres), P_iter $ X0 $ h $ i $ PHI::'a set option nres) \ ?R" unfolding P_iter_def uncurry_rec_nat APP_def including art - by (autoref_monadic) + by autoref_monadic concrete_definition P_iter_impl for X0i hi i_i PHIi uses P_iter_impl lemmas [autoref_rules] = P_iter_impl.refine @@ -2197,10 +2197,11 @@ notes [autoref_rules] = autoref_parameters shows "(nres_of (?f::?'r dres), rk2_step $ (X::'a set) $ h) \