Commit 735bf89c authored by Stefan Berghofer's avatar Stefan Berghofer Committed by MARCHE Claude

Adapted to Isabelle2014

parent a94b5657
...@@ -574,7 +574,7 @@ else ...@@ -574,7 +574,7 @@ else
ISABELLEVERSION=`$ISABELLE version | sed -n -e 's|Isabelle\([[^:]]*\).*$|\1|p' ` ISABELLEVERSION=`$ISABELLE version | sed -n -e 's|Isabelle\([[^:]]*\).*$|\1|p' `
case $ISABELLEVERSION in case $ISABELLEVERSION in
2013-2) 2014*)
enable_isabelle_support=yes enable_isabelle_support=yes
AC_MSG_RESULT($ISABELLEVERSION) AC_MSG_RESULT($ISABELLEVERSION)
;; ;;
......
...@@ -104,7 +104,7 @@ theory list.Reverse ...@@ -104,7 +104,7 @@ theory list.Reverse
end end
theory list.Mem theory list.Mem
syntax predicate mem "<app><const name=\"Set.member\"/>%1<app><const name=\"List.set\"/>%2</app></app>" syntax predicate mem "<app><const name=\"Set.member\"/>%1<app><const name=\"List.list.set\"/>%2</app></app>"
end end
theory list.NthNoOpt theory list.NthNoOpt
...@@ -112,8 +112,8 @@ theory list.NthNoOpt ...@@ -112,8 +112,8 @@ theory list.NthNoOpt
end end
theory list.HdTlNoOpt theory list.HdTlNoOpt
syntax function hd "<app><const name=\"List.hd\"/>%1</app>" syntax function hd "<app><const name=\"List.list.hd\"/>%1</app>"
syntax function tl "<app><const name=\"List.tl\"/>%1</app>" syntax function tl "<app><const name=\"List.list.tl\"/>%1</app>"
end end
theory list.Distinct theory list.Distinct
...@@ -148,7 +148,7 @@ end ...@@ -148,7 +148,7 @@ end
theory number.Parity theory number.Parity
syntax predicate even "<app><const name=\"Parity.even_odd_class.even\"/>%1</app>" syntax predicate even "<app><const name=\"Parity.even_odd_class.even\"/>%1</app>"
syntax predicate odd "<app><const name=\"Parity.odd\"/>%1</app>" syntax predicate odd "<app><const name=\"Parity.even_odd_class.odd\"/>%1</app>"
end end
theory number.Divisibility theory number.Divisibility
...@@ -160,7 +160,7 @@ theory number.Gcd ...@@ -160,7 +160,7 @@ theory number.Gcd
end end
theory number.Prime theory number.Prime
syntax predicate prime "<app><const name=\"Primes.prime_class.prime\"/>%1</app>" syntax predicate prime "<app><const name=\"Primes.prime\"/><app><const name=\"Int.nat\"/>%1</app></app>"
end end
theory number.Coprime theory number.Coprime
......
...@@ -108,9 +108,9 @@ why3_vc Div_inf_neg ...@@ -108,9 +108,9 @@ why3_vc Div_inf_neg
zdiv_zminus1_eq_if div_pos_pos_trivial mod_pos_pos_trivial) zdiv_zminus1_eq_if div_pos_pos_trivial mod_pos_pos_trivial)
why3_vc Div_mod why3_vc Div_mod
by (simp add: ediv_def emod_def mult_assoc [symmetric] abs_sgn) by (simp add: ediv_def emod_def mult.assoc [symmetric] abs_sgn)
why3_vc Div_mult using assms by (simp add: ediv_def add_commute) why3_vc Div_mult using assms by (simp add: ediv_def add.commute)
why3_vc Div_bound why3_vc Div_bound
proof - proof -
...@@ -145,7 +145,7 @@ why3_vc Mod_minus1_left ...@@ -145,7 +145,7 @@ why3_vc Mod_minus1_left
using assms using assms
by (simp only: emod_def zmod_zminus1_eq_if) (simp add: mod_pos_pos_trivial) by (simp only: emod_def zmod_zminus1_eq_if) (simp add: mod_pos_pos_trivial)
why3_vc Mod_mult using assms by (simp add: emod_def add_commute) why3_vc Mod_mult using assms by (simp add: emod_def add.commute)
why3_vc Mod_bound using assms by (simp_all add: emod_def) why3_vc Mod_bound using assms by (simp_all add: emod_def)
...@@ -194,7 +194,7 @@ proof (cases "y = 0") ...@@ -194,7 +194,7 @@ proof (cases "y = 0")
case False case False
with assms show ?thesis with assms show ?thesis
by (cases "z = 0") by (cases "z = 0")
(simp_all add: cdiv_def add_commute add_pos_pos mult_nonneg_nonneg mult_pos_pos) (simp_all add: cdiv_def add.commute add_pos_pos mult_nonneg_nonneg mult_pos_pos)
qed simp qed simp
why3_vc Div_bound why3_vc Div_bound
...@@ -224,7 +224,7 @@ proof (cases "y = 0") ...@@ -224,7 +224,7 @@ proof (cases "y = 0")
case False case False
with assms show ?thesis with assms show ?thesis
by (cases "z = 0") (simp_all add: cmod_def by (cases "z = 0") (simp_all add: cmod_def
add_commute add_pos_pos mult_nonneg_nonneg mult_pos_pos) add.commute add_pos_pos mult_nonneg_nonneg mult_pos_pos)
qed simp qed simp
why3_vc Mod_bound why3_vc Mod_bound
......
...@@ -37,7 +37,7 @@ section {* Divisibility *} ...@@ -37,7 +37,7 @@ section {* Divisibility *}
why3_open "number/Divisibility.xml" why3_open "number/Divisibility.xml"
why3_vc divides_def by (simp add: dvd_def mult_commute) why3_vc divides_def by (simp add: dvd_def mult.commute)
why3_vc divides_refl by simp why3_vc divides_refl by simp
...@@ -98,14 +98,14 @@ why3_vc divides_mod_computer ...@@ -98,14 +98,14 @@ why3_vc divides_mod_computer
by (simp add: cmod_def dvd_eq_mod_eq_0 zabs_def by (simp add: cmod_def dvd_eq_mod_eq_0 zabs_def
zmod_zminus1_eq_if zmod_zminus2_eq_if) zmod_zminus1_eq_if zmod_zminus2_eq_if)
why3_vc even_divides by (rule int_even_iff_2_dvd) why3_vc even_divides by (rule even_iff_2_dvd)
why3_vc odd_divides by (simp add: int_even_iff_2_dvd) why3_vc odd_divides by (simp add: even_iff_2_dvd)
why3_end why3_end
section {* Greateast Common Divisor *} section {* Greatest Common Divisor *}
why3_open "number/Gcd.xml" why3_open "number/Gcd.xml"
...@@ -155,11 +155,11 @@ section {* Prime numbers *} ...@@ -155,11 +155,11 @@ section {* Prime numbers *}
why3_open "number/Prime.xml" why3_open "number/Prime.xml"
why3_vc prime_def why3_vc prime_def
unfolding prime_int_altdef unfolding prime_def
proof proof
assume "1 < p \<and> (\<forall>m\<ge>0. m dvd p \<longrightarrow> m = 1 \<or> m = p)" assume "1 < nat p \<and> (\<forall>m. m dvd nat p \<longrightarrow> m = 1 \<or> m = nat p)"
then have "1 < p" and H: "\<And>m. m \<ge> 0 \<Longrightarrow> m dvd p \<Longrightarrow> m = 1 \<or> m = p" then have "1 < p" and H: "\<And>m. m \<ge> 0 \<Longrightarrow> m dvd p \<Longrightarrow> m = 1 \<or> m = p"
by auto by (auto simp add: dvd_int_iff)
show "2 \<le> p \<and> (\<forall>n. 1 < n \<and> n < p \<longrightarrow> \<not> n dvd p)" show "2 \<le> p \<and> (\<forall>n. 1 < n \<and> n < p \<longrightarrow> \<not> n dvd p)"
proof proof
from `1 < p` show "2 \<le> p" by simp from `1 < p` show "2 \<le> p" by simp
...@@ -173,25 +173,25 @@ proof ...@@ -173,25 +173,25 @@ proof
qed qed
next next
assume "2 \<le> p \<and> (\<forall>n. 1 < n \<and> n < p \<longrightarrow> \<not> n dvd p)" assume "2 \<le> p \<and> (\<forall>n. 1 < n \<and> n < p \<longrightarrow> \<not> n dvd p)"
then have "2 \<le> p" and H: "\<And>n. 1 < n \<Longrightarrow> n < p \<Longrightarrow> \<not> n dvd p" then have "2 \<le> p" and H: "\<And>n. 1 < n \<Longrightarrow> n < nat p \<Longrightarrow> \<not> n dvd p"
by auto by auto
show "1 < p \<and> (\<forall>m\<ge>0. m dvd p \<longrightarrow> m = 1 \<or> m = p)" show "1 < nat p \<and> (\<forall>m. m dvd nat p \<longrightarrow> m = 1 \<or> m = nat p)"
proof proof
from `2 \<le> p` show "1 < p" by simp from `2 \<le> p` show "1 < nat p" by simp
show "\<forall>m\<ge>0. m dvd p \<longrightarrow> m = 1 \<or> m = p" show "\<forall>m. m dvd nat p \<longrightarrow> m = 1 \<or> m = nat p"
proof (intro strip) proof (intro strip)
fix m fix m
assume "0 \<le> m" "m dvd p" assume "m dvd nat p"
with `2 \<le> p` have "1 \<le> m" by (cases "m = 0") auto with `2 \<le> p` have "1 \<le> m" by (cases "m = 0") auto
show "m = 1 \<or> m = p" show "m = 1 \<or> m = nat p"
proof (cases "m = 1") proof (cases "m = 1")
case False case False
show ?thesis show ?thesis
proof (cases "m = p") proof (cases "m = nat p")
case False case False
from `2 \<le> p` `m dvd p` have "m \<le> p" by (simp add: zdvd_imp_le) from `2 \<le> p` `m dvd nat p` have "m \<le> nat p" by (simp add: dvd_imp_le)
with False `m \<noteq> 1` `1 \<le> m` `m dvd p` H show ?thesis by simp with False `m \<noteq> 1` `1 \<le> m` `m dvd nat p` H show ?thesis by (simp add: int_dvd_iff)
qed simp qed simp
qed simp qed simp
qed qed
...@@ -261,28 +261,30 @@ proof ...@@ -261,28 +261,30 @@ proof
then have "\<exists>d. prime d \<and> d * d \<le> nat p \<and> d dvd (nat p)" then have "\<exists>d. prime d \<and> d * d \<le> nat p \<and> d dvd (nat p)"
by (rule small_divisors_aux) by (rule small_divisors_aux)
with `2 \<le> p` obtain d with `2 \<le> p` obtain d
where d: "prime (int d)" "int d * int d \<le> p" "int d dvd p" where d: "prime d" "d * d \<le> p" "d dvd p"
by (auto simp add: prime_int_def int_dvd_iff le_nat_iff int_mult) by (auto simp add: int_dvd_iff le_nat_iff int_mult)
from `prime (int d)` have "2 \<le> int d" by auto from `prime d` have "2 \<le> d" by auto
then have "2 \<le> int d" by simp
with `2 \<le> int d` have "2 * 2 \<le> int d * int d" with `2 \<le> int d` have "2 * 2 \<le> int d * int d"
by (rule mult_mono) simp_all by (rule mult_mono) simp_all
with d assms `2 \<le> int d` show False by auto with d assms `2 \<le> d` show False by auto
qed qed
qed qed
qed qed
why3_vc even_prime why3_vc even_prime
proof - proof -
from `prime p` have "2 \<le> p" by auto from `prime (nat p)` have "0 \<le> p" by (simp add: prime_def)
with `prime p` `even p` show ?thesis from `prime (nat p)` have "2 \<le> nat p" by auto
by (auto simp add: order_le_less prime_odd_int) with `prime (nat p)` `even p` `0 \<le> p` show ?thesis
by (auto simp add: order_le_less prime_odd_nat pos_int_even_equiv_nat_even)
qed qed
why3_vc odd_prime why3_vc odd_prime
proof - proof -
from `prime p` have "2 \<le> p" by auto from `prime (nat p)` have "2 \<le> nat p" by auto
with `prime p` `3 \<le> p` show ?thesis with `prime (nat p)` `3 \<le> p` show ?thesis
by (auto simp add: order_le_less prime_odd_int) by (auto simp add: order_le_less prime_odd_nat pos_int_even_equiv_nat_even)
qed qed
why3_end why3_end
...@@ -337,11 +339,18 @@ qed ...@@ -337,11 +339,18 @@ qed
why3_vc Gauss why3_vc Gauss
proof - proof -
from assms from assms
have "coprime a b" "a dvd c * b" by (simp_all add: mult_commute) have "coprime a b" "a dvd c * b" by (simp_all add: mult.commute)
then show ?thesis by (rule coprime_dvd_mult_int) then show ?thesis by (rule coprime_dvd_mult_int)
qed qed
why3_vc Euclid using assms by auto why3_vc Euclid
proof -
from `p dvd a * b` have "nat \<bar>p\<bar> dvd nat \<bar>a\<bar> * nat \<bar>b\<bar>"
by (simp add: dvd_int_iff abs_mult nat_mult_distrib)
moreover from `prime (nat p)` have "prime (nat \<bar>p\<bar>)"
by (simp add: prime_def)
ultimately show ?thesis by (simp add: dvd_int_iff)
qed
why3_vc gcd_coprime why3_vc gcd_coprime
proof - proof -
......
theory Why3_Setup theory Why3_Setup
imports Main imports Main
keywords keywords
"why3_open" "why3_end" "why3_open" :: thy_load and
"why3_consts" "why3_types" "why3_thms" "why3_defs" :: thy_decl and "why3_end" "why3_consts" "why3_types" "why3_thms" "why3_defs" :: thy_decl and
"why3_vc" :: thy_goal and "why3_status" :: diag "why3_vc" :: thy_goal and "why3_status" :: diag
begin begin
......
...@@ -65,7 +65,7 @@ fun parse_xml s = ...@@ -65,7 +65,7 @@ fun parse_xml s =
(**** terms and types ****) (**** terms and types ****)
(* replace occurrences of dummy_pattern by distinct variables *) (* replace occurrences of dummy_pattern by distinct variables *)
fun replace_dummies (Const (@{const_name dummy_pattern}, T)) used = fun replace_dummies (Const (@{const_name Pure.dummy_pattern}, T)) used =
let val (x, used') = Name.variant "x" used let val (x, used') = Name.variant "x" used
in (Free (x, T), used') end in (Free (x, T), used') end
| replace_dummies (t $ u) used = | replace_dummies (t $ u) used =
...@@ -275,10 +275,10 @@ fun add_qualified add prep (s, x) thy = ...@@ -275,10 +275,10 @@ fun add_qualified add prep (s, x) thy =
(Long_Name.base_name s, prep (Proof_Context.init_global thy) x) thy); (Long_Name.base_name s, prep (Proof_Context.init_global thy) x) thy);
val add_why3_const = add_qualified add_const_raw (fn ctxt => fn cname => val add_why3_const = add_qualified add_const_raw (fn ctxt => fn cname =>
fst (dest_Const (Proof_Context.read_const_proper ctxt false cname))); fst (dest_Const (Proof_Context.read_const {proper = true, strict = false} ctxt cname)));
val add_why3_type = add_qualified add_type_raw (fn ctxt => fn tyname => val add_why3_type = add_qualified add_type_raw (fn ctxt => fn tyname =>
fst (dest_Type (Proof_Context.read_type_name_proper ctxt false tyname))); fst (dest_Type (Proof_Context.read_type_name {proper = true, strict = false} ctxt tyname)));
val add_why3_thm = add_qualified add_thm_raw Attrib.eval_thms; val add_why3_thm = add_qualified add_thm_raw Attrib.eval_thms;
...@@ -780,10 +780,13 @@ fun show_status thy sel = ...@@ -780,10 +780,13 @@ fun show_status thy sel =
(**** commands ****) (**** commands ****)
fun why3_open ((name, consts), types) thy = process_decls fun why3_open ((files, consts), types) thy =
(map (apsnd (Sign.intern_const thy)) consts) let val ([{lines, ...}: Token.file], thy') = files thy;
(map (apsnd (Sign.intern_type thy)) types) in process_decls
(parse_xml (snd (Thy_Load.load_file thy (Path.explode name)))) thy; (map (apsnd (Sign.intern_const thy)) consts)
(map (apsnd (Sign.intern_type thy)) types)
(parse_xml (cat_lines lines)) thy'
end;
fun prove_vc vc_name lthy = fun prove_vc vc_name lthy =
let let
...@@ -799,7 +802,7 @@ fun prove_vc vc_name lthy = ...@@ -799,7 +802,7 @@ fun prove_vc vc_name lthy =
val _ = val _ =
Outer_Syntax.command @{command_spec "why3_open"} Outer_Syntax.command @{command_spec "why3_open"}
"open a new Why3 environment and load a Why3-generated .xml file" "open a new Why3 environment and load a Why3-generated .xml file"
(Parse.name -- (Resources.provide_parse_files "why3_open" --
Scan.optional (Parse.reserved "constants" |-- Parse.!!! (Scan.repeat1 Scan.optional (Parse.reserved "constants" |-- Parse.!!! (Scan.repeat1
(Parse.name --| Args.$$$ "=" -- Parse.!!! Parse.xname))) [] -- (Parse.name --| Args.$$$ "=" -- Parse.!!! Parse.xname))) [] --
Scan.optional (Parse.reserved "types" |-- (Scan.repeat1 Scan.optional (Parse.reserved "types" |-- (Scan.repeat1
...@@ -810,7 +813,7 @@ val _ = ...@@ -810,7 +813,7 @@ val _ =
Outer_Syntax.command @{command_spec "why3_vc"} Outer_Syntax.command @{command_spec "why3_vc"}
"enter into proof mode for a specific verification condition" "enter into proof mode for a specific verification condition"
(Parse.name >> (fn name => (Parse.name >> (fn name =>
(Toplevel.print o Toplevel.local_theory_to_proof NONE (prove_vc name)))); (Toplevel.local_theory_to_proof NONE (prove_vc name))));
val _ = val _ =
Outer_Syntax.improper_command @{command_spec "why3_status"} Outer_Syntax.improper_command @{command_spec "why3_status"}
......
...@@ -160,7 +160,7 @@ let print_abs info pr fmt (v, t) = ...@@ -160,7 +160,7 @@ let print_abs info pr fmt (v, t) =
let p_type p = p.pat_ty let p_type p = p.pat_ty
let rec print_pat info fmt p = match p.pat_node with let rec print_pat info fmt p = match p.pat_node with
| Pwild -> print_const fmt "dummy_pattern" | Pwild -> print_const fmt "Pure.dummy_pattern"
| Pvar v -> print_var info fmt v | Pvar v -> print_var info fmt v
| Pas _ -> | Pas _ ->
assert false assert false
......
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