Theory Member

Up to index of Isabelle/HOL/Marvin2002

Member = RefPoint +

primrec
  "(V :- C) ^@ y = Command.substC C V y"
  "(re pid . pc er) ^@ y = pc ^@ y"
rules
  elems_def "apply ''elems'' [l] = (if [l]:(domF ''elems'')
                                    then setV (set (listof(l)))
                                    else undefV)"
  elems_dom "domF ''elems'' = {x . ? l. x = [listV l]}"
  apply_cons "apply ''cons'' [e, s] = (if [e,s]:(domF ''cons'')
                                       then (listV ((natof e)#(listof s)))
                                       else undefV)"
  cons_dom "domF ''cons'' = {x. ? e s. x = [natV e, listV s]}"
  In_def "rapply ''In'' [natV x, setV s] = (x : s)"
  emptyl_def "apply ''emptyl'' [] = listV []"
  emptyl_dom "domF ''emptyl'' = {x . x = []}"
  pcmd_apply "(V :- S) ^@ y = Command.substC S V y"
  use_environment "[| pid : dom p; (the (p(pid))) =  PC; env (p(pid:=None)) ass A ||- C  [= (PC ^@ V) |] ==> env p ass A ||- C [= pcall pid V"
(*  exists_point_mono "entails (refsto_point c1 p c2)(refsto_point (exists v c1) p (exists v c2))"
  pspec "entails (pall v P) (Pred.substp P v y)" *)
end

theorem member_refine:

  ''W'' :- exists ''X''
            (exists ''L''
              (spec (varT ''W'' == funT ''pair'' [varT ''X'', varT ''L'']) sand
               assert (isNat (varT ''X'') && isList (varT ''L'')) sand
               spec (relT ''In''
                      [varT ''X'',
                       funT ''elems''
                        [varT ''L'']]))) prefsto(empty) re ''Member'' . ''W'' :- exists
  ''X''
  (exists ''L''
    (spec (varT ''W'' == funT ''pair'' [varT ''X'', varT ''L'']) sand
     assert (isNat (varT ''X'') && isList (varT ''L'')) sand
     (spec (varT ''L'' == funT ''emptyl'' []) sand spec pfalse) por
     exists ''H''
      (exists ''T''
        (spec (varT ''L'' == funT ''cons'' [varT ''H'', varT ''T'']) sand
         spec (varT ''X'' == varT ''H'') por
         pcall ''Member'' (funT ''pair'' [varT ''X'', varT ''T'']))))) er