{- |

Module : $Header$

Copyright : (c) Uni Bremen 2005

Licence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

Maintainer : maeder@tzi.de

Stability : provisional

Portability : portable

String constants of Isabelle keywords to be excluded by translations

obtained by manually taking @lexicon@ and @consts@ from

@print_syntax(theory "...")@

(initial empty strings omitted)

-}

module Isabelle.IsaStrings where

import qualified Common.Lib.Set as Set

-- | convert pasted strings to a relevant set of strings

mkIsaSet :: [String] -> Set.Set String

mkIsaSet = Set.fromList . concatMap words

{- fewer list elements are better to optimize ("\",\"" -> " ")

keep all words in case we also want to use symbols

-}

pureS :: Set.Set String

pureS = mkIsaSet [

"!! % ( ) , . ... :: ; == ==> => OFCLASS",

"PROP TYPE [ [| \\<And> \\<Colon> \\<Longrightarrow>",

"\\<Rightarrow> \\<^sub> \\<dots> \\<equiv> \\<equiv>\\<^sup>?",

"\\<index> \\<lambda> \\<lbrakk> \\<rbrakk> \\<struct> ] _",

"_:: op { {} |] }",

"!! !! #prop == == ==> ==> ==> =?= Goal",

"Goal TYPE _DDDOT _DDDOT _K _TYPE _abs _appl _appl",

"_aprop _args _asms _bigimpl _bigimpl _bracket _bracket",

"_classes _constify _constrain _constrain _dummy_ofsort _idts",

"_idtyp _idtyp _index _indexvar _lambda _lambda",

"_meta_conjunction _mk_ofclass _noindex _ofclass _ofsort",

"_ofsort _pttrns _sort _struct _tapp _tappl _topsort _types",

"all any aprop args asms cargs classes dummy dummy",

"dummy_pattern dummy_pattern fun fun fun id idt idts",

"index itself logic logic logic_class longid num num_const",

"prop pttrn pttrns sort struct tid tvar type types var",

"xnum xstr"

]

holS :: Set.Set String

holS = mkIsaSet [

"! !! % & ( ) * + , - --> . ... / 0",

"1 :: ; < <= = == ==> => ? ?! ALL EX EX!",

"LEAST OFCLASS PROP THE TYPE [ [| \\<And> \\<Colon>",

"\\<Longrightarrow> \\<Rightarrow> \\<^sub> \\<^sub>1 \\<and>",

"\\<bar> \\<dots> \\<equiv> \\<equiv>\\<^sup>? \\<exists>",

"\\<exists>! \\<forall> \\<index> \\<lambda> \\<lbrakk> \\<le>",

"\\<longrightarrow> \\<not> \\<noteq> \\<or> \\<rbrakk>",

"\\<struct> ] _ _:: case else if in let of op then",

"{ {} | |] } ~ ~=",

"!! !! #prop 0 1 == == ==> ==> ==>",

"=?= ALL ALL ALL ALL All EX EX EX EX EX! ",

"EX! EX! EX! Ex Ex1 False Goal Goal If LEAST ",

"Least Let Not Not Not TYPE The True Trueprop _DDDOT",

"_DDDOT _K _Let _TYPE _The _abs _appl _applC _aprop",

"_args _asms _bigimpl _bigimpl _bind _binds _bracket",

"_bracket _cargs _case1 _case1 _case2 _case_syntax _classes",

"_constify _constrain _constrain _dummy_ofsort _idts _idtyp",

"_idtyp _index _index1 _indexvar _lambda _lambda _leAll",

"_leAll _leAll _leAll _leEx _leEx _leEx _leEx _lessAll",

"_lessAll _lessAll _lessAll _lessEx _lessEx _lessEx _lessEx",

"_meta_conjunction _mk_ofclass _noindex _not_equal _not_equal",

"_not_equal _not_equal _not_equal _ofclass _ofsort _ofsort",

"_pttrns _sort _struct _tapp _tappl _topsort _types abs",

"abs abs all any aprop arbitrary args asms bool cargs",

"case_syn cases_syn classes divide dummy dummy dummy_pattern",

"dummy_pattern fun fun fun id idt idts index induct_conj",

"induct_equal induct_forall induct_implies inverse inverse",

"inverse_class itself letbind letbinds linorder linorder_class",

"logic logic logic_class longid max min minus minus_class",

"mono num num_const one one_class op & op & op & op *",

"op + op - op --> op --> op < op < op <= op <= op <=",

"op <= op = op = op | op | op | ord ord_class order",

"order_class plus plus_class prop pttrn pttrns sort struct",

"tid times times_class tvar type type type_class types",

"uminus var xnum xstr zero zero_class"

]

