# HG changeset patch # User wenzelm # Date 1465404369 -7200 # Node ID 0edec65d0633a44dad56d1a5f8614ebd549b612e # Parent 414e3550e9c0976110cc3a777298da76175141df# Parent 29fe61d5f748e8d603fcd657a8de940c803fe02f merged diff -r 414e3550e9c0 -r 0edec65d0633 NEWS --- 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 \simp add: ...\) + *** Pure *** diff -r 414e3550e9c0 -r 0edec65d0633 src/HOL/Eisbach/Eisbach.thy --- 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 = \ + Attrib.thms -- (Scan.lift @{keyword "in"} |-- Method_Closure.method_text) >> + (fn (thms, text) => fn ctxt => fn _ => Method_Closure.method_evaluate text ctxt thms) +\ \indicate method facts and context for method expression\ + end diff -r 414e3550e9c0 -r 0edec65d0633 src/HOL/Eisbach/method_closure.ML --- 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; diff -r 414e3550e9c0 -r 0edec65d0633 src/HOL/MicroJava/BV/BVNoTypeError.thy --- 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 \ D \C C" - by - (drule non_npD, assumption, clarsimp) + by (auto dest: non_npD) hence "hp (the_Addr x) \ 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 \ ?P2 \ ?P3" by blast } diff -r 414e3550e9c0 -r 0edec65d0633 src/HOL/MicroJava/BV/BVSpecTypeSafe.thy --- 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 \ set (match_any G pc (e#es))" by simp moreover - from False C + from False have "\ 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 \auto simp add: match_exception_entry_def\) 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) \ "the other instructions don't generate exceptions" + qed (use xp' in auto) \ "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 \h ?hp' \" - by - (rule hconf_newref, - auto simp add: oconf_def dest: fields_is_type) + by (rule hconf_newref) (use wf is_class_X in \auto simp add: oconf_def dest: fields_is_type\) moreover from hp have sup: "hp \| ?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 \ oX ::\ RefT T" @@ -909,7 +904,7 @@ "G \ rT' \ rT0" by (auto dest: subtype_widen_methd intro: that) - from mX mD have rT': "G \ rT' \ rT" by - (rule widen_trans) + from mD(2) mX(2) have rT': "G \ rT' \ 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 ("\") and Phi :: prog_type ("\") - assumes welltyped: "wt_jvm_prog \ \" and - main_method: "is_class \ C" "method (\,C) (m,[]) = Some (C, b)" - shows typesafe: - "G \ start_state \ C m \jvm\ s \ \,\ \JVM s \" +theorem typesafe: + fixes G :: jvm_prog ("\") + and Phi :: prog_type ("\") + assumes welltyped: "wt_jvm_prog \ \" + and main_method: "is_class \ C" "method (\,C) (m,[]) = Some (C, b)" + and exec_all: "G \ start_state \ C m \jvm\ s" + shows "\,\ \JVM s \" proof - - from welltyped main_method - have "\,\ \JVM start_state \ C m \" by (rule BV_correct_initial) - moreover - assume "G \ start_state \ C m \jvm\ s" - ultimately - show "\,\ \JVM s \" using welltyped by - (rule BV_correct) + from welltyped main_method have "\,\ \JVM start_state \ C m \" + by (rule BV_correct_initial) + with welltyped exec_all show "\,\ \JVM s \" + by (rule BV_correct) qed end diff -r 414e3550e9c0 -r 0edec65d0633 src/HOL/MicroJava/BV/EffectMono.thy --- 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 diff -r 414e3550e9c0 -r 0edec65d0633 src/HOL/MicroJava/Comp/TypeInf.thy --- 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 diff -r 414e3550e9c0 -r 0edec65d0633 src/HOL/MicroJava/DFA/Err.thy --- 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) diff -r 414e3550e9c0 -r 0edec65d0633 src/HOL/MicroJava/DFA/LBVComplete.thy --- 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 \" - by (insert top) simp + using top by simp lemma (in lbv) merge_mono: diff -r 414e3550e9c0 -r 0edec65d0633 src/HOL/MicroJava/DFA/LBVSpec.thy --- 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]: "\ <=_r x" - by (insert bot) (simp add: bottom_def) + using bot by (simp add: bottom_def) lemma (in lbv) le_bottom [simp]: "x <=_r \ = (x = \)" diff -r 414e3550e9c0 -r 0edec65d0633 src/HOL/MicroJava/DFA/Semilat.thy --- 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?]: "\ x \ A; y \ A \ \ x \\<^sub>r x \\<^sub>f y" - (*<*) by (insert semilat) (unfold semilat_Def, simp) (*>*) + (*<*) using semilat by (simp add: semilat_Def) (*>*) lemma (in Semilat) ub2 [simp, intro?]: "\ x \ A; y \ A \ \ y \\<^sub>r x \\<^sub>f y" - (*<*) by (insert semilat) (unfold semilat_Def, simp) (*>*) + (*<*) using semilat by (simp add: semilat_Def) (*>*) lemma (in Semilat) lub [simp, intro?]: "\ x \\<^sub>r z; y \\<^sub>r z; x \ A; y \ A; z \ A \ \ x \\<^sub>f y \\<^sub>r z" - (*<*) by (insert semilat) (unfold semilat_Def, simp) (*>*) + (*<*) using semilat by (simp add: semilat_Def) (*>*) lemma (in Semilat) plus_le_conv [simp]: "\ x \ A; y \ A; z \ A \ \ (x \\<^sub>f y \\<^sub>r z) = (x \\<^sub>r z \ y \\<^sub>r z)" diff -r 414e3550e9c0 -r 0edec65d0633 src/HOL/MicroJava/J/JBasis.thy --- 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 \Some Auxiliary Definitions\ -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 diff -r 414e3550e9c0 -r 0edec65d0633 src/Pure/Isar/method.ML --- 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; diff -r 414e3550e9c0 -r 0edec65d0633 src/Pure/Isar/proof.ML --- 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 = diff -r 414e3550e9c0 -r 0edec65d0633 src/Pure/Isar/proof_context.ML --- 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; diff -r 414e3550e9c0 -r 0edec65d0633 src/Pure/facts.ML --- 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;