Skip to content

Commit 74f0a51

Browse files
yutakangyutakang
yutakang
authored and
yutakang
committed
Merge branch 'master' of github.com:data61/PSL
2 parents b8ae4a9 + 85c4097 commit 74f0a51

23 files changed

Lines changed: 2258 additions & 26 deletions

‎Example/Kaiserslautern.thy‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -17,8 +17,8 @@ fun rev2::"'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
1717
strategy CDInd = Thens [Conjecture, Fastforce, Quickcheck,
1818
Dynamic (Induct), Auto, IsSolved]
1919

20-
lemma "rev2 xs [] = rev1 xs"
21-
find_proof CDInd
22-
oops
20+
lemma assumes "True = True"
21+
shows "rev2 xs [] = rev1 xs"
22+
oops
2323

2424
end

‎PSL/Dynamic_Tactic_Generation.ML‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -633,8 +633,8 @@ fun get_fact_names_mesh (state: Proof.state) =
633633
val keywords = Thy_Header.get_keywords' context: Keyword.keywords;
634634
val rule_table = Sledgehammer_Fact.clasimpset_rule_table_of context
635635
: ATP_Problem_Generate.status Termtab.table;
636-
val all_facts = Sledgehammer_Fact.all_facts context true true keywords [] facts rule_table
637-
: Sledgehammer_Fact.raw_fact list;
636+
val all_facts = Sledgehammer_Fact.all_facts context true keywords [] facts rule_table
637+
: Sledgehammer_Fact.lazy_fact list;
638638
val no_override = Sledgehammer_Fact.no_fact_override: Sledgehammer_Fact.fact_override;
639639
val relevant_facts : (string * Sledgehammer_MaSh.fact list) list =
640640
Sledgehammer_MaSh.relevant_facts context params (hd provers) 200 no_override hyps cncl all_facts;

