Check-in [925c93ea0a]

Not logged in

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

Overview
Comment:Fixed demo IH to conform to the new vertical-bar encoding.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:925c93ea0ac1059125ed5184e3ab9ba93adf127e
User & Date: andy 2015-04-16 22:01:04
Context
2015-04-16
22:02
Fixed many small bugs in elaboration, checking of incomplete proofs. check-in: 6ca1a452f3 user: andy tags: trunk
22:01
Fixed demo IH to conform to the new vertical-bar encoding. check-in: 925c93ea0a user: andy tags: trunk
22:00
Fixed a bug in merging of substitutions with some arguments unbound. check-in: acfcbdeb7a user: andy tags: trunk
Changes
Hide Diffs Unified Diffs Show Whitespace Changes 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'), '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])),