Attention une mise à jour du service Gitlab va être effectuée le mardi 30 novembre entre 17h30 et 18h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes. Cette mise à jour intermédiaire en version 14.0.12 nous permettra de rapidement pouvoir mettre à votre disposition une version plus récente.

Commit 41614a56 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Support for map.Const in isabelle and Coq realizations

parent ac61df48
......@@ -1148,7 +1148,7 @@ ISABELLELIBS_NUMBER = $(addsuffix .xml, $(addprefix lib/isabelle/number/, $(ISAB
ISABELLELIBS_SET_FILES = Set Fset
ISABELLELIBS_SET = $(addsuffix .xml, $(addprefix lib/isabelle/set/, $(ISABELLELIBS_SET_FILES)))
ISABELLELIBS_MAP_FILES = Map Occ MapPermut MapInjection
ISABELLELIBS_MAP_FILES = Map Const Occ MapPermut MapInjection
ISABELLELIBS_MAP = $(addsuffix .xml, $(addprefix lib/isabelle/map/, $(ISABELLELIBS_MAP_FILES)))
ISABELLELIBS_LIST_FILES = List Length Mem Nth NthNoOpt NthLength HdTl NthHdTl Append NthLengthAppend Reverse HdTlNoOpt RevAppend Combine Distinct NumOcc Permut
......
......@@ -134,7 +134,11 @@ theory map.Map
syntax function ([]) "<app>%1%2</app>"
syntax function set "<app><const name=\"Fun.fun_upd\"/>%1%2%3</app>"
syntax function ([<-]) "<app><const name=\"Fun.fun_upd\"/>%1%2%3</app>"
end
theory map.Const
syntax function const "<app><const name=\"_type_constraint_\"><fun>%t0%t0</fun></const><abs name=\"\"><type name=\"dummy\"/>%1</abs></app>"
end
theory set.SetGen
......
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2015 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require map.Map.
(* Why3 goal *)
Definition const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
b -> (map.Map.map a b).
intros a a_WT b b_WT v.
constructor; intros i.
exact v.
Defined.
(* Why3 goal *)
Lemma Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (b1:b) (a1:a), ((map.Map.get (const b1: (map.Map.map a b))
a1) = b1).
intros a a_WT b b_WT b1 a1.
unfold const.
auto.
Qed.
......@@ -6,8 +6,6 @@ section {* Generic Maps *}
why3_open "map/Map.xml"
why3_vc Const by simp
why3_vc Select_eq
using assms
by simp
......@@ -19,6 +17,15 @@ why3_vc Select_neq
why3_end
section {* Constant Maps *}
why3_open "map/Const.xml"
why3_vc Const by simp
why3_end
section {* Number of occurrences *}
definition occ :: "'a \<Rightarrow> (int \<Rightarrow> 'a) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int" where
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment