This file is indexed.

/usr/share/hol88-2.02.19940316/Library/trs/user.ml is in hol88-library-source 2.02.19940316-15.

This file is owned by root:root, with mode 0o644.

The actual contents of the file can be viewed below.

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
% user.ml                                               (c) R.J.Boulton 1990 %
%----------------------------------------------------------------------------%


% Abbreviation for `find_theorems' %

let FT = find_theorems;;

   % : (thmpattern -> source -> searchstep) %


% Abbreviation for `continue_search' %

let CS = continue_search;;

   % : (searchstep -> searchstep) %


% Function to complete a stepwise search in one step %

% This function repeatedly attempts to continue a search, until this fails  %
% because there are no more theories to search. When this happens, the list %
% of theorems found during the search is extracted and returned as result.  %

letrec run_search srchstp =

   % : (searchstep -> foundthm list) %

   (  (run_search (continue_search srchstp))
   ?? [`continue_search`] (show_step srchstp)
   );;


% Function to perform a search in a single step %

% Given a pattern and a source, this function searches the source in one %
% step, and returns a list of theorems which match the pattern.          %

let full_search thmp src = run_search (find_theorems thmp src);;

   % : (thmpattern -> source -> foundthm list) %


% Function to continue a search until a match is found %

% If the found theorem list of the searchstep given is empty, the search is %
% continued. The evaluation will fail if no theorems are found before the   %
% list of theories to search is exhausted.                                  %

letrec search_until_find srchstp =

   % : (searchstep -> searchstep) %

   if (null o show_step) srchstp
   then (search_until_find o continue_search) srchstp
   else srchstp;;


% Function to continue with a search for a number of steps %

% If n is greater than zero, and the end of the search has not been reached, %
% the search is continued.                                                   %

letrec search_n_theories n srchstp =

   % : (int -> searchstep -> searchstep) %

   if (n < 1)
   then srchstp
   else case srchstp
        of (Endofsearch _) . srchstp
         | (Step _) . (search_n_theories (n-1) (continue_search srchstp));;


% Function to continue with a search for a number of steps, or until a %
% theorem is found.                                                    %

% If n is greater than zero, and the searchstep given does not contain any %
% theorems, the search is continued.                                       %

letrec search_n_until_find n srchstp =

   % : (int -> searchstep -> searchstep) %

   if (n > 0) & ((null o show_step) srchstp)
   then (search_n_until_find (n-1) (continue_search srchstp))
   else srchstp;;


%----------------------------------------------------------------------------%


% Function to allow a user to set up a constructor equivalent to `Ancestors' %
% but with the a default value for the exclusion list.                       %

let ancestors_excluding exclusions ancestors =

   % : (string list -> string list -> searchpath) %

   Ancestors (ancestors,exclusions);;


% `Ancestry' is an example of the use of `ancestors_excluding' and is likely %
% to be the most useful default exclusion.                                   %

let Ancestry = ancestors_excluding [`HOL`];;


% Function to make a `source' of the form `List ...' from a `searchstep' %

% The `foundthm list' is extracted from the `searchstep', and then `List' is %
% applied to it.                                                             %

let List_from srchstp =

   % : (searchstep -> source) %

   (List o show_step) srchstp;;


%----------------------------------------------------------------------------%


% Functions which can be used in place of certain `thmpattern' constructors, %
% so that the arguments can be given as the representing types of abstract   %
% types rather than as the abstract types themselves.                        %

% `kind' and `side' are only included for consistency. %

let kind = Kind

   % : (thmkind -> thmpattern) %

and thryname = Thryname o autonamepattern

   % : (string -> thmpattern) %

and thmname = Thmname o autonamepattern

   % : (string -> thmpattern) %

and conc = Conc o autotermpattern

   % : (term -> thmpattern) %

and hypP = HypP o (map autotermpattern)

   % : (term list -> thmpattern) %

and hypF = HypF o (map autotermpattern)

   % : (term list -> thmpattern) %

and side = Side;;

   % : (side_condition -> thmpattern) %


%----------------------------------------------------------------------------%


% `BigAnd' is an additional thmpattern constructor, useful when large %
% numbers of thmpatterns are to be ANDed together.                    %

letrec BigAnd thmpl =

   % : (thmpattern list -> thmpattern) %

   if (null thmpl)
   then failwith `BigAnd -- null list prohibited`
   else if (null (tl thmpl))
        then (hd thmpl)
        else ((hd thmpl) Andalso (BigAnd (tl thmpl)));;


% `BigOr' is an additional thmpattern constructor, useful when large %
% numbers of thmpatterns are to be ORed together.                    %

letrec BigOr thmpl =

   % : (thmpattern list -> thmpattern) %

   if (null thmpl)
   then failwith `BigOr -- null list prohibited`
   else if (null (tl thmpl))
        then (hd thmpl)
        else ((hd thmpl) Orelse (BigOr (tl thmpl)));;


%----------------------------------------------------------------------------%