holcfS :: Set.Set String

holcfS = mkIsaSet [

"! !! # $ % & ( () (: (] (| (} ) * **",

"+ ++ , - --> -> -` . .. ... ..} / // 0 1 :",

":) :: := ; < <*> <*lex*> <+> << <<| <= <| = ==",

"==> => > >. ? ?! @ ALL BIT CHR EX EX! GREATEST",

"INF INT If Int LAM LEAST LUB Let MOST O OFCLASS",

"PROP SIGMA SOME THE TYPE UN Un WRT [ [\\<mapsto>] []",

"[| [|->] \\<And> \\<Colon> \\<Inter> \\<Inter>\\<^bsub>",

"\\<Lambda> \\<Longrightarrow> \\<Prod> \\<Rightarrow> \\<Sigma>",

"\\<Squnion> \\<Sum> \\<Union> \\<Union>\\<^bsub> \\<^esub>",

"\\<^sub> \\<^sub>1 \\<^sup>* \\<^sup>+ \\<^sup>= \\<and>",

"\\<bar> \\<bottom> \\<cdot> \\<circ> \\<dots> \\<epsilon>",

"\\<equiv> \\<equiv>\\<^sup>? \\<exists> \\<exists>!",

"\\<exists>\\<^sub>\\<infinity> \\<forall>",

"\\<forall>\\<^sub>\\<infinity> \\<in> \\<index> \\<int>",

"\\<inter> \\<inverse> \\<lambda> \\<lbrakk> \\<le> \\<leadsto>",

"\\<lfloor> \\<longrightarrow> \\<lparr> \\<mapsto>",

"\\<mapsto>\\<lambda> \\<nat> \\<not> \\<noteq> \\<notin>",

"\\<oplus> \\<or> \\<otimes> \\<rbrakk> \\<rightarrow>",

"\\<rightharpoonup> \\<rparr> \\<sqsubseteq> \\<struct>",

"\\<subset> \\<subseteq> \\<subseteq>\\<^sub>m \\<times>",

"\\<twosuperior> \\<union> ] ^ ^* ^+ ^-1 ^= _ _:: `",

"`> `` andalso case choose div dvd else fi if in",

"let mem mod o of oo op orelse then { {) {..",

"{\\<mapsto>} {|->} {} | |) |-> |] |_ } ~ ~: ~=",

"~=> ~>",

"!! #prop * ** + ++ -> 0 1 == ==> =?=",

"@Coll @Finset @INTER @INTER1 @INTER_le @INTER_less @LUB",

"@SetCompr @Sigma @Times @UNION @UNION1 @UNION_le @UNION_less",

"@andalso @chg_map @cifte @ctuple @filter @list @oo @orelse",

"@stuple ACe ALL Abs_CFun Abs_Integ Abs_Nat Abs_Node",

"Abs_Prod Abs_Sprod Abs_Ssum Abs_Sum Abs_Up Abs_bin Abs_char",

"Abs_discr Abs_lift Abs_list Abs_nibble Abs_option Abs_sumbool",

"Abs_unit All Alm_all Atom Ball Bex Bit CFun CLet Case",

"Char Cletbind Cletbinds Collect Cons Def Discr Domain",

"EX EX! Eps Ex Ex1 FF False Field Finites GREATEST ",

"Goal Greatest GreatestM ID INF INTER Icifte Id If If2",

"Ifix Ifup Image In0 In1 Inf_many Inl Inl_Rep Inr",

"Inr_Rep Integ Inter Ints Inv Isfst Isinl Isinr Ispair",

"Issnd Istrictify Iup Iwhen LAM LC LEAST LUB Leaf",

"Least LeastM Left Let Lim MOST Max Min NCons Nat",

"Nats Nibble0 Nibble1 Nibble2 Nibble3 Nibble4 Nibble5",

"Nibble6 Nibble7 Nibble8 Nibble9 NibbleA NibbleB NibbleC",

"NibbleD NibbleE NibbleF Nil Node None Not Numb Numeral0",

"Numeral1 ONE Pair Pair_Rep Part Pls Plus Pow Prod Push",

"Push_Node Range Rep_CFun Rep_Integ Rep_Nat Rep_Node Rep_Prod",

"Rep_Sprod Rep_Ssum Rep_Sum Rep_Up Rep_bin Rep_char Rep_discr",

"Rep_lift Rep_list Rep_nibble Rep_option Rep_sumbool Rep_unit",

"Right Scons Sigma Sinl_Rep Sinr_Rep Some Spair_Rep Split",

"Sprod Ssum Suc Suc_Rep Sum Suml Summation Sumr TT TYPE",

"The True Trueprop UNION UNIV UU Undef Union Unity Up",

"Zero_Rep _Ball _Bex _CLet _Cbind _Cbinds _Char _DDDOT",

"_Eps _GreatestM _K _LAM _LUpdate _LeastM _Let _Map",

"_MapUpd _Maplets _Numeral _String _Summation _TYPE _The",

"_Update _abs _appl _applC _aprop _args _asms _bigimpl",

"_bind _binds _bracket _cargs _case1 _case2 _case_syntax",

"_classes _constify _constrain _dummy_ofsort _field _field_type",

"_field_types _fields _idts _idtyp _index _index1 _indexvar",

"_lambda _leAll _leEx _lessAll _lessEx _lupdbind _lupdbinds",

"_maplet _maplets _meta_conjunction _mk_ofclass _noindex",

"_not_equal _ofclass _ofsort _pattern _patterns _pttrns",

"_record _record_scheme _record_type _record_type_scheme",

"_record_update _reflcl _setle _setless _setprod _setsum",

"_sort _square _struct _tapp _tappl _topsort _tuple",

"_tuple_arg _tuple_args _types _update _update_name _updates",

"_updbind _updbinds abelian_group abelian_group_class",

"abelian_semigroup abelian_semigroup_class abs acyclic adjust",

"adm adm_wf admw all almost_ordered_semiring",

"almost_ordered_semiring_class almost_semiring almost_semiring_class",

"antisym any apfst aprop arbitrary args asms atLeast",

"atLeastAtMost atLeastLessThan atMost atmost_one bij bin",

"bin_add bin_case bin_minus bin_mult bin_pred bin_rec",

"bin_rec_set bin_rep_set bin_succ binomial bool bool_case",

"bool_rec bool_rec_set butlast card cardR cargs case_syn",

"cases_syn cfcomp cfst chain char char_case char_rec",

"char_rec_set char_rep_set chfin chfin_class chg_map classes",

"comp concat congruent congruent2 cont contents contlub",

"converse cpair cpo cpo_class csnd csplit curry cut diag",

"discr discr_case discr_rec discr_rec_set discr_rep_set",

"distinct div divAlg div_class divide division_by_zero",

"division_by_zero_class dom dprod drop dropWhile dsum dtree",

"dummy dummy_pattern empty equiv even even_odd even_odd_class",

"field field_class field_type field_types fields filter",

"finite finite_chain finite_class finite_psubset fix flat",

"flat_class flift1 flift2 fold foldSet foldl foldr fst",

"fun fun_upd fup gfp greaterThan greaterThanAtMost",

"greaterThanLessThan hd id ident idt idts image ind index",

"induct_conj induct_equal induct_forall induct_implies infinite",

"inj inj_on insert int int_aux internal_split intrel inv",

"inv_image inverse inverse_class iszero item iterate itself",

"last length lessThan less_cfun less_than letbind letbinds",

"lex lex_prod lexico lexn lfp lift lift_case lift_rec",

"lift_rec_set liftpair linorder linorder_class list list_all",

"list_all2 list_case list_rec list_rec_set list_rep_set",

"list_update lists logic logic_class longid lub lupdbind",

"lupdbinds map map_add map_image map_le map_of map_subst",

"map_upd_s map_upds maplet maplets max max_in_chain measure",

"min minus minus_class mono monofun myinv nat nat_aux",

"nat_case nat_rec nat_rec_set ndepth neg negDivAlg negateSnd",

"nibble nibble_case nibble_rec nibble_rec_set nibble_rep_set",

"node nth ntrunc null num num_const number number_class",

"number_of number_ring number_ring_class o2s odd of_int",

"of_nat one one_class op & op * op + op - op --> op :",

"op < op << op <<| op <= op <| op = op @ op Int op Un",

"op div op dvd op mem op mod op | op ~: option option_case",

"option_map option_rec option_rec_set option_rep_set ord",

"ord_class order order_class ordered_field ordered_field_class",

"ordered_ring ordered_ring_class ordered_semiring",

"ordered_semiring_class overwrite patterns pcpo pcpo_class plus",

"plus_ac0 plus_ac0_class plus_class po po_class posDivAlg",

"power power_class pred_nat prod_case prod_fun prod_rec",

"prod_rec_set product_type prop pttrn pttrns quorem quotient",

"ran range refl reflexive rel_comp remdups replicate",

"restrict_map rev ring ring_class ringpower ringpower_class",

"rtrancl same_fst semiring semiring_class set setprod setsum",

"sfst single_valued sinl sinr size snd sort spair split",

"sq_ord sq_ord_class sscase ssnd ssplit strictify string",

"struct sublist sum_case sum_rec sum_rec_set sumbool",

"sumbool_case sumbool_rec sumbool_rec_set sumbool_rep_set surj",

"sym take takeWhile the tid times times_ac1 times_ac1_class",

"times_class tl tord tr trancl trand trans tror",

"tuple_args tvar type type_class type_definition types u",

"uminus undiscr unit unit_case unit_rec unit_rec_set up",

"upd_fst upd_snd update updates updbind updbinds uprod upt",

"upto usum var vimage wellorder wellorder_class wf wfrec",

"wfrec_rel xnum xstr zero zero_class zip {} ~=>"

]

