Check-in [4a035bbfc0]

Not logged in

 ``` ``` ``` ``` ```> > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > ``` ```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 ``` ```%%% %%% nat_spec_demo.pl %%% Sample specification for natural numbers, but modified to work with the %%% demo. %%% :- module(nat_spec_demo, [spec/1]). 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])), rule('Add-succ', add(s(' x'),' y',s(' z')), and([add(' x',' y',' z')])), % Greater-than rules rule('GT-z', (s(' _') > z), and([true])), rule('GT-succ', (s(' x') > s(' y')), and([' x' > ' y'])), % Natlist formation rules rule('NL-nil', natlist(nil), and([true])), rule('NL-cons',natlist(cons(' n',' l')), and([nat(' n'), natlist(' l')])), % List concatenation rule('Cat-nil', cat(nil,' l',' l'), and([true])), rule('Cat-cons',cat(cons(' n',' l'),' l1',cons(' n',' l2')), and([cat(' l',' l1',' l2')])), % List length rule('Len-nil', nlen(nil,z), and([true])), rule('Len-cons',nlen(cons(' _',' l'),s(' m')), and([nlen(' l',' m')])), % List membership rule('Elem-cons', elem(' e',cons(' e', ' _')), and([true])), rule('Elem-tail', elem(' e',cons(' _', ' l')), and([elem(' e', ' l')])) ]). ```