Check-in [95a716e7e5]

Not logged in

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Overview
Comment:Fixed the body of the hard-coded IH to be a conjunction, as required by the (current) call expansion predicate.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:95a716e7e5720454efda602616362f2c32281dad
User & Date: andy 2015-04-18 16:44:05
Context
2015-04-18
16:44
Fixed a bug in proofs that involve backchaining on the IH. check-in: c4c963bcde user: andy tags: trunk
16:44
Fixed the body of the hard-coded IH to be a conjunction, as required by the (current) call expansion predicate. check-in: 95a716e7e5 user: andy tags: trunk
2015-04-16
22:02
Fixed many small bugs in elaboration, checking of incomplete proofs. check-in: 6ca1a452f3 user: andy tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to plsrc/nat_spec_demo.pl.

9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
spec([

    % Due to an oversight on my part, the way we handle inductive proofs, 
    % although correct, will not work with the kind of incremental proofs
    % construction we are aiming to do. More permanent solutions will have to
    % come later, but for now we hard-code the IH into the specification.
    % (Which, yes, means that you can only prove one thing by induction!)
    ih('IH',         add(' x', z, ' x'), 'nat|sml'(' x')),

    % Nat formation rules
    rule('Nat-z',    nat(z),       and([true])),
    rule('Nat-succ', nat(s(' n')), and([nat(' n')])),

    % Addition rules
    rule('Add-z',    add(z,' x', ' x'),         and([true])),







|







9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
spec([

    % Due to an oversight on my part, the way we handle inductive proofs, 
    % although correct, will not work with the kind of incremental proofs
    % construction we are aiming to do. More permanent solutions will have to
    % come later, but for now we hard-code the IH into the specification.
    % (Which, yes, means that you can only prove one thing by induction!)
    ih('IH',         add(' x', z, ' x'), and(['nat|sml'(' x')])),

    % Nat formation rules
    rule('Nat-z',    nat(z),       and([true])),
    rule('Nat-succ', nat(s(' n')), and([nat(' n')])),

    % Addition rules
    rule('Add-z',    add(z,' x', ' x'),         and([true])),