--- a/src/HOL/Eisbach/Tests.thy Wed May 13 19:12:59 2015 +0200
+++ b/src/HOL/Eisbach/Tests.thy Sat May 16 12:05:52 2015 +0200
@@ -9,8 +9,7 @@
begin
-
-section \<open>Named Theorems Tests\<close>
+subsection \<open>Named Theorems Tests\<close>
named_theorems foo
@@ -22,8 +21,10 @@
apply foo
done
+method abs_used for P = (match (P) in "\<lambda>a. ?Q" \<Rightarrow> \<open>fail\<close> \<bar> _ \<Rightarrow> \<open>-\<close>)
-section \<open>Match Tests\<close>
+
+subsection \<open>Match Tests\<close>
notepad
begin
@@ -75,7 +76,8 @@
apply (intro conjI)
apply (match premises in Y: "\<And>z :: 'a. A z" and Y'[intro]:"\<And>z :: 'b. B z" \<Rightarrow> \<open>fastforce\<close>)
apply (match premises in Y: "\<And>z :: 'a. A z" \<Rightarrow> \<open>match premises in Y'[intro]:"\<And>z :: 'b. B z" \<Rightarrow> \<open>fastforce\<close>\<close>)
- apply (match premises in Y[thin]: "\<And>z :: 'a. A z" \<Rightarrow> \<open>(match premises in Y':"\<And>z :: 'a. A z" \<Rightarrow> \<open>print_fact Y,fail\<close> \<bar> Y': "?H" \<Rightarrow> \<open>-\<close>)\<close>)
+ apply (match premises in Y[thin]: "\<And>z :: 'a. A z" \<Rightarrow> \<open>(match premises in Y':"\<And>z :: 'a. A z" \<Rightarrow> \<open>print_fact Y,fail\<close> \<bar> _ \<Rightarrow> \<open>print_fact Y\<close>)\<close>)
+ (*apply (match premises in Y: "\<And>z :: 'b. B z" \<Rightarrow> \<open>(match premises in Y'[thin]:"\<And>z :: 'b. B z" \<Rightarrow> \<open>(match premises in Y':"\<And>z :: 'a. A z" \<Rightarrow> \<open>fail\<close> \<bar> Y': _ \<Rightarrow> \<open>-\<close>)\<close>)\<close>)*)
apply assumption
done
@@ -106,16 +108,41 @@
apply (match premises in Y: "C y" \<Rightarrow> \<open>rule Y\<close>)
done
+ fix A B C P Q and x :: 'a and y :: 'a
+ have "(\<And>x y :: 'a. A x y \<and> Q) \<Longrightarrow> (\<And>a b. B (a :: 'a) (b :: 'a) \<and> Q) \<Longrightarrow> (\<And>x y. C (x :: 'a) (y :: 'a) \<and> P) \<Longrightarrow> A y x \<and> B y x"
+ by (match premises in Y: "\<And>z a. ?A (z :: 'a) (a :: 'a) \<and> R" (multi) for R \<Rightarrow> \<open>rule conjI, rule Y[where z=x,THEN conjunct1], rule Y[THEN conjunct1]\<close>)
+
(*We may use for-fixes in multi-matches too. All bound facts must agree on the fixed term *)
fix A B C x
have "(\<And>y :: 'a. B y \<and> C y) \<Longrightarrow> (\<And>x :: 'a. A x \<and> B x) \<Longrightarrow> (\<And>y :: 'a. A y \<and> C y) \<Longrightarrow> C y \<Longrightarrow> (A x \<and> B y \<and> C y)"
- apply (match premises in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow> \<open>intro conjI Y[THEN conjunct1]\<close>)
+ apply (match premises in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow>
+ \<open>match (P) in B \<Rightarrow> \<open>fail\<close>
+ \<bar> "\<lambda>a. B" \<Rightarrow> \<open>fail\<close>
+ \<bar> _ \<Rightarrow> \<open>-\<close>,
+ intro conjI, (rule Y[THEN conjunct1])\<close>)
+ apply (rule dup)
+ apply (match premises in Y':"\<And>x :: 'a. ?U x \<and> Q x" and Y: "\<And>x :: 'a. Q x \<and> ?U x" (multi) for Q \<Rightarrow> \<open>insert Y[THEN conjunct1]\<close>)
+ apply assumption (* Previous match requires that Q is consistent *)
apply (match premises in Y: "\<And>z :: 'a. ?A z \<longrightarrow> False" (multi) \<Rightarrow> \<open>print_fact Y, fail\<close> \<bar> "C y" \<Rightarrow> \<open>print_term C\<close>) (* multi-match must bind something *)
apply (match premises in Y: "\<And>x. B x \<and> C x" \<Rightarrow> \<open>intro conjI Y[THEN conjunct1]\<close>)
apply (match premises in Y: "C ?x" \<Rightarrow> \<open>rule Y\<close>)
done
+ (* All bindings must be tried for a particular theorem.
+ However all combinations are NOT explored. *)
+ fix B A C
+ assume asms:"\<And>a b. B (a :: 'a) (b :: 'a) \<and> Q" "\<And>x :: 'a. A x x \<and> Q" "\<And>a b. C (a :: 'a) (b :: 'a) \<and> Q"
+ have "B y x \<and> C x y \<and> B x y \<and> C y x \<and> A x x"
+ apply (intro conjI)
+ apply (match asms in Y: "\<And>z a. ?A (z :: 'a) (a :: 'a) \<and> R" (multi) for R \<Rightarrow> \<open>rule Y[where z=x,THEN conjunct1]\<close>)
+ apply (match asms in Y: "\<And>z a. ?A (z :: 'a) (a :: 'a) \<and> R" (multi) for R \<Rightarrow> \<open>rule Y[where a=x,THEN conjunct1]\<close>)
+ apply (match asms in Y: "\<And>z a. ?A (z :: 'a) (a :: 'a) \<and> R" (multi) for R \<Rightarrow> \<open>rule Y[where a=x,THEN conjunct1]\<close>)
+ apply (match asms in Y: "\<And>z a. ?A (z :: 'a) (a :: 'a) \<and> R" (multi) for R \<Rightarrow> \<open>rule Y[where z=x,THEN conjunct1]\<close>)
+ apply (match asms in Y: "\<And>z a. A (z :: 'a) (a :: 'a) \<and> R" for R \<Rightarrow> \<open>fail\<close> \<bar> _ \<Rightarrow> \<open>-\<close>)
+ apply (rule asms[THEN conjunct1])
+ done
+
(* Attributes *)
fix A B C x
have "(\<And>x :: 'a. A x \<and> B x) \<Longrightarrow> (\<And>y :: 'a. A y \<and> C y) \<Longrightarrow> (\<And>y :: 'a. B y \<and> C y) \<Longrightarrow> C y \<Longrightarrow> (A x \<and> B y \<and> C y)"
@@ -145,6 +172,10 @@
by (((match premises in I: "P \<and> Q" (cut)
and I': "P \<longrightarrow> ?U" for P Q \<Rightarrow> \<open>rule mp [OF I' I[THEN conjunct1]]\<close>)?), simp)
+ have "D \<and> C \<Longrightarrow> A \<and> B \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> D \<longrightarrow> True \<Longrightarrow> C"
+ by (match premises in I: "P \<and> Q" (cut 2)
+ and I': "P \<longrightarrow> ?U" for P Q \<Rightarrow> \<open>rule mp [OF I' I[THEN conjunct1]]\<close>)
+
have "A \<and> B \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> C"
by (((match premises in I: "P \<and> Q" (cut)
and I': "P \<longrightarrow> ?U" for P Q \<Rightarrow> \<open>rule mp [OF I' I[THEN conjunct1]]\<close>)?, simp) | simp)
@@ -156,13 +187,39 @@
fix A B C
assume X: "A \<and> B" "A \<and> C" C
have "A \<and> B \<and> C"
- by (match X in H: "A \<and> ?H" (multi,cut) \<Rightarrow>
+ by (match X in H: "A \<and> ?H" (multi, cut) \<Rightarrow>
\<open>match H in "A \<and> C" and "A \<and> B" \<Rightarrow> \<open>fail\<close>\<close>
| simp add: X)
+
+ (* Thinning an inner focus *)
+ (* Thinning should persist within a match, even when on an external premise *)
+
+ fix A
+ have "(\<And>x. A x \<and> B) \<Longrightarrow> B \<and> C \<Longrightarrow> C"
+ apply (match premises in H:"\<And>x. A x \<and> B" \<Rightarrow>
+ \<open>match premises in H'[thin]: "\<And>x. A x \<and> B" \<Rightarrow>
+ \<open>match premises in H'':"\<And>x. A x \<and> B" \<Rightarrow> \<open>fail\<close>
+ \<bar> _ \<Rightarrow> \<open>-\<close>\<close>
+ ,match premises in H'':"\<And>x. A x \<and> B" \<Rightarrow> \<open>fail\<close> \<bar> _ \<Rightarrow> \<open>-\<close>\<close>)
+ apply (match premises in H:"\<And>x. A x \<and> B" \<Rightarrow> \<open>fail\<close>
+ \<bar> H':_ \<Rightarrow> \<open>rule H'[THEN conjunct2]\<close>)
+ done
+
+
+ (* Local premises *)
+ (* Only match premises which actually existed in the goal we just focused.*)
+
+ fix A
+ assume asms: "C \<and> D"
+ have "B \<and> C \<Longrightarrow> C"
+ by (match premises in _ \<Rightarrow> \<open>insert asms,
+ match premises (local) in "B \<and> C" \<Rightarrow> \<open>fail\<close>
+ \<bar> H:"C \<and> D" \<Rightarrow> \<open>rule H[THEN conjunct1]\<close>\<close>)
end
+
(* Testing inner focusing. This fails if we don't smash flex-flex pairs produced
by retrofitting. This needs to be done more carefully to avoid smashing
legitimate pairs.*)
@@ -193,7 +250,8 @@
fun test_internal_fact ctxt factnm =
(case try (Proof_Context.get_thms ctxt) factnm of
NONE => ()
- | SOME _ => error "Found internal fact")\<close>
+ | SOME _ => error "Found internal fact");
+\<close>
method uses_test\<^sub>1 uses uses_test\<^sub>1_uses = (rule uses_test\<^sub>1_uses)
@@ -205,7 +263,7 @@
ML \<open>test_internal_fact @{context} "Tests.uses_test\<^sub>1.uses_test\<^sub>1_uses"\<close>
-(* Testing term and fact passing in recursion *)
+subsection \<open>Testing term and fact passing in recursion\<close>
method recursion_example for x :: bool uses facts =
(match (x) in
@@ -219,6 +277,23 @@
apply simp
done
+(* uses facts are not accumulated *)
+
+method recursion_example' for A :: bool and B :: bool uses facts =
+ (match facts in
+ H: "A" and H': "B" \<Rightarrow> \<open>recursion_example' "A" "B" facts: H TrueI\<close>
+ \<bar> "A" and "True" \<Rightarrow> \<open>recursion_example' "A" "B" facts: TrueI\<close>
+ \<bar> "True" \<Rightarrow> \<open>-\<close>
+ \<bar> "PROP ?P" \<Rightarrow> \<open>fail\<close>)
+
+lemma
+ assumes asms: "A" "B"
+ shows "True"
+ apply (recursion_example' "A" "B" facts: asms)
+ apply simp
+ done
+
+
(*Method.sections in existing method*)
method my_simp\<^sub>1 uses my_simp\<^sub>1_facts = (simp add: my_simp\<^sub>1_facts)
lemma assumes A shows A by (my_simp\<^sub>1 my_simp\<^sub>1_facts: assms)
@@ -265,13 +340,14 @@
-(* Polymorphism test *)
+subsection \<open>Polymorphism test\<close>
axiomatization foo' :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> bool"
axiomatization where foo'_ax1: "foo' x y z \<Longrightarrow> z \<and> y"
axiomatization where foo'_ax2: "foo' x y y \<Longrightarrow> x \<and> z"
+axiomatization where foo'_ax3: "foo' (x :: int) y y \<Longrightarrow> y \<and> y"
-lemmas my_thms = foo'_ax1 foo'_ax2
+lemmas my_thms = foo'_ax1 foo'_ax2 foo'_ax3
definition first_id where "first_id x = x"
@@ -294,6 +370,36 @@
done
+subsection \<open>Unchecked rule instantiation, with the possibility of runtime errors\<close>
+
+named_theorems my_thms_named
+
+declare foo'_ax3[my_thms_named]
+
+method foo_method3 declares my_thms_named =
+ (match my_thms_named[of (unchecked) z for z] in R:"PROP ?H" \<Rightarrow> \<open>rule R\<close>)
+
+notepad
+begin
+
+ (*FIXME: Shouldn't need unchecked keyword here. See Tests_Failing.thy *)
+ fix A B x
+ have "foo' x B A \<Longrightarrow> A \<and> B"
+ by (match my_thms[of (unchecked) z for z] in R:"PROP ?H" \<Rightarrow> \<open>rule R\<close>)
+
+ fix A B x
+ note foo'_ax1[my_thms_named]
+ have "foo' x B A \<Longrightarrow> A \<and> B"
+ by (match my_thms_named[where x=z for z] in R:"PROP ?H" \<Rightarrow> \<open>rule R\<close>)
+
+ fix A B x
+ note foo'_ax1[my_thms_named] foo'_ax2[my_thms_named] foo'_ax3[my_thms_named]
+ have "foo' x B A \<Longrightarrow> A \<and> B"
+ by foo_method3
+
+end
+
+
ML \<open>
structure Data = Generic_Data
(
@@ -324,34 +430,36 @@
end
-notepad begin
+notepad
+begin
fix A x
assume X: "\<And>x. A x"
have "A x"
- by (match X in H[of x]:"\<And>x. A x" \<Rightarrow> \<open>print_fact H,match H in "A x" \<Rightarrow> \<open>rule H\<close>\<close>)
+ by (match X in H[of x]:"\<And>x. A x" \<Rightarrow> \<open>print_fact H,match H in "A x" \<Rightarrow> \<open>rule H\<close>\<close>)
fix A x B
assume X: "\<And>x :: bool. A x \<Longrightarrow> B" "\<And>x. A x"
assume Y: "A B"
have "B \<and> B \<and> B \<and> B \<and> B \<and> B"
- apply (intro conjI)
- apply (match X in H[OF X(2)]:"\<And>x. A x \<Longrightarrow> B" \<Rightarrow> \<open>print_fact H,rule H\<close>)
- apply (match X in H':"\<And>x. A x" and H[OF H']:"\<And>x. A x \<Longrightarrow> B" \<Rightarrow> \<open>print_fact H',print_fact H,rule H\<close>)
- apply (match X in H[of Q]:"\<And>x. A x \<Longrightarrow> ?R" and "?P \<Longrightarrow> Q" for Q \<Rightarrow> \<open>print_fact H,rule H, rule Y\<close>)
- apply (match X in H[of Q,OF Y]:"\<And>x. A x \<Longrightarrow> ?R" and "?P \<Longrightarrow> Q" for Q \<Rightarrow> \<open>print_fact H,rule H\<close>)
- apply (match X in H[OF Y,intro]:"\<And>x. A x \<Longrightarrow> ?R" \<Rightarrow> \<open>print_fact H,fastforce\<close>)
- apply (match X in H[intro]:"\<And>x. A x \<Longrightarrow> ?R" \<Rightarrow> \<open>rule H[where x=B], rule Y\<close>)
- done
-
+ apply (intro conjI)
+ apply (match X in H[OF X(2)]:"\<And>x. A x \<Longrightarrow> B" \<Rightarrow> \<open>print_fact H,rule H\<close>)
+ apply (match X in H':"\<And>x. A x" and H[OF H']:"\<And>x. A x \<Longrightarrow> B" \<Rightarrow> \<open>print_fact H',print_fact H,rule H\<close>)
+ apply (match X in H[of Q]:"\<And>x. A x \<Longrightarrow> ?R" and "?P \<Longrightarrow> Q" for Q \<Rightarrow> \<open>print_fact H,rule H, rule Y\<close>)
+ apply (match X in H[of Q,OF Y]:"\<And>x. A x \<Longrightarrow> ?R" and "?P \<Longrightarrow> Q" for Q \<Rightarrow> \<open>print_fact H,rule H\<close>)
+ apply (match X in H[OF Y,intro]:"\<And>x. A x \<Longrightarrow> ?R" \<Rightarrow> \<open>print_fact H,fastforce\<close>)
+ apply (match X in H[intro]:"\<And>x. A x \<Longrightarrow> ?R" \<Rightarrow> \<open>rule H[where x=B], rule Y\<close>)
+ done
+
fix x :: "prop" and A
assume X: "TERM x"
assume Y: "\<And>x :: prop. A x"
have "A TERM x"
- apply (match X in "PROP y" for y \<Rightarrow> \<open>rule Y[where x="PROP y"]\<close>)
- done
+ apply (match X in "PROP y" for y \<Rightarrow> \<open>rule Y[where x="PROP y"]\<close>)
+ done
end
-(* Method name internalization test *)
+
+subsection \<open>Method name internalization test\<close>
method test2 = (simp)
--- a/src/HOL/Eisbach/eisbach_rule_insts.ML Wed May 13 19:12:59 2015 +0200
+++ b/src/HOL/Eisbach/eisbach_rule_insts.ML Sat May 16 12:05:52 2015 +0200
@@ -72,39 +72,59 @@
|> restore_tags thm
end;
+(* FIXME unused *)
+fun read_instantiate_no_thm ctxt insts fixes =
+ let
+ val (type_insts, term_insts) =
+ List.partition (fn (((x, _) : indexname), _) => String.isPrefix "'" x) insts;
+
+ val ctxt1 =
+ ctxt
+ |> Context_Position.not_really
+ |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2;
+
+ val typs =
+ map snd type_insts
+ |> Syntax.read_typs ctxt1
+ |> Syntax.check_typs ctxt1;
+
+ val typ_insts' = map2 (fn (xi, _) => fn T => (xi,T)) type_insts typs;
+
+ val terms =
+ map snd term_insts
+ |> Syntax.read_terms ctxt1
+ |> Syntax.check_terms ctxt1;
+
+ val term_insts' = map2 (fn (xi, _) => fn t => (xi, t)) term_insts terms;
+
+ in (typ_insts',term_insts') end;
+
datatype rule_inst =
- Named_Insts of ((indexname * string) * (term -> unit)) list
-| Term_Insts of (indexname * term) list;
+ Named_Insts of ((indexname * string) * (term -> unit)) list * (binding * string option * mixfix) list
+(*| Unchecked_Of_Insts of (string option list * string option list) * (binding * string option * mixfix) list*)
+| Term_Insts of (indexname * term) list
+| Unchecked_Term_Insts of term option list * term option list;
+
+fun mk_pair (t, t') = Logic.mk_conjunction (Logic.mk_term t, Logic.mk_term t');
+
+fun dest_pair t = apply2 Logic.dest_term (Logic.dest_conjunction t);
fun embed_indexname ((xi, s), f) =
- let
- fun wrap_xi xi t =
- Logic.mk_conjunction (Logic.mk_term (Var (xi, fastype_of t)), Logic.mk_term t);
+ let fun wrap_xi xi t = mk_pair (Var (xi, fastype_of t), t);
in ((xi, s), f o wrap_xi xi) end;
-fun unembed_indexname t =
- let
- val (t, t') = apply2 Logic.dest_term (Logic.dest_conjunction t);
- val (xi, _) = Term.dest_Var t;
- in (xi, t') end;
+fun unembed_indexname t = dest_pair t |> apfst (Term.dest_Var #> fst);
-fun read_where_insts toks =
+fun read_where_insts (insts, fixes) =
let
- val parser =
- Parse.!!!
- (Parse.and_list1 (Args.var -- (Args.$$$ "=" |-- Parse_Tools.name_term)) -- Parse.for_fixes)
- --| Scan.ahead Parse.eof;
- val (insts, fixes) = the (Scan.read Token.stopper parser toks);
-
val insts' =
if forall (fn (_, v) => Parse_Tools.is_real_val v) insts
- then Term_Insts (map (fn (_, t) => unembed_indexname (Parse_Tools.the_real_val t)) insts)
- else Named_Insts (map (fn (xi, p) => embed_indexname
- ((xi, Parse_Tools.the_parse_val p), Parse_Tools.the_parse_fun p)) insts);
- in
- (insts', fixes)
- end;
+ then Term_Insts (map (unembed_indexname o Parse_Tools.the_real_val o snd) insts)
+ else
+ Named_Insts (map (fn (xi, p) => embed_indexname
+ ((xi, Parse_Tools.the_parse_val p), Parse_Tools.the_parse_fun p)) insts, fixes);
+ in insts' end;
fun of_rule thm (args, concl_args) =
let
@@ -120,32 +140,55 @@
val inst = Args.maybe Parse_Tools.name_term;
val concl = Args.$$$ "concl" -- Args.colon;
-fun read_of_insts toks thm =
+fun close_unchecked_insts context ((insts,concl_inst), fixes) =
let
- val parser =
- Parse.!!!
- ((Scan.repeat (Scan.unless concl inst) -- Scan.optional (concl |-- Scan.repeat inst) [])
- -- Parse.for_fixes) --| Scan.ahead Parse.eof;
- val ((insts, concl_insts), fixes) =
- the (Scan.read Token.stopper parser toks);
+ val ctxt = Context.proof_of context;
+ val ctxt1 = ctxt
+ |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2;
+
+ val insts' = insts @ concl_inst;
+
+ val term_insts =
+ map (the_list o (Option.map Parse_Tools.the_parse_val)) insts'
+ |> burrow (Syntax.read_terms ctxt1
+ #> Syntax.check_terms ctxt1
+ #> Variable.export_terms ctxt1 ctxt)
+ |> map (try the_single);
- val insts' =
- if forall (fn SOME t => Parse_Tools.is_real_val t | NONE => true) (insts @ concl_insts)
- then
- Term_Insts
- (map_filter
- (Option.map (Parse_Tools.the_real_val #> unembed_indexname)) (insts @ concl_insts))
- else
+ val _ =
+ (insts', term_insts)
+ |> ListPair.app (fn (SOME p, SOME t) => Parse_Tools.the_parse_fun p t | _ => ());
+ val (insts'',concl_insts'') = chop (length insts) term_insts;
+ in Unchecked_Term_Insts (insts'', concl_insts'') end;
+
+fun read_of_insts checked context ((insts, concl_insts), fixes) =
+ if forall (fn SOME t => Parse_Tools.is_real_val t | NONE => true) (insts @ concl_insts)
+ then
+ if checked
+ then
+ (fn _ =>
+ Term_Insts
+ (map (unembed_indexname o Parse_Tools.the_real_val) (map_filter I (insts @ concl_insts))))
+ else
+ (fn _ =>
+ Unchecked_Term_Insts
+ (map (Option.map Parse_Tools.the_real_val) insts,
+ map (Option.map Parse_Tools.the_real_val) concl_insts))
+ else
+ if checked
+ then
+ (fn thm =>
Named_Insts
(apply2
(map (Option.map (fn p => (Parse_Tools.the_parse_val p, Parse_Tools.the_parse_fun p))))
(insts, concl_insts)
- |> of_rule thm |> map ((fn (xi, (nm, tok)) => embed_indexname ((xi, nm), tok))));
- in
- (insts', fixes)
- end;
+ |> of_rule thm |> map ((fn (xi, (nm, f)) => embed_indexname ((xi, nm), f))), fixes))
+ else
+ let val result = close_unchecked_insts context ((insts, concl_insts), fixes);
+ in fn _ => result end;
-fun read_instantiate_closed ctxt ((Named_Insts insts), fixes) thm =
+
+fun read_instantiate_closed ctxt (Named_Insts (insts, fixes)) thm =
let
val insts' = map (fn ((v, t), _) => ((v, Position.none), t)) insts;
@@ -170,22 +213,42 @@
in
(thm'' |> restore_tags thm)
end
- | read_instantiate_closed _ ((Term_Insts insts), _) thm = instantiate_xis insts thm;
-
-val parse_all : Token.T list context_parser = Scan.lift (Scan.many Token.not_eof);
+ | read_instantiate_closed ctxt (Unchecked_Term_Insts insts) thm =
+ let
+ val (xis, ts) = ListPair.unzip (of_rule thm insts);
+ val ctxt' = Variable.declare_maxidx (Thm.maxidx_of thm) ctxt;
+ val (ts', ctxt'') = Variable.import_terms false ts ctxt';
+ val ts'' = Variable.export_terms ctxt'' ctxt ts';
+ val insts' = ListPair.zip (xis, ts'');
+ in instantiate_xis insts' thm end
+ | read_instantiate_closed _ (Term_Insts insts) thm = instantiate_xis insts thm;
val _ =
Theory.setup
- (Attrib.setup @{binding "where"} (parse_all >>
- (fn toks => Thm.rule_attribute (fn context =>
- read_instantiate_closed (Context.proof_of context) (read_where_insts toks))))
+ (Attrib.setup @{binding "where"}
+ (Scan.lift
+ (Parse.and_list1 (Args.var -- (Args.$$$ "=" |-- Parse_Tools.name_term)) -- Parse.for_fixes)
+ >> (fn args => let val args' = read_where_insts args in Thm.rule_attribute (fn context =>
+ read_instantiate_closed (Context.proof_of context) args') end))
"named instantiation of theorem");
val _ =
Theory.setup
- (Attrib.setup @{binding "of"} (parse_all >>
- (fn toks => Thm.rule_attribute (fn context => fn thm =>
- read_instantiate_closed (Context.proof_of context) (read_of_insts toks thm) thm)))
+ (Attrib.setup @{binding "of"}
+ (Scan.lift
+ (Args.mode "unchecked" --
+ (Scan.repeat (Scan.unless concl inst) --
+ Scan.optional (concl |-- Scan.repeat inst) [] --
+ Parse.for_fixes)) -- Scan.state >>
+ (fn ((unchecked, args), context) =>
+ let
+ val read_insts = read_of_insts (not unchecked) context args;
+ in
+ Thm.rule_attribute (fn context => fn thm =>
+ if Method_Closure.is_free_thm thm andalso unchecked
+ then Method_Closure.dummy_free_thm
+ else read_instantiate_closed (Context.proof_of context) (read_insts thm) thm)
+ end))
"positional instantiation of theorem");
end;
--- a/src/HOL/Eisbach/match_method.ML Wed May 13 19:12:59 2015 +0200
+++ b/src/HOL/Eisbach/match_method.ML Sat May 16 12:05:52 2015 +0200
@@ -40,20 +40,20 @@
Match_Term of term Item_Net.T
| Match_Fact of thm Item_Net.T
| Match_Concl
- | Match_Prems;
+ | Match_Prems of bool;
val aconv_net = Item_Net.init (op aconv) single;
val parse_match_kind =
Scan.lift @{keyword "conclusion"} >> K Match_Concl ||
- Scan.lift @{keyword "premises"} >> K Match_Prems ||
+ Scan.lift (@{keyword "premises"} |-- Args.mode "local") >> Match_Prems ||
Scan.lift (@{keyword "("}) |-- Args.term --| Scan.lift (@{keyword ")"}) >>
(fn t => Match_Term (Item_Net.update t aconv_net)) ||
Attrib.thms >> (fn thms => Match_Fact (fold Item_Net.update thms Thm.full_rules));
-fun nameable_match m = (case m of Match_Fact _ => true | Match_Prems => true | _ => false);
+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_term : (term, binding) Parse_Tools.parse_val parser =
@@ -66,28 +66,24 @@
val for_fixes = Scan.optional (@{keyword "for"} |-- fixes) [];
-fun pos_of dyn =
- (case dyn of
- Parse_Tools.Parse_Val (b, _) => Binding.pos_of b
- | _ => raise Fail "Not a parse value");
-
+fun pos_of dyn = Parse_Tools.the_parse_val dyn |> Binding.pos_of;
(*FIXME: Dynamic facts modify the background theory, so we have to resort
to token replacement for matched facts. *)
fun dynamic_fact ctxt =
bound_term -- Args.opt_attribs (Attrib.check_name ctxt);
-type match_args = {multi : bool, cut : bool};
+type match_args = {multi : bool, cut : int};
val parse_match_args =
Scan.optional (Args.parens (Parse.enum1 ","
- (Args.$$$ "multi" || Args.$$$ "cut"))) [] >>
+ (Args.$$$ "multi" -- Scan.succeed ~1 || Args.$$$ "cut" -- Scan.optional Parse.int 1))) [] >>
(fn ss =>
fold (fn s => fn {multi, cut} =>
(case s of
- "multi" => {multi = true, cut = cut}
- | "cut" => {multi = multi, cut = true}))
- ss {multi = false, cut = false});
+ ("multi", _) => {multi = true, cut = cut}
+ | ("cut", n) => {multi = multi, cut = n}))
+ ss {multi = false, cut = ~1});
fun parse_named_pats match_kind =
Args.context :|-- (fn ctxt =>
@@ -126,8 +122,22 @@
then Syntax.parse_prop ctxt3 term
else Syntax.parse_term ctxt3 term;
+ fun drop_Trueprop_dummy t =
+ (case t of
+ Const (@{const_name Trueprop}, _) $
+ (Const (@{syntax_const "_type_constraint_"}, T) $
+ Const (@{const_name Pure.dummy_pattern}, _)) =>
+ Const (@{syntax_const "_type_constraint_"}, T) $
+ Const (@{const_name Pure.dummy_pattern}, propT)
+ | t1 $ t2 => drop_Trueprop_dummy t1 $ drop_Trueprop_dummy t2
+ | Abs (a, T, b) => Abs (a, T, drop_Trueprop_dummy b)
+ | _ => t);
+
val pats =
map (fn (_, (term, _)) => parse_term (Parse_Tools.the_parse_val term)) ts
+ |> map drop_Trueprop_dummy
+ |> (fn ts => fold_map Term.replace_dummy_patterns ts (Variable.maxidx_of ctxt3 + 1))
+ |> fst
|> Syntax.check_terms ctxt3;
val pat_fixes = fold (Term.add_frees) pats [] |> map fst;
@@ -138,7 +148,7 @@
error ("For-fixed variable must be bound in some pattern" ^ Position.here pos))
fix_nms fixes;
- val _ = map (Term.map_types Type.no_tvars) pats
+ val _ = map (Term.map_types Type.no_tvars) pats;
val ctxt4 = fold Variable.declare_term pats ctxt3;
@@ -200,14 +210,14 @@
|> Variable.declare_maxidx (Variable.maxidx_of ctxt6));
val pats' = map (Term.map_types Type_Infer.paramify_vars #> Morphism.term morphism) pats;
- val _ = ListPair.app (fn ((_, (Parse_Tools.Parse_Val (_, f), _)), t) => f t) (ts, pats');
+ val _ = ListPair.app (fn ((_, (v, _)), t) => Parse_Tools.the_parse_fun v t) (ts, pats');
fun close_src src =
let
val src' = Token.closure_src src |> Token.transform_src morphism;
val _ =
map2 (fn tok1 => fn tok2 =>
- (case (Token.get_value tok2) of
+ (case Token.get_value tok2 of
SOME value => Token.assign (SOME value) tok1
| NONE => ()))
(Token.args_of_src src)
@@ -219,14 +229,14 @@
val _ =
ListPair.app
- (fn ((SOME ((Parse_Tools.Parse_Val (_, f), _)), _), SOME (t, _)) => f t
+ (fn ((SOME ((v, _)), _), SOME (t, _)) => Parse_Tools.the_parse_fun v t
| ((NONE, _), NONE) => ()
| _ => error "Mismatch between real and parsed bound variables")
(ts, binds');
val real_fixes' = map (Morphism.term morphism) real_fixes;
val _ =
- ListPair.app (fn (( (Parse_Tools.Parse_Val (_, f), _) , _), t) => f t)
+ ListPair.app (fn (((v, _) , _), t) => Parse_Tools.the_parse_fun v t)
(fixes, real_fixes');
val match_args = map (fn (_, (_, match_args)) => match_args) ts;
@@ -255,7 +265,6 @@
let
val ts' = map (Envir.norm_term env) ts;
val insts = map (Thm.cterm_of ctxt) ts' ~~ map (Thm.cterm_of ctxt) params;
-
in
Drule.cterm_instantiate insts thm
end;
@@ -309,7 +318,6 @@
val pat'' :: params'' = map (Morphism.term morphism) (pat' :: params');
fun prep_head (t, att) = (dest_internal_fact t, att);
-
in
((((Option.map prep_head x, args), params''), pat''), ctxt')
end;
@@ -326,19 +334,28 @@
tenv = tenv, tyenv = tyenv}
end
-fun match_filter_env inner_ctxt morphism pat_vars fixes (ts, params) thm inner_env =
+fun morphism_env morphism env =
let
- val tenv = Envir.term_env inner_env
+ val tenv = Envir.term_env env
|> Vartab.map (K (fn (T, t) => (Morphism.typ morphism T, Morphism.term morphism t)));
+ val tyenv = Envir.type_env env
+ |> Vartab.map (K (fn (S, T) => (S, Morphism.typ morphism T)));
+ in Envir.Envir {maxidx = Envir.maxidx_of env, tenv = tenv, tyenv = tyenv} end;
- val tyenv = Envir.type_env inner_env
- |> Vartab.map (K (fn (S, T) => (S, Morphism.typ morphism T)));
+fun export_with_params ctxt morphism (SOME ts, params) thm env =
+ let
+ val outer_env = morphism_env morphism env;
+ val thm' = Morphism.thm morphism thm;
+ in inst_thm ctxt outer_env params ts thm' end
+ | export_with_params _ morphism (NONE,_) thm _ = Morphism.thm morphism thm;
- val outer_env = Envir.Envir {maxidx = Envir.maxidx_of inner_env, tenv = tenv, tyenv = tyenv};
-
+fun match_filter_env is_newly_fixed pat_vars fixes params env =
+ let
val param_vars = map Term.dest_Var params;
- val params' = map (fn (xi, _) => Vartab.lookup (Envir.term_env outer_env) xi) param_vars;
+ val tenv = Envir.term_env env;
+
+ val params' = map (fn (xi, _) => Vartab.lookup tenv xi) param_vars;
val fixes_vars = map Term.dest_Var fixes;
@@ -346,24 +363,21 @@
val extra_vars = subtract (fn ((xi, _), xi') => xi = xi') fixes_vars all_vars;
- val tenv' = tenv
- |> fold (Vartab.delete_safe) extra_vars;
+ val tenv' = tenv |> fold (Vartab.delete_safe) extra_vars;
val env' =
- Envir.Envir {maxidx = Envir.maxidx_of outer_env, tenv = tenv', tyenv = tyenv}
- |> recalculate_maxidx;
+ Envir.Envir {maxidx = Envir.maxidx_of env, tenv = tenv', tyenv = Envir.type_env env}
- val all_params_bound = forall (fn SOME (_, Var _) => true | _ => false) params';
+ val all_params_bound = forall (fn SOME (_, Free (x,_)) => is_newly_fixed x | _ => false) params';
+
+ val all_params_distinct = not (has_duplicates (op =) params');
val pat_fixes = inter (eq_fst (op =)) fixes_vars pat_vars;
val all_pat_fixes_bound = forall (fn (xi, _) => is_some (Vartab.lookup tenv' xi)) pat_fixes;
-
- val thm' = Morphism.thm morphism thm;
-
in
- if all_params_bound andalso all_pat_fixes_bound then
- SOME (case ts of SOME ts => inst_thm inner_ctxt outer_env params ts thm' | _ => thm', env')
+ if all_params_bound andalso all_pat_fixes_bound andalso all_params_distinct
+ then SOME env'
else NONE
end;
@@ -374,7 +388,7 @@
fun prem_id_eq ((id, _ : thm), (id', _ : thm)) = id = id';
val prem_rules : (int * thm) Item_Net.T =
- Item_Net.init prem_id_eq (single o Thm.full_prop_of o snd);
+ Item_Net.init prem_id_eq (single o Thm.full_prop_of o snd);
fun raw_thm_to_id thm =
(case Properties.get (Thm.get_tags thm) prem_idN of NONE => NONE | SOME id => Int.fromString id)
@@ -394,13 +408,34 @@
val focus_prems = #1 o Focus_Data.get;
+fun hyp_from_premid ctxt (ident, prem) =
+ let
+ val ident = Thm.cterm_of ctxt (HOLogic.mk_number @{typ nat} ident |> Logic.mk_term);
+ val hyp =
+ (case #hyps (Thm.crep_thm prem) of
+ [hyp] => hyp
+ | _ => error "Prem should have exactly one hyp"); (* FIXME error vs. raise Fail !? *)
+ val ct = Drule.mk_term (hyp) |> Thm.cprop_of;
+ in Drule.protect (Conjunction.mk_conjunction (ident, ct)) end;
+
+fun hyp_from_ctermid ctxt (ident,cterm) =
+ let
+ val ident = Thm.cterm_of ctxt (HOLogic.mk_number @{typ nat} ident |> Logic.mk_term);
+ in Drule.protect (Conjunction.mk_conjunction (ident, cterm)) end;
+
+fun add_premid_hyp premid ctxt =
+ Thm.declare_hyps (hyp_from_premid ctxt premid) ctxt;
+
fun add_focus_prem prem =
+ `(Focus_Data.get #> #1 #> #1) ##>
(Focus_Data.map o @{apply 3(1)}) (fn (next, net) =>
(next + 1, Item_Net.update (next, Thm.tag_rule (prem_idN, string_of_int next) prem) net));
-fun remove_focus_prem thm =
+fun remove_focus_prem' (ident, thm) =
(Focus_Data.map o @{apply 3(1)} o apsnd)
- (Item_Net.remove (raw_thm_to_id thm, thm));
+ (Item_Net.remove (ident, thm));
+
+fun remove_focus_prem thm = remove_focus_prem' (raw_thm_to_id thm, thm);
(*TODO: Preliminary analysis to see if we're trying to clear in a non-focus match?*)
val _ =
@@ -429,22 +464,48 @@
(Focus_Data.map o @{apply 3(3)})
(append (map (fn (_, ct) => Thm.term_of ct) params));
+fun solve_term ct = Thm.trivial ct OF [Drule.termI];
+
+fun get_thinned_prems goal =
+ let
+ val chyps = Thm.crep_thm goal |> #hyps;
+
+ fun prem_from_hyp hyp goal =
+ let
+ val asm = Thm.assume hyp;
+ val (identt,ct) = asm |> Goal.conclude |> Thm.cprop_of |> Conjunction.dest_conjunction;
+ val ident = HOLogic.dest_number (Thm.term_of identt |> Logic.dest_term) |> snd;
+ val thm = Conjunction.intr (solve_term identt) (solve_term ct) |> Goal.protect 0
+ val goal' = Thm.implies_elim (Thm.implies_intr hyp goal) thm;
+ in
+ (SOME (ident,ct),goal')
+ end handle TERM _ => (NONE,goal) | THM _ => (NONE,goal);
+ in
+ fold_map prem_from_hyp chyps goal
+ |>> map_filter I
+ end;
+
(* Add focus elements as proof data *)
-fun augment_focus
- ({context, params, prems, asms, concl, schematics} : Subgoal.focus) : Subgoal.focus =
+fun augment_focus (focus: Subgoal.focus) : (int list * Subgoal.focus) =
let
- val context' = context
+ val {context, params, prems, asms, concl, schematics} = focus;
+
+ val (prem_ids,ctxt') = context
|> add_focus_params params
|> add_focus_schematics (snd schematics)
- |> fold add_focus_prem (rev prems);
+ |> fold_map add_focus_prem (rev prems)
+
+ val local_prems = map2 pair prem_ids (rev prems);
+
+ val ctxt'' = fold add_premid_hyp local_prems ctxt';
in
- {context = context',
+ (prem_ids,{context = ctxt'',
params = params,
prems = prems,
concl = concl,
schematics = schematics,
- asms = asms}
+ asms = asms})
end;
@@ -467,25 +528,17 @@
schematics = schematics', asms = asms} : Subgoal.focus, goal'')
end;
-exception MATCH_CUT;
-
-val raise_match : (thm * Envir.env) Seq.seq = Seq.make (fn () => raise MATCH_CUT);
-
-fun map_handle seq =
- Seq.make (fn () =>
- (case (Seq.pull seq handle MATCH_CUT => NONE) of
- SOME (x, seq') => SOME (x, map_handle seq')
- | NONE => NONE));
fun deduplicate eq prev seq =
Seq.make (fn () =>
- (case (Seq.pull seq) of
+ (case Seq.pull seq of
SOME (x, seq') =>
if member eq prev x
then Seq.pull (deduplicate eq prev seq')
else SOME (x, deduplicate eq (x :: prev) seq')
| NONE => NONE));
+
fun consistent_env env =
let
val tenv = Envir.term_env env;
@@ -494,84 +547,135 @@
forall (fn (_, (T, t)) => Envir.norm_type tyenv T = fastype_of t) (Vartab.dest tenv)
end;
+fun term_eq_wrt (env1,env2) (t1,t2) =
+ Envir.eta_contract (Envir.norm_term env1 t1) aconv
+ Envir.eta_contract (Envir.norm_term env2 t2);
+
+fun type_eq_wrt (env1,env2) (T1,T2) =
+ Envir.norm_type (Envir.type_env env1) T1 = Envir.norm_type (Envir.type_env env2) T2
+
+
fun eq_env (env1, env2) =
- let
- val tyenv1 = Envir.type_env env1;
- val tyenv2 = Envir.type_env env2;
- in
Envir.maxidx_of env1 = Envir.maxidx_of env1 andalso
ListPair.allEq (fn ((var, (_, t)), (var', (_, t'))) =>
- (var = var' andalso
- Envir.eta_contract (Envir.norm_term env1 t) aconv
- Envir.eta_contract (Envir.norm_term env2 t')))
+ (var = var' andalso term_eq_wrt (env1,env2) (t,t')))
(apply2 Vartab.dest (Envir.term_env env1, Envir.term_env env2))
andalso
ListPair.allEq (fn ((var, (_, T)), (var', (_, T'))) =>
- var = var' andalso Envir.norm_type tyenv1 T = Envir.norm_type tyenv2 T')
- (apply2 Vartab.dest (Envir.type_env env1, Envir.type_env env2))
- end;
+ var = var' andalso type_eq_wrt (env1,env2) (T,T'))
+ (apply2 Vartab.dest (Envir.type_env env1, Envir.type_env env2));
+
+
+fun merge_env (env1,env2) =
+ let
+ val tenv =
+ Vartab.merge (eq_snd (term_eq_wrt (env1, env2))) (Envir.term_env env1, Envir.term_env env2);
+ val tyenv =
+ Vartab.merge (eq_snd (type_eq_wrt (env1, env2)) andf eq_fst (op =))
+ (Envir.type_env env1,Envir.type_env env2);
+ val maxidx = Int.max (Envir.maxidx_of env1, Envir.maxidx_of env2);
+ in Envir.Envir {maxidx = maxidx, tenv = tenv, tyenv = tyenv} end;
+
+fun import_with_tags thms ctxt =
+ let
+ val ((_, thms'), ctxt') = Variable.import false thms ctxt;
+ val thms'' = map2 (fn thm => Thm.map_tags (K (Thm.get_tags thm))) thms thms';
+ in (thms'', ctxt') end;
+
+
+fun try_merge (env, env') = SOME (merge_env (env, env')) handle Vartab.DUP _ => NONE
+
+
+fun Seq_retrieve seq f =
+ let
+ fun retrieve' (list, seq) f =
+ (case Seq.pull seq of
+ SOME (x, seq') =>
+ if f x then (SOME x, (list, seq'))
+ else retrieve' (list @ [x], seq') f
+ | NONE => (NONE, (list, seq)));
+
+ val (result, (list, seq)) = retrieve' ([], seq) f;
+ in (result, Seq.append (Seq.of_list list) seq) end;
fun match_facts ctxt fixes prop_pats get =
let
fun is_multi (((_, x : match_args), _), _) = #multi x;
- fun is_cut (_, x : match_args) = #cut x;
+ fun get_cut (((_, x : match_args), _), _) = #cut x;
+ fun do_cut n = if n = ~1 then I else Seq.take n;
+
+ val raw_thmss = map (get o snd) prop_pats;
+ val (thmss,ctxt') = fold_burrow import_with_tags raw_thmss ctxt;
- fun match_thm (((x, params), pat), thm) env =
+ val newly_fixed = Variable.is_newly_fixed ctxt' ctxt;
+
+ val morphism = Variable.export_morphism ctxt' ctxt;
+
+ fun match_thm (((x, params), pat), thm) =
let
val pat_vars = Term.add_vars pat [];
- val pat' = pat |> Envir.norm_term env;
-
- val (((Tinsts', insts), [thm']), inner_ctxt) = Variable.import false [thm] ctxt;
-
- val item' = Thm.prop_of thm';
-
val ts = Option.map (fst o fst) (fst x);
- val outer_ctxt = ctxt |> Variable.declare_maxidx (Envir.maxidx_of env);
-
- val morphism = Variable.export_morphism inner_ctxt outer_ctxt;
+ val item' = Thm.prop_of thm;
val matches =
- (Unify.matchers (Context.Proof ctxt) [(pat', item')])
+ (Unify.matchers (Context.Proof ctxt) [(pat, item')])
|> Seq.filter consistent_env
|> Seq.map_filter (fn env' =>
- match_filter_env inner_ctxt morphism pat_vars fixes
- (ts, params) thm' (Envir.merge (env, env')))
+ (case match_filter_env newly_fixed pat_vars fixes params env' of
+ SOME env'' => SOME (export_with_params ctxt morphism (ts,params) thm env',env'')
+ | NONE => NONE))
|> Seq.map (apfst (Thm.map_tags (K (Thm.get_tags thm))))
- |> deduplicate (eq_snd eq_env) []
- |> is_cut x ? (fn t => Seq.make (fn () =>
- Option.map (fn (x, _) => (x, raise_match)) (Seq.pull t)));
- in
- matches
- end;
+ |> deduplicate (eq_pair Thm.eq_thm_prop eq_env) []
+ in matches end;
val all_matches =
- map (fn pat => (pat, get (snd pat))) prop_pats
+ map2 pair prop_pats thmss
|> map (fn (pat, matches) => (pat, map (fn thm => match_thm (pat, thm)) matches));
fun proc_multi_match (pat, thmenvs) (pats, env) =
- if is_multi pat then
- let
- val empty = ([], Envir.empty ~1);
+ do_cut (get_cut pat)
+ (if is_multi pat then
+ let
+ fun maximal_set tail seq envthms =
+ Seq.make (fn () =>
+ (case Seq.pull seq of
+ SOME ((thm, env'), seq') =>
+ let
+ val (result, envthms') =
+ Seq_retrieve envthms (fn (env, _) => eq_env (env, env'));
+ in
+ (case result of
+ SOME (_,thms) => SOME ((env', thm :: thms), maximal_set tail seq' envthms')
+ | NONE => Seq.pull (maximal_set (tail @ [(env', [thm])]) seq' envthms'))
+ end
+ | NONE => Seq.pull (Seq.append envthms (Seq.of_list tail))));
- val thmenvs' =
- Seq.EVERY (map (fn e => fn (thms, env) =>
- Seq.append (Seq.map (fn (thm, env') => (thm :: thms, env')) (e env))
- (Seq.single (thms, env))) thmenvs) empty;
- in
- Seq.map_filter (fn (fact, env') =>
- if not (null fact) then SOME ((pat, fact) :: pats, env') else NONE) thmenvs'
- end
- else
- fold (fn e => Seq.append (Seq.map (fn (thm, env') =>
- ((pat, [thm]) :: pats, env')) (e env))) thmenvs Seq.empty;
+ val maximal_sets = fold (maximal_set []) thmenvs Seq.empty;
+ in
+ maximal_sets
+ |> Seq.map swap
+ |> Seq.filter (fn (thms, _) => not (null thms))
+ |> Seq.map_filter (fn (thms, env') =>
+ (case try_merge (env, env') of
+ SOME env'' => SOME ((pat, thms) :: pats, env'')
+ | NONE => NONE))
+ end
+ else
+ let
+ fun just_one (thm, env') =
+ (case try_merge (env,env') of
+ SOME env'' => SOME ((pat,[thm]) :: pats, env'')
+ | NONE => NONE);
+ in fold (fn seq => Seq.append (Seq.map_filter just_one seq)) thmenvs Seq.empty end);
val all_matches =
- Seq.EVERY (map proc_multi_match all_matches) ([], Envir.empty ~1)
+ Seq.EVERY (map proc_multi_match all_matches) ([], Envir.empty ~1);
in
- map_handle all_matches
+ all_matches
+ |> Seq.map (apsnd (morphism_env morphism))
end;
fun real_match using ctxt fixes m text pats goal =
@@ -611,20 +715,24 @@
let
fun focus_cases f g =
(case match_kind of
- Match_Prems => f
+ Match_Prems b => f b
| Match_Concl => g
| _ => raise Fail "Match kind fell through");
- val ({context = focus_ctxt, params, asms, concl, ...}, focused_goal) =
- focus_cases (Subgoal.focus_prems) (focus_concl) ctxt 1 goal
+ val (goal_thins,goal) = get_thinned_prems goal;
+
+ val ((local_premids,{context = focus_ctxt, params, asms, concl, ...}), focused_goal) =
+ focus_cases (K Subgoal.focus_prems) (focus_concl) ctxt 1 goal
|>> augment_focus;
val texts =
focus_cases
- (fn _ =>
+ (fn is_local => fn _ =>
make_fact_matches focus_ctxt
- (Item_Net.retrieve (focus_prems focus_ctxt |> snd) #>
- order_list))
+ (Item_Net.retrieve (focus_prems focus_ctxt |> snd)
+ #> filter_out (member (eq_fst (op =)) goal_thins)
+ #> is_local ? filter (fn (p,_) => exists (fn id' => id' = p) local_premids)
+ #> order_list))
(fn _ =>
make_term_matches focus_ctxt (fn _ => [Logic.strip_imp_concl (Thm.term_of concl)]))
();
@@ -633,13 +741,34 @@
fun do_retrofit inner_ctxt goal' =
let
- val cleared_prems =
- subtract (eq_fst (op =))
+ val (goal'_thins,goal') = get_thinned_prems goal';
+
+ val thinned_prems =
+ ((subtract (eq_fst (op =))
(focus_prems inner_ctxt |> snd |> Item_Net.content)
- (focus_prems focus_ctxt |> snd |> Item_Net.content)
- |> map (fn (_, thm) =>
- Thm.hyps_of thm
- |> (fn [hyp] => hyp | _ => error "Prem should have only one hyp"));
+ (focus_prems focus_ctxt |> snd |> Item_Net.content))
+ |> map (fn (id, thm) =>
+ #hyps (Thm.crep_thm thm)
+ |> (fn [chyp] => (id, (SOME chyp, NONE))
+ | _ => error "Prem should have only one hyp")));
+
+ val all_thinned_prems =
+ thinned_prems @
+ map (fn (id, prem) => (id, (NONE, SOME prem))) (goal'_thins @ goal_thins);
+
+ val (thinned_local_prems,thinned_extra_prems) =
+ List.partition (fn (id, _) => member (op =) local_premids id) all_thinned_prems;
+
+ val local_thins =
+ thinned_local_prems
+ |> map (fn (_, (SOME t, _)) => Thm.term_of t
+ | (_, (_, SOME pt)) => Thm.term_of pt |> Logic.dest_term);
+
+ val extra_thins =
+ thinned_extra_prems
+ |> map (fn (id, (SOME ct, _)) => (id, Drule.mk_term ct |> Thm.cprop_of)
+ | (id, (_, SOME pt)) => (id, pt))
+ |> map (hyp_from_ctermid inner_ctxt);
val n_subgoals = Thm.nprems_of goal';
fun prep_filter t =
@@ -648,12 +777,13 @@
if member (op =) prems t then SOME (remove1 (op aconv) t prems) else NONE;
in
Subgoal.retrofit inner_ctxt ctxt params asms 1 goal' goal |>
- (if n_subgoals = 0 orelse null cleared_prems then I
+ (if n_subgoals = 0 orelse null local_thins then I
else
Seq.map (Goal.restrict 1 n_subgoals)
#> Seq.maps (ALLGOALS (fn i =>
- DETERM (filter_prems_tac' ctxt prep_filter filter_test cleared_prems i)))
+ DETERM (filter_prems_tac' ctxt prep_filter filter_test local_thins i)))
#> Seq.map (Goal.unrestrict 1))
+ |> Seq.map (fold Thm.weaken extra_thins)
end;
fun apply_text (text, ctxt') =
@@ -661,7 +791,7 @@
val goal' =
DROP_CASES (Method_Closure.method_evaluate text ctxt' using) focused_goal
|> Seq.maps (DETERM (do_retrofit ctxt'))
- |> Seq.map (fn goal => ([]: cases, goal))
+ |> Seq.map (fn goal => ([]: cases, goal));
in goal' end;
in
Seq.map apply_text texts