ViewVC logotype

Log of /metaprl/theories/itt/itt_int_ext.mli

Parent Directory Parent Directory | Revision Log Revision Log

Sticky Revision:
(Current path doesn't exist after revision 7950)

Revision 3586 - (view) (download) (annotate) - [select for diffs]
Modified Sat Apr 27 01:42:23 2002 UTC (19 years, 1 month ago) by nogin
File length: 9082 byte(s)
Diff to previous 3442
Noop commit - I've only fixed the CRLF/LF mixed line terminators.

Revision 3442 - (view) (download) (annotate) - [select for diffs]
Modified Thu Nov 15 20:25:28 2001 UTC (19 years, 7 months ago) by yegor
File length: 9082 byte(s)
Diff to previous 3329
Itt_int_ext: more conversions added to reduce resource

Itt_int_arih: first working version of arithT!!!
You can observe proof of test rule and try to replace it with just arithT
in the root.
While now arithT knows only numbers, variables and +

Revision 3329 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jul 13 21:34:19 2001 UTC (19 years, 11 months ago) by nogin
File length: 9082 byte(s)
Diff to previous 3257
I've removed old Itt_int* theories and switched all the ITT to Yegor's
new theories.

Revision 3257 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 13 19:32:30 2001 UTC (20 years ago) by kopylov
File length: 9275 byte(s)
Diff to previous 3246
1. I added new primitive rules:

   The last two rules show the differences between pointwise and pairwise functionality.
   They are valid in pointwise functionality (as well as quoationtElimination2).

2. Itt_struct3 contains some rules that derived from these new ones.
   But thesd rules are valid in both functionalities.

3. I moved definition of natural numbers to a new theory Itt_nat.
   To prove induction for natural numbers one needs Itt_struct3.
   I almost proved it (leaving some simple arithmetic subgoals, that should
   be killed by arith)

4. I defined record type.
   Itt_record is a main theory of records.
   Itt_record_exm contains some examples.

5. I add a new conversion
        * applyAllC : conv list -> conv
   that applies all conversions to all subterms and a tactic
        * rwa : conv list -> int -> tactic
        = rw (applyAllC convs)

Revision 3246 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 1 20:57:31 2001 UTC (20 years ago) by kopylov
File length: 9326 byte(s)
Diff to previous 3223
- The theory ctt_markov (Constructive type theory with Markov
  Principle) is added.

- Some definitions and simple facts are added to itt_int_ext

Revision 3223 - (view) (download) (annotate) - [select for diffs]
Modified Tue May 8 23:59:11 2001 UTC (20 years, 1 month ago) by nogin
File length: 9276 byte(s)
Diff to previous 3207
Finally, I am able to commit what I was getting to
in all these commits over the last several days.

I changed the parser to index declared opnames by its "shape" -
last string of opname + parameter types + subterm arities
instead of just the last string (as it used to be). This means that
the parser now checks whether the usage of an opname corresponds
to its declaration. This allowed me to detect numerous typos in
display forms and even some rules and rewrites and, hopefully,
will prevent people from making such typos in the future.

This is only the first pass of the implementation. I still need to:
- make sure none of my fixes broke any display forms that used to work
  because of typos cancelling each other
- update the documentation
- implement checking of shapes on the opnames specified using the
  Module!name notation (currently no checking is done on such opnames)

Revision 3207 - (view) (download) (annotate) - [select for diffs]
Modified Fri May 4 08:45:12 2001 UTC (20 years, 1 month ago) by yegor
File length: 9280 byte(s)
Diff to previous 3163
1.Some minor changes in old files
2.First ugly approach to Arith implementation. It just can find contradiction
  and construct contradictory inequality. Next step will be polynoms and
  inequalities normalization. It will increase range of input inequalities and
  let easily prove resulting contradictory inequality.

Revision 3163 - (view) (download) (annotate) - [select for diffs]
Modified Fri Mar 2 13:56:49 2001 UTC (20 years, 3 months ago) by yegor
File length: 8973 byte(s)
Diff to previous 3159
~-rules are duplicated by appropriate rewrites

Revision 3159 - (view) (download) (annotate) - [select for diffs]
Modified Sat Feb 24 13:04:46 2001 UTC (20 years, 3 months ago) by nogin
File length: 8083 byte(s)
Diff to previous 3151
- Fixed a nasty bug in indEquality. Yegor, can you dbl-check, please?
- Renamed "uni_minus" to "minus".
- << (- 'a) >> is now parsed correctly as minus{'a} instead of sub{'a}.
- Rewrote Yegor's theories to use the parser shortcut for "minus".
- Fixed the minus_df.

Revision 3151 - (view) (download) (annotate) - [select for diffs]
Modified Wed Feb 21 13:58:17 2001 UTC (20 years, 4 months ago) by yegor
File length: 8101 byte(s)
Diff to previous 3091
1.Display forms taken from old itt_int
2.meta-evaluation on constants taken from old itt_int
3.Some proofs added, "terrible" elim-rule fixed once again

Revision 3091 - (view) (download) (annotate) - [select for diffs]
Modified Wed Dec 13 12:04:15 2000 UTC (20 years, 6 months ago) by yegor
File length: 7341 byte(s)
Diff to previous 3083
Moved from old style conditional rewrites to rules with '~' operator instead of '<-->'.
Just now all reduce resources are commented out.

Revision 3083 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 10 12:29:43 2000 UTC (20 years, 8 months ago) by yegor
File length: 6235 byte(s)
Diff to previous 3081
reduce_resources added and theories added to Makefile

Revision 3081 - (view) (download) (annotate) - [select for diffs]
Modified Fri Oct 6 17:17:39 2000 UTC (20 years, 8 months ago) by yegor
File length: 6155 byte(s)
Diff to previous 3061
some documenting markup and resource annotation added

Revision 3061 - (view) (download) (annotate) - [select for diffs]
Added Tue Sep 12 07:56:23 2000 UTC (20 years, 9 months ago) by yegor
File length: 4970 byte(s)
itt_int_bool_new was split into itt_int_base (beq_int, lt_bool, lt, add, uni_minus, sub, int, ind, number)
and itt_int_ext (ge_bool, le_bool, gt_bool, ge, le, gt, mul, div, rem)

This form allows you to request diffs between any two revisions of this file. For each of the two "sides" of the diff, enter a numeric revision.

  Diffs between and
  Type of Diff should be a

  ViewVC Help
Powered by ViewVC 1.1.26