src/ZF/UNITY/GenPrefix.thy

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