mainS :: Set.Set String

mainS = mkIsaSet [

"! !! # % & ( () (] (| (} ) * + ++ ,",

"- --> -` . .. ... ..} / // 0 1 : :: := ; <",

"<*> <*lex*> <+> <= = == ==> => ? ?! @ ALL BIT",

"CHR EX EX! GREATEST INF INT Int LEAST MOST O OFCLASS",

"PROP SIGMA SOME THE TYPE UN Un WRT [ [\\<mapsto>] []",

"[| [|->] \\<And> \\<Colon> \\<Inter> \\<Inter>\\<^bsub>",

"\\<Longrightarrow> \\<Prod> \\<Rightarrow> \\<Sigma> \\<Sum>",

"\\<Union> \\<Union>\\<^bsub> \\<^esub> \\<^sub> \\<^sub>1",

"\\<^sup>* \\<^sup>+ \\<^sup>= \\<and> \\<bar> \\<circ>",

"\\<dots> \\<epsilon> \\<equiv> \\<equiv>\\<^sup>? \\<exists>",

"\\<exists>! \\<exists>\\<^sub>\\<infinity> \\<forall>",

"\\<forall>\\<^sub>\\<infinity> \\<in> \\<index> \\<int>",

"\\<inter> \\<inverse> \\<lambda> \\<lbrakk> \\<le> \\<leadsto>",

"\\<lfloor> \\<longrightarrow> \\<lparr> \\<mapsto>",

"\\<mapsto>\\<lambda> \\<nat> \\<not> \\<noteq> \\<notin>",

"\\<or> \\<rbrakk> \\<rightharpoonup> \\<rparr> \\<struct>",

"\\<subset> \\<subseteq> \\<subseteq>\\<^sub>m \\<times>",

"\\<twosuperior> \\<union> ] ^ ^* ^+ ^-1 ^= _ _:: `",

"`> `` case choose div dvd else if in let mem mod",

"o of op then { {) {.. {\\<mapsto>} {|->} {} | |)",

"|-> |] |_ } ~ ~: ~= ~=> ~>",

"!! #prop * + 0 1 == ==> =?= @Coll @Finset",

"@INTER @INTER1 @INTER_le @INTER_less @SetCompr @Sigma @Times",

"@UNION @UNION1 @UNION_le @UNION_less @chg_map @filter @list",

"ACe ALL Abs_Integ Abs_Nat Abs_Node Abs_Prod Abs_Sum",

"Abs_bin Abs_char Abs_list Abs_nibble Abs_option Abs_sumbool",

"Abs_unit All Alm_all Atom Ball Bex Bit Case Char",

"Collect Cons Domain EX EX! Eps Ex Ex1 False Field",

"Finites GREATEST Goal Greatest GreatestM INF INTER Id",

"If Image In0 In1 Inf_many Inl Inl_Rep Inr Inr_Rep",

"Integ Inter Ints Inv LC LEAST Leaf Least LeastM Left",

"Let Lim MOST Max Min NCons Nat Nats Nibble0 Nibble1",

"Nibble2 Nibble3 Nibble4 Nibble5 Nibble6 Nibble7 Nibble8",

"Nibble9 NibbleA NibbleB NibbleC NibbleD NibbleE NibbleF",

"Nil Node None Not Numb Numeral0 Numeral1 Pair Pair_Rep",

"Part Pls Plus Pow Prod Push Push_Node Range Rep_Integ",

"Rep_Nat Rep_Node Rep_Prod Rep_Sum Rep_bin Rep_char Rep_list",

"Rep_nibble Rep_option Rep_sumbool Rep_unit Right Scons Sigma",

"Some Split Suc Suc_Rep Sum Suml Summation Sumr TYPE",

"The True Trueprop UNION UNIV Union Unity Zero_Rep _Ball",

"_Bex _Char _DDDOT _Eps _GreatestM _K _LUpdate _LeastM",

"_Let _Map _MapUpd _Maplets _Numeral _String _Summation",

"_TYPE _The _Update _abs _appl _applC _aprop _args _asms",

"_bigimpl _bind _binds _bracket _cargs _case1 _case2",

"_case_syntax _classes _constify _constrain _dummy_ofsort",

"_field _field_type _field_types _fields _idts _idtyp _index",

"_index1 _indexvar _lambda _leAll _leEx _lessAll _lessEx",

"_lupdbind _lupdbinds _maplet _maplets _meta_conjunction",

"_mk_ofclass _noindex _not_equal _ofclass _ofsort _pattern",

"_patterns _pttrns _record _record_scheme _record_type",

"_record_type_scheme _record_update _reflcl _setle _setless",

"_setprod _setsum _sort _square _struct _tapp _tappl",

"_topsort _tuple _tuple_arg _tuple_args _types _update",

"_update_name _updates _updbind _updbinds abelian_group",

"abelian_group_class abelian_semigroup abelian_semigroup_class abs",

"acyclic adjust adm_wf all almost_ordered_semiring",

"almost_ordered_semiring_class almost_semiring almost_semiring_class",

"antisym any apfst aprop arbitrary args asms atLeast",

"atLeastAtMost atLeastLessThan atMost atmost_one bij bin",

"bin_add bin_case bin_minus bin_mult bin_pred bin_rec",

"bin_rec_set bin_rep_set bin_succ binomial bool bool_case",

"bool_rec bool_rec_set butlast card cardR cargs case_syn",

"cases_syn char char_case char_rec char_rec_set char_rep_set",

"chg_map classes comp concat congruent congruent2 contents",

"converse curry cut diag distinct div divAlg div_class",

"divide division_by_zero division_by_zero_class dom dprod drop",

"dropWhile dsum dtree dummy dummy_pattern empty equiv even",

"even_odd even_odd_class field field_class field_type",

"field_types fields filter finite finite_class finite_psubset",

"fold foldSet foldl foldr fst fun fun_upd gfp greaterThan",

"greaterThanAtMost greaterThanLessThan hd id ident idt idts",

"image ind index induct_conj induct_equal induct_forall",

"induct_implies infinite inj inj_on insert int int_aux",

"internal_split intrel inv inv_image inverse inverse_class",

"iszero item itself last length lessThan less_than letbind",

"letbinds lex lex_prod lexico lexn lfp linorder",

"linorder_class list list_all list_all2 list_case list_rec",

"list_rec_set list_rep_set list_update lists logic logic_class",

"longid lupdbind lupdbinds map map_add map_image map_le",

"map_of map_subst map_upd_s map_upds maplet maplets max",

"measure min minus minus_class mono myinv nat nat_aux",

"nat_case nat_rec nat_rec_set ndepth neg negDivAlg negateSnd",

"nibble nibble_case nibble_rec nibble_rec_set nibble_rep_set",

"node nth ntrunc null num num_const number number_class",

"number_of number_ring number_ring_class o2s odd of_int",

"of_nat one one_class op & op * op + op - op --> op :",

"op < op <= op = op @ op Int op Un op div op dvd op mem",

"op mod op | op ~: option option_case option_map option_rec",

"option_rec_set option_rep_set ord ord_class order order_class",

"ordered_field ordered_field_class ordered_ring ordered_ring_class",

"ordered_semiring ordered_semiring_class overwrite patterns plus",

"plus_ac0 plus_ac0_class plus_class posDivAlg power power_class",

"pred_nat prod_case prod_fun prod_rec prod_rec_set product_type",

"prop pttrn pttrns quorem quotient ran range refl",

"reflexive rel_comp remdups replicate restrict_map rev ring",

"ring_class ringpower ringpower_class rtrancl same_fst semiring",

"semiring_class set setprod setsum single_valued size snd",

"sort split string struct sublist sum_case sum_rec",

"sum_rec_set sumbool sumbool_case sumbool_rec sumbool_rec_set",

"sumbool_rep_set surj sym take takeWhile the tid times",

"times_ac1 times_ac1_class times_class tl trancl trans",

"tuple_args tvar type type_class type_definition types uminus",

"unit unit_case unit_rec unit_rec_set upd_fst upd_snd update",

"updates updbind updbinds uprod upt upto usum var vimage",

"wellorder wellorder_class wf wfrec wfrec_rel xnum xstr",

"zero zero_class zip {} ~=>"

]