‎PaMpeR/PaMpeR_Interface.ML‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ val path_to_rtree = path ^ "/regression_trees.txt";
3030
val all_method_names =
3131
let
3232
val bash_script = "while read line; do echo -e \"$line\n\"; done <" ^ path_to_meth_names : string;
33-
val bash_input = Bash.process bash_script |> #out : string;
33+
val bash_input = Isabelle_System.bash_output bash_script |> fst : string;
3434
val dist_meth_names = bash_input |> String.tokens (fn c => c = #"\n") |> distinct (op =);
3535
in
3636
dist_meth_names : string list

‎README.md‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,26 +1,26 @@
11
# News
2-
- We updated this repository to Isabelle2021.
2+
- We updated this repository to Isabelle2021-1.
33
- LiFtEr and Smart_Induct are no-longer supported, since their successors, SeLFiE and sem_ind, have shown superior performance.
44
- This is the development version of PSL, PaMpeR, SeLFiE, and sem_ind where we try out possibly immature ideas. In case you find problems, please send your feedback.
5-
- The main developer of this repository, Yutaka Ng, has taken a full-time position for the [SuSLik](https://github.com/TyGuS/suslik) project at Yale-NUS, and he will work on [PSL and all that](https://github.com/data61/PSL/) only in his spare time. Therefore, the progress of this project, unfortunately, will be slow for the foreseeable future. In case you find problems and requests about data61/PSL, contact Yutaka Ng (email: yutaka.nagashima@cvut.cz, twitter: [YutakangE](https://twitter.com/YutakangE)).
5+
- The main developer of this repository, Yutaka Ng, has taken a full-time position for the [SuSLik](https://github.com/TyGuS/suslik) project at Yale-NUS, and he will work on [PSL and all that](https://github.com/data61/PSL/) only in his spare time. Therefore, the progress of this project, unfortunately, will be slow for the foreseeable future. In case you find problems and requests about data61/PSL, contact Yutaka Ng (email: yutaka.nagashima@student.uibk.ac.at, twitter: [YutakangE](https://twitter.com/YutakangE)).
66

77
# Smart_Isabelle
88

99
This repository contains various tools to support interactive theorem proving in Isabelle/HOL using artificial intelligence.
1010
This repository contains the implementation of *proof strategy language (PSL)* and its default strategy,
11-
**try_hard**, for [Isabelle20**21**](https://isabelle.in.tum.de). Past versions of Isabelle, such as Isabelle2019, are no longer supported.
11+
**try_hard**, for [Isabelle20**21-1**](https://isabelle.in.tum.de). Past versions of Isabelle, such as Isabelle2019, are no longer supported.
1212

1313
## YouTube
1414

1515
We opened [a YouTube channel](https://www.youtube.com/channel/UCjnY6hIaryOEgG92udvogAw/) to introduce aspects of this project.
1616

1717
## Installation (of SeLFiE, PaMpeR, PSL, and sem_ind in one go)
18-
1. Install [Isabelle2021](https://isabelle.in.tum.de).
18+
1. Install [Isabelle2021-1](https://isabelle.in.tum.de).
1919
2. Download or clone this repository (git clone https://github.com/data61/PSL.git).
2020
3. Open Isabelle/jEdit with PSL and all that. You can do this by opening Isabelle/jEdit as following:
2121
* `(path to the Isabelle binary)isabelle jedit -d (path to the directory that contains this README file) -l Smart_Isabelle`
2222
* If you are a MacOS user and your current directory is this one with this README.md, probably you should type something like this in Terminal:
23-
* `/Applications/Isabelle2021.app/bin/isabelle jedit -d . -l Smart_Isabelle`
23+
* `/Applications/Isabelle2021-1.app/bin/isabelle jedit -d . -l Smart_Isabelle`
2424
4. Then, You can use SeLFiE/PaMpeR/PSL/LiFtEr/Smart_Induct to your theory files
2525
with the Isabelle keyword, **imports** as ``imports "Smart_Isabelle.Smart_Isabelle"``.
2626
5. Open `Example/Example.thy` to see if the installation is successful.
@@ -79,4 +79,4 @@ We also plan to improve the proof automation using evolutionary computation. We
7979
- a PSL example
8080
![Screenshot](./image/screen_shot_tall.png)
8181
- a PGT example
82-
![Screenshot](./image/screen_shot_pgt.png)
82+
![Screenshot](./image/screen_shot_pgt.png)

‎SeLFiE/Example/afp-2020-05-16/thys/Isabelle_C/C11-FrontEnd/document/DOF-COL.sty‎

Lines changed: 0 additions & 1 deletion
This file was deleted.

‎SeLFiE/Example/afp-2020-05-16/thys/Isabelle_C/C11-FrontEnd/document/DOF-COL.sty‎

Lines changed: 98 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,98 @@
1+
%% Copyright (C) 2018 The University of Sheffield
2+
%% 2018 The University of Paris-Sud
3+
%% 2019 The University of Exeter
4+
%%
5+
%% License:
6+
%% This program can be redistributed and/or modified under the terms
7+
%% of the LaTeX Project Public License Distributed from CTAN
8+
%% archives in directory macros/latex/base/lppl.txt; either
9+
%% version 1 of the License, or any later version.
10+
%% OR
11+
%% The 2-clause BSD-style license.
12+
%%
13+
%% SPDX-License-Identifier: LPPL-1.0+ OR BSD-2-Clause
14+
15+
\NeedsTeXFormat{LaTeX2e}\relax
16+
\ProvidesPackage{DOF-COL}
17+
[0000/00/00 Unreleased v0.0.0+%
18+
Document-Type Support Framework for Isabelle.]
19+
20+
\RequirePackage{DOF-core}
21+
22+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
23+
% begin: figure*
24+
\NewEnviron{isamarkupfigure*}[1][]{\isaDof[env={figure},#1]{\BODY}}
25+
\newisadof{figure.Isa_COL.figure}%
26+
[label=,type=%
27+
,Isa_COL.figure.relative_width=%
28+
,Isa_COL.figure.placement=%
29+
,Isa_COL.figure.src=%
30+
,Isa_COL.figure.spawn_columns=enum False True%
31+
][1]{%
32+
\begin{figure}[]
33+
\centering
34+
\ifcommandkey{Isa_COL.figure.relative_width}
35+
{%
36+
\gdef\dof@width{\commandkey{Isa_COL.figure.relative_width}}
37+
\gdef\dof@src{\commandkey{Isa_COL.figure.src}}
38+
\FPdiv\scale{\dof@width}{100}%
39+
\includegraphics[width=\scale\textwidth]{\dof@src}%
40+
}{%
41+
\gdef\dof@src{\commandkey{Isa_COL.figure.src}}
42+
\includegraphics[]{\dof@src}%
43+
}
44+
\caption{#1}\label{\commandkey{label}}%
45+
\end{figure}
46+
}
47+
% end: figure*
48+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
49+
50+
51+
52+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
53+
% begin: side_by_side_figure*
54+
\NewEnviron{isamarkupsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigure*}[1][]{\isaDof[env={side_by_side_figure},#1]{\BODY}}
55+
\newisadof{side_by_side_figure.Isa_COL.side_by_side_figure}%
56+
[label=,type=%
57+
,Isa_COL.figure.relative_width=%
58+
,Isa_COL.figure.src=%
59+
,Isa_COL.side_by_side_figure.anchor=%
60+
,Isa_COL.side_by_side_figure.caption=%
61+
,Isa_COL.side_by_side_figure.relative_width2=%
62+
,Isa_COL.side_by_side_figure.src2=%
63+
,Isa_COL.side_by_side_figure.anchor2=%
64+
,Isa_COL.side_by_side_figure.caption2=%
65+
,Isa_COL.side_by_side_figure.placement=%
66+
,Isa_COL.figure.spawn_columns=enum False True%
67+
][1]{%
68+
\begin{figure}[]
69+
\subfloat[\label{\commandkey{Isa_COL.side_by_side_figure.anchor}}\commandkey{Isa_COL.side_by_side_figure.caption}]%
70+
{\ifcommandkey{Isa_COL.figure.relative_width}%
71+
{%
72+
\gdef\dof@width{\commandkey{Isa_COL.figure.relative_width}}
73+
\gdef\dof@src{\commandkey{Isa_COL.figure.src}}
74+
\FPdiv\scale{\dof@width}{100}%
75+
\includegraphics[width=\scale\textwidth]{\dof@src}%
76+
}{%
77+
\gdef\dof@src{\commandkey{Isa_COL.figure.src}}
78+
\includegraphics[]{\dof@src}%
79+
}%
80+
}%
81+
\hfill%
82+
\subfloat[\label{\commandkey{Isa_COL.side_by_side_figure.anchor2}}\commandkey{Isa_COL.side_by_side_figure.caption2}]%
83+
{\ifcommandkey{Isa_COL.side_by_side_figure.relative_width2}%
84+
{%
85+
\gdef\dof@width{\commandkey{Isa_COL.side_by_side_figure.relative_width2}}
86+
\gdef\dof@src{\commandkey{Isa_COL.side_by_side_figure.src2}}
87+
\FPdiv\scale{\dof@width}{100}%
88+
\includegraphics[width=\scale\textwidth]{\dof@src}%
89+
}{%
90+
\gdef\dof@src{\commandkey{Isa_COL.side_by_side_figure.src2}}
91+
\includegraphics[]{\dof@src}%
92+
}%
93+
}%
94+
\caption{#1}\label{\commandkey{label}}%
95+
\end{figure}
96+
}
97+
% end: side_by_side_figure*
98+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

‎SeLFiE/Example/afp-2020-05-16/thys/Isabelle_C/C11-FrontEnd/document/DOF-core.sty‎

Lines changed: 0 additions & 1 deletion
This file was deleted.

‎SeLFiE/Example/afp-2020-05-16/thys/Isabelle_C/C11-FrontEnd/document/DOF-core.sty‎

Lines changed: 135 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,135 @@
1+
%% Copyright (C) 2018 The University of Sheffield
2+
%% 2018 The University of Paris-Sud
3+
%% 2019 The University of Exeter
4+
%%
5+
%% License:
6+
%% This program can be redistributed and/or modified under the terms
7+
%% of the LaTeX Project Public License Distributed from CTAN
8+
%% archives in directory macros/latex/base/lppl.txt; either
9+
%% version 1 of the License, or any later version.
10+
%% OR
11+
%% The 2-clause BSD-style license.
12+
%%
13+
%% SPDX-License-Identifier: LPPL-1.0+ OR BSD-2-Clause
14+
15+
\NeedsTeXFormat{LaTeX2e}\relax
16+
\ProvidesPackage{DOF-core}
17+
[0000/00/00 Unreleased v0.0.0+%
18+
Document-Type Support Framework for Isabelle.]
19+
20+
\RequirePackage{keycommand}
21+
\RequirePackage{environ}
22+
\RequirePackage{graphicx}
23+
\RequirePackage{xspace}
24+
\RequirePackage{etoolbox}
25+
\RequirePackage{fp}
26+
27+
\newcommand{\isadof}{Isabelle/DOF\xspace}
28+
29+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
30+
% begin: newcommand wrapper
31+
\newcommand\newisadof[1]{\expandafter\newkeycommand\csname isaDof.#1\endcsname}%
32+
\newcommand\renewisadof[1]{\expandafter\renewkeycommand\csname isaDof.#1\endcsname}%
33+
\newcommand\provideisadof[1]{\expandafter\providekeycommand\csname isaDof.#1\endcsname}%
34+
% end: newcommand wrapper
35+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
36+
37+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
38+
% begin: generic dispatcher
39+
\newkeycommand+[\|]\isaDof[env={UNKNOWN},label=,type={dummyT},args={}][1]{%
40+
\ifcsname isaDof.\commandkey{type}\endcsname%
41+
\csname isaDof.\commandkey{type}\endcsname%
42+
[label=\commandkey{label},\commandkey{args}]{#1}%
43+
\else\relax\fi%
44+
\ifcsname isaDof.\commandkey{env}.\commandkey{type}\endcsname%
45+
\csname isaDof.\commandkey{env}.\commandkey{type}\endcsname%
46+
[label=\commandkey{label},\commandkey{args}]{#1}%
47+
\else%
48+
\message{Isabelle/DOF: Using default LaTeX representation for concept %
49+
"\commandkey{env}.\commandkey{type}".}%
50+
\ifcsname isaDof.\commandkey{env}\endcsname%
51+
\csname isaDof.\commandkey{env}\endcsname%
52+
[label=\commandkey{label}]{#1}%
53+
\else%
54+
\errmessage{Isabelle/DOF: No LaTeX representation for concept %
55+
"\commandkey{env}.\commandkey{type}" defined and no default %
56+
definition for "\commandkey{env}" available either.}%
57+
\fi%
58+
\fi%
59+
}
60+
% end: generic dispatcher
61+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
62+
63+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
64+
% begin: text*-dispatcher
65+
\NewEnviron{isamarkuptext*}[1][]{\isaDof[env={text},#1]{\BODY}}
66+
% end: text*-dispatcher
67+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
68+
69+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
70+
% begin: chapter*-dispatcher
71+
\NewEnviron{isamarkupchapter*}[1][]{\isaDof[env={chapter},#1]{\BODY}}
72+
% end: chapter*-dispatcher
73+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
74+
75+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
76+
% begin: section*-dispatcher
77+
\NewEnviron{isamarkupsection*}[1][]{\isaDof[env={section},#1]{\BODY}}
78+
% end: section*-dispatcher
79+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
80+
81+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
82+
% begin: subsection*-dispatcher
83+
\NewEnviron{isamarkupsubsection*}[1][]{\isaDof[env={subsection},#1]{\BODY}}
84+
% end: subsection*-dispatcher
85+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
86+
87+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
88+
% begin: subsubsection*-dispatcher
89+
\NewEnviron{isamarkupsubsubsection*}[1][]{\isaDof[env={subsubsection},#1]{\BODY}}
90+
% end: subsubsection*-dispatcher
91+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92+
93+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
94+
% begin: paragraph*-dispatcher
95+
\NewEnviron{isamarkupparagraph*}[1][]{\isaDof[env={paragraph},#1]{\BODY}}
96+
% end: paragraph*-dispatcher
97+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
98+
99+
100+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
101+
% begin: text default implementation
102+
\newisadof{text}[label=,type=][1]{%
103+
\begin{isamarkuptext}\label{\commandkey{label}}%
104+
#1
105+
\end{isamarkuptext}%
106+
}
107+
% end: text default implementation
108+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
109+
110+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
111+
% begin: chapter/section default implementations
112+
\newisadof{chapter}[label=,type=][1]{%
113+
\isamarkupfalse\isamarkupchapter{#1}\label{\commandkey{label}}\isamarkuptrue%
114+
}
115+
\newisadof{section}[label=,type=][1]{%
116+
\isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue%
117+
}
118+
\newisadof{subsection}[label=,type=][1]{%
119+
\isamarkupfalse\isamarkupsubsection{#1}\label{\commandkey{label}}\isamarkuptrue%
120+
}
121+
\newisadof{subsubsection}[label=,type=][1]{%
122+
\isamarkupfalse\isamarkupsubsubsection{#1}\label{\commandkey{label}}\isamarkuptrue%
123+
}
124+
\newisadof{paragraph}[label=,type=][1]{%
125+
\isamarkupfalse\isamarkupparagraph{#1}\label{\commandkey{label}}\isamarkuptrue%
126+
}
127+
% end: chapter/section default implementations
128+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
129+
130+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
131+
% begin: label and ref
132+
\newisadof{label}[label=,type=][1]{\label{#1}}
133+
\newisadof{ref}[label=,type=][1]{\autoref{#1}}
134+
% end: label and ref
135+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

‎SeLFiE/Example/afp-2020-05-16/thys/Isabelle_C/C11-FrontEnd/document/DOF-scholarly_paper.sty‎

Lines changed: 0 additions & 1 deletion
This file was deleted.

0 commit comments

Comments
 (0)