%
\begin{isabellebody}%
\setisabellecontext{FCTactics}%
%
\isamarkupsection{Tactics%
}
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ FCTactics\isanewline
\isakeyword{imports}\ FranklImpl\ SomeShareNegativeImpl\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
%
\isadelimML
\isanewline
%
\endisadelimML
%
\isatagML
\isacommand{ML{\isacharunderscore}file}\isamarkupfalse%
\ {\isachardoublequoteopen}eval{\isacharunderscore}tac{\isachardot}ML{\isachardoublequoteclose}%
\endisatagML
{\isafoldML}%
%
\isadelimML
%
\endisadelimML
%
\isamarkupsubsection{Tactics for verifying FC families%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Tactic relies on applying the \isa{SomeShareNegativeImpl{\isachardot}some{\isacharunderscore}share{\isacharunderscore}negative} function.%
\end{isamarkuptext}\isamarkuptrue%
%
\isadelimML
%
\endisadelimML
%
\isatagML
\isacommand{ML}\isamarkupfalse%
{\isacharverbatimopen}\isanewline
fun\ FC{\isacharunderscore}family{\isacharunderscore}uce{\isacharunderscore}shares{\isacharunderscore}nonneg{\isacharunderscore}inst\ w\ {\isacharequal}\isanewline
\ Thm{\isachardot}instantiate{\isacharprime}\ \isanewline
\ \ \ \ \ {\isacharbrackleft}SOME\ %
\isaantiq
ctyp\ {\isachardoublequote}nat{\isachardoublequote}{}%
\endisaantiq
{\isacharbrackright}\isanewline
\ \ \ \ \ {\isacharbrackleft}SOME\ {\isacharparenleft}Thm{\isachardot}cterm{\isacharunderscore}of\ %
\isaantiq
context{}%
\endisaantiq
\ w{\isacharparenright}{\isacharbrackright}\isanewline
\ \ \ \ \ %
\isaantiq
thm\ FC{\isacharunderscore}family{\isacharunderscore}uce{\isacharunderscore}shares{\isacharunderscore}nonneg{}%
\endisaantiq
{\isacharsemicolon}\isanewline
\isanewline
fun\ SomeShareNegativeSound{\isacharunderscore}nats{\isacharunderscore}inst\ A\ A{\isacharprime}\ w\ w{\isacharprime}\ {\isacharequal}\isanewline
\ Thm{\isachardot}instantiate{\isacharprime}\ \isanewline
\ \ \ \ {\isacharbrackleft}{\isacharbrackright}\isanewline
\ \ \ \ {\isacharparenleft}map\ {\isacharparenleft}fn\ x\ {\isacharequal}{\isachargreater}\ SOME\ {\isacharparenleft}Thm{\isachardot}cterm{\isacharunderscore}of\ %
\isaantiq
context{}%
\endisaantiq
\ x{\isacharparenright}{\isacharparenright}\ {\isacharbrackleft}A{\isacharcomma}\ A{\isacharprime}{\isacharcomma}\ w{\isacharprime}{\isacharcomma}\ w{\isacharbrackright}{\isacharparenright}\ %
\isaantiq
thm\ some{\isacharunderscore}share{\isacharunderscore}negative{\isacharunderscore}soundness{\isacharunderscore}nats{}%
\endisaantiq
{\isacharsemicolon}\isanewline
\isanewline
fun\ fc{\isacharunderscore}family{\isacharunderscore}tac\ ctx\ A\ Al\ wl\ \ {\isacharequal}\ \isanewline
\ \ let\isanewline
\ \ \ \ val\ term{\isacharunderscore}zip\ {\isacharequal}\ %
\isaantiq
term\ {\isachardoublequote}{\isacharparenleft}zip{\isacharcolon}{\isacharcolon}{\isacharparenleft}nat\ list\ {\isasymRightarrow}\ nat\ list\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymtimes}\ nat{\isacharparenright}\ list{\isacharparenright}{\isacharparenright}\ {\isacharbrackleft}{\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}{\isadigit{6}}{\isacharcolon}{\isacharcolon}nat{\isacharbrackright}{\isachardoublequote}{}%
\endisaantiq
\isanewline
\ \ \ \ val\ term{\isacharunderscore}weights{\isadigit{2}}map\ {\isacharequal}\ %
\isaantiq
term\ {\isachardoublequote}weights{\isadigit{2}}map{\isacharcolon}{\isacharcolon}{\isacharparenleft}nat\ {\isasymtimes}\ nat{\isacharparenright}\ list\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}{}%
\endisaantiq
{\isacharsemicolon}\isanewline
\ \ \ \ val\ term{\isacharunderscore}sls\ {\isacharequal}\ %
\isaantiq
term\ {\isachardoublequote}sorted{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}set{\isacharcolon}{\isacharcolon}nat\ set{\isasymRightarrow}nat\ list{\isachardoublequote}{}%
\endisaantiq
{\isacharsemicolon}\isanewline
\ \ \ \ val\ term{\isacharunderscore}tabulate\ {\isacharequal}\ %
\isaantiq
term\ {\isachardoublequote}Mapping{\isachardot}tabulate{\isacharcolon}{\isacharcolon}nat\ list\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}nat{\isacharcomma}\ nat{\isacharparenright}\ mapping{\isachardoublequote}{}%
\endisaantiq
{\isacharsemicolon}\isanewline
\ \ \ \ val\ term{\isacharunderscore}sup\ {\isacharequal}\ %
\isaantiq
term\ {\isachardoublequote}Sup{\isacharcolon}{\isacharcolon}{\isacharparenleft}nat\ set\ set{\isasymRightarrow}nat\ set{\isacharparenright}{\isachardoublequote}{}%
\endisaantiq
{\isacharsemicolon}\isanewline
\isanewline
\ \ \ \ val\ w\ {\isacharequal}\ \ term{\isacharunderscore}weights{\isadigit{2}}map\ {\isachardollar}\ {\isacharparenleft}term{\isacharunderscore}zip\ {\isachardollar}\ wl{\isacharparenright}{\isacharsemicolon}\isanewline
\ \ \ \ val\ w{\isacharprime}\ {\isacharequal}\ list{\isacharunderscore}comb\ {\isacharparenleft}term{\isacharunderscore}tabulate{\isacharcomma}\ {\isacharbrackleft}term{\isacharunderscore}sls\ {\isachardollar}\ {\isacharparenleft}term{\isacharunderscore}sup\ {\isachardollar}\ A{\isacharparenright}{\isacharcomma}\ w{\isacharbrackright}{\isacharparenright}{\isacharsemicolon}\isanewline
\ \ in\isanewline
\ \ \ \ \ \ \ \ \ \ resolve{\isacharunderscore}tac\ ctx\ {\isacharbrackleft}FC{\isacharunderscore}family{\isacharunderscore}uce{\isacharunderscore}shares{\isacharunderscore}nonneg{\isacharunderscore}inst\ w{\isacharbrackright}\isanewline
\ \ \ \ THEN{\isacharprime}\ asm{\isacharunderscore}full{\isacharunderscore}simp{\isacharunderscore}tac\ {\isacharparenleft}ctx\ addsimps\ {\isacharbrackleft}%
\isaantiq
thm\ weight{\isacharunderscore}fun{\isacharunderscore}def{}%
\endisaantiq
{\isacharcomma}\ %
\isaantiq
thm\ weights{\isadigit{2}}map{\isacharunderscore}def{}%
\endisaantiq
{\isacharcomma}\ %
\isaantiq
thm\ upt{\isacharunderscore}def{}%
\endisaantiq
{\isacharbrackright}{\isacharparenright}\isanewline
\ \ \ \ THEN{\isacharprime}\ resolve{\isacharunderscore}tac\ ctx\ {\isacharbrackleft}SomeShareNegativeSound{\isacharunderscore}nats{\isacharunderscore}inst\ A\ Al\ w\ w{\isacharprime}{\isacharbrackright}\isanewline
\ \ \ \ THEN{\isacharprime}\ asm{\isacharunderscore}full{\isacharunderscore}simp{\isacharunderscore}tac\ ctx\isanewline
\ \ \ \ THEN{\isacharprime}\ asm{\isacharunderscore}full{\isacharunderscore}simp{\isacharunderscore}tac\ ctx\isanewline
\ \ \ \ THEN{\isacharprime}\ asm{\isacharunderscore}full{\isacharunderscore}simp{\isacharunderscore}tac\ ctx\isanewline
\ \ \ \ THEN{\isacharprime}\ asm{\isacharunderscore}full{\isacharunderscore}simp{\isacharunderscore}tac\ ctx\isanewline
\ \ \ \ THEN{\isacharprime}\ asm{\isacharunderscore}full{\isacharunderscore}simp{\isacharunderscore}tac\ ctx\isanewline
\ \ end\isanewline
{\isacharverbatimclose}%
\endisatagML
{\isafoldML}%
%
\isadelimML
%
\endisadelimML
%
\isamarkupsubsection{Tactics for verifying nonFC families%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Tactic for checking if a family belongs to the union-closed extension of a given family%
\end{isamarkuptext}\isamarkuptrue%
\isacommand{thm}\isamarkupfalse%
\ SetUnionImpl{\isacharunderscore}nats{\isachardot}union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharunderscore}set\isanewline
%
\isadelimML
\isanewline
%
\endisadelimML
%
\isatagML
\isacommand{ML}\isamarkupfalse%
{\isacharverbatimopen}\isanewline
\isanewline
{\isacharparenleft}{\isacharasterisk}\isanewline
fun\ union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharunderscore}tac{\isacharprime}\ ctx\ F\ I\ i\ {\isacharequal}\ \isanewline
\ \ EqSubst{\isachardot}eqsubst{\isacharunderscore}tac\ ctx\ {\isacharbrackleft}{\isadigit{0}}{\isacharbrackright}\ {\isacharbrackleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l{\isacharunderscore}thm\ F{\isacharbrackright}\ i\ THEN\isanewline
\ \ EqSubst{\isachardot}eqsubst{\isacharunderscore}tac\ ctx\ {\isacharbrackleft}{\isadigit{0}}{\isacharbrackright}\ {\isacharbrackleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l{\isacharunderscore}thm\ I{\isacharbrackright}\ i\ \ THEN\isanewline
\ \ resolve{\isacharunderscore}tac\ ctx\ {\isacharbrackleft}%
\isaantiq
thm\ SetUnionImpl{\isacharunderscore}lists{\isachardot}union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharunderscore}set{}%
\endisaantiq
{\isacharbrackright}\ i\ THEN\isanewline
\ \ eval{\isacharunderscore}tac\ ctx\ i\ \isanewline
{\isacharasterisk}{\isacharparenright}\isanewline
\isanewline
fun\ union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharunderscore}tac{\isacharprime}\ ctx\ F\ I\ i\ {\isacharequal}\ \isanewline
\ \ EqSubst{\isachardot}eqsubst{\isacharunderscore}tac\ ctx\ {\isacharbrackleft}{\isadigit{0}}{\isacharbrackright}\ {\isacharbrackleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}n{\isacharunderscore}thm\ F{\isacharbrackright}\ i\ THEN\isanewline
\ \ EqSubst{\isachardot}eqsubst{\isacharunderscore}tac\ ctx\ {\isacharbrackleft}{\isadigit{0}}{\isacharbrackright}\ {\isacharbrackleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}n{\isacharunderscore}thm\ I{\isacharbrackright}\ i\ \ THEN\isanewline
\ \ resolve{\isacharunderscore}tac\ ctx\ {\isacharbrackleft}%
\isaantiq
thm\ SetUnionImpl{\isacharunderscore}nats{\isachardot}union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharunderscore}set{}%
\endisaantiq
{\isacharbrackright}\ i\ THEN\isanewline
\ \ eval{\isacharunderscore}tac\ ctx\ i\isanewline
\isanewline
\isanewline
fun\ union{\isacharunderscore}closed{\isacharunderscore}tac{\isacharprime}\ ctx\ F\ i\ {\isacharequal}\isanewline
\ \ EqSubst{\isachardot}eqsubst{\isacharunderscore}tac\ ctx\ {\isacharbrackleft}{\isadigit{0}}{\isacharbrackright}\ {\isacharbrackleft}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l{\isacharunderscore}thm\ F{\isacharbrackright}\ i\ THEN\isanewline
\ \ resolve{\isacharunderscore}tac\ ctx\ {\isacharbrackleft}%
\isaantiq
thm\ SetUnionImpl{\isacharunderscore}lists{\isachardot}union{\isacharunderscore}closed{\isacharunderscore}set{}%
\endisaantiq
{\isacharbrackright}\ i\ THEN\isanewline
\ \ eval{\isacharunderscore}tac\ ctx\ i\isanewline
\isanewline
fun\ union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharunderscore}select{\isacharunderscore}tac\ ctx\ {\isacharparenleft}t{\isacharcomma}\ i{\isacharparenright}\ {\isacharequal}\isanewline
\ \ case\ t\ of\isanewline
\ \ \ \ %
\isaantiq
term\ {\isachardoublequote}Trueprop{\isachardoublequote}{}%
\endisaantiq
\ {\isachardollar}\ t{\isacharprime}\ {\isacharequal}{\isachargreater}\ union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharunderscore}select{\isacharunderscore}tac\ ctx\ {\isacharparenleft}t{\isacharprime}{\isacharcomma}\ i{\isacharparenright}\isanewline
\ \ {\isacharbar}\ %
\isaantiq
term\ {\isachardoublequote}UnionClosed{\isachardot}union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharcolon}{\isacharcolon}nat\ set\ set\ {\isasymRightarrow}\ nat\ set\ set\ {\isasymRightarrow}\ bool{\isachardoublequote}{}%
\endisaantiq
\ {\isachardollar}\ F\ {\isachardollar}\ I\ {\isacharequal}{\isachargreater}\ union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharunderscore}tac{\isacharprime}\ ctx\ F\ I\ i\isanewline
\ \ {\isacharbar}\ {\isacharunderscore}\ {\isacharequal}{\isachargreater}\ raise\ Fail\ {\isacharparenleft}{\isachardoublequote}select{\isacharunderscore}tac{\isacharcolon}\ pattern\ not\ matched{\isachardoublequote}{\isacharparenright}\isanewline
\isanewline
fun\ union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharunderscore}tac\ ctx\ i\ {\isacharequal}\ \isanewline
\ \ SUBGOAL\ {\isacharparenleft}union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharunderscore}select{\isacharunderscore}tac\ ctx{\isacharparenright}\ i\isanewline
\isanewline
fun\ union{\isacharunderscore}closed{\isacharunderscore}select{\isacharunderscore}tac\ ctx\ {\isacharparenleft}t{\isacharcomma}\ i{\isacharparenright}\ {\isacharequal}\isanewline
\ \ case\ t\ of\isanewline
\ \ \ \ %
\isaantiq
term\ {\isachardoublequote}Trueprop{\isachardoublequote}{}%
\endisaantiq
\ {\isachardollar}\ t{\isacharprime}\ {\isacharequal}{\isachargreater}\ union{\isacharunderscore}closed{\isacharunderscore}select{\isacharunderscore}tac\ ctx\ {\isacharparenleft}t{\isacharprime}{\isacharcomma}\ i{\isacharparenright}\isanewline
\ \ {\isacharbar}\ %
\isaantiq
term\ {\isachardoublequote}UnionClosed{\isachardot}union{\isacharunderscore}closed{\isacharcolon}{\isacharcolon}nat\ set\ set\ {\isasymRightarrow}\ bool{\isachardoublequote}{}%
\endisaantiq
\ {\isachardollar}\ F\ {\isacharequal}{\isachargreater}\ union{\isacharunderscore}closed{\isacharunderscore}tac{\isacharprime}\ ctx\ F\ i\isanewline
\ \ {\isacharbar}\ {\isacharunderscore}\ {\isacharequal}{\isachargreater}\ raise\ Fail\ {\isacharparenleft}{\isachardoublequote}select{\isacharunderscore}tac{\isacharcolon}\ pattern\ not\ matched{\isachardoublequote}{\isacharparenright}\isanewline
\isanewline
fun\ union{\isacharunderscore}closed{\isacharunderscore}tac\ ctx\ i\ {\isacharequal}\ \isanewline
\ \ SUBGOAL\ {\isacharparenleft}union{\isacharunderscore}closed{\isacharunderscore}select{\isacharunderscore}tac\ ctx{\isacharparenright}\ i\isanewline
\isanewline
fun\ union{\isacharunderscore}closed{\isacharunderscore}extension{\isacharunderscore}tac\ ctx\ {\isacharequal}\ \isanewline
\ \ rewrite{\isacharunderscore}goals{\isacharunderscore}tac\ ctx\ {\isacharbrackleft}%
\isaantiq
thm\ union{\isacharunderscore}closed{\isacharunderscore}extensions{\isacharunderscore}def{}%
\endisaantiq
{\isacharbrackright}\ THEN\isanewline
\ \ EqSubst{\isachardot}eqsubst{\isacharunderscore}tac\ ctx\ {\isacharbrackleft}{\isadigit{0}}{\isacharbrackright}\ {\isacharbrackleft}%
\isaantiq
thm\ mem{\isacharunderscore}Collect{\isacharunderscore}eq{}%
\endisaantiq
{\isacharbrackright}\ {\isadigit{1}}\ THEN\ \isanewline
\ \ resolve{\isacharunderscore}tac\ ctx\ {\isacharbrackleft}%
\isaantiq
thm\ conjI{}%
\endisaantiq
{\isacharbrackright}\ {\isadigit{1}}\ THEN\ \isanewline
\ \ union{\isacharunderscore}closed{\isacharunderscore}additional{\isacharunderscore}tac\ ctx\ {\isadigit{2}}\ THEN\isanewline
\ \ auto{\isacharunderscore}tac\ ctx\isanewline
{\isacharverbatimclose}%
\endisatagML
{\isafoldML}%
%
\isadelimML
%
\endisadelimML
%
\begin{isamarkuptext}%
Tactic for checking if the given coefficients c satisfy the given system of 
   inequalities determined by the given families Fs%
