--- a/NEWS Wed Jun 08 16:46:48 2016 +0200
+++ b/NEWS Wed Jun 08 18:46:09 2016 +0200
@@ -98,6 +98,16 @@
* The old proof method "default" has been removed (legacy since
Isabelle2016). INCOMPATIBILITY, use "standard" instead.
+* Proof methods may refer to the main facts via the dynamic fact
+"method_facts". This is particularly useful for Eisbach method
+definitions.
+
+* Eisbach provides method "use" to modify the main facts of a given
+method expression, e.g.
+
+ (use facts in simp)
+ (use facts in \<open>simp add: ...\<close>)
+
*** Pure ***
--- a/src/HOL/Eisbach/Eisbach.thy Wed Jun 08 16:46:48 2016 +0200
+++ b/src/HOL/Eisbach/Eisbach.thy Wed Jun 08 18:46:09 2016 +0200
@@ -22,4 +22,9 @@
method solves methods m = (m; fail)
+method_setup use = \<open>
+ Attrib.thms -- (Scan.lift @{keyword "in"} |-- Method_Closure.method_text) >>
+ (fn (thms, text) => fn ctxt => fn _ => Method_Closure.method_evaluate text ctxt thms)
+\<close> \<open>indicate method facts and context for method expression\<close>
+
end
--- a/src/HOL/Eisbach/method_closure.ML Wed Jun 08 16:46:48 2016 +0200
+++ b/src/HOL/Eisbach/method_closure.ML Wed Jun 08 18:46:09 2016 +0200
@@ -122,7 +122,7 @@
text |> (Method.map_source o map o Token.map_facts)
(fn SOME name =>
(case Proof_Context.lookup_fact ctxt name of
- SOME (false, ths) => K ths
+ SOME {dynamic = true, thms} => K thms
| _ => I)
| NONE => I);
val ctxt' = Config.put Method.closure false ctxt;
--- a/src/HOL/MicroJava/BV/BVNoTypeError.thy Wed Jun 08 16:46:48 2016 +0200
+++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy Wed Jun 08 18:46:09 2016 +0200
@@ -354,7 +354,7 @@
obtain D fs where
hp: "hp (the_Addr x) = Some (D,fs)" and
D: "G \<turnstile> D \<preceq>C C"
- by - (drule non_npD, assumption, clarsimp)
+ by (auto dest: non_npD)
hence "hp (the_Addr x) \<noteq> None" (is ?P1) by simp
moreover
from wf mth hp D
@@ -366,9 +366,9 @@
hence "list_all2 (conf G hp) (rev aps) (rev (rev apTs))"
by (simp only: list_all2_rev)
hence "list_all2 (conf G hp) (rev aps) apTs" by simp
- with wf widen
+ from wf this widen
have "list_all2 (conf G hp) (rev aps) ps" (is ?P3)
- by - (rule list_all2_conf_widen)
+ by (rule list_all2_conf_widen)
ultimately
have "?P1 \<and> ?P2 \<and> ?P3" by blast
}
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Wed Jun 08 16:46:48 2016 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Wed Jun 08 18:46:09 2016 +0200
@@ -89,10 +89,9 @@
from set
have "C \<in> set (match_any G pc (e#es))" by simp
moreover
- from False C
+ from False
have "\<not> match_exception_entry G C pc e"
- by - (erule contrapos_nn,
- auto simp add: match_exception_entry_def)
+ by (rule contrapos_nn) (use C in \<open>auto simp add: match_exception_entry_def\<close>)
with m
have "match_exception_table G C pc (e#es) = Some pc'" by simp
moreover note C
@@ -571,7 +570,7 @@
}
ultimately
show ?thesis by (rule that)
- qed (insert xp', auto) \<comment> "the other instructions don't generate exceptions"
+ qed (use xp' in auto) \<comment> "the other instructions don't generate exceptions"
from state' meth hp_ok "class" frames phi_pc' frame' prehp
have ?thesis by (unfold correct_state_def) simp
@@ -772,10 +771,9 @@
(is "state' = Norm (?hp', ?f # frs)")
by simp
moreover
- from wf hp heap_ok is_class_X
+ from hp heap_ok
have hp': "G \<turnstile>h ?hp' \<surd>"
- by - (rule hconf_newref,
- auto simp add: oconf_def dest: fields_is_type)
+ by (rule hconf_newref) (use wf is_class_X in \<open>auto simp add: oconf_def dest: fields_is_type\<close>)
moreover
from hp
have sup: "hp \<le>| ?hp'" by (rule hext_new)
@@ -786,10 +784,9 @@
apply (blast intro: approx_stk_sup_heap approx_loc_sup_heap sup)
done
moreover
- from hp frames wf heap_ok is_class_X
+ from hp frames
have "correct_frames G ?hp' phi rT sig frs"
- by - (rule correct_frames_newref,
- auto simp add: oconf_def dest: fields_is_type)
+ by (rule correct_frames_newref)
moreover
from hp prealloc have "preallocated ?hp'" by (rule preallocated_newref)
ultimately
@@ -851,10 +848,8 @@
s': "phi C sig ! Suc pc = Some (ST', LT')"
by (simp add: norm_eff_def split_paired_Ex) blast
- from X
- obtain T where
- X_Ref: "X = RefT T"
- by - (drule widen_RefT2, erule exE, rule that)
+ from X obtain T where X_Ref: "X = RefT T"
+ by (blast dest: widen_RefT2)
from s ins frame
obtain
@@ -871,7 +866,7 @@
stk': "stk = opTs @ oX # stk'" and
l_o: "length opTs = length apTs"
"length stk' = length ST"
- by - (drule approx_stk_append, auto)
+ by (auto dest: approx_stk_append)
from oX X_Ref
have oX_conf: "G,hp \<turnstile> oX ::\<preceq> RefT T"
@@ -909,7 +904,7 @@
"G \<turnstile> rT' \<preceq> rT0"
by (auto dest: subtype_widen_methd intro: that)
- from mX mD have rT': "G \<turnstile> rT' \<preceq> rT" by - (rule widen_trans)
+ from mD(2) mX(2) have rT': "G \<turnstile> rT' \<preceq> rT" by (rule widen_trans)
from is_class X'_subcls D_subcls
have is_class_D: "is_class G D" by (auto dest: subcls_is_class2)
@@ -1351,19 +1346,18 @@
apply (auto simp add: sup_state_conv approx_val_def dest!: widen_RefT split: err.splits)
done
-theorem
- fixes G :: jvm_prog ("\<Gamma>") and Phi :: prog_type ("\<Phi>")
- assumes welltyped: "wt_jvm_prog \<Gamma> \<Phi>" and
- main_method: "is_class \<Gamma> C" "method (\<Gamma>,C) (m,[]) = Some (C, b)"
- shows typesafe:
- "G \<turnstile> start_state \<Gamma> C m \<midarrow>jvm\<rightarrow> s \<Longrightarrow> \<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
+theorem typesafe:
+ fixes G :: jvm_prog ("\<Gamma>")
+ and Phi :: prog_type ("\<Phi>")
+ assumes welltyped: "wt_jvm_prog \<Gamma> \<Phi>"
+ and main_method: "is_class \<Gamma> C" "method (\<Gamma>,C) (m,[]) = Some (C, b)"
+ and exec_all: "G \<turnstile> start_state \<Gamma> C m \<midarrow>jvm\<rightarrow> s"
+ shows "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
proof -
- from welltyped main_method
- have "\<Gamma>,\<Phi> \<turnstile>JVM start_state \<Gamma> C m \<surd>" by (rule BV_correct_initial)
- moreover
- assume "G \<turnstile> start_state \<Gamma> C m \<midarrow>jvm\<rightarrow> s"
- ultimately
- show "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>" using welltyped by - (rule BV_correct)
+ from welltyped main_method have "\<Gamma>,\<Phi> \<turnstile>JVM start_state \<Gamma> C m \<surd>"
+ by (rule BV_correct_initial)
+ with welltyped exec_all show "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
+ by (rule BV_correct)
qed
end
--- a/src/HOL/MicroJava/BV/EffectMono.thy Wed Jun 08 16:46:48 2016 +0200
+++ b/src/HOL/MicroJava/BV/EffectMono.thy Wed Jun 08 18:46:09 2016 +0200
@@ -55,7 +55,7 @@
fix b
assume "length (l # ls) = length (b::ty list)"
with Cons
- show "?Q (l # ls) b" by - (cases b, auto)
+ show "?Q (l # ls) b" by (cases b) auto
qed
qed
--- a/src/HOL/MicroJava/Comp/TypeInf.thy Wed Jun 08 16:46:48 2016 +0200
+++ b/src/HOL/MicroJava/Comp/TypeInf.thy Wed Jun 08 18:46:09 2016 +0200
@@ -4,7 +4,7 @@
(* Exact position in theory hierarchy still to be determined *)
theory TypeInf
-imports "../J/WellType" "~~/src/HOL/Eisbach/Eisbach"
+imports "../J/WellType"
begin
--- a/src/HOL/MicroJava/DFA/Err.thy Wed Jun 08 16:46:48 2016 +0200
+++ b/src/HOL/MicroJava/DFA/Err.thy Wed Jun 08 18:46:09 2016 +0200
@@ -131,7 +131,7 @@
lemma semilat_errI [intro]:
assumes semilat: "semilat (A, r, f)"
shows "semilat(err A, Err.le r, lift2(%x y. OK(f x y)))"
- apply(insert semilat)
+ using semilat
apply (simp only: semilat_Def closed_def plussub_def lesub_def
lift2_def Err.le_def err_def)
apply (simp split: err.split)
--- a/src/HOL/MicroJava/DFA/LBVComplete.thy Wed Jun 08 16:46:48 2016 +0200
+++ b/src/HOL/MicroJava/DFA/LBVComplete.thy Wed Jun 08 18:46:09 2016 +0200
@@ -65,7 +65,7 @@
lemma (in lbv) le_top [simp, intro]:
"x <=_r \<top>"
- by (insert top) simp
+ using top by simp
lemma (in lbv) merge_mono:
--- a/src/HOL/MicroJava/DFA/LBVSpec.thy Wed Jun 08 16:46:48 2016 +0200
+++ b/src/HOL/MicroJava/DFA/LBVSpec.thy Wed Jun 08 18:46:09 2016 +0200
@@ -121,7 +121,7 @@
lemma (in lbv) bottom_le [simp, intro]:
"\<bottom> <=_r x"
- by (insert bot) (simp add: bottom_def)
+ using bot by (simp add: bottom_def)
lemma (in lbv) le_bottom [simp]:
"x <=_r \<bottom> = (x = \<bottom>)"
--- a/src/HOL/MicroJava/DFA/Semilat.thy Wed Jun 08 16:46:48 2016 +0200
+++ b/src/HOL/MicroJava/DFA/Semilat.thy Wed Jun 08 18:46:09 2016 +0200
@@ -135,14 +135,14 @@
(*<*) by (auto intro: order_trans) (*>*)
lemma (in Semilat) ub1 [simp, intro?]: "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^sub>r x \<squnion>\<^sub>f y"
- (*<*) by (insert semilat) (unfold semilat_Def, simp) (*>*)
+ (*<*) using semilat by (simp add: semilat_Def) (*>*)
lemma (in Semilat) ub2 [simp, intro?]: "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> y \<sqsubseteq>\<^sub>r x \<squnion>\<^sub>f y"
- (*<*) by (insert semilat) (unfold semilat_Def, simp) (*>*)
+ (*<*) using semilat by (simp add: semilat_Def) (*>*)
lemma (in Semilat) lub [simp, intro?]:
"\<lbrakk> x \<sqsubseteq>\<^sub>r z; y \<sqsubseteq>\<^sub>r z; x \<in> A; y \<in> A; z \<in> A \<rbrakk> \<Longrightarrow> x \<squnion>\<^sub>f y \<sqsubseteq>\<^sub>r z"
- (*<*) by (insert semilat) (unfold semilat_Def, simp) (*>*)
+ (*<*) using semilat by (simp add: semilat_Def) (*>*)
lemma (in Semilat) plus_le_conv [simp]:
"\<lbrakk> x \<in> A; y \<in> A; z \<in> A \<rbrakk> \<Longrightarrow> (x \<squnion>\<^sub>f y \<sqsubseteq>\<^sub>r z) = (x \<sqsubseteq>\<^sub>r z \<and> y \<sqsubseteq>\<^sub>r z)"
--- a/src/HOL/MicroJava/J/JBasis.thy Wed Jun 08 16:46:48 2016 +0200
+++ b/src/HOL/MicroJava/J/JBasis.thy Wed Jun 08 18:46:09 2016 +0200
@@ -6,7 +6,12 @@
section \<open>Some Auxiliary Definitions\<close>
-theory JBasis imports Main "~~/src/HOL/Library/Transitive_Closure_Table" begin
+theory JBasis
+imports
+ Main
+ "~~/src/HOL/Library/Transitive_Closure_Table"
+ "~~/src/HOL/Eisbach/Eisbach"
+begin
lemmas [simp] = Let_def
--- a/src/Pure/Isar/method.ML Wed Jun 08 16:46:48 2016 +0200
+++ b/src/Pure/Isar/method.ML Wed Jun 08 18:46:09 2016 +0200
@@ -54,6 +54,9 @@
val drule: Proof.context -> int -> thm list -> method
val frule: Proof.context -> int -> thm list -> method
val set_tactic: (morphism -> thm list -> tactic) -> Context.generic -> Context.generic
+ val clean_facts: thm list -> thm list
+ val set_facts: thm list -> Proof.context -> Proof.context
+ val get_facts: Proof.context -> thm list
type combinator_info
val no_combinator_info: combinator_info
datatype combinator = Then | Then_All_New | Orelse | Try | Repeat1 | Select_Goals of int
@@ -322,26 +325,37 @@
structure Data = Generic_Data
(
type T =
- ((Token.src -> Proof.context -> method) * string) Name_Space.table * (*methods*)
- (morphism -> thm list -> tactic) option; (*ML tactic*)
- val empty : T = (Name_Space.empty_table "method", NONE);
+ {methods: ((Token.src -> Proof.context -> method) * string) Name_Space.table,
+ ml_tactic: (morphism -> thm list -> tactic) option,
+ facts: thm list option};
+ val empty : T =
+ {methods = Name_Space.empty_table "method", ml_tactic = NONE, facts = NONE};
val extend = I;
- fun merge ((tab, tac), (tab', tac')) : T =
- (Name_Space.merge_tables (tab, tab'), merge_options (tac, tac'));
+ fun merge
+ ({methods = methods1, ml_tactic = ml_tactic1, facts = facts1},
+ {methods = methods2, ml_tactic = ml_tactic2, facts = facts2}) : T =
+ {methods = Name_Space.merge_tables (methods1, methods2),
+ ml_tactic = merge_options (ml_tactic1, ml_tactic2),
+ facts = merge_options (facts1, facts2)};
);
-val get_methods = fst o Data.get;
-val map_methods = Data.map o apfst;
+fun map_data f = Data.map (fn {methods, ml_tactic, facts} =>
+ let val (methods', ml_tactic', facts') = f (methods, ml_tactic, facts)
+ in {methods = methods', ml_tactic = ml_tactic', facts = facts'} end);
-val ops_methods = {get_data = get_methods, put_data = map_methods o K};
+val get_methods = #methods o Data.get;
+
+val ops_methods =
+ {get_data = get_methods,
+ put_data = fn methods => map_data (fn (_, ml_tactic, facts) => (methods, ml_tactic, facts))};
(* ML tactic *)
-val set_tactic = Data.map o apsnd o K o SOME;
+fun set_tactic ml_tactic = map_data (fn (methods, _, facts) => (methods, SOME ml_tactic, facts));
fun the_tactic context =
- (case snd (Data.get context) of
+ (case #ml_tactic (Data.get context) of
SOME tac => tac
| NONE => raise Fail "Undefined ML tactic");
@@ -361,6 +375,22 @@
end)) >> (fn decl => Morphism.form (the_tactic (Morphism.form decl context))));
+(* method facts *)
+
+val clean_facts = filter_out Thm.is_dummy;
+
+fun set_facts facts =
+ (Context.proof_map o map_data)
+ (fn (methods, ml_tactic, _) => (methods, ml_tactic, SOME (clean_facts facts)));
+
+val get_facts_generic = these o #facts o Data.get;
+val get_facts = get_facts_generic o Context.Proof;
+
+val _ =
+ Theory.setup
+ (Global_Theory.add_thms_dynamic (Binding.make ("method_facts", @{here}), get_facts_generic));
+
+
(* method text *)
datatype combinator_info = Combinator_Info of {keywords: Position.T list};
@@ -535,18 +565,14 @@
in
-fun evaluate text ctxt =
+fun evaluate text ctxt0 facts =
let
- fun eval0 m facts = Seq.single #> Seq.maps_results (m facts);
+ val ctxt = set_facts facts ctxt0;
+ fun eval0 m = Seq.single #> Seq.maps_results (m facts);
fun eval (Basic m) = eval0 (m ctxt)
| eval (Source src) = eval0 (method_cmd ctxt src ctxt)
- | eval (Combinator (_, c, txts)) =
- let
- val comb = combinator c;
- val meths = map eval txts;
- in fn facts => comb (map (fn meth => meth facts) meths) end;
- val meth = eval text;
- in fn facts => fn ctxt_st => meth facts (Seq.Result ctxt_st) end;
+ | eval (Combinator (_, c, txts)) = combinator c (map eval txts);
+ in eval text o Seq.Result end;
end;
--- a/src/Pure/Isar/proof.ML Wed Jun 08 16:46:48 2016 +0200
+++ b/src/Pure/Isar/proof.ML Wed Jun 08 18:46:09 2016 +0200
@@ -315,7 +315,7 @@
else state
end;
-fun put_goal goal = map_top (fn (ctxt, using, mode, _) => (ctxt, using, mode, goal));
+fun put_goal goal = map_top (fn (ctxt, facts, mode, _) => (ctxt, facts, mode, goal));
val set_goal = put_goal o SOME;
val reset_goal = put_goal NONE;
@@ -553,15 +553,15 @@
(* goal views -- corresponding to methods *)
fun raw_goal state =
- let val (ctxt, (facts, goal)) = get_goal state
- in {context = ctxt, facts = facts, goal = goal} end;
+ let val (ctxt, (using, goal)) = get_goal state
+ in {context = ctxt, facts = using, goal = goal} end;
val goal = raw_goal o refine_insert [];
fun simple_goal state =
let
- val (_, (facts, _)) = get_goal state;
- val (ctxt, (_, goal)) = get_goal (refine_insert facts state);
+ val (_, (using, _)) = get_goal state;
+ val (ctxt, (_, goal)) = get_goal (refine_insert using state);
in {context = ctxt, goal = goal} end;
fun status_markup state =
@@ -716,12 +716,9 @@
(* chain *)
-fun clean_facts ctxt =
- set_facts (filter_out Thm.is_dummy (the_facts ctxt)) ctxt;
-
val chain =
assert_forward
- #> clean_facts
+ #> (fn state => set_facts (Method.clean_facts (the_facts state)) state)
#> enter_chain;
fun chain_facts facts =
--- a/src/Pure/Isar/proof_context.ML Wed Jun 08 16:46:48 2016 +0200
+++ b/src/Pure/Isar/proof_context.ML Wed Jun 08 18:46:09 2016 +0200
@@ -116,7 +116,7 @@
(term list list * (indexname * term) list)
val fact_tac: Proof.context -> thm list -> int -> tactic
val some_fact_tac: Proof.context -> int -> tactic
- val lookup_fact: Proof.context -> string -> (bool * thm list) option
+ val lookup_fact: Proof.context -> string -> {dynamic: bool, thms: thm list} option
val dynamic_facts_dummy: bool Config.T
val get_fact_generic: Context.generic -> Facts.ref -> string option * thm list
val get_fact: Proof.context -> Facts.ref -> thm list
@@ -1008,23 +1008,23 @@
| retrieve pick context (Facts.Named ((xname, pos), sel)) =
let
val thy = Context.theory_of context;
- fun immediate thm = {name = xname, static = true, thms = [Thm.transfer thy thm]};
- val {name, static, thms} =
+ fun immediate thm = {name = xname, dynamic = false, thms = [Thm.transfer thy thm]};
+ val {name, dynamic, thms} =
(case xname of
"" => immediate Drule.dummy_thm
| "_" => immediate Drule.asm_rl
| _ => retrieve_generic context (xname, pos));
val thms' =
- if not static andalso Config.get_generic context dynamic_facts_dummy
+ if dynamic andalso Config.get_generic context dynamic_facts_dummy
then [Drule.free_dummy_thm]
else Facts.select (Facts.Named ((name, pos), sel)) thms;
- in pick (static orelse is_some sel) (name, pos) thms' end;
+ in pick (dynamic andalso is_none sel) (name, pos) thms' end;
in
val get_fact_generic =
- retrieve (fn static => fn (name, _) => fn thms =>
- (if static then NONE else SOME name, thms));
+ retrieve (fn dynamic => fn (name, _) => fn thms =>
+ (if dynamic then SOME name else NONE, thms));
val get_fact = retrieve (K (K I)) o Context.Proof;
val get_fact_single = retrieve (K Facts.the_single) o Context.Proof;
--- a/src/Pure/facts.ML Wed Jun 08 16:46:48 2016 +0200
+++ b/src/Pure/facts.ML Wed Jun 08 18:46:09 2016 +0200
@@ -30,9 +30,9 @@
val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
val defined: T -> string -> bool
val is_dynamic: T -> string -> bool
- val lookup: Context.generic -> T -> string -> (bool * thm list) option
+ val lookup: Context.generic -> T -> string -> {dynamic: bool, thms: thm list} option
val retrieve: Context.generic -> T -> xstring * Position.T ->
- {name: string, static: bool, thms: thm list}
+ {name: string, dynamic: bool, thms: thm list}
val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
val dest_static: bool -> T list -> T -> (string * thm list) list
val dest_all: Context.generic -> bool -> T list -> T -> (string * thm list) list
@@ -178,22 +178,23 @@
fun lookup context facts name =
(case Name_Space.lookup (facts_of facts) name of
NONE => NONE
- | SOME (Static ths) => SOME (true, ths)
- | SOME (Dynamic f) => SOME (false, f context));
+ | SOME (Static ths) => SOME {dynamic = false, thms = ths}
+ | SOME (Dynamic f) => SOME {dynamic = true, thms = f context});
fun retrieve context facts (xname, pos) =
let
val name = check context facts (xname, pos);
- val (static, thms) =
+ val {dynamic, thms} =
(case lookup context facts name of
- SOME (static, thms) =>
- (if static then ()
- else Context_Position.report_generic context pos (Markup.dynamic_fact name);
- (static, thms))
+ SOME res =>
+ (if #dynamic res
+ then Context_Position.report_generic context pos (Markup.dynamic_fact name)
+ else ();
+ res)
| NONE => error ("Unknown fact " ^ quote name ^ Position.here pos));
in
{name = name,
- static = static,
+ dynamic = dynamic,
thms = map (Thm.transfer (Context.theory_of context)) thms}
end;