--- a/Admin/components/components.sha1 Sat Sep 29 16:30:44 2018 -0400
+++ b/Admin/components/components.sha1 Sun Sep 30 18:19:28 2018 -0400
@@ -212,6 +212,7 @@
1636556167dff2c191baf502c23f12e09181ef78 scala-2.12.4.tar.gz
8171f494bba54fb0d01c887f889ab8fde7171c2a scala-2.12.5.tar.gz
54c1b06fa2c5f6c2ab3d391ef342c0532cd7f392 scala-2.12.6.tar.gz
+02358f00acc138371324b6248fdb62eed791c6bd scala-2.12.7.tar.gz
b447017e81600cc5e30dd61b5d4962f6da01aa80 scala-2.8.1.final.tar.gz
5659440f6b86db29f0c9c0de7249b7e24a647126 scala-2.9.2.tar.gz
abe7a3b50da529d557a478e9f631a22429418a67 smbc-0.4.1.tar.gz
--- a/Admin/components/main Sat Sep 29 16:30:44 2018 -0400
+++ b/Admin/components/main Sun Sep 30 18:19:28 2018 -0400
@@ -13,7 +13,7 @@
nunchaku-0.5
polyml-5.7.1-8
postgresql-42.2.2
-scala-2.12.6
+scala-2.12.7
smbc-0.4.1
ssh-java-20161009
spass-3.8ds-1
--- a/NEWS Sat Sep 29 16:30:44 2018 -0400
+++ b/NEWS Sun Sep 30 18:19:28 2018 -0400
@@ -34,15 +34,18 @@
SUPREMUM, UNION, INTER should now rarely occur in output and are just
retained as migration auxiliary. INCOMPATIBILITY.
-* Sledgehammer: The URL for SystemOnTPTP, which is used by remote
-provers, has been updated.
+* Theory List: the precedence of the list_update operator has changed:
+"f a [n := x]" now needs to be written "(f a)[n := x]".
+
+* Theory "HOL-Library.Multiset": the <Union># operator now has the same
+precedence as any other prefix function symbol.
* Facts sum_mset.commute and prod_mset.commute renamed to sum_mset.swap
and prod_mset.swap, similarly to sum.swap and prod.swap.
INCOMPATIBILITY.
-* Theory "HOL-Library.Multiset": the <Union># operator now has the same
-precedence as any other prefix function symbol.
+* Sledgehammer: The URL for SystemOnTPTP, which is used by remote
+provers, has been updated.
*** ML ***
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy Sat Sep 29 16:30:44 2018 -0400
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy Sun Sep 30 18:19:28 2018 -0400
@@ -2258,11 +2258,11 @@
by (simp add: natpermute_def)
from i have i': "i < length (replicate (k+1) 0)" "i < k+1"
unfolding length_replicate by presburger+
- have "xs = replicate (k+1) 0 [i := n]"
+ have "xs = (replicate (k+1) 0) [i := n]"
proof (rule nth_equalityI)
- show "length xs = length (replicate (k + 1) 0[i := n])"
+ show "length xs = length ((replicate (k + 1) 0)[i := n])"
by (metis length_list_update length_replicate xsl)
- show "xs ! j = replicate (k + 1) 0[i := n] ! j" if "j < length xs" for j
+ show "xs ! j = (replicate (k + 1) 0)[i := n] ! j" if "j < length xs" for j
proof (cases "j = i")
case True
then show ?thesis
@@ -2279,7 +2279,7 @@
proof
fix xs
assume "xs \<in> ?B"
- then obtain i where i: "i \<in> {0..k}" and xs: "xs = replicate (k + 1) 0 [i:=n]"
+ then obtain i where i: "i \<in> {0..k}" and xs: "xs = (replicate (k + 1) 0) [i:=n]"
by auto
have nxs: "n \<in> set xs"
unfolding xs
@@ -2292,7 +2292,7 @@
unfolding sum_list_sum_nth xsl ..
also have "\<dots> = sum (\<lambda>j. if j = i then n else 0) {0..< k+1}"
by (rule sum.cong) (simp_all add: xs del: replicate.simps)
- also have "\<dots> = n" using i by (simp add: sum.delta)
+ also have "\<dots> = n" using i by (simp)
finally have "xs \<in> natpermute n (k + 1)"
using xsl unfolding natpermute_def mem_Collect_eq by blast
then show "xs \<in> ?A"
@@ -2395,32 +2395,32 @@
shows "card {xs \<in> natpermute n (k + 1). n \<in> set xs} = k + 1"
unfolding natpermute_contain_maximal
proof -
- let ?A = "\<lambda>i. {replicate (k + 1) 0[i := n]}"
+ let ?A = "\<lambda>i. {(replicate (k + 1) 0)[i := n]}"
let ?K = "{0 ..k}"
have fK: "finite ?K"
by simp
have fAK: "\<forall>i\<in>?K. finite (?A i)"
by auto
have d: "\<forall>i\<in> ?K. \<forall>j\<in> ?K. i \<noteq> j \<longrightarrow>
- {replicate (k + 1) 0[i := n]} \<inter> {replicate (k + 1) 0[j := n]} = {}"
+ {(replicate (k + 1) 0)[i := n]} \<inter> {(replicate (k + 1) 0)[j := n]} = {}"
proof clarify
fix i j
assume i: "i \<in> ?K" and j: "j \<in> ?K" and ij: "i \<noteq> j"
- have False if eq: "replicate (k+1) 0 [i:=n] = replicate (k+1) 0 [j:= n]"
+ have False if eq: "(replicate (k+1) 0)[i:=n] = (replicate (k+1) 0)[j:= n]"
proof -
- have "(replicate (k+1) 0 [i:=n] ! i) = n"
+ have "(replicate (k+1) 0) [i:=n] ! i = n"
using i by (simp del: replicate.simps)
moreover
- have "(replicate (k+1) 0 [j:=n] ! i) = 0"
+ have "(replicate (k+1) 0) [j:=n] ! i = 0"
using i ij by (simp del: replicate.simps)
ultimately show ?thesis
using eq n0 by (simp del: replicate.simps)
qed
- then show "{replicate (k + 1) 0[i := n]} \<inter> {replicate (k + 1) 0[j := n]} = {}"
+ then show "{(replicate (k + 1) 0)[i := n]} \<inter> {(replicate (k + 1) 0)[j := n]} = {}"
by auto
qed
from card_UN_disjoint[OF fK fAK d]
- show "card (\<Union>i\<in>{0..k}. {replicate (k + 1) 0[i := n]}) = k + 1"
+ show "card (\<Union>i\<in>{0..k}. {(replicate (k + 1) 0)[i := n]}) = k + 1"
by simp
qed
@@ -2712,7 +2712,7 @@
fix v assume v: "v \<in> {xs \<in> natpermute n (k + 1). n \<in> set xs}"
let ?ths = "(\<Prod>j\<in>{0..k}. fps_radical r (Suc k) a $ v ! j) =
fps_radical r (Suc k) a $ n * r (Suc k) (a $ 0) ^ k"
- from v obtain i where i: "i \<in> {0..k}" "v = replicate (k+1) 0 [i:= n]"
+ from v obtain i where i: "i \<in> {0..k}" "v = (replicate (k+1) 0) [i:= n]"
unfolding natpermute_contain_maximal by auto
have "(\<Prod>j\<in>{0..k}. fps_radical r (Suc k) a $ v ! j) =
(\<Prod>j\<in>{0..k}. if j = i then fps_radical r (Suc k) a $ n else r (Suc k) (a$0))"
@@ -2847,7 +2847,7 @@
fix v
assume v: "v \<in> {xs \<in> natpermute n (Suc k). n \<in> set xs}"
let ?ths = "(\<Prod>j\<in>{0..k}. a $ v ! j) = a $ n * (?r$0)^k"
- from v obtain i where i: "i \<in> {0..k}" "v = replicate (k+1) 0 [i:= n]"
+ from v obtain i where i: "i \<in> {0..k}" "v = (replicate (k+1) 0) [i:= n]"
unfolding Suc_eq_plus1 natpermute_contain_maximal
by (auto simp del: replicate.simps)
have "(\<Prod>j\<in>{0..k}. a $ v ! j) = (\<Prod>j\<in>{0..k}. if j = i then a $ n else r (Suc k) (b$0))"
--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy Sat Sep 29 16:30:44 2018 -0400
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy Sun Sep 30 18:19:28 2018 -0400
@@ -130,7 +130,7 @@
assumes "cl \<in> array_ran a (Array.update a i (Some b) h)"
shows "cl \<in> array_ran a h \<or> cl = b"
proof -
- have "set (Array.get h a[i := Some b]) \<subseteq> insert (Some b) (set (Array.get h a))" by (rule set_update_subset_insert)
+ have "set ((Array.get h a)[i := Some b]) \<subseteq> insert (Some b) (set (Array.get h a))" by (rule set_update_subset_insert)
with assms show ?thesis
unfolding array_ran_def Array.update_def by fastforce
qed
@@ -139,7 +139,7 @@
assumes "cl \<in> array_ran a (Array.update a i None h)"
shows "cl \<in> array_ran a h"
proof -
- have "set (Array.get h a[i := None]) \<subseteq> insert None (set (Array.get h a))" by (rule set_update_subset_insert)
+ have "set ((Array.get h a)[i := None]) \<subseteq> insert None (set (Array.get h a))" by (rule set_update_subset_insert)
with assms show ?thesis
unfolding array_ran_def Array.update_def by auto
qed
--- a/src/HOL/Imperative_HOL/ex/Subarray.thy Sat Sep 29 16:30:44 2018 -0400
+++ b/src/HOL/Imperative_HOL/ex/Subarray.thy Sun Sep 30 18:19:28 2018 -0400
@@ -23,7 +23,7 @@
apply simp
done
-lemma subarray_upd3: "\<lbrakk> n \<le> i; i < m\<rbrakk> \<Longrightarrow> subarray n m a (Array.update a i v h) = subarray n m a h[i - n := v]"
+lemma subarray_upd3: "\<lbrakk> n \<le> i; i < m\<rbrakk> \<Longrightarrow> subarray n m a (Array.update a i v h) = (subarray n m a h)[i - n := v]"
unfolding subarray_def Array.update_def
by (simp add: nths'_update3)
--- a/src/HOL/List.thy Sat Sep 29 16:30:44 2018 -0400
+++ b/src/HOL/List.thy Sun Sep 30 18:19:28 2018 -0400
@@ -130,7 +130,7 @@
"_lupdbind":: "['a, 'a] => lupdbind" ("(2_ :=/ _)")
"" :: "lupdbind => lupdbinds" ("_")
"_lupdbinds" :: "[lupdbind, lupdbinds] => lupdbinds" ("_,/ _")
- "_LUpdate" :: "['a, lupdbinds] => 'a" ("_/[(_)]" [900,0] 900)
+ "_LUpdate" :: "['a, lupdbinds] => 'a" ("_/[(_)]" [1000,0] 900)
translations
"_LUpdate xs (_lupdbinds b bs)" == "_LUpdate (_LUpdate xs b) bs"
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Sat Sep 29 16:30:44 2018 -0400
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Sun Sep 30 18:19:28 2018 -0400
@@ -174,7 +174,7 @@
\<lbrakk> G \<turnstile> T \<preceq> T'; is_type G T'; length pns = length pTs; distinct pns; unique lvars;
snd (local_env G C (mn, pTs) pns lvars) vname = Some T' \<rbrakk>
\<Longrightarrow>
- comp G \<turnstile> inited_LT C pTs lvars [index (pns, lvars, blk, res) vname := OK T] <=l
+ comp G \<turnstile> (inited_LT C pTs lvars) [index (pns, lvars, blk, res) vname := OK T] <=l
inited_LT C pTs lvars"
apply (subgoal_tac " index (pns, lvars, blk, res) vname < length (inited_LT C pTs lvars)")
apply (frule_tac blk=blk and res=res in local_env_inited_LT, assumption+)
--- a/src/HOL/MicroJava/Comp/Index.thy Sat Sep 29 16:30:44 2018 -0400
+++ b/src/HOL/MicroJava/Comp/Index.thy Sun Sep 30 18:19:28 2018 -0400
@@ -70,7 +70,7 @@
lemma update_at_index: "
\<lbrakk> distinct (gjmb_plns (gmb G C S));
x \<in> set (gjmb_plns (gmb G C S)); x \<noteq> This \<rbrakk> \<Longrightarrow>
- locvars_xstate G C S (Norm (h, l))[index (gmb G C S) x := val] =
+ (locvars_xstate G C S (Norm (h, l)))[index (gmb G C S) x := val] =
locvars_xstate G C S (Norm (h, l(x\<mapsto>val)))"
apply (simp only: locvars_xstate_def locvars_locals_def index_def)
apply (case_tac "gmb G C S" rule: prod.exhaust, simp)
--- a/src/HOL/ROOT Sat Sep 29 16:30:44 2018 -0400
+++ b/src/HOL/ROOT Sun Sep 30 18:19:28 2018 -0400
@@ -852,7 +852,7 @@
SMT_Word_Examples
SMT_Tests
-session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
+session "HOL-SPARK" in "SPARK" = "HOL-Word" +
theories
SPARK
--- a/src/HOL/Tools/Lifting/lifting_info.ML Sat Sep 29 16:30:44 2018 -0400
+++ b/src/HOL/Tools/Lifting/lifting_info.ML Sun Sep 30 18:19:28 2018 -0400
@@ -9,7 +9,7 @@
type quot_map = {rel_quot_thm: thm}
val lookup_quot_maps: Proof.context -> string -> quot_map option
val print_quot_maps: Proof.context -> unit
-
+
type pcr = {pcrel_def: thm, pcr_cr_eq: thm}
type quotient = {quot_thm: thm, pcr_info: pcr option}
val pcr_eq: pcr * pcr -> bool
@@ -24,14 +24,14 @@
type restore_data = {quotient : quotient, transfer_rules: thm Item_Net.T}
val lookup_restore_data: Proof.context -> string -> restore_data option
val init_restore_data: string -> quotient -> Context.generic -> Context.generic
- val add_transfer_rules_in_restore_data: string -> thm Item_Net.T -> Context.generic -> Context.generic
+ val add_transfer_rules_in_restore_data: string -> thm Item_Net.T -> Context.generic -> Context.generic
val get_relator_eq_onp_rules: Proof.context -> thm list
-
+
val get_reflexivity_rules: Proof.context -> thm list
val add_reflexivity_rule_attribute: attribute
- type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm,
+ type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm,
pos_distr_rules: thm list, neg_distr_rules: thm list}
val lookup_relator_distr_data: Proof.context -> string -> relator_distr_data option
@@ -50,37 +50,33 @@
open Lifting_Util
-(** data container **)
+
+(* context data *)
type quot_map = {rel_quot_thm: thm}
type pcr = {pcrel_def: thm, pcr_cr_eq: thm}
type quotient = {quot_thm: thm, pcr_info: pcr option}
-type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm,
+type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm,
pos_distr_rules: thm list, neg_distr_rules: thm list}
type restore_data = {quotient : quotient, transfer_rules: thm Item_Net.T}
fun pcr_eq ({pcrel_def = pcrel_def1, pcr_cr_eq = pcr_cr_eq1},
- {pcrel_def = pcrel_def2, pcr_cr_eq = pcr_cr_eq2}) =
+ {pcrel_def = pcrel_def2, pcr_cr_eq = pcr_cr_eq2}) =
Thm.eq_thm (pcrel_def1, pcrel_def2) andalso Thm.eq_thm (pcr_cr_eq1, pcr_cr_eq2)
-fun option_eq _ (NONE,NONE) = true
- | option_eq _ (NONE,_) = false
- | option_eq _ (_,NONE) = false
- | option_eq cmp (SOME x, SOME y) = cmp (x,y);
-
fun quotient_eq ({quot_thm = quot_thm1, pcr_info = pcr_info1},
{quot_thm = quot_thm2, pcr_info = pcr_info2}) =
- Thm.eq_thm (quot_thm1, quot_thm2) andalso option_eq pcr_eq (pcr_info1, pcr_info2)
+ Thm.eq_thm (quot_thm1, quot_thm2) andalso eq_option pcr_eq (pcr_info1, pcr_info2)
fun join_restore_data key (rd1:restore_data, rd2) =
if pointer_eq (rd1, rd2) then raise Symtab.SAME else
if not (quotient_eq (#quotient rd1, #quotient rd2)) then raise Symtab.DUP key else
- { quotient = #quotient rd1,
+ { quotient = #quotient rd1,
transfer_rules = Item_Net.merge (#transfer_rules rd1, #transfer_rules rd2)}
structure Data = Generic_Data
(
- type T =
+ type T =
{ quot_maps : quot_map Symtab.table,
quotients : quotient Symtab.table,
reflexivity_rules : thm Item_Net.T,
@@ -98,7 +94,7 @@
}
val extend = I
fun merge
- ( { quot_maps = qm1, quotients = q1, reflexivity_rules = rr1, relator_distr_data = rdd1,
+ ( { quot_maps = qm1, quotients = q1, reflexivity_rules = rr1, relator_distr_data = rdd1,
restore_data = rd1, no_code_types = nct1 },
{ quot_maps = qm2, quotients = q2, reflexivity_rules = rr2, relator_distr_data = rdd2,
restore_data = rd2, no_code_types = nct2 } ) =
@@ -127,7 +123,7 @@
fun map_relator_distr_data f = map_data I I I f I I
fun map_restore_data f = map_data I I I I f I
fun map_no_code_types f = map_data I I I I I f
-
+
val get_quot_maps' = #quot_maps o Data.get
val get_quotients' = #quotients o Data.get
val get_reflexivity_rules' = #reflexivity_rules o Data.get
@@ -141,14 +137,15 @@
fun get_restore_data ctxt = get_restore_data' (Context.Proof ctxt)
fun get_no_code_types ctxt = get_no_code_types' (Context.Proof ctxt)
+
(* info about Quotient map theorems *)
val lookup_quot_maps = Symtab.lookup o get_quot_maps
fun quot_map_thm_sanity_check rel_quot_thm ctxt =
let
- fun quot_term_absT ctxt quot_term =
- let
+ fun quot_term_absT ctxt quot_term =
+ let
val (_, abs, _, _) = (dest_Quotient o HOLogic.dest_Trueprop) quot_term
handle TERM (_, [t]) => error (Pretty.string_of (Pretty.block
[Pretty.str "The Quotient map theorem is not in the right form.",
@@ -166,32 +163,32 @@
val rel_quot_thm_prems = Logic.strip_imp_prems rel_quot_thm_prop;
val concl_absT = quot_term_absT ctxt' rel_quot_thm_concl
val concl_tfrees = Term.add_tfree_namesT (concl_absT) []
- val prems_tfrees = fold (fn typ => fn list => Term.add_tfree_namesT (quot_term_absT ctxt' typ) list)
+ val prems_tfrees = fold (fn typ => fn list => Term.add_tfree_namesT (quot_term_absT ctxt' typ) list)
rel_quot_thm_prems []
val extra_prem_tfrees =
case subtract (op =) concl_tfrees prems_tfrees of
[] => []
| extras => [Pretty.block ([Pretty.str "Extra type variables in the premises:",
- Pretty.brk 1] @
+ Pretty.brk 1] @
((Pretty.commas o map (Pretty.str o quote)) extras) @
[Pretty.str "."])]
- val errs = extra_prem_tfrees
+ val errs = extra_prem_tfrees
in
- if null errs then () else error (cat_lines (["Sanity check of the quotient map theorem failed:",""]
+ if null errs then () else error (cat_lines (["Sanity check of the quotient map theorem failed:",""]
@ (map Pretty.string_of errs)))
end
-fun add_quot_map rel_quot_thm ctxt =
+fun add_quot_map rel_quot_thm context =
let
- val _ = Context.cases (K ()) (quot_map_thm_sanity_check rel_quot_thm) ctxt
+ val _ = Context.cases (K ()) (quot_map_thm_sanity_check rel_quot_thm) context
val rel_quot_thm_concl = (Logic.strip_imp_concl o Thm.prop_of) rel_quot_thm
val (_, abs, _, _) = (dest_Quotient o HOLogic.dest_Trueprop) rel_quot_thm_concl
val relatorT_name = (fst o dest_Type o fst o dest_funT o fastype_of) abs
val minfo = {rel_quot_thm = rel_quot_thm}
in
- Data.map (map_quot_maps (Symtab.update (relatorT_name, minfo))) ctxt
- end
+ Data.map (map_quot_maps (Symtab.update (relatorT_name, minfo))) context
+ end
val _ =
Theory.setup
@@ -202,9 +199,9 @@
let
fun prt_map (ty_name, {rel_quot_thm}) =
Pretty.block (separate (Pretty.brk 2)
- [Pretty.str "type:",
+ [Pretty.str "type:",
Pretty.str ty_name,
- Pretty.str "quot. theorem:",
+ Pretty.str "quot. theorem:",
Syntax.pretty_term ctxt (Thm.prop_of rel_quot_thm)])
in
map prt_map (Symtab.dest (get_quot_maps ctxt))
@@ -212,6 +209,7 @@
|> Pretty.writeln
end
+
(* info about quotient types *)
fun transform_pcr_info phi {pcrel_def, pcr_cr_eq} =
@@ -233,24 +231,24 @@
| NONE => NONE
end
-fun update_quotients type_name qinfo ctxt =
- Data.map (map_quotients (Symtab.update (type_name, qinfo))) ctxt
+fun update_quotients type_name qinfo context =
+ Data.map (map_quotients (Symtab.update (type_name, qinfo))) context
-fun delete_quotients quot_thm ctxt =
+fun delete_quotients quot_thm context =
let
val (_, qtyp) = quot_thm_rty_qty quot_thm
val qty_full_name = (fst o dest_Type) qtyp
in
- if is_some (lookup_quot_thm_quotients (Context.proof_of ctxt) quot_thm)
- then Data.map (map_quotients (Symtab.delete qty_full_name)) ctxt
- else ctxt
+ if is_some (lookup_quot_thm_quotients (Context.proof_of context) quot_thm)
+ then Data.map (map_quotients (Symtab.delete qty_full_name)) context
+ else context
end
fun print_quotients ctxt =
let
fun prt_quot (qty_name, {quot_thm, pcr_info}: quotient) =
Pretty.block (separate (Pretty.brk 2)
- [Pretty.str "type:",
+ [Pretty.str "type:",
Pretty.str qty_name,
Pretty.str "quot. thm:",
Syntax.pretty_term ctxt (Thm.prop_of quot_thm),
@@ -273,23 +271,26 @@
fun lookup_restore_data ctxt bundle_name = Symtab.lookup (get_restore_data ctxt) bundle_name
-fun update_restore_data bundle_name restore_data ctxt =
- Data.map (map_restore_data (Symtab.update (bundle_name, restore_data))) ctxt
+fun update_restore_data bundle_name restore_data context =
+ Data.map (map_restore_data (Symtab.update (bundle_name, restore_data))) context
-fun init_restore_data bundle_name qinfo ctxt =
- update_restore_data bundle_name { quotient = qinfo, transfer_rules = Thm.full_rules } ctxt
+fun init_restore_data bundle_name qinfo context =
+ update_restore_data bundle_name { quotient = qinfo, transfer_rules = Thm.full_rules } context
-fun add_transfer_rules_in_restore_data bundle_name transfer_rules ctxt =
- case Symtab.lookup (get_restore_data' ctxt) bundle_name of
- SOME restore_data => update_restore_data bundle_name { quotient = #quotient restore_data,
- transfer_rules = Item_Net.merge ((#transfer_rules restore_data), transfer_rules) } ctxt
- | NONE => error ("The restore data " ^ quote bundle_name ^ " is not defined.")
+fun add_transfer_rules_in_restore_data bundle_name transfer_rules context =
+ (case Symtab.lookup (get_restore_data' context) bundle_name of
+ SOME restore_data =>
+ update_restore_data bundle_name { quotient = #quotient restore_data,
+ transfer_rules = Item_Net.merge ((#transfer_rules restore_data), transfer_rules) } context
+ | NONE => error ("The restore data " ^ quote bundle_name ^ " is not defined."))
+
(* theorems that a relator of an eq_onp is an eq_onp of the corresponding predicate *)
fun get_relator_eq_onp_rules ctxt =
map safe_mk_meta_eq (rev (Named_Theorems.get ctxt @{named_theorems relator_eq_onp}))
+
(* info about reflexivity rules *)
fun get_reflexivity_rules ctxt = Item_Net.content (get_reflexivity_rules' (Context.Proof ctxt))
@@ -297,18 +298,19 @@
fun add_reflexivity_rule thm = Data.map (map_reflexivity_rules (Item_Net.update thm))
val add_reflexivity_rule_attribute = Thm.declaration_attribute add_reflexivity_rule
+
(* info about relator distributivity theorems *)
fun map_relator_distr_data' f1 f2 f3 f4
{pos_mono_rule, neg_mono_rule, pos_distr_rules, neg_distr_rules} =
- {pos_mono_rule = f1 pos_mono_rule,
+ {pos_mono_rule = f1 pos_mono_rule,
neg_mono_rule = f2 neg_mono_rule,
- pos_distr_rules = f3 pos_distr_rules,
+ pos_distr_rules = f3 pos_distr_rules,
neg_distr_rules = f4 neg_distr_rules}
fun map_pos_mono_rule f = map_relator_distr_data' f I I I
fun map_neg_mono_rule f = map_relator_distr_data' I f I I
-fun map_pos_distr_rules f = map_relator_distr_data' I I f I
+fun map_pos_distr_rules f = map_relator_distr_data' I I f I
fun map_neg_distr_rules f = map_relator_distr_data' I I I f
fun introduce_polarities rule =
@@ -317,132 +319,137 @@
val prems_pairs = map (dest_less_eq o HOLogic.dest_Trueprop) (Thm.prems_of rule)
val equal_prems = filter op= prems_pairs
val _ =
- if null equal_prems then ()
+ if null equal_prems then ()
else error "The rule contains reflexive assumptions."
- val concl_pairs = rule
+ val concl_pairs = rule
|> Thm.concl_of
|> HOLogic.dest_Trueprop
|> dest_less_eq
|> apply2 (snd o strip_comb)
|> op ~~
|> filter_out op =
-
- val _ = if has_duplicates op= concl_pairs
+
+ val _ = if has_duplicates op= concl_pairs
then error "The rule contains duplicated variables in the conlusion." else ()
- fun rewrite_prem prem_pair =
+ fun rewrite_prem prem_pair =
if member op= concl_pairs prem_pair
then HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm POS_def}))
else if member op= concl_pairs (swap prem_pair)
then HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm NEG_def}))
else error "The rule contains a non-relevant assumption."
-
+
fun rewrite_prems [] = Conv.all_conv
| rewrite_prems (x::xs) = Conv.implies_conv (rewrite_prem x) (rewrite_prems xs)
-
+
val rewrite_prems_conv = rewrite_prems prems_pairs
- val rewrite_concl_conv =
+ val rewrite_concl_conv =
Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm POS_def})))
in
(Conv.fconv_rule (rewrite_prems_conv then_conv rewrite_concl_conv)) rule
end
- handle
+ handle
TERM _ => error "The rule has a wrong format."
| CTERM _ => error "The rule has a wrong format."
-fun negate_mono_rule mono_rule =
+fun negate_mono_rule mono_rule =
let
val rewr_conv = HOLogic.Trueprop_conv (Conv.rewrs_conv [@{thm POS_NEG}, @{thm NEG_POS}])
in
Conv.fconv_rule (Conv.prems_conv ~1 rewr_conv then_conv Conv.concl_conv ~1 rewr_conv) mono_rule
end;
-fun add_reflexivity_rules mono_rule ctxt =
+fun add_reflexivity_rules mono_rule context =
let
fun find_eq_rule thm ctxt =
let
val concl_rhs = (hd o get_args 1 o HOLogic.dest_Trueprop o Thm.concl_of) thm;
val rules = Item_Net.retrieve (Transfer.get_relator_eq_item_net ctxt) concl_rhs;
in
- find_first (fn thm => Pattern.matches (Proof_Context.theory_of ctxt) (concl_rhs,
+ find_first (fn thm => Pattern.matches (Proof_Context.theory_of ctxt) (concl_rhs,
(fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.concl_of) thm)) rules
end
- val eq_rule = find_eq_rule mono_rule (Context.proof_of ctxt);
- val eq_rule = if is_some eq_rule then the eq_rule else error
+ val eq_rule = find_eq_rule mono_rule (Context.proof_of context);
+ val eq_rule = if is_some eq_rule then the eq_rule else error
"No corresponding rule that the relator preserves equality was found."
in
- ctxt
+ context
|> add_reflexivity_rule (Drule.zero_var_indexes (@{thm ord_le_eq_trans} OF [mono_rule, eq_rule]))
- |> add_reflexivity_rule
+ |> add_reflexivity_rule
(Drule.zero_var_indexes (@{thm ord_eq_le_trans} OF [sym OF [eq_rule], mono_rule]))
end
-fun add_mono_rule mono_rule ctxt =
+fun add_mono_rule mono_rule context =
let
val pol_mono_rule = introduce_polarities mono_rule
- val mono_ruleT_name = (fst o dest_Type o fst o relation_types o fst o relation_types o snd o
+ val mono_ruleT_name = (fst o dest_Type o fst o relation_types o fst o relation_types o snd o
dest_Const o head_of o HOLogic.dest_Trueprop o Thm.concl_of) pol_mono_rule
- val _ = if Symtab.defined (get_relator_distr_data' ctxt) mono_ruleT_name
- then error ("Monotocity rule for type " ^ quote mono_ruleT_name ^ " is already_defined.")
- else ()
- val neg_mono_rule = negate_mono_rule pol_mono_rule
- val relator_distr_data = {pos_mono_rule = pol_mono_rule, neg_mono_rule = neg_mono_rule,
- pos_distr_rules = [], neg_distr_rules = []}
in
- ctxt
- |> Data.map (map_relator_distr_data (Symtab.update (mono_ruleT_name, relator_distr_data)))
- |> add_reflexivity_rules mono_rule
+ if Symtab.defined (get_relator_distr_data' context) mono_ruleT_name
+ then
+ (if Context_Position.is_visible_generic context then
+ warning ("Monotonicity rule for type " ^ quote mono_ruleT_name ^ " is already_defined.")
+ else (); context)
+ else
+ let
+ val neg_mono_rule = negate_mono_rule pol_mono_rule
+ val relator_distr_data = {pos_mono_rule = pol_mono_rule, neg_mono_rule = neg_mono_rule,
+ pos_distr_rules = [], neg_distr_rules = []}
+ in
+ context
+ |> Data.map (map_relator_distr_data (Symtab.update (mono_ruleT_name, relator_distr_data)))
+ |> add_reflexivity_rules mono_rule
+ end
end;
-local
- fun add_distr_rule update_entry distr_rule ctxt =
+local
+ fun add_distr_rule update_entry distr_rule context =
let
- val distr_ruleT_name = (fst o dest_Type o fst o relation_types o fst o relation_types o snd o
+ val distr_ruleT_name = (fst o dest_Type o fst o relation_types o fst o relation_types o snd o
dest_Const o head_of o HOLogic.dest_Trueprop o Thm.concl_of) distr_rule
in
- if Symtab.defined (get_relator_distr_data' ctxt) distr_ruleT_name then
- Data.map (map_relator_distr_data (Symtab.map_entry distr_ruleT_name (update_entry distr_rule)))
- ctxt
- else error "The monoticity rule is not defined."
+ if Symtab.defined (get_relator_distr_data' context) distr_ruleT_name then
+ Data.map (map_relator_distr_data (Symtab.map_entry distr_ruleT_name (update_entry distr_rule)))
+ context
+ else error "The monotonicity rule is not defined."
end
- fun rewrite_concl_conv thm ctm =
- Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric thm))) ctm
- handle CTERM _ => error "The rule has a wrong format."
+ fun rewrite_concl_conv thm ctm =
+ Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric thm))) ctm
+ handle CTERM _ => error "The rule has a wrong format."
in
- fun add_pos_distr_rule distr_rule ctxt =
+ fun add_pos_distr_rule distr_rule context =
let
val distr_rule = Conv.fconv_rule (rewrite_concl_conv @{thm POS_def}) distr_rule
- fun update_entry distr_rule data =
+ fun update_entry distr_rule data =
map_pos_distr_rules (cons (@{thm POS_trans} OF [distr_rule, #pos_mono_rule data])) data
in
- add_distr_rule update_entry distr_rule ctxt
+ add_distr_rule update_entry distr_rule context
end
handle THM _ => error "Combining of the distr. rule and the monotonicity rule together has failed."
-
- fun add_neg_distr_rule distr_rule ctxt =
+ fun add_neg_distr_rule distr_rule context =
let
val distr_rule = Conv.fconv_rule (rewrite_concl_conv @{thm NEG_def}) distr_rule
- fun update_entry distr_rule data =
+ fun update_entry distr_rule data =
map_neg_distr_rules (cons (@{thm NEG_trans} OF [distr_rule, #neg_mono_rule data])) data
in
- add_distr_rule update_entry distr_rule ctxt
+ add_distr_rule update_entry distr_rule context
end
handle THM _ => error "Combining of the distr. rule and the monotonicity rule together has failed."
end
-local
+local
val eq_refl2 = sym RS @{thm eq_refl}
in
- fun add_eq_distr_rule distr_rule ctxt =
- let
+ fun add_eq_distr_rule distr_rule context =
+ let
val pos_distr_rule = @{thm eq_refl} OF [distr_rule]
val neg_distr_rule = eq_refl2 OF [distr_rule]
in
- ctxt
+ context
|> add_pos_distr_rule pos_distr_rule
|> add_neg_distr_rule neg_distr_rule
end
@@ -462,7 +469,7 @@
| Const (@{const_name HOL.eq}, _) $ (lhs as Const (@{const_name relcompp},_) $ _ $ _) $ rhs =>
(lhs, rhs)
| _ => error "The rule has a wrong format.")
-
+
val lhs_vars = Term.add_vars lhs []
val rhs_vars = Term.add_vars rhs []
val assms_vars = fold Term.add_vars assms [];
@@ -470,10 +477,10 @@
if has_duplicates op= lhs_vars
then error "Left-hand side has variable duplicates" else ()
val _ =
- if subset op= (rhs_vars, lhs_vars) then ()
+ if subset op= (rhs_vars, lhs_vars) then ()
else error "Extra variables in the right-hand side of the rule"
val _ =
- if subset op= (assms_vars, lhs_vars) then ()
+ if subset op= (assms_vars, lhs_vars) then ()
else error "Extra variables in the assumptions of the rule"
val rhs_args = (snd o strip_comb) rhs;
fun check_comp t =
@@ -484,35 +491,35 @@
in () end
in
- fun add_distr_rule distr_rule ctxt =
+ fun add_distr_rule distr_rule context =
let
val _ = sanity_check distr_rule
val concl = (perhaps (try HOLogic.dest_Trueprop)) (Thm.concl_of distr_rule)
in
(case concl of
Const (@{const_name less_eq}, _) $ (Const (@{const_name relcompp},_) $ _ $ _) $ _ =>
- add_pos_distr_rule distr_rule ctxt
+ add_pos_distr_rule distr_rule context
| Const (@{const_name less_eq}, _) $ _ $ (Const (@{const_name relcompp},_) $ _ $ _) =>
- add_neg_distr_rule distr_rule ctxt
+ add_neg_distr_rule distr_rule context
| Const (@{const_name HOL.eq}, _) $ (Const (@{const_name relcompp},_) $ _ $ _) $ _ =>
- add_eq_distr_rule distr_rule ctxt)
+ add_eq_distr_rule distr_rule context)
end
end
-fun get_distr_rules_raw ctxt = Symtab.fold
- (fn (_, {pos_distr_rules, neg_distr_rules, ...}) => fn rules => pos_distr_rules @ neg_distr_rules @ rules)
- (get_relator_distr_data' ctxt) []
+fun get_distr_rules_raw context = Symtab.fold
+ (fn (_, {pos_distr_rules, neg_distr_rules, ...}) => fn rules => pos_distr_rules @ neg_distr_rules @ rules)
+ (get_relator_distr_data' context) []
-fun get_mono_rules_raw ctxt = Symtab.fold
- (fn (_, {pos_mono_rule, neg_mono_rule, ...}) => fn rules => [pos_mono_rule, neg_mono_rule] @ rules)
- (get_relator_distr_data' ctxt) []
+fun get_mono_rules_raw context = Symtab.fold
+ (fn (_, {pos_mono_rule, neg_mono_rule, ...}) => fn rules => [pos_mono_rule, neg_mono_rule] @ rules)
+ (get_relator_distr_data' context) []
val lookup_relator_distr_data = Symtab.lookup o get_relator_distr_data
val _ =
Theory.setup
(Attrib.setup @{binding relator_mono} (Scan.succeed (Thm.declaration_attribute add_mono_rule))
- "declaration of relator's monoticity"
+ "declaration of relator's monotonicity"
#> Attrib.setup @{binding relator_distr} (Scan.succeed (Thm.declaration_attribute add_distr_rule))
"declaration of relator's distributivity over OO"
#> Global_Theory.add_thms_dynamic
@@ -520,12 +527,14 @@
#> Global_Theory.add_thms_dynamic
(@{binding relator_mono_raw}, get_mono_rules_raw))
+
(* no_code types *)
-fun add_no_code_type type_name ctxt =
- Data.map (map_no_code_types (Symtab.update (type_name, ()))) ctxt;
+fun add_no_code_type type_name context =
+ Data.map (map_no_code_types (Symtab.update (type_name, ()))) context;
-fun is_no_code_type ctxt type_name = (Symtab.defined o get_no_code_types) ctxt type_name
+fun is_no_code_type context type_name = (Symtab.defined o get_no_code_types) context type_name
+
(* setup fixed eq_onp rules *)
@@ -534,12 +543,14 @@
Transfer.prep_transfer_domain_thm @{context})
@{thms composed_equiv_rel_eq_onp composed_equiv_rel_eq_eq_onp})
+
(* setup fixed reflexivity rules *)
-val _ = Context.>> (fold add_reflexivity_rule
+val _ = Context.>> (fold add_reflexivity_rule
@{thms order_refl[of "(=)"] eq_onp_le_eq Quotient_composition_le_eq Quotient_composition_ge_eq
bi_unique_OO bi_total_OO right_unique_OO right_total_OO left_unique_OO left_total_OO})
+
(* outer syntax commands *)
val _ =
--- a/src/Pure/Isar/experiment.ML Sat Sep 29 16:30:44 2018 -0400
+++ b/src/Pure/Isar/experiment.ML Sun Sep 30 18:19:28 2018 -0400
@@ -6,6 +6,7 @@
signature EXPERIMENT =
sig
+ val is_experiment: theory -> string -> bool
val experiment: Element.context_i list -> theory -> Binding.scope * local_theory
val experiment_cmd: Element.context list -> theory -> Binding.scope * local_theory
end;
@@ -13,10 +14,23 @@
structure Experiment: EXPERIMENT =
struct
+structure Data = Theory_Data
+(
+ type T = Symtab.set;
+ val empty = Symtab.empty;
+ val extend = I;
+ val merge = Symtab.merge (K true);
+);
+
+fun is_experiment thy name = Symtab.defined (Data.get thy) name;
+
fun gen_experiment add_locale elems thy =
let
val experiment_name = Binding.name ("experiment" ^ serial_string ()) |> Binding.concealed;
- val (_, lthy) = thy |> add_locale experiment_name Binding.empty ([], []) elems;
+ val lthy =
+ thy
+ |> add_locale experiment_name Binding.empty ([], []) elems
+ |-> (Local_Theory.background_theory o Data.map o Symtab.insert_set);
val (scope, naming) =
Name_Space.new_scope (Proof_Context.naming_of (Local_Theory.target_of lthy));
val naming' = naming |> Name_Space.private_scope scope;
--- a/src/Pure/Thy/export_theory.ML Sat Sep 29 16:30:44 2018 -0400
+++ b/src/Pure/Thy/export_theory.ML Sun Sep 30 18:19:28 2018 -0400
@@ -101,7 +101,7 @@
(fold_types o fold_atyps) (fn TFree (a, S) => is_free used a ? insert (op =) (a, S) | _ => I);
-(* locale content *)
+(* locales content *)
fun locale_content thy loc =
let
@@ -127,24 +127,31 @@
val typargs = rev (fold Term.add_tfrees (map (Free o #1) args @ axioms) []);
in {typargs = typargs, args = args, axioms = axioms} end;
-fun locale_dependency_subst thy (dep: Locale.locale_dependency) =
- let
- val (type_params, params) = Locale.parameters_of thy (#source dep);
- (* FIXME proper type_params wrt. locale_content (!?!) *)
- val typargs = fold (Term.add_tfreesT o #2 o #1) params type_params;
- val substT =
- typargs |> map_filter (fn v =>
- let
- val T = TFree v;
- val T' = Morphism.typ (#morphism dep) T;
- in if T = T' then NONE else SOME (v, T') end);
- val subst =
- params |> map_filter (fn (v, _) =>
- let
- val t = Free v;
- val t' = Morphism.term (#morphism dep) t;
- in if t aconv t' then NONE else SOME (v, t') end);
- in (substT, subst) end;
+fun get_locales thy =
+ Locale.get_locales thy |> map_filter (fn loc =>
+ if Experiment.is_experiment thy loc then NONE else SOME (loc, ()));
+
+fun get_dependencies prev_thys thy =
+ Locale.dest_dependencies prev_thys thy |> map_filter (fn dep =>
+ if Experiment.is_experiment thy (#source dep) orelse
+ Experiment.is_experiment thy (#target dep) then NONE
+ else
+ let
+ val (type_params, params) = Locale.parameters_of thy (#source dep);
+ val typargs = fold (Term.add_tfreesT o #2 o #1) params type_params;
+ val substT =
+ typargs |> map_filter (fn v =>
+ let
+ val T = TFree v;
+ val T' = Morphism.typ (#morphism dep) T;
+ in if T = T' then NONE else SOME (v, T') end);
+ val subst =
+ params |> map_filter (fn (v, _) =>
+ let
+ val t = Free v;
+ val t' = Morphism.term (#morphism dep) t;
+ in if t aconv t' then NONE else SOME (v, t') end);
+ in SOME (dep, (substT, subst)) end);
(* general setup *)
@@ -331,14 +338,13 @@
val _ =
export_entities "locales" (fn loc => fn () => SOME (export_locale loc))
- Locale.locale_space
- (map (rpair ()) (Locale.get_locales thy));
+ Locale.locale_space (get_locales thy);
(* locale dependencies *)
- fun encode_locale_dependency (dep: Locale.locale_dependency) =
- (#source dep, (#target dep, (#prefix dep, locale_dependency_subst thy dep))) |>
+ fun encode_locale_dependency (dep: Locale.locale_dependency, subst) =
+ (#source dep, (#target dep, (#prefix dep, subst))) |>
let
open XML.Encode Term_XML.Encode;
val encode_subst =
@@ -346,15 +352,16 @@
in pair string (pair string (pair (list (pair string bool)) encode_subst)) end;
val _ =
- (case Locale.dest_dependencies parents thy of
+ (case get_dependencies parents thy of
[] => ()
| deps =>
deps |> map_index (fn (i, dep) =>
let
val xname = string_of_int (i + 1);
val name = Long_Name.implode [Context.theory_name thy, xname];
+ val markup = make_entity_markup name xname (#pos (#1 dep)) (#serial (#1 dep));
val body = encode_locale_dependency dep;
- in XML.Elem (make_entity_markup name xname (#pos dep) (#serial dep), body) end)
+ in XML.Elem (markup, body) end)
|> export_body thy "locale_dependencies");