def glob.thm

bend-osdev-apparmor@0.1.0.0 · PROOF.bend:240
import bend-osdev-apparmor@0.1.0.0/PROOF.bend as PROOF
import Base
import bend-osdev-apparmor@0.1.0.0/glob.bend as G

240# the matcher agrees with the list model: induction on the sequence, and on
241# the path under a star
242def glob.thm(+seq: List<&2, G.AaGTok>, +s: List<&2, U32>) -> {G.AaGSeq.matches(seq, s) == G.AaGSeq.model(seq, s) : Bool}:
243  match seq:
244    case Nil{}:
245      match s:
246        case Nil{}:
247          {==}
248        case Con{h, t}:
249          {==}
250    case Con{tok, r}:
251      match tok:
252        case G.AaGChar{c}:
253          match s:
254            case Nil{}:
255              Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Nil{}))), False{}, ef_char(c, r, G.AaGCuts.all(G.AaGSeq.len(r), Nil{})))
256            case Con{h, t}:
257              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.append(G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), Bool.or(G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), fa_app(Con{G.AaGChar{c}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : {Bool.and(U32.is_eq(h, c), G.AaGSeq.matches(r, t)) == _ : Bool}
258              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), False{}, ef_char(c, r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))) : {Bool.and(U32.is_eq(h, c), G.AaGSeq.matches(r, t)) == Bool.or(_, G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : Bool}
259              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), Bool.and(U32.is_eq(h, c), fe_any(r, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), gr_char(c, r, h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))) : {Bool.and(U32.is_eq(h, c), G.AaGSeq.matches(r, t)) == Bool.or(False{}, _) : Bool}
260              %Equal.sym(Bool, fe_any(r, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)), G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), t)), fe_cuts(r, t)) : {Bool.and(U32.is_eq(h, c), G.AaGSeq.matches(r, t)) == Bool.or(False{}, Bool.and(U32.is_eq(h, c), _)) : Bool}
261              %glob.thm(r, t) : {Bool.and(U32.is_eq(h, c), G.AaGSeq.matches(r, t)) == Bool.or(False{}, Bool.and(U32.is_eq(h, c), _)) : Bool}
262              {==}
263        case G.AaGAny{}:
264          match s:
265            case Nil{}:
266              Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Nil{}))), False{}, ef_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Nil{})))
267            case Con{h, t}:
268              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.append(G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), Bool.or(G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), fa_app(Con{G.AaGAny{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : {Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(r, t)) == _ : Bool}
269              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), False{}, ef_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))) : {Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(r, t)) == Bool.or(_, G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : Bool}
270              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), Bool.and(U32.is_ne(h, 47), fe_any(r, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), gr_any(r, h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))) : {Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(r, t)) == Bool.or(False{}, _) : Bool}
271              %Equal.sym(Bool, fe_any(r, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)), G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), t)), fe_cuts(r, t)) : {Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(r, t)) == Bool.or(False{}, Bool.and(U32.is_ne(h, 47), _)) : Bool}
272              %glob.thm(r, t) : {Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(r, t)) == Bool.or(False{}, Bool.and(U32.is_ne(h, 47), _)) : Bool}
273              {==}
274        case G.AaGClass{n, rs}:
275          match s:
276            case Nil{}:
277              Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Nil{}))), False{}, ef_class(n, rs, r, G.AaGCuts.all(G.AaGSeq.len(r), Nil{})))
278            case Con{h, t}:
279              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.append(G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), Bool.or(G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), fa_app(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : {Bool.and(G.AaGClass.has(n, rs, h), G.AaGSeq.matches(r, t)) == _ : Bool}
280              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), False{}, ef_class(n, rs, r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))) : {Bool.and(G.AaGClass.has(n, rs, h), G.AaGSeq.matches(r, t)) == Bool.or(_, G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : Bool}
281              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), Bool.and(G.AaGClass.has(n, rs, h), fe_any(r, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), gr_class(n, rs, r, h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))) : {Bool.and(G.AaGClass.has(n, rs, h), G.AaGSeq.matches(r, t)) == Bool.or(False{}, _) : Bool}
282              %Equal.sym(Bool, fe_any(r, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)), G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), t)), fe_cuts(r, t)) : {Bool.and(G.AaGClass.has(n, rs, h), G.AaGSeq.matches(r, t)) == Bool.or(False{}, Bool.and(G.AaGClass.has(n, rs, h), _)) : Bool}
283              %glob.thm(r, t) : {Bool.and(G.AaGClass.has(n, rs, h), G.AaGSeq.matches(r, t)) == Bool.or(False{}, Bool.and(G.AaGClass.has(n, rs, h), _)) : Bool}
284              {==}
285        case G.AaGStar{}:
286          match s:
287            case Nil{}:
288              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Nil{}))), G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Nil{})), ef_star(r, G.AaGCuts.all(G.AaGSeq.len(r), Nil{}))) : {G.AaGSeq.matches(r, Nil{}) == _ : Bool}
289              glob.thm(r, Nil{})
290            case Con{h, t}:
291              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.append(G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), Bool.or(G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), fa_app(Con{G.AaGStar{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(Con{G.AaGStar{}, r}, t))) == _ : Bool}
292              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), ef_star(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(Con{G.AaGStar{}, r}, t))) == Bool.or(_, G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : Bool}
293              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), Bool.and(U32.is_ne(h, 47), G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), gr_star(r, h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(Con{G.AaGStar{}, r}, t))) == Bool.or(G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), _) : Bool}
294              %glob.thm(r, Con{h, t}) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(Con{G.AaGStar{}, r}, t))) == Bool.or(_, Bool.and(U32.is_ne(h, 47), G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : Bool}
295              %glob.thm(seq, t) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(Con{G.AaGStar{}, r}, t))) == Bool.or(G.AaGSeq.matches(r, Con{h, t}), Bool.and(U32.is_ne(h, 47), _)) : Bool}
296              {==}
297        case G.AaGStar2{}:
298          match s:
299            case Nil{}:
300              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Nil{}))), G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Nil{})), ef_star2(r, G.AaGCuts.all(G.AaGSeq.len(r), Nil{}))) : {G.AaGSeq.matches(r, Nil{}) == _ : Bool}
301              glob.thm(r, Nil{})
302            case Con{h, t}:
303              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.append(G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), Bool.or(G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), fa_app(Con{G.AaGStar2{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), G.AaGSeq.matches(Con{G.AaGStar2{}, r}, t)) == _ : Bool}
304              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), ef_star2(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), G.AaGSeq.matches(Con{G.AaGStar2{}, r}, t)) == Bool.or(_, G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : Bool}
305              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)), gr_star2(r, h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), G.AaGSeq.matches(Con{G.AaGStar2{}, r}, t)) == Bool.or(G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), _) : Bool}
306              %glob.thm(r, Con{h, t}) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), G.AaGSeq.matches(Con{G.AaGStar2{}, r}, t)) == Bool.or(_, G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))) : Bool}
307              %glob.thm(seq, t) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), G.AaGSeq.matches(Con{G.AaGStar2{}, r}, t)) == Bool.or(G.AaGSeq.matches(r, Con{h, t}), _) : Bool}
308              {==}
def glob.thm

Uses (32)

Used by (3)
