diff --git a/vdm2isa/isa/FcnEx/TestV2IFcns.thy b/vdm2isa/isa/FcnEx/TestV2IFcns.thy new file mode 100644 index 00000000..f699fa38 --- /dev/null +++ b/vdm2isa/isa/FcnEx/TestV2IFcns.thy @@ -0,0 +1,468 @@ +(* VDM to Isabelle Translation @2022-12-13T10:09:37.730Z + Copyright 2019-22, Leo Freitas, leo.freitas@newcastle.ac.uk + + VDM translation of module TestV2IFcns + in 'TestV2IFcns.vdmsl' at line 1:8 + files = [TestV2IFcns.vdmsl] +*) +theory TestV2IFcns +imports VDMToolkit +begin + + +\\VDM source: const: (() -> nat) + const() == +10\ +\\in 'TestV2IFcns' (TestV2IFcns.vdmsl) at line 8:5\ + +\\VDM source: pre_const: (() +> bool) + pre_const() == +null\ +\\in 'TestV2IFcns' (TestV2IFcns.vdmsl) at line 8:5\ +definition + pre_const :: \bool\ +where + \pre_const \ True\ + + +\\VDM source: post_const: (nat +> bool) + post_const(RESULT) == +null\ +\\in 'TestV2IFcns' (TestV2IFcns.vdmsl) at line 8:5\ +definition + post_const :: \VDMNat \ bool\ +where + \post_const RESULT \ + \\Implicitly defined type invariant checks for undeclared `post_const` specification.\ + ((inv_VDMNat RESULT))\ + +definition + const :: \VDMNat\ +where + \const \ (if (pre_const ) then + + \\User defined body of const.\ + (10::VDMNat1) + else undefined)\ + + +\\VDM source: constS: (() -> nat) + constS() == +10 + pre (10 > 5) + post (RESULT > 0)\ +\\in 'TestV2IFcns' (TestV2IFcns.vdmsl) at line 12:5\ + +\\VDM source: pre_constS: (() +> bool) + pre_constS() == +(10 > 5)\ +\\in 'TestV2IFcns' (TestV2IFcns.vdmsl) at line 14:12\ +definition + pre_constS :: \bool\ +where + \pre_constS \ + \\Implicitly defined type invariant checks for `pre_constS` specification.\ + + \\User defined body of pre_constS.\ + ((10::VDMNat1) > (5::VDMNat1))\ + + +\\VDM source: post_constS: (nat +> bool) + post_constS(RESULT) == +(RESULT > 0)\ +\\in 'TestV2IFcns' (TestV2IFcns.vdmsl) at line 15:17\ +definition + post_constS :: \VDMNat \ bool\ +where + \post_constS RESULT \ + \\Implicitly defined type invariant checks for `post_constS` specification.\ + ((inv_VDMNat RESULT)) \ + \\User defined body of post_constS.\ + (RESULT > (0::VDMNat))\ + +definition + constS :: \VDMNat\ +where + \constS \ (if (pre_constS ) then + + \\User defined body of constS.\ + (10::VDMNat1) + else undefined)\ + + +\\VDM source: f: (nat * nat1 -> nat1) + f(x, y) == +(x + y)\ +\\in 'TestV2IFcns' (TestV2IFcns.vdmsl) at line 18:5\ + +\\VDM source: pre_f: (nat * nat1 +> bool) + pre_f(x, y) == +null\ +\\in 'TestV2IFcns' (TestV2IFcns.vdmsl) at line 18:5\ +definition + pre_f :: \VDMNat \ VDMNat1 \ bool\ +where + \pre_f x y \ + \\Implicitly defined type invariant checks for undeclared `pre_f` specification.\ + ((inv_VDMNat x) \ (inv_VDMNat1 y))\ + + +\\VDM source: post_f: (nat * nat1 * nat1 +> bool) + post_f(x, y, RESULT) == +null\ +\\in 'TestV2IFcns' (TestV2IFcns.vdmsl) at line 18:5\ +definition + post_f :: \VDMNat \ VDMNat1 \ VDMNat1 \ bool\ +where + \post_f x y RESULT \ + \\Implicitly defined type invariant checks for undeclared `post_f` specification.\ + ((inv_VDMNat x) \ (inv_VDMNat1 y) \ (inv_VDMNat1 RESULT))\ + +definition + f :: \VDMNat \ VDMNat1 \ VDMNat1\ +where + \f x y \ (if (pre_f x y) then + + \\User defined body of f.\ + (x + y) + else undefined)\ + + +\\VDM source: g: (nat * nat1 -> nat1) + g(x, y) == +(x + y) + pre (x > 10) + post (x < RESULT)\ +\\in 'TestV2IFcns' (TestV2IFcns.vdmsl) at line 22:5\ + +\\VDM source: pre_g: (nat * nat1 +> bool) + pre_g(x, y) == +(x > 10)\ +\\in 'TestV2IFcns' (TestV2IFcns.vdmsl) at line 24:11\ +definition + pre_g :: \VDMNat \ VDMNat1 \ bool\ +where + \pre_g x y \ + \\Implicitly defined type invariant checks for `pre_g` specification.\ + ((inv_VDMNat x) \ (inv_VDMNat1 y)) \ + \\User defined body of pre_g.\ + (x > (10::VDMNat1))\ + + +\\VDM source: post_g: (nat * nat1 * nat1 +> bool) + post_g(x, y, RESULT) == +(x < RESULT)\ +\\in 'TestV2IFcns' (TestV2IFcns.vdmsl) at line 25:12\ +definition + post_g :: \VDMNat \ VDMNat1 \ VDMNat1 \ bool\ +where + \post_g x y RESULT \ + \\Implicitly defined type invariant checks for `post_g` specification.\ + ((inv_VDMNat x) \ (inv_VDMNat1 y) \ (inv_VDMNat1 RESULT)) \ + \\User defined body of post_g.\ + (x < RESULT)\ + +definition + g :: \VDMNat \ VDMNat1 \ VDMNat1\ +where + \g x y \ (if (pre_g x y) then + + \\User defined body of g.\ + (x + y) + else undefined)\ + + +\\VDM source: h: (nat -> nat) + h(x) == +g(x, x) + pre pre_g(x, x) + post post_g(x, x, RESULT)\ +\\in 'TestV2IFcns' (TestV2IFcns.vdmsl) at line 28:5\ + +\\VDM source: pre_h: (nat +> bool) + pre_h(x) == +pre_g(x, x)\ +\\in 'TestV2IFcns' (TestV2IFcns.vdmsl) at line 30:9\ +definition + pre_h :: \VDMNat \ bool\ +where + \pre_h x \ + \\Implicitly defined type invariant checks for `pre_h` specification.\ + ((inv_VDMNat x)) \ + \\User defined body of pre_h.\ + (pre_g x x)\ + + +\\VDM source: post_h: (nat * nat +> bool) + post_h(x, RESULT) == +post_g(x, x, RESULT)\ +\\in 'TestV2IFcns' (TestV2IFcns.vdmsl) at line 31:10\ +definition + post_h :: \VDMNat \ VDMNat \ bool\ +where + \post_h x RESULT \ + \\Implicitly defined type invariant checks for `post_h` specification.\ + ((inv_VDMNat x) \ (inv_VDMNat RESULT)) \ + \\User defined body of post_h.\ + (post_g x x RESULT)\ + +definition + h :: \VDMNat \ VDMNat\ +where + \h x \ (if (pre_h x) then + + \\User defined body of h.\ + (g x x) + else undefined)\ + + +\\VDM source: h': (nat -> nat) + h'(x) == +g(x, x) + pre (x < 20) + post (x > 20)\ +\\in 'TestV2IFcns' (TestV2IFcns.vdmsl) at line 34:5\ + +\\VDM source: pre_h': (nat +> bool) + pre_h'(x) == +(x < 20)\ +\\in 'TestV2IFcns' (TestV2IFcns.vdmsl) at line 36:11\ +definition + pre_h' :: \VDMNat \ bool\ +where + \pre_h' x \ + \\Implicitly defined type invariant checks for `pre_h'` specification.\ + ((inv_VDMNat x)) \ + \\User defined body of pre_h'.\ + (x < (20::VDMNat1))\ + + +\\VDM source: post_h': (nat * nat +> bool) + post_h'(x, RESULT) == +(x > 20)\ +\\in 'TestV2IFcns' (TestV2IFcns.vdmsl) at line 37:12\ +definition + post_h' :: \VDMNat \ VDMNat \ bool\ +where + \post_h' x RESULT \ + \\Implicitly defined type invariant checks for `post_h'` specification.\ + ((inv_VDMNat x) \ (inv_VDMNat RESULT)) \ + \\User defined body of post_h'.\ + (x > (20::VDMNat1))\ + +definition + h' :: \VDMNat \ VDMNat\ +where + \h' x \ (if (pre_h' x) then + + \\User defined body of h'.\ + (g x x) + else undefined)\ + + +\\VDM source: h'': (nat -> nat) + h''(x) == +g(x, x) + pre (x < 20) + post pre_g(x, RESULT)\ +\\in 'TestV2IFcns' (TestV2IFcns.vdmsl) at line 40:5\ + +\\VDM source: pre_h'': (nat +> bool) + pre_h''(x) == +(x < 20)\ +\\in 'TestV2IFcns' (TestV2IFcns.vdmsl) at line 42:11\ +definition + pre_h'' :: \VDMNat \ bool\ +where + \pre_h'' x \ + \\Implicitly defined type invariant checks for `pre_h''` specification.\ + ((inv_VDMNat x)) \ + \\User defined body of pre_h''.\ + (x < (20::VDMNat1))\ + + +\\VDM source: post_h'': (nat * nat +> bool) + post_h''(x, RESULT) == +pre_g(x, RESULT)\ +\\in 'TestV2IFcns' (TestV2IFcns.vdmsl) at line 43:10\ +definition + post_h'' :: \VDMNat \ VDMNat \ bool\ +where + \post_h'' x RESULT \ + \\Implicitly defined type invariant checks for `post_h''` specification.\ + ((inv_VDMNat x) \ (inv_VDMNat RESULT)) \ + \\User defined body of post_h''.\ + (pre_g x RESULT)\ + +definition + h'' :: \VDMNat \ VDMNat\ +where + \h'' x \ (if (pre_h'' x) then + + \\User defined body of h''.\ + (g x x) + else undefined)\ + + +\\VDM source: curried: (nat -> (nat -> nat)) + curried(x)(y) == +(x + y)\ +\\in 'TestV2IFcns' (TestV2IFcns.vdmsl) at line 46:5\ + +\\VDM source: pre_curried: (nat +> (nat +> bool)) + pre_curried(x)(y) == +null\ +\\in 'TestV2IFcns' (TestV2IFcns.vdmsl) at line 46:5\ +definition + pre_curried :: \VDMNat \ VDMNat \ bool\ +where + \pre_curried x y \ + \\Implicitly defined type invariant checks for undeclared `pre_curried` specification.\ + ((inv_VDMNat x)) \ ((inv_VDMNat y))\ + + +\\VDM source: post_curried: (nat +> (nat * nat +> bool)) + post_curried(x)(y, RESULT) == +null\ +\\in 'TestV2IFcns' (TestV2IFcns.vdmsl) at line 46:5\ +definition + post_curried :: \VDMNat \ VDMNat \ VDMNat \ bool\ +where + \post_curried x y RESULT \ + \\Implicitly defined type invariant checks for undeclared `post_curried` specification.\ + ((inv_VDMNat x)) \ ((inv_VDMNat y))\ + +definition + curried :: \VDMNat \ VDMNat \ VDMNat\ +where + \curried x y \ (if (pre_curried x y) then + + \\User defined body of curried.\ + (x + y) + else undefined)\ + + +\\VDM source: curriedS: (nat -> (nat -> nat)) + curriedS(x)(y) == +(x + y) + pre (x > y) + post ((x < RESULT) and (y < RESULT))\ +\\in 'TestV2IFcns' (TestV2IFcns.vdmsl) at line 50:5\ + +\\VDM source: pre_curriedS: (nat +> (nat +> bool)) + pre_curriedS(x)(y) == +(x > y)\ +\\in 'TestV2IFcns' (TestV2IFcns.vdmsl) at line 52:11\ +definition + pre_curriedS :: \VDMNat \ VDMNat \ bool\ +where + \pre_curriedS x y \ + \\Implicitly defined type invariant checks for `pre_curriedS` specification.\ + ((inv_VDMNat x)) \ ((inv_VDMNat y)) \ + \\User defined body of pre_curriedS.\ + (x > y)\ + + +\\VDM source: + post_curriedS: (nat +> (nat * nat +> bool)) + post_curriedS(x)(y, RESULT) == + ((x < RESULT) and (y < RESULT))\ +\\in 'TestV2IFcns' (TestV2IFcns.vdmsl) at line 53:21\ +definition + post_curriedS :: \VDMNat \ VDMNat \ VDMNat \ bool\ +where + \post_curriedS x y RESULT \ + \\Implicitly defined type invariant checks for `post_curriedS` specification.\ + ((inv_VDMNat x)) \ ((inv_VDMNat y)) \ + \\User defined body of post_curriedS.\ + ((x < RESULT) \ (y < RESULT))\ + +definition + curriedS :: \VDMNat \ VDMNat \ VDMNat\ +where + \curriedS x y \ (if (pre_curriedS x y) then + + \\User defined body of curriedS.\ + (x + y) + else undefined)\ + + +\\VDM source: static private implicit((x, y:nat), (z:set of (nat)))r:seq of (nat) + pre ((x < y) and (x in set z)) + post (x > (len r))\ +\\in 'TestV2IFcns' (TestV2IFcns.vdmsl) at line 55:5\ + +\\VDM source: pre_implicit: (nat * nat * set of (nat) +> bool) + pre_implicit(x, y, z) == +((x < y) and (x in set z))\ +\\in 'TestV2IFcns' (TestV2IFcns.vdmsl) at line 56:15\ +definition + pre_implicit :: \VDMNat \ VDMNat \ VDMNat VDMSet \ bool\ +where + \pre_implicit x y z \ + \\Implicitly defined type invariant checks for `pre_implicit` specification.\ + ((inv_VDMNat x) \ (inv_VDMNat y) \ (inv_VDMSet' (inv_VDMNat) z)) \ + \\User defined body of pre_implicit.\ + ((x < y) \ (x \ z))\ + + +\\VDM source: post_implicit: (nat * nat * set of (nat) * seq of (nat) +> bool) + post_implicit(x, y, z, r) == +(x > (len r))\ +\\in 'TestV2IFcns' (TestV2IFcns.vdmsl) at line 57:12\ +definition + post_implicit :: \VDMNat \ VDMNat \ VDMNat VDMSet \ VDMNat VDMSeq \ bool\ +where + \post_implicit x y z r \ + \\Implicitly defined type invariant checks for `post_implicit` specification.\ + ((inv_VDMNat x) \ (inv_VDMNat y) \ (inv_VDMSet' (inv_VDMNat) z) \ (inv_VDMSeq' (inv_VDMNat) r)) \ + \\User defined body of post_implicit.\ + (x > (len r))\ + + + +\\VDM source: static private implicitexplicit((x, y:nat), (z:set of (nat)))r:seq of (nat) == + [x, y] + pre ((x < y) and (x in set z)) + post (x > (len r))\ +\\in 'TestV2IFcns' (TestV2IFcns.vdmsl) at line 59:5\ + +\\VDM source: pre_implicitexplicit: (nat * nat * set of (nat) +> bool) + pre_implicitexplicit(x, y, z) == +((x < y) and (x in set z))\ +\\in 'TestV2IFcns' (TestV2IFcns.vdmsl) at line 61:15\ +definition + pre_implicitexplicit :: \VDMNat \ VDMNat \ VDMNat VDMSet \ bool\ +where + \pre_implicitexplicit x y z \ + \\Implicitly defined type invariant checks for `pre_implicitexplicit` specification.\ + ((inv_VDMNat x) \ (inv_VDMNat y) \ (inv_VDMSet' (inv_VDMNat) z)) \ + \\User defined body of pre_implicitexplicit.\ + ((x < y) \ (x \ z))\ + + +\\VDM source: post_implicitexplicit: (nat * nat * set of (nat) * seq of (nat) +> bool) + post_implicitexplicit(x, y, z, r) == +(x > (len r))\ +\\in 'TestV2IFcns' (TestV2IFcns.vdmsl) at line 62:12\ +definition + post_implicitexplicit :: \VDMNat \ VDMNat \ VDMNat VDMSet \ VDMNat VDMSeq \ bool\ +where + \post_implicitexplicit x y z r \ + \\Implicitly defined type invariant checks for `post_implicitexplicit` specification.\ + ((inv_VDMNat x) \ (inv_VDMNat y) \ (inv_VDMSet' (inv_VDMNat) z) \ (inv_VDMSeq' (inv_VDMNat) r)) \ + \\User defined body of post_implicitexplicit.\ + (x > (len r))\ + +definition + implicitexplicit :: \VDMNat \ VDMNat \ VDMNat VDMSet \ VDMNat VDMSeq\ +where + \implicitexplicit x y z \ (if (pre_implicitexplicit x y z) then + + \\User defined body of implicitexplicit.\ + [x , y] + else undefined)\ + + + +end \ No newline at end of file diff --git a/vdm2isa/isa/FcnEx/TestV2IFcns_PO.thy b/vdm2isa/isa/FcnEx/TestV2IFcns_PO.thy new file mode 100644 index 00000000..26f39289 --- /dev/null +++ b/vdm2isa/isa/FcnEx/TestV2IFcns_PO.thy @@ -0,0 +1,486 @@ +(* VDM to Isabelle Translation @2022-05-26T11:45:34.996Z + Copyright 2021, Leo Freitas, leo.freitas@newcastle.ac.uk + +in 'TestV2IFcns' (/Users/nljsf/Local/reps/git/VDM_Toolkit/plugins/vdm2isa/src/test/resources/TestV2IFcns.vdmsl) at line 12:5 +files = [/Users/nljsf/Local/reps/git/VDM_Toolkit/plugins/vdm2isa/src/test/resources/TestV2IFcns.vdmsl] +*) +theory TestV2IFcns_PO +imports TestV2IFcns +begin + + +\\VDM source: constS = ?\ +\\in 'TestV2IFcns' (/Users/nljsf/Local/reps/git/VDM_Toolkit/plugins/vdm2isa/src/test/resources/TestV2IFcns.vdmsl) at line 12:5\ + + +definition + PO_01_constS_FUNC_POST_CONDITION :: "\" +where + "PO_01_constS_FUNC_POST_CONDITION \ ((pre_constS ) \ (post_constS (10::VDMNat1)))" + + + + +\\VDM source: g = ?\ +\\in 'TestV2IFcns' (/Users/nljsf/Local/reps/git/VDM_Toolkit/plugins/vdm2isa/src/test/resources/TestV2IFcns.vdmsl) at line 22:5\ + +\\Implicitly defined type invariant checks for quantified type binds\ + +definition + PO_02_g_FUNC_POST_CONDITION :: "\" +where + "PO_02_g_FUNC_POST_CONDITION \ (\ (x :: VDMNat) (y :: VDMNat1) . ((((inv_VDMNat x))) \ (((inv_VDMNat1 y))) \ ((pre_g x y) \ (post_g x y (x + y)))))" + + + + +\\VDM source: h = ?\ +\\in 'TestV2IFcns' (/Users/nljsf/Local/reps/git/VDM_Toolkit/plugins/vdm2isa/src/test/resources/TestV2IFcns.vdmsl) at line 30:18\ + +\\Implicitly defined type invariant checks for quantified type binds\ + +definition + PO_03_h_SUB_TYPE :: "\" +where + "PO_03_h_SUB_TYPE \ (\ (x :: VDMNat) . ((((inv_VDMNat x))) \ (x > (0::VDMNat))))" + + + + +\\VDM source: h = ?\ +\\in 'TestV2IFcns' (/Users/nljsf/Local/reps/git/VDM_Toolkit/plugins/vdm2isa/src/test/resources/TestV2IFcns.vdmsl) at line 28:5\ + +\\Implicitly defined type invariant checks for quantified type binds\ + +definition + PO_04_h_FUNC_POST_CONDITION :: "\" +where + "PO_04_h_FUNC_POST_CONDITION \ (\ (x :: VDMNat) . ((((inv_VDMNat x))) \ ((pre_h x) \ (post_h x (g x x)))))" + + + + +\\VDM source: h = ?\ +\\in 'TestV2IFcns' (/Users/nljsf/Local/reps/git/VDM_Toolkit/plugins/vdm2isa/src/test/resources/TestV2IFcns.vdmsl) at line 31:20\ + +\\Implicitly defined type invariant checks for quantified type binds\ + +definition + PO_05_h_SUB_TYPE :: "\" +where + "PO_05_h_SUB_TYPE \ (\ (x :: VDMNat) . ((((inv_VDMNat x))) \ ((pre_h x) \ ( + let +(RESULT::VDMNat) = (g x x) + in + + (if ((inv_VDMNat RESULT)) then + (x > (0::VDMNat)) + else + undefined + ) + ))))" + + + + +\\VDM source: h = ?\ +\\in 'TestV2IFcns' (/Users/nljsf/Local/reps/git/VDM_Toolkit/plugins/vdm2isa/src/test/resources/TestV2IFcns.vdmsl) at line 31:23\ + +\\Implicitly defined type invariant checks for quantified type binds\ + +definition + PO_06_h_SUB_TYPE :: "\" +where + "PO_06_h_SUB_TYPE \ (\ (x :: VDMNat) . ((((inv_VDMNat x))) \ ((pre_h x) \ ( + let +(RESULT::VDMNat) = (g x x) + in + + (if ((inv_VDMNat RESULT)) then + (RESULT > (0::VDMNat)) + else + undefined + ) + ))))" + + + + +\\VDM source: h = ?\ +\\in 'TestV2IFcns' (/Users/nljsf/Local/reps/git/VDM_Toolkit/plugins/vdm2isa/src/test/resources/TestV2IFcns.vdmsl) at line 29:13\ + +\\Implicitly defined type invariant checks for quantified type binds\ + +definition + PO_07_h_FUNC_APPLY :: "\" +where + "PO_07_h_FUNC_APPLY \ (\ (x :: VDMNat) . ((((inv_VDMNat x))) \ ((pre_h x) \ (pre_g x x))))" + + + + +\\VDM source: h = ?\ +\\in 'TestV2IFcns' (/Users/nljsf/Local/reps/git/VDM_Toolkit/plugins/vdm2isa/src/test/resources/TestV2IFcns.vdmsl) at line 29:18\ + +\\Implicitly defined type invariant checks for quantified type binds\ + +definition + PO_08_h_SUB_TYPE :: "\" +where + "PO_08_h_SUB_TYPE \ (\ (x :: VDMNat) . ((((inv_VDMNat x))) \ ((pre_h x) \ (x > (0::VDMNat)))))" + + + + +\\VDM source: h' = ?\ +\\in 'TestV2IFcns' (/Users/nljsf/Local/reps/git/VDM_Toolkit/plugins/vdm2isa/src/test/resources/TestV2IFcns.vdmsl) at line 34:5\ + +\\Implicitly defined type invariant checks for quantified type binds\ + +definition + PO_09_h'_FUNC_POST_CONDITION :: "\" +where + "PO_09_h'_FUNC_POST_CONDITION \ (\ (x :: VDMNat) . ((((inv_VDMNat x))) \ ((pre_h' x) \ (post_h' x (g x x)))))" + + + + +\\VDM source: h' = ?\ +\\in 'TestV2IFcns' (/Users/nljsf/Local/reps/git/VDM_Toolkit/plugins/vdm2isa/src/test/resources/TestV2IFcns.vdmsl) at line 35:14\ + +\\Implicitly defined type invariant checks for quantified type binds\ + +definition + PO_10_h'_FUNC_APPLY :: "\" +where + "PO_10_h'_FUNC_APPLY \ (\ (x :: VDMNat) . ((((inv_VDMNat x))) \ ((pre_h' x) \ (pre_g x x))))" + + + + +\\VDM source: h' = ?\ +\\in 'TestV2IFcns' (/Users/nljsf/Local/reps/git/VDM_Toolkit/plugins/vdm2isa/src/test/resources/TestV2IFcns.vdmsl) at line 35:19\ + +\\Implicitly defined type invariant checks for quantified type binds\ + +definition + PO_11_h'_SUB_TYPE :: "\" +where + "PO_11_h'_SUB_TYPE \ (\ (x :: VDMNat) . ((((inv_VDMNat x))) \ ((pre_h' x) \ (x > (0::VDMNat)))))" + + + + +\\VDM source: h'' = ?\ +\\in 'TestV2IFcns' (/Users/nljsf/Local/reps/git/VDM_Toolkit/plugins/vdm2isa/src/test/resources/TestV2IFcns.vdmsl) at line 40:5\ + +\\Implicitly defined type invariant checks for quantified type binds\ + +definition + PO_12_h''_FUNC_POST_CONDITION :: "\" +where + "PO_12_h''_FUNC_POST_CONDITION \ (\ (x :: VDMNat) . ((((inv_VDMNat x))) \ ((pre_h'' x) \ (post_h'' x (g x x)))))" + + + + +\\VDM source: h'' = ?\ +\\in 'TestV2IFcns' (/Users/nljsf/Local/reps/git/VDM_Toolkit/plugins/vdm2isa/src/test/resources/TestV2IFcns.vdmsl) at line 43:18\ + +\\Implicitly defined type invariant checks for quantified type binds\ + +definition + PO_13_h''_SUB_TYPE :: "\" +where + "PO_13_h''_SUB_TYPE \ (\ (x :: VDMNat) . ((((inv_VDMNat x))) \ ((pre_h'' x) \ ( + let +(RESULT::VDMNat) = (g x x) + in + + (if ((inv_VDMNat RESULT)) then + (RESULT > (0::VDMNat)) + else + undefined + ) + ))))" + + + + +\\VDM source: h'' = ?\ +\\in 'TestV2IFcns' (/Users/nljsf/Local/reps/git/VDM_Toolkit/plugins/vdm2isa/src/test/resources/TestV2IFcns.vdmsl) at line 41:15\ + +\\Implicitly defined type invariant checks for quantified type binds\ + +definition + PO_14_h''_FUNC_APPLY :: "\" +where + "PO_14_h''_FUNC_APPLY \ (\ (x :: VDMNat) . ((((inv_VDMNat x))) \ ((pre_h'' x) \ (pre_g x x))))" + + + + +\\VDM source: h'' = ?\ +\\in 'TestV2IFcns' (/Users/nljsf/Local/reps/git/VDM_Toolkit/plugins/vdm2isa/src/test/resources/TestV2IFcns.vdmsl) at line 41:20\ + +\\Implicitly defined type invariant checks for quantified type binds\ + +definition + PO_15_h''_SUB_TYPE :: "\" +where + "PO_15_h''_SUB_TYPE \ (\ (x :: VDMNat) . ((((inv_VDMNat x))) \ ((pre_h'' x) \ (x > (0::VDMNat)))))" + + + + +\\VDM source: curriedS = ?\ +\\in 'TestV2IFcns' (/Users/nljsf/Local/reps/git/VDM_Toolkit/plugins/vdm2isa/src/test/resources/TestV2IFcns.vdmsl) at line 50:5\ + +\\Implicitly defined type invariant checks for quantified type binds\ + +definition + PO_16_curriedS_FUNC_POST_CONDITION :: "\" +where + "PO_16_curriedS_FUNC_POST_CONDITION \ (\ (x :: VDMNat) (y :: VDMNat) . ((((inv_VDMNat x))) \ (((inv_VDMNat y))) \ (((pre_curriedS x) y) \ ((post_curriedS x) y (x + y)))))" + + + + +\\VDM source: implicit = ?\ +\\in 'TestV2IFcns' (/Users/nljsf/Local/reps/git/VDM_Toolkit/plugins/vdm2isa/src/test/resources/TestV2IFcns.vdmsl) at line 56:15\ + +\\Implicitly defined type invariant checks for quantified type binds\ + +definition + PO_17_implicit_TOTAL :: "\" +where + "PO_17_implicit_TOTAL \ (\ (x :: VDMNat) (y :: VDMNat) (z :: VDMNat VDMSet) . ((((inv_VDMNat x))) \ (((inv_VDMNat y))) \ (((inv_VDMSet' (inv_VDMNat) z))) \ isTest ((pre_implicit x y z)) (inv_bool)))" + + + + +\\VDM source: implicit = ?\ +\\in 'TestV2IFcns' (/Users/nljsf/Local/reps/git/VDM_Toolkit/plugins/vdm2isa/src/test/resources/TestV2IFcns.vdmsl) at line 55:5\ + +\\Implicitly defined type invariant checks for quantified type binds\ + +definition + PO_18_implicit_FUNC_SATISFIABILITY :: "\" +where + "PO_18_implicit_FUNC_SATISFIABILITY \ (\ (x :: VDMNat) (y :: VDMNat) (z :: VDMNat VDMSet) . ((((inv_VDMNat x))) \ (((inv_VDMNat y))) \ (((inv_VDMSet' (inv_VDMNat) z))) \ ((pre_implicit x y z) \ (\ (r :: VDMNat VDMSeq) . ((((inv_VDMSeq' (inv_VDMNat) r))) \ (post_implicit x y z r))))))" + + + + +\\VDM source: implicitexplicit = ?\ +\\in 'TestV2IFcns' (/Users/nljsf/Local/reps/git/VDM_Toolkit/plugins/vdm2isa/src/test/resources/TestV2IFcns.vdmsl) at line 61:15\ + +\\Implicitly defined type invariant checks for quantified type binds\ + +definition + PO_19_implicitexplicit_TOTAL :: "\" +where + "PO_19_implicitexplicit_TOTAL \ (\ (x :: VDMNat) (y :: VDMNat) (z :: VDMNat VDMSet) . ((((inv_VDMNat x))) \ (((inv_VDMNat y))) \ (((inv_VDMSet' (inv_VDMNat) z))) \ isTest ((pre_implicitexplicit x y z)) (inv_bool)))" + + + + +\\VDM source: implicitexplicit = ?\ +\\in 'TestV2IFcns' (/Users/nljsf/Local/reps/git/VDM_Toolkit/plugins/vdm2isa/src/test/resources/TestV2IFcns.vdmsl) at line 59:5\ + +\\Implicitly defined type invariant checks for quantified type binds\ + +definition + PO_20_implicitexplicit_FUNC_POST_CONDITION :: "\" +where + "PO_20_implicitexplicit_FUNC_POST_CONDITION \ (\ (x :: VDMNat) (y :: VDMNat) (z :: VDMNat VDMSet) . ((((inv_VDMNat x))) \ (((inv_VDMNat y))) \ (((inv_VDMSet' (inv_VDMNat) z))) \ ((pre_implicitexplicit x y z) \ (post_implicitexplicit x y z [x , y]))))" + + +\\Processing VDM exports as Isabelle hidden declarations\ + + +locale TestV2IFcns_POG = + assumes + TestV2IFcns_PO_01: PO_01_constS_FUNC_POST_CONDITION + and TestV2IFcns_PO_02: PO_02_g_FUNC_POST_CONDITION + and TestV2IFcns_PO_03: PO_03_h_SUB_TYPE + and TestV2IFcns_PO_04: PO_04_h_FUNC_POST_CONDITION + and TestV2IFcns_PO_05: PO_05_h_SUB_TYPE + and TestV2IFcns_PO_06: PO_06_h_SUB_TYPE + and TestV2IFcns_PO_07: PO_07_h_FUNC_APPLY + and TestV2IFcns_PO_08: PO_08_h_SUB_TYPE + and TestV2IFcns_PO_09: PO_09_h'_FUNC_POST_CONDITION + and TestV2IFcns_PO_10: PO_10_h'_FUNC_APPLY + and TestV2IFcns_PO_11: PO_11_h'_SUB_TYPE + and TestV2IFcns_PO_12: PO_12_h''_FUNC_POST_CONDITION + and TestV2IFcns_PO_13: PO_13_h''_SUB_TYPE + and TestV2IFcns_PO_14: PO_14_h''_FUNC_APPLY + and TestV2IFcns_PO_15: PO_15_h''_SUB_TYPE + and TestV2IFcns_PO_16: PO_16_curriedS_FUNC_POST_CONDITION + and TestV2IFcns_PO_17: PO_17_implicit_TOTAL + and TestV2IFcns_PO_18: PO_18_implicit_FUNC_SATISFIABILITY + and TestV2IFcns_PO_19: PO_19_implicitexplicit_TOTAL + and TestV2IFcns_PO_20: PO_20_implicitexplicit_FUNC_POST_CONDITION +begin + \\User defined lemmas for TestV2IFcns POs\ +end + +lemma TestV2IFcns_POG_l1[simp]: \PO_01_constS_FUNC_POST_CONDITION\ + \\Inferred proof strategy for lemma:\ + by (simp add: PO_01_constS_FUNC_POST_CONDITION_def inv_VDMNat_def post_constS_def) + +lemma TestV2IFcns_POG_l2[simp]: \PO_02_g_FUNC_POST_CONDITION\ + \\Inferred proof strategy for lemma:\ + using PO_02_g_FUNC_POST_CONDITION_def inv_VDMNat1_def inv_VDMNat_def post_g_def by force + + +lemma TestV2IFcns_POG_l3[simp]: \PO_03_h_SUB_TYPE\ + \\Inferred proof strategy for lemma:\ + nitpick + + + oops + + +lemma TestV2IFcns_POG_l4[simp]: \PO_04_h_FUNC_POST_CONDITION\ + \\Inferred proof strategy for lemma:\ + by (smt (verit, ccfv_SIG) PO_02_g_FUNC_POST_CONDITION_def PO_04_h_FUNC_POST_CONDITION_def TestV2IFcns_POG_l2 g_def inv_VDMNat_def post_h_def pre_g_def pre_h_def) + + +lemma TestV2IFcns_POG_l5[simp]: \PO_05_h_SUB_TYPE\ + \\Inferred proof strategy for lemma:\ + by (simp add: PO_05_h_SUB_TYPE_def g_def inv_VDMNat_def pre_g_def pre_h_def) + +lemma TestV2IFcns_POG_l6[simp]: \PO_06_h_SUB_TYPE\ + \\Inferred proof strategy for lemma:\ + using PO_05_h_SUB_TYPE_def PO_06_h_SUB_TYPE_def g_def pre_h_def by force + +lemma TestV2IFcns_POG_l7[simp]: \PO_07_h_FUNC_APPLY\ + \\Inferred proof strategy for lemma:\ + using PO_07_h_FUNC_APPLY_def pre_h_def by blast + +lemma TestV2IFcns_POG_l8[simp]: \PO_08_h_SUB_TYPE\ + \\Inferred proof strategy for lemma:\ + using PO_08_h_SUB_TYPE_def pre_g_def pre_h_def by force + +lemma TestV2IFcns_POG_l9[simp]: \PO_09_h'_FUNC_POST_CONDITION\ + \\Inferred proof strategy for lemma:\ + nitpick + + + oops + + +lemma TestV2IFcns_POG_l10[simp]: \PO_10_h'_FUNC_APPLY\ + \\Inferred proof strategy for lemma:\ + nitpick + + + oops + + +lemma TestV2IFcns_POG_l11[simp]: \PO_11_h'_SUB_TYPE\ + \\Inferred proof strategy for lemma:\ + nitpick + + + oops + + +lemma TestV2IFcns_POG_l12[simp]: \PO_12_h''_FUNC_POST_CONDITION\ + \\Inferred proof strategy for lemma:\ + nitpick + + + oops + + +lemma TestV2IFcns_POG_l13[simp]: \PO_13_h''_SUB_TYPE\ + \\Inferred proof strategy for lemma:\ + nitpick + + + oops + + +lemma TestV2IFcns_POG_l14[simp]: \PO_14_h''_FUNC_APPLY\ + \\Inferred proof strategy for lemma:\ + nitpick + + + oops + + +lemma TestV2IFcns_POG_l15[simp]: \PO_15_h''_SUB_TYPE\ + \\Inferred proof strategy for lemma:\ + nitpick + + + oops + + +lemma TestV2IFcns_POG_l16[simp]: \PO_16_curriedS_FUNC_POST_CONDITION\ + \\Inferred proof strategy for lemma:\ + nitpick + + + oops + + +lemma TestV2IFcns_POG_l17[simp]: \PO_17_implicit_TOTAL\ + \\Inferred proof strategy for lemma:\ + by (simp add: PO_17_implicit_TOTAL_def) + +named_theorems Fcns_defs and Fcns_PO_defs + +lemmas [Fcns_PO_defs] = PO_18_implicit_FUNC_SATISFIABILITY_def +lemmas [Fcns_defs] = post_implicit_def pre_implicit_def Fcns_PO_defs + +lemma TestV2IFcns_POG_l18[simp]: \PO_18_implicit_FUNC_SATISFIABILITY\ + thm Fcns_PO_defs + apply (simp add: Fcns_PO_defs, safe?)+ + thm Fcns_defs + apply (simp add: Fcns_defs, safe?)+ + thm VDM_seq_defs + apply (simp add: VDM_seq_defs, safe?)+ + apply (simp add: VDM_set_defs, safe?)+ + apply (metis diff_ge_0_iff_ge inv_VDMNat_def inv_VDMSeq'_defs(2) l_inv_SeqElems_append not_one_le_zero) + done + +lemma TestV2IFcns_POG_l18[simp]: \PO_18_implicit_FUNC_SATISFIABILITY\ + \\Inferred proof strategy for lemma:\ + unfolding PO_18_implicit_FUNC_SATISFIABILITY_def + apply (safe?, simp?) + unfolding post_implicit_def pre_implicit_def + apply (safe?, simp?) + unfolding inv_VDMSeq'_def inv_SeqElems_def + apply (safe?, simp?) + unfolding inv_VDMSet'_def inv_VDMSet_def inv_SetElems_def + apply (safe?, simp?) + unfolding inv_VDMNat_def + by (metis linorder_not_le list.pred_inject(2) zle_diff1_eq) + +lemma TestV2IFcns_POG_l19[simp]: \PO_19_implicitexplicit_TOTAL\ + \\Inferred proof strategy for lemma:\ + by (simp add: PO_19_implicitexplicit_TOTAL_def) + + +lemma TestV2IFcns_POG_l20[simp]: \PO_20_implicitexplicit_FUNC_POST_CONDITION\ + \\Inferred proof strategy for lemma:\ + unfolding PO_20_implicitexplicit_FUNC_POST_CONDITION_def + apply (safe?, simp?) + unfolding post_implicitexplicit_def pre_implicitexplicit_def + apply (safe?, simp?) + unfolding inv_VDMSeq'_def inv_SeqElems_def + apply (safe?, simp?) + unfolding inv_VDMSet'_def inv_VDMSet_def inv_SetElems_def + apply (safe?, simp?) + unfolding inv_VDMNat_def + oops + + +interpretation TestV2IFcns_POG + apply unfold_locales + apply simp_all + oops +end \ No newline at end of file