\end{isamarkuptext}\isamarkuptrue%
%
\begin{isamarkuptext}%
Lemma that allows to reformulate the statement as a problem over lists and gain faster 
   executability.%
\end{isamarkuptext}\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
\ nonFC{\isacharunderscore}is{\isacharunderscore}system{\isacharunderscore}solution{\isacharunderscore}lists{\isacharcolon}\isanewline
\ \ \isakeyword{assumes}\ {\isachardoublequoteopen}Fs\ {\isacharequal}\ map\ f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l\ Fs{\isacharunderscore}l{\isachardoublequoteclose}\ {\isachardoublequoteopen}set\ Fc{\isacharunderscore}l\ {\isacharequal}\ {\isasymUnion}\ Fc{\isachardoublequoteclose}\ \ {\isachardoublequoteopen}{\isasymforall}\ F\ {\isasymin}\ set\ Fs{\isacharunderscore}l{\isachardot}\ distinct\ F{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymforall}\ F\ {\isasymin}\ set\ Fs{\isacharunderscore}l{\isachardot}\ {\isasymforall}\ A\ {\isasymin}\ set\ F{\isachardot}\ sorted\ A\ {\isasymand}\ distinct\ A{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}let\ Fs{\isacharprime}\ {\isacharequal}\ Fs\ in\ {\isasymforall}\ a\ {\isasymin}\ {\isasymUnion}\ Fc{\isachardot}\ sum{\isacharunderscore}list\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ int\ x\ {\isacharasterisk}\ y{\isacharparenright}\ {\isacharparenleft}zip\ c\ {\isacharparenleft}map\ {\isacharparenleft}Frankl{\isachardot}frankl{\isacharunderscore}fun\ a{\isacharparenright}\ Fs{\isacharprime}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharless}\ {\isadigit{0}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
\ \ \ \ \ \ \ \ \ {\isacharparenleft}list{\isacharunderscore}all\ {\isacharparenleft}{\isasymlambda}\ a{\isachardot}\ sum{\isacharunderscore}list\ {\isacharparenleft}map\ {\isacharparenleft}{\isasymlambda}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ int\ x\ {\isacharasterisk}\ y{\isacharparenright}\ {\isacharparenleft}zip\ c\ {\isacharparenleft}map\ {\isacharparenleft}frankl{\isacharunderscore}fun{\isacharunderscore}l\ a{\isacharparenright}\ Fs{\isacharunderscore}l{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharless}\ {\isadigit{0}}{\isacharparenright}\ Fc{\isacharunderscore}l{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
{\isacharminus}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymforall}\ a{\isachardot}\ map\ {\isacharparenleft}Frankl{\isachardot}frankl{\isacharunderscore}fun\ a{\isacharparenright}\ Fs\ {\isacharequal}\ map\ {\isacharparenleft}frankl{\isacharunderscore}fun{\isacharunderscore}l\ a{\isacharparenright}\ Fs{\isacharunderscore}l{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms\ SetImpl{\isacharunderscore}lists{\isachardot}frankl{\isacharunderscore}fun{\isacharunderscore}set\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ count{\isacharunderscore}l{\isacharunderscore}def{\isacharparenright}\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
\ {\isacharquery}thesis\isanewline
\ \ \ \ \isacommand{using}\isamarkupfalse%
\ assms{\isacharparenleft}{\isadigit{2}}{\isacharparenright}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ list{\isacharunderscore}all{\isacharunderscore}iff\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
%
\isadelimML
\isanewline
%
\endisadelimML
%
\isatagML
\isacommand{ML}\isamarkupfalse%
{\isacharverbatimopen}\isanewline
\isanewline
fun\ nonFC{\isacharunderscore}is{\isacharunderscore}system{\isacharunderscore}solution{\isacharunderscore}tac{\isacharprime}\ ctx\ FF\ Fc{\isacharunderscore}l\ i\ {\isacharequal}\isanewline
let\isanewline
\ \ \ val\ thm\ {\isacharequal}\ %
\isaantiq
thm\ nonFC{\isacharunderscore}is{\isacharunderscore}system{\isacharunderscore}solution{\isacharunderscore}lists{}%
\endisaantiq
\ OF\ {\isacharbrackleft}list{\isacharunderscore}f{\isacharunderscore}to{\isacharunderscore}set{\isacharunderscore}l{\isacharunderscore}thm\ FF{\isacharbrackright}\isanewline
\ \ \ val\ thm\ {\isacharequal}\ Thm{\isachardot}instantiate{\isacharprime}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}SOME\ {\isacharparenleft}Thm{\isachardot}cterm{\isacharunderscore}of\ %
\isaantiq
context{}%
\endisaantiq
\ Fc{\isacharunderscore}l{\isacharparenright}{\isacharbrackright}\ thm\isanewline
in\isanewline
\ \ EqSubst{\isachardot}eqsubst{\isacharunderscore}tac\ ctx\ {\isacharbrackleft}{\isadigit{0}}{\isacharbrackright}\ {\isacharbrackleft}thm{\isacharbrackright}\ i\isanewline
end\isanewline
\isanewline
fun\ nonFC{\isacharunderscore}is{\isacharunderscore}system{\isacharunderscore}solution{\isacharunderscore}tac{\isacharunderscore}select\ ctx\ Fc{\isacharunderscore}l\ {\isacharparenleft}t{\isacharcomma}\ i{\isacharparenright}\ {\isacharequal}\ \isanewline
\ \ case\ t\ of\isanewline
\ \ \ \ \ %
\isaantiq
term\ {\isachardoublequote}Trueprop{\isachardoublequote}{}%
\endisaantiq
\ {\isachardollar}\ t\ {\isacharequal}{\isachargreater}\isanewline
\ \ \ \ \ \ \ \ \ \ \ nonFC{\isacharunderscore}is{\isacharunderscore}system{\isacharunderscore}solution{\isacharunderscore}tac{\isacharunderscore}select\ ctx\ Fc{\isacharunderscore}l\ {\isacharparenleft}t{\isacharcomma}\ i{\isacharparenright}\isanewline
\ \ \ {\isacharbar}\ %
\isaantiq
term\ {\isachardoublequote}HOL{\isachardot}Let\ {\isacharcolon}{\isacharcolon}\ nat\ set\ set\ list\ {\isasymRightarrow}\ {\isacharparenleft}nat\ set\ set\ list\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequote}{}%
\endisaantiq
\ {\isachardollar}\ FF\ {\isachardollar}\ {\isacharunderscore}\ {\isacharequal}{\isachargreater}\isanewline
\ \ \ \ \ \ \ \ \ \ \ nonFC{\isacharunderscore}is{\isacharunderscore}system{\isacharunderscore}solution{\isacharunderscore}tac{\isacharprime}\ ctx\ FF\ Fc{\isacharunderscore}l\ i\isanewline
\ \ \ {\isacharbar}\ {\isacharunderscore}\ {\isachardollar}\ t\ {\isacharequal}{\isachargreater}\ nonFC{\isacharunderscore}is{\isacharunderscore}system{\isacharunderscore}solution{\isacharunderscore}tac{\isacharunderscore}select\ ctx\ Fc{\isacharunderscore}l\ {\isacharparenleft}t{\isacharcomma}\ i{\isacharparenright}\isanewline
\ \ \ {\isacharbar}\ {\isacharunderscore}\ {\isacharequal}{\isachargreater}\ no{\isacharunderscore}tac\isanewline
\isanewline
fun\ nonFC{\isacharunderscore}is{\isacharunderscore}system{\isacharunderscore}solution{\isacharunderscore}tac\ ctx\ Fc{\isacharunderscore}l\ i\ {\isacharequal}\ \isanewline
\ \ SUBGOAL\ {\isacharparenleft}nonFC{\isacharunderscore}is{\isacharunderscore}system{\isacharunderscore}solution{\isacharunderscore}tac{\isacharunderscore}select\ ctx\ Fc{\isacharunderscore}l{\isacharparenright}\ i\ THEN\isanewline
\ \ eval{\isacharunderscore}tac\ ctx\ i\ THEN\isanewline
\ \ eval{\isacharunderscore}tac\ ctx\ i\ THEN\isanewline
\ \ eval{\isacharunderscore}tac\ ctx\ i\ THEN\isanewline
\ \ eval{\isacharunderscore}tac\ ctx\ i\isanewline
{\isacharverbatimclose}%
\endisatagML
{\isafoldML}%
%
\isadelimML
\isanewline
%
\endisadelimML
%
\isadelimtheory
\isanewline
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End:
