Implemented printer for Isabelle

.gitignore

@@ -134,6 +134,11 @@ orphaned-proofs.prf
 /lib/pvs/*/*.summary
 pvsbin/
 
+# Isabelle
+/lib/isabelle/*.xml
+/lib/isabelle/int/*.xml
+/lib/isabelle/real/*.xml
+
 # /src/driver/
 /src/driver/driver_lexer.ml
 /src/driver/driver_parser.ml
@@ -166,6 +171,7 @@ pvsbin/
 # /drivers
 /drivers/coq-realizations.aux
 /drivers/pvs-realizations.aux
+/drivers/isabelle-realizations.aux
 
 # /tests/
 /tests/test-jcf/

Makefile.in

@@ -128,7 +128,7 @@ LIB_TRANSFORM = simplify_formula inlining split_goal induction \
 		introduction abstraction close_epsilon lift_epsilon \
 		eval_match instantiate_predicate smoke_detector
 
-LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 coq pvs \
+LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 coq pvs isabelle \
 		simplify gappa cvc3 yices mathematica
 
 LIB_SESSION = xml termcode session session_tools session_scheduler
@@ -1047,6 +1047,103 @@ opt byte: drivers/pvs-realizations.aux
 clean::
 	rm -f drivers/pvs-realizations.aux
 
+#######################
+# Isabelle realizations
+#######################
+
+ifeq (@enable_isabelle_libs@,yes)
+
+ISABELLELIBS_INT_FILES = Exponentiation Abs ComputerDivision Div2 EuclideanDivision Int MinMax Power
+ISABELLELIBS_INT = $(addsuffix .xml, $(addprefix lib/isabelle/int/, $(ISABELLELIBS_INT_FILES)))
+
+ISABELLELIBS_BOOL_FILES = Bool
+ISABELLELIBS_BOOL = $(addsuffix .xml, $(addprefix lib/isabelle/, $(ISABELLELIBS_BOOL_FILES)))
+
+ISABELLELIBS_REAL_FILES = Abs ExpLog FromInt MinMax PowerInt Real Square RealInfix
+ISABELLELIBS_REAL = $(addsuffix .xml, $(addprefix lib/isabelle/real/, $(ISABELLELIBS_REAL_FILES)))
+
+ISABELLELIBS_NUMBER_FILES = Divisibility Gcd Parity Prime
+ISABELLELIBS_NUMBER = $(addsuffix .xml, $(addprefix lib/isabelle/, $(ISABELLELIBS_NUMBER_FILES)))
+
+ISABELLELIBS_SET_FILES = Set Fset
+ISABELLELIBS_SET = $(addsuffix .xml, $(addprefix lib/isabelle/, $(ISABELLELIBS_SET_FILES)))
+
+ISABELLELIBS_MAP_FILES = Map MapPermut
+ISABELLELIBS_MAP = $(addsuffix .xml, $(addprefix lib/isabelle/, $(ISABELLELIBS_MAP_FILES)))
+
+ISABELLELIBS_LIST_FILES = List Length Mem Nth NthNoOpt NthLength HdTl NthHdTl Append NthLengthAppend Reverse
+ISABELLELIBS_LIST = $(addsuffix .xml, $(addprefix lib/isabelle/, $(ISABELLELIBS_LIST_FILES)))
+
+drivers/isabelle-realizations.aux: Makefile
+	$(if $(QUIET),@echo 'Generate $@' &&) \
+	(echo "(* generated automatically at compilation time *)"; \
+	echo 'theory BuiltIn meta "realized_theory" "BuiltIn", "" end'; \
+	for f in $(ISABELLELIBS_INT_FILES); do \
+	echo 'theory int.'"$$f"' meta "realized_theory" "int.'"$$f"'", "" end'; done; \
+	for f in $(ISABELLELIBS_BOOL_FILES); do \
+	echo 'theory bool.'"$$f"' meta "realized_theory" "bool.'"$$f"'", "" end'; done; \
+	for f in $(ISABELLELIBS_REAL_FILES); do \
+	echo 'theory real.'"$$f"' meta "realized_theory" "real.'"$$f"'", "" end'; done; \
+	for f in $(ISABELLELIBS_NUMBER_FILES); do \
+	echo 'theory number.'"$$f"' meta "realized_theory" "number.'"$$f"'", "" end'; done; \
+	for f in $(ISABELLELIBS_SET_FILES); do \
+	echo 'theory set.'"$$f"' meta "realized_theory" "set.'"$$f"'", "" end'; done; \
+	for f in $(ISABELLELIBS_MAP_FILES); do \
+	echo 'theory map.'"$$f"' meta "realized_theory" "map.'"$$f"'", "" end'; done; \
+	for f in $(ISABELLELIBS_LIST_FILES); do \
+	echo 'theory list.'"$$f"' meta "realized_theory" "list.'"$$f"'", "" end'; done; \
+	for f in $(ISABELLELIBS_OPTION_FILES); do \
+	echo 'theory option.'"$$f"' meta "realized_theory" "option.'"$$f"'", "" end'; done; \
+	) > $@
+
+install_no_local::
+	cp -r lib/isabelle $(LIBDIR)/why3
+	cp drivers/isabelle-realizations.aux $(DATADIR)/why3/drivers/
+
+update-isabelle: $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION)
+
+$(ISABELLELIBS_INT): bin/why3 drivers/isabelle-realizations.aux \
+  drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/int.why
+	mkdir -p lib/isabelle/int/
+	WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/isabelle-realize.drv -T int.$(notdir $(basename $@)) -o lib/isabelle/int/
+
+$(ISABELLELIBS_BOOL): bin/why3 drivers/isabelle-realizations.aux \
+  drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/int.why
+	WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/isabelle-realize.drv -T bool.$(notdir $(basename $@)) -o lib/isabelle/
+
+$(ISABELLELIBS_REAL): bin/why3 drivers/isabelle-realizations.aux \
+  drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/int.why
+	mkdir -p lib/isabelle/real/
+	WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/isabelle-realize.drv -T real.$(notdir $(basename $@)) -o lib/isabelle/real/
+
+$(ISABELLELIBS_NUMBER): bin/why3 drivers/isabelle-realizations.aux \
+  drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/int.why
+	WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/isabelle-realize.drv -T number.$(notdir $(basename $@)) -o lib/isabelle/
+
+$(ISABELLELIBS_SET): bin/why3 drivers/isabelle-realizations.aux \
+  drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/int.why
+	WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/isabelle-realize.drv -T set.$(notdir $(basename $@)) -o lib/isabelle/
+
+$(ISABELLELIBS_MAP): bin/why3 drivers/isabelle-realizations.aux \
+  drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/int.why
+	WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/isabelle-realize.drv -T map.$(notdir $(basename $@)) -o lib/isabelle/
+
+$(ISABELLELIBS_LIST): bin/why3 drivers/isabelle-realizations.aux \
+  drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/int.why
+	WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/isabelle-realize.drv -T list.$(notdir $(basename $@)) -o lib/isabelle/
+
+$(ISABELLELIBS_OPTION): bin/why3 drivers/isabelle-realizations.aux \
+  drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/int.why
+	WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/isabelle-realize.drv -T option.$(notdir $(basename $@)) -o lib/isabelle/
+
+opt byte: update-isabelle
+
+clean::
+	rm -f drivers/isabelle-realizations.aux
+	rm -rf lib/isabelle/*.xml lib/isabelle/int lib/isabelle/real
+
+endif
+
 ################
 # Jessie3 plugin
 ################

configure.in

@@ -97,6 +97,12 @@ AC_ARG_ENABLE(pvs-libs,
     [  --enable-pvs-libs       enable PVS realizations],,
     enable_pvs_libs=yes)
 
+# Isabelle libraries
+
+AC_ARG_ENABLE(isabelle-libs,
+    [  --enable-isabelle-libs       enable Isabelle realizations],,
+    enable_isabelle_libs=yes)
+
 # hypothesis selection
 
 AC_ARG_ENABLE(hypothesis-selection,
@@ -527,6 +533,41 @@ else
    COMPILETIMEPVS="\\\"PVS\\\", \\\"$PVSVERSION\\\"; "
 fi
 
+# Isabelle
+
+if test "$enable_isabelle_libs" = no; then
+    enable_isabelle_support=no
+    AC_MSG_WARN(Isabelle support disabled)
+    reason_isabelle_support=" (disabled by user)"
+else
+    AC_CHECK_PROG(ISABELLE,isabelle,isabelle,no)
+    if test "$ISABELLE" = no ; then
+        enable_isabelle_support=no
+        AC_MSG_WARN(Cannot find isabelle.)
+        reason_isabelle_support=" (isabelle not found)"
+    else
+        AC_MSG_CHECKING(Isabelle version)
+        ISABELLEVERSION=`$ISABELLE version | sed -n -e 's|Isabelle\([[^:]]*\).*$|\1|p' `
+
+        case $ISABELLEVERSION in
+          2013-1)
+	        enable_isabelle_support=yes
+                AC_MSG_RESULT($ISABELLEVERSION)
+                ;;
+          *)
+                AC_MSG_RESULT($ISABELLEVERSION)
+                enable_isabelle_support=no
+	        AC_MSG_WARN(You need Isabelle2013-1 or higher; Isabelle discarded)
+                reason_isabelle_support=" (need version 2013-1 or higher)"
+                ;;
+        esac
+    fi
+fi
+
+if test "$enable_isabelle_support" = no; then
+   enable_isabelle_libs=no
+fi
+
 if test "$enable_pvs_libs" = yes; then
    AC_MSG_CHECKING([for NASA PVS library])
    enable_pvs_libs=no
@@ -654,6 +695,10 @@ AC_SUBST(PVS)
 AC_SUBST(PVSVERSION)
 AC_SUBST(COMPILETIMEPVS)
 
+AC_SUBST(enable_isabelle_libs)
+AC_SUBST(ISABELLE)
+AC_SUBST(ISABELLEVERSION)
+
 AC_SUBST(enable_hypothesis_selection)
 
 AC_SUBST(enable_doc)
@@ -725,6 +770,11 @@ if test "$enable_pvs_support" = yes ; then
    echo "    Library path        : $PVSLIB"
    echo "    Realization support : $enable_pvs_libs$reason_pvs_libs"
 fi
+echo "Isabelle support        : $enable_isabelle_support$reason_isabelle_support"
+if test "$enable_isabelle_support" = yes ; then
+   echo "    Version             : $ISABELLEVERSION"
+   echo "    Realization support : $enable_isabelle_libs$reason_isabelle_libs"
+fi
 echo "Frama-C support         : $enable_frama_c$reason_frama_c"
 if test "$enable_frama_c" = yes ; then
    echo "    Version             : $FRAMAC_VERSION"

drivers/isabelle-common.gen

+valid "Finished Why3 theory"
+fail "\\*\\*\\* \\(.*\\)$" "\\1"
+time "why3cpulimit time : %s s"
+
+transformation "eliminate_projections"
+
+transformation "simplify_formula"
+
+theory BuiltIn
+  syntax type int "<type name=\"Int.int\"/>"
+  syntax type real "<type name=\"Real.real\"/>"
+
+  syntax predicate  (=)   "<app><const name=\"HOL.eq\"/>%1%2</app>"
+end
+
+theory Bool
+  syntax type bool   "<type name=\"HOL.bool\"/>"
+
+  syntax function True  "<const name=\"HOL.True\"/>"
+  syntax function False "<const name=\"HOL.False\"/>"
+end
+
+theory bool.Bool
+  syntax function andb  "<app><const name=\"HOL.conj\"/>%1%2</app>"
+  syntax function orb   "<app><const name=\"HOL.disj\"/>%1%2</app>"
+  syntax function notb  "<app><const name=\"HOL.Not\"/>%1</app>"
+  syntax function implb "<app><const name=\"HOL.implies\"/>%1%2</app>"
+end
+
+theory int.Int
+  syntax function zero "<number val=\"0\"><type name=\"Int.int\"/></number>"
+  syntax function one  "<number val=\"1\"><type name=\"Int.int\"/></number>"
+
+  syntax function (+)  "<app><const name=\"Groups.plus_class.plus\"/>%1%2</app>"
+  syntax function (-)  "<app><const name=\"Groups.minus_class.minus\"/>%1%2</app>"
+  syntax function (*)  "<app><const name=\"Groups.times_class.times\"/>%1%2</app>"
+  syntax function (-_) "<app><const name=\"Groups.uminus_class.uminus\"/>%1</app>"
+
+  syntax predicate (<=) "<app><const name=\"Orderings.ord_class.less_eq\"/>%1%2</app>"
+  syntax predicate (<)  "<app><const name=\"Orderings.ord_class.less\"/>%1%2</app>"
+  syntax predicate (>=) "<app><const name=\"Orderings.ord_class.less_eq\"/>%2%1</app>"
+  syntax predicate (>)  "<app><const name=\"Orderings.ord_class.less\"/>%2%1</app>"
+
+  remove prop CommutativeGroup.Comm.Comm
+  remove prop CommutativeGroup.Assoc
+  remove prop CommutativeGroup.Unit_def_l
+  remove prop CommutativeGroup.Unit_def_r
+  remove prop CommutativeGroup.Inv_def_l
+  remove prop CommutativeGroup.Inv_def_r
+  remove prop Assoc.Assoc
+  remove prop Mul_distr_l
+  remove prop Mul_distr_r
+  remove prop Comm.Comm
+  remove prop Unitary
+  remove prop Refl
+  remove prop Trans
+  remove prop Antisymm
+  remove prop Total
+  remove prop NonTrivialRing
+  remove prop CompatOrderAdd
+  remove prop CompatOrderMult
+  remove prop ZeroLessOne
+end
+
+theory int.Abs
+  syntax function abs "<app><const name=\"Groups.abs_class.abs\"/>%1</app>"
+
+  remove prop Abs_pos
+end
+
+theory int.MinMax
+  syntax function min "<app><const name=\"Orderings.ord_class.min\"/>%1%2</app>"
+  syntax function max "<app><const name=\"Orderings.ord_class.max\"/>%1%2</app>"
+end
+
+theory int.EuclideanDivision
+  syntax function div "<app><const name=\"Divides.div_class.div\"/>%1%2</app>"
+  syntax function mod "<app><const name=\"Divides.div_class.mod\"/>%1%2</app>"
+
+  remove prop Div_mod
+  remove prop Div_bound
+  remove prop Mod_bound
+  remove prop Mod_1
+  remove prop Div_1
+end
+
+theory list.List
+  syntax type list "<type name=\"List.list\">%1</type>"
+
+  syntax function Nil "<const name=\"List.list.Nil\">%t0</const>"
+  syntax function Cons "<app><const name=\"List.list.Cons\"/>%1%2</app>"
+end
+
+theory list.Length
+  syntax function length "<app><const name=\"Nat.semiring_1_class.of_nat\"><fun><type name=\"Nat.nat\"/><type name=\"Int.int\"/></fun></const><app><const name=\"List.length\"/>%1</app></app>"
+end
+
+theory list.Append
+  syntax function (++) "<app><const name=\"List.append\"/>%1%2</app>"
+end
+
+theory list.Reverse
+  syntax function reverse "<app><const name=\"List.rev\"/>%1</app>"
+end
+
+theory list.Mem
+  syntax predicate mem "<app><const name=\"Set.member\"/>%1<app><const name=\"List.set\"/>%2</app></app>"
+end
+
+theory list.NthNoOpt
+  syntax function nth "<app><const name=\"List.nth\"/>%2<app><const name=\"Int.nat\"/>%1</app></app>"
+end
+
+theory option.Option
+  syntax type option "<type name=\"Option.option\">%1</type>"
+
+  syntax function None "<const name=\"Option.option.None\">%t0</const>"
+  syntax function Some "<app><const name=\"Option.option.Some\"/>%1</app>"
+end
+
+theory map.Map
+  syntax type  map "<fun>%1%2</fun>"
+
+  syntax function get "<app>%1%2</app>"
+  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 set.SetGen
+  syntax predicate (==) "<app><const name=\"HOL.eq\"/>%1%2</app>"
+  syntax predicate subset "<app><const name=\"Orderings.ord_class.less_eq\"/>%1%2</app>"
+end
+
+theory set.Fset
+  syntax function cardinal "<app><const name=\"Nat.semiring_1_class.of_nat\"><fun><type name=\"Nat.nat\"/><type name=\"Int.int\"/></fun></const><app><const name=\"FSet.fcard\"/>%1</app></app>"
+end
+
+(* this file has an extension .aux rather than .gen since it should not be distributed *)
+import "isabelle-realizations.aux"

drivers/isabelle-realize.drv

+printer "isabelle-realize"
+filename "%t.xml"
+
+transformation "inline_trivial"
+
+import "isabelle-common.gen"

drivers/isabelle.drv

+printer "isabelle"
+filename "%f_%t_%g.xml"
+
+transformation "inline_trivial"
+transformation "eliminate_builtin"
+
+import "isabelle-common.gen"

lib/isabelle/ROOT

+chapter Why3
+
+session Why3 = HOL +
+  options [document = false]
+  theories Why3

lib/isabelle/Tools/why3

+#!/usr/bin/env bash
+#
+# DESCRIPTION: process files generated by Why3
+
+
+## diagnostics
+
+PRG="$(basename "$0")"
+
+function usage()
+{
+  echo
+  echo "Usage: isabelle $PRG [OPTIONS] WHY3_FILE"
+  echo
+  echo "  Options are:"
+  echo "    -b           batch mode"
+  echo "    -i NAME      interactive mode using interface NAME"
+  echo
+  echo "  Process files generated by Why3"
+  exit 1
+}
+
+
+## utilities
+
+function make_theory()
+{
+  BNAME=`basename "$1"`
+
+  if [ ! -e "$1.thy" ]; then
+    sed \
+      -e "s/<theory[^>]*>/theory $BNAME\nimports Why3\nbegin\n\nwhy3_open \"$BNAME\.xml\"\n\n/g" \
+      -e 's/<lemma name="\([^"]*\)"[^>]*>/why3_vc \1\n\n/g' \
+      -e 's/<\/theory>/why3_end\n\nend\n/g' \
+      -e 's/<[^tl\/][^>]*>//g' \
+      -e 's/<type[^>]*>//g' \
+      -e 's/<tvar[^>]*>//g' \
+      -e 's/<\/[^t][^>]*>//g' \
+      -e 's/<\/type[^>]*>//g' \
+      -e 's/<\/tvar[^>]*>//g' \
+      "$1.xml" > "$1.thy"
+  fi
+}
+
+
+## process command line
+
+while getopts "bi:" OPT
+do
+  case "$OPT" in
+    b)
+      BATCH=true
+      ;;
+    i)
+      INTERACTIVE=true
+      INTERFACE="$OPTARG"
+      ;;
+    \?)
+      usage
+      ;;
+  esac
+done
+
+
+## main
+
+shift $(($OPTIND - 1))
+
+if [ "$1" = "" ]; then
+  usage
+else
+  NAME=`dirname "$1"`/`basename "$1" .xml`
+fi
+
+if [ "$BATCH" = true ]; then
+  $ISABELLE_PROCESS -e "use_thy \"$NAME\";" -rq Why3
+elif [ "$INTERACTIVE" = true ]; then
+  if [ "$INTERFACE" = emacs ]; then
+    LOGIC="-L"
+  else
+    LOGIC="-l"
+  fi
+  make_theory "$NAME"
+  $ISABELLE_TOOL $INTERFACE $LOGIC Why3 "$NAME.thy"
+else
+  usage
+fi

lib/isabelle/Why3.thy

+theory Why3
+imports Why3_Set Why3_List
+begin
+
+end

lib/isabelle/Why3_List.thy

+theory Why3_List
+imports Why3_Setup
+begin
+
+section {* Length of a list *}
+
+why3_open "Length.xml"
+
+why3_vc length_def by (cases l) simp_all
+
+why3_vc Length_nil by simp
+
+why3_vc Length_nonnegative by simp
+
+why3_end
+
+
+section {* Membership in a list *}
+
+why3_open "Mem.xml"
+
+why3_vc mem_def by (simp split add: list.split)
+
+why3_end
+
+
+section {* Nth element of a list *}
+
+why3_open "Nth.xml"
+
+why3_end
+
+
+why3_open "NthNoOpt.xml"
+
+why3_vc nth_cons_0 by simp
+
+why3_vc nth_cons_n
+  using assms
+  by (simp add: nat_diff_distrib)
+
+why3_end
+
+
+why3_open "NthLength.xml"
+
+why3_vc nth_none_1
+  using assms
+  by (induct l arbitrary: i) simp_all
+
+why3_vc nth_none_2
+  using assms
+  by (induct l arbitrary: i) simp_all
+
+why3_vc nth_none_3
+  using assms
+proof (induct l arbitrary: i)
+  case Nil
+  then show ?case by simp arith
+next
+  case (Cons x xs)
+  show ?case
+  proof (cases "i < 0")
+    case False
+    with Cons have "0 < i" by (simp split add: split_if_asm)
+    with Cons have "Nth.nth (i - 1) xs = None" by simp
+    then have "i - 1 < 0 \<or> int (length xs) \<le> i - 1"
+      by (rule Cons)
+    with `0 < i` show ?thesis by auto
+  qed simp
+qed
+
+why3_end
+
+end

lib/isabelle/Why3_Set.thy

+theory Why3_Set
+imports Why3_Setup "~~/src/HOL/Library/FSet"
+begin
+
+section {* Potentially infinite sets *}
+
+definition choose :: "'a set \<Rightarrow> 'a" where
+  "choose S = (\<some>x. x \<in> S)"
+
+why3_open "Set.xml"
+  constants
+    mem = Set.member
+    empty = bot
+    add = insert
+    remove = Set.remove
+    union = sup
+    inter = inf
+    diff = minus
+    choose = choose
+    all = top
+  types
+    set = set
+
+why3_vc all_def by simp
+
+why3_vc add_def1 by simp
+
+why3_vc diff_def1 by simp
+
+why3_vc mem_empty by simp
+
+why3_vc add_remove
+  using assms
+  by (auto simp add: remove_def)
+
+why3_vc remove_add by (simp add: remove_def)
+
+why3_vc choose_def
+  using assms
+  by (auto simp add: is_empty_def choose_def intro: someI_ex)
+
+why3_vc empty_def1 by (simp add: is_empty_def)
+
+why3_vc inter_def1 by simp
+
+why3_vc union_def1 by simp
+
+why3_vc remove_def1 by (auto simp add: remove_def)
+
+why3_vc subset_diff by auto
+
+why3_vc subset_def by auto
+
+why3_vc subset_refl by simp
+
+why3_vc subset_trans
+  using assms
+  by simp
+
+why3_vc subset_remove by (auto simp add: remove_def)
+
+why3_vc extensionality
+  using assms
+  by simp
+
+why3_vc infix_eqeq_def by auto
+
+why3_end
+
+
+section {* Finite sets *}
+
+definition fremove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
+  "fremove x A = A - {|x|}"
+
+definition fchoose :: "'a fset \<Rightarrow> 'a" where
+  "fchoose S = (\<some>x. x |\<in>| S)"
+
+why3_open "Fset.xml"
+  constants
+    mem = fmember
+    empty = bot
+    add = finsert
+    remove = fremove
+    union = sup
+    inter = inf
+    diff = minus
+    choose = fchoose
+    all = top
+  types
+    set = fset
+
+why3_vc add_def1 by simp
+
+why3_vc diff_def1 by simp
+
+why3_vc mem_empty by simp
+
+why3_vc add_remove
+  using assms
+  by (auto simp add: fremove_def)
+
+why3_vc remove_add by (simp add: fremove_def)
+
+why3_vc choose_def
+  using assms
+  by (auto simp add: is_empty_def fchoose_def intro: someI_ex)
+
+why3_vc empty_def1 by (simp add: is_empty_def)
+
+why3_vc inter_def1 by simp
+
+why3_vc union_def1 by simp
+
+why3_vc remove_def1 by (auto simp add: fremove_def)
+
+why3_vc subset_diff by auto
+
+why3_vc subset_def by auto
+
+why3_vc subset_refl by simp
+
+why3_vc subset_trans
+  using assms
+  by simp
+
+why3_vc subset_remove by (auto simp add: fremove_def)
+
+why3_vc extensionality