replaced apply-style proof for instance Multiset :: plus_ac0 by recommended Isar proof style
(* Title: ZF/UNITY/GenPrefix.thy
ID: $Id$
Author: Sidi O Ehmety, Cambridge University Computer Laboratory
Copyright 2001 University of Cambridge
Charpentier's Generalized Prefix Relation
<xs,ys>:gen_prefix(r)
if ys = xs' @ zs where length(xs) = length(xs')
and corresponding elements of xs, xs' are pairwise related by r
Based on Lex/Prefix
*)
GenPrefix = Main +
constdefs (*really belongs in ZF/Trancl*)
part_order :: [i, i] => o
"part_order(A, r) == refl(A,r) & trans[A](r) & antisym(r)"
consts
gen_prefix :: "[i, i] => i"
inductive
(* Parameter A is the domain of zs's elements *)
domains "gen_prefix(A, r)" <= "list(A)*list(A)"
intrs
Nil "<[],[]>:gen_prefix(A, r)"
prepend "[| <xs,ys>:gen_prefix(A, r); <x,y>:r; x:A; y:A |]
==> <Cons(x,xs), Cons(y,ys)>: gen_prefix(A, r)"
append "[| <xs,ys>:gen_prefix(A, r); zs:list(A) |]
==> <xs, ys@zs>:gen_prefix(A, r)"
type_intrs "list.intrs@[app_type]"
constdefs
prefix :: i=>i
"prefix(A) == gen_prefix(A, id(A))"
strict_prefix :: i=>i
"strict_prefix(A) == prefix(A) - id(list(A))"
syntax
(* less or equal and greater or equal over prefixes *)
pfixLe :: [i, i] => o (infixl "pfixLe" 50)
pfixGe :: [i, i] => o (infixl "pfixGe" 50)
translations
"xs pfixLe ys" == "<xs, ys>:gen_prefix(nat, Le)"
"xs pfixGe ys" == "<xs, ys>:gen_prefix(nat, Ge)"
end