# HG changeset patch # User matichuk # Date 1464588713 -36000 # Node ID 08369e33c1851c804c66c21bcea991acbc5e0961 # Parent dd6cd88cebd97776a17f237b9446e215340be324 apply current morphism to method text before evaluating; diff -r dd6cd88cebd9 -r 08369e33c185 src/HOL/Eisbach/Tests.thy --- a/src/HOL/Eisbach/Tests.thy Mon May 30 20:58:54 2016 +0200 +++ b/src/HOL/Eisbach/Tests.thy Mon May 30 16:11:53 2016 +1000 @@ -262,9 +262,21 @@ ML \test_internal_fact @{context} "Tests.uses_test\<^sub>1_uses"\ ML \test_internal_fact @{context} "Tests.uses_test\<^sub>1.uses_test\<^sub>1_uses"\ +subsection \Basic fact passing\ + +method find_fact for x y :: bool uses facts1 facts2 = + (match facts1 in U: "x" \ \insert U, + match facts2 in U: "y" \ \insert U\\) + +lemma assumes A: A and B: B shows "A \ B" + apply (find_fact "A" "B" facts1: A facts2: B) + apply (rule conjI; assumption) + done + subsection \Testing term and fact passing in recursion\ + method recursion_example for x :: bool uses facts = (match (x) in "A \ B" for A B \ \(recursion_example A facts: facts, recursion_example B facts: facts)\ @@ -530,4 +542,53 @@ apply (test_method' a b rule: assms [symmetric])? done +subsection \Eisbach methods in locales\ + +locale my_locale1 = fixes A assumes A: A begin + +method apply_A = + (match conclusion in "A" \ + \match A in U:"A" \ + \print_term A, print_fact A, rule U\\) + end + +locale my_locale2 = fixes B assumes B: B begin + +interpretation my_locale1 B by (unfold_locales; rule B) + +lemma B by apply_A + +end + +context fixes C assumes C: C begin + +interpretation my_locale1 C by (unfold_locales; rule C) + +lemma C by apply_A + +end + +context begin + +interpretation my_locale1 "True \ True" by (unfold_locales; blast) + +lemma "True \ True" by apply_A + +end + +locale locale_poly = fixes P assumes P: "\x :: 'a. P x" begin + +method solve_P for z :: 'a = (rule P[where x = z]) + +end + +context begin + +interpretation locale_poly "\x:: nat. 0 \ x" by (unfold_locales; blast) + +lemma "0 \ (n :: nat)" by (solve_P n) + +end + +end diff -r dd6cd88cebd9 -r 08369e33c185 src/HOL/Eisbach/match_method.ML --- a/src/HOL/Eisbach/match_method.ML Mon May 30 20:58:54 2016 +0200 +++ b/src/HOL/Eisbach/match_method.ML Mon May 30 16:11:53 2016 +1000 @@ -54,6 +54,9 @@ fun nameable_match m = (case m of Match_Fact _ => true | Match_Prems _ => true | _ => false); fun prop_match m = (case m of Match_Term _ => false | _ => true); +val bound_thm : (thm, binding) Parse_Tools.parse_val parser = + Parse_Tools.parse_thm_val Parse.binding; + val bound_term : (term, binding) Parse_Tools.parse_val parser = Parse_Tools.parse_term_val Parse.binding; @@ -69,7 +72,7 @@ (*FIXME: Dynamic facts modify the background theory, so we have to resort to token replacement for matched facts. *) val dynamic_fact = - Scan.lift bound_term -- Attrib.opt_attribs; + Scan.lift bound_thm -- Attrib.opt_attribs; type match_args = {multi : bool, cut : int}; @@ -190,7 +193,7 @@ |> snd |> Variable.declare_maxidx (Thm.maxidx_of head_thm); in - (SOME (Thm.prop_of head_thm, att) :: tms, ctxt''') + (SOME (head_thm, att) :: tms, ctxt''') end | upd_ctxt NONE _ (tms, ctxt) = (NONE :: tms, ctxt); @@ -221,7 +224,7 @@ in src' end; val binds' = - map (Option.map (fn (t, atts) => (Morphism.term morphism t, map close_src atts))) binds; + map (Option.map (fn (t, atts) => (Morphism.thm morphism t, map close_src atts))) binds; val _ = ListPair.app @@ -245,13 +248,14 @@ end)); -fun dest_internal_fact t = +fun dest_internal_term t = (case try Logic.dest_conjunction t of SOME (params, head) => (params |> Logic.dest_conjunctions |> map Logic.dest_term, head |> Logic.dest_term) | NONE => ([], t |> Logic.dest_term)); +fun dest_internal_fact thm = dest_internal_term (Thm.prop_of thm); fun inst_thm ctxt env ts params thm = let @@ -266,7 +270,7 @@ (fn ((((SOME ((_, head), att), _), _), _), thms) => SOME (head, (thms, att)) | _ => NONE) fact_insts'; - fun try_dest_term thm = try (Thm.prop_of #> dest_internal_fact #> snd) thm; + fun try_dest_term thm = try (dest_internal_fact #> snd) thm; fun expand_fact fact_insts thm = the_default [thm] diff -r dd6cd88cebd9 -r 08369e33c185 src/HOL/Eisbach/method_closure.ML --- a/src/HOL/Eisbach/method_closure.ML Mon May 30 20:58:54 2016 +0200 +++ b/src/HOL/Eisbach/method_closure.ML Mon May 30 16:11:53 2016 +1000 @@ -260,14 +260,18 @@ val text' = (Method.map_source o map) (Token.transform morphism) text; val term_args' = map (Morphism.term morphism) term_args; + val full_name = Local_Theory.full_name lthy name; in lthy3 |> Local_Theory.close_target |> Proof_Context.restore_naming lthy |> put_closure name {vars = term_args', named_thms = named_thms, methods = method_args, body = text'} - |> Method.local_setup name (parser term_args' (recursive_method term_args' text')) "" - |> pair (Local_Theory.full_name lthy name) + |> Method.local_setup name + (Args.context :|-- (fn ctxt => + let val {body, vars, ...} = get_closure ctxt full_name in + parser vars (recursive_method vars body) end)) "" + |> pair full_name end; in diff -r dd6cd88cebd9 -r 08369e33c185 src/HOL/Eisbach/parse_tools.ML --- a/src/HOL/Eisbach/parse_tools.ML Mon May 30 20:58:54 2016 +0200 +++ b/src/HOL/Eisbach/parse_tools.ML Mon May 30 16:11:53 2016 +1000 @@ -20,6 +20,8 @@ val parse_term_val : 'b parser -> (term, 'b) parse_val parser val name_term : (term, string) parse_val parser + + val parse_thm_val : 'b parser -> (thm, 'b) parse_val parser end; structure Parse_Tools: PARSE_TOOLS = @@ -36,6 +38,11 @@ val name_term = parse_term_val Args.embedded_inner_syntax; +fun parse_thm_val scan = + Scan.ahead Parse.not_eof -- Scan.ahead (Scan.option (Args.internal_fact >> the_single)) -- scan >> + (fn ((_, SOME t), _) => Real_Val t + | ((tok, NONE), v) => Parse_Val (v, fn t => ignore (Token.assign (SOME (Token.Fact (NONE, [t]))) tok))); + fun is_real_val (Real_Val _) = true | is_real_val _ = false;