Theory Included

Up to index of Isabelle/HOL/Marvin2002

Included = RefPoint +

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"
  exists_point_mono "entails (refsto_point c1 p c2)(refsto_point (exists v c1) p (exists v c2))"
  forall_distrib "Cmd.all V (S pand T) [=](p) (Cmd.all V S) pand (Cmd.all V T)"
  forall_one_point "entails B (A t) ==> env p ass B ||- Cmd.all X (spec((A (varT X) && ((varT X) == t)) => P (varT X))) [=] spec(P t)"
end

theorem equiv_implication_spec:

  entails A (B <=> C) ==> env p ass A ||- spec (B => D) [=] spec (C => D)

theorem In_simp:

  entails (isNat (varT ''X'') && isNat (varT ''H'') && isList (varT ''T''))
   (relT ''In''
     [varT ''X'', funT ''elems'' [funT ''cons'' [varT ''H'', varT ''T'']]] <=>
    (varT ''X'' == varT ''H'' ||
     relT ''In'' [varT ''X'', funT ''elems'' [varT ''T'']]))

theorem distrib_land_over_lor:

  entails P ((A && B || C) <=> ((A && B) || (A && C)))

theorem gregs_rule:

  entails P (((A || B) => C) <=> (A => C && B => C))

theorem included:

  ''W'' :- exists ''U''
            (exists ''V''
              (spec (varT ''W'' == funT ''pair'' [varT ''U'', varT ''V'']) sand
               (assert (isList (varT ''U'')) sand
                assert (isList (varT ''V''))) sand
               spec (pall ''X''
                      ((isNat (varT ''X'') &&
                        relT ''In'' [varT ''X'', funT ''elems'' [varT ''U'']]) =>
                       relT ''In''
                        [varT ''X'',
                         funT ''elems''
                          [varT ''V'']])))) prefsto(p) re Included . ''W'' :- exists
                                       ''U''
                                       (exists ''V''
                                         (spec
   (varT ''W'' == funT ''pair'' [varT ''U'', varT ''V'']) sand
  (spec (varT ''U'' == funT ''emptyl'' []) sand spec ptrue) por
  exists ''H''
   (exists ''T''
     (spec (varT ''U'' == funT ''cons'' [varT ''H'', varT ''T'']) sand
      spec (relT ''In'' [varT ''H'', funT ''elems'' [varT ''V'']]) sand
      pcall Included (funT ''pair'' [varT ''T'', varT ''V'']))))) er

theorem spec_pand_true:

  env p ||- spec P pand spec ptrue [=] spec P