more standard nesting of sub-language: Parse.text allows atomic entities without quotes;
--- a/src/Doc/Eisbach/Manual.thy Tue Dec 22 17:14:35 2015 +0100
+++ b/src/Doc/Eisbach/Manual.thy Tue Dec 22 17:41:46 2015 +0100
@@ -284,7 +284,7 @@
further defined in @{cite "isabelle-isar-ref"}.
@{rail \<open>
- @@{method match} kind @'in' (pattern '\<Rightarrow>' cartouche + '\<bar>')
+ @@{method match} kind @'in' (pattern '\<Rightarrow>' @{syntax text} + '\<bar>')
;
kind:
(@'conclusion' | @'premises' ('(' 'local' ')')? |
--- a/src/HOL/Eisbach/Examples.thy Tue Dec 22 17:14:35 2015 +0100
+++ b/src/HOL/Eisbach/Examples.thy Tue Dec 22 17:41:46 2015 +0100
@@ -154,7 +154,7 @@
(assumption |
rule intros | erule elims |
subst subst | subst (asm) subst |
- (erule notE; solves \<open>prop_solver\<close>))+
+ (erule notE; solves prop_solver))+
lemmas [intros] =
conjI
@@ -199,7 +199,7 @@
done
method fol_solver =
- ((guess_ex | guess_all | prop_solver) ; solves \<open>fol_solver\<close>)
+ ((guess_ex | guess_all | prop_solver); solves fol_solver)
declare
allI [intros]
@@ -241,7 +241,7 @@
assumes imps: "A \<Longrightarrow> B \<Longrightarrow> C" "D \<Longrightarrow> C" "E \<Longrightarrow> D \<Longrightarrow> A"
shows "(A \<longrightarrow> B \<longrightarrow> C) \<and> (D \<longrightarrow> C)"
by (match imps[uncurry] in H[curry]:"_ \<Longrightarrow> C" (cut, multi) \<Rightarrow>
- \<open>match H in "E \<Longrightarrow> _" \<Rightarrow> \<open>fail\<close>
+ \<open>match H in "E \<Longrightarrow> _" \<Rightarrow> fail
\<bar> _ \<Rightarrow> \<open>simp add: H\<close>\<close>)
end
--- a/src/HOL/Eisbach/Tests.thy Tue Dec 22 17:14:35 2015 +0100
+++ b/src/HOL/Eisbach/Tests.thy Tue Dec 22 17:41:46 2015 +0100
@@ -21,7 +21,7 @@
apply foo
done
-method abs_used for P = (match (P) in "\<lambda>a. ?Q" \<Rightarrow> \<open>fail\<close> \<bar> _ \<Rightarrow> \<open>-\<close>)
+method abs_used for P = (match (P) in "\<lambda>a. ?Q" \<Rightarrow> fail \<bar> _ \<Rightarrow> -)
subsection \<open>Match Tests\<close>
@@ -74,10 +74,10 @@
fix C
have "(\<And>x :: 'a. A x) \<Longrightarrow> (\<And>z. B z) \<Longrightarrow> A y \<Longrightarrow> B x \<and> B x \<and> A y"
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: "\<And>z :: 'a. A z" and Y'[intro]:"\<And>z :: 'b. B z" \<Rightarrow> fastforce)
+ apply (match premises in Y: "\<And>z :: 'a. A z" \<Rightarrow> \<open>match premises in Y'[intro]:"\<And>z :: 'b. B z" \<Rightarrow> fastforce\<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 (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> fail \<bar> Y': _ \<Rightarrow> -)\<close>)\<close>)*)
apply assumption
done
@@ -97,14 +97,14 @@
fix A B C x
have "(\<And>x :: 'a. A x) \<Longrightarrow> (\<And>y :: 'a. B y) \<Longrightarrow> C y \<Longrightarrow> (A x \<and> B y \<and> C y)"
apply (match premises in Y[thin]: "\<And>z :: 'a. ?A z" (multi) \<Rightarrow> \<open>intro conjI, (rule Y)+\<close>)
- apply (match premises in Y[thin]: "\<And>z :: 'a. ?A z" (multi) \<Rightarrow> \<open>fail\<close> \<bar> "C y" \<Rightarrow> \<open>-\<close>) (* multi-match must bind something *)
+ apply (match premises in Y[thin]: "\<And>z :: 'a. ?A z" (multi) \<Rightarrow> fail \<bar> "C y" \<Rightarrow> -) (* multi-match must bind something *)
apply (match premises in Y: "C y" \<Rightarrow> \<open>rule Y\<close>)
done
fix A B C x
have "(\<And>x :: 'a. A x) \<Longrightarrow> (\<And>y :: 'a. B y) \<Longrightarrow> C y \<Longrightarrow> (A x \<and> B y \<and> C y)"
apply (match premises in Y[thin]: "\<And>z. ?A z" (multi) \<Rightarrow> \<open>intro conjI, (rule Y)+\<close>)
- apply (match premises in Y[thin]: "\<And>z. ?A z" (multi) \<Rightarrow> \<open>fail\<close> \<bar> "C y" \<Rightarrow> \<open>-\<close>) (* multi-match must bind something *)
+ apply (match premises in Y[thin]: "\<And>z. ?A z" (multi) \<Rightarrow> fail \<bar> "C y" \<Rightarrow> -) (* multi-match must bind something *)
apply (match premises in Y: "C y" \<Rightarrow> \<open>rule Y\<close>)
done
@@ -117,9 +117,9 @@
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>match (P) in B \<Rightarrow> \<open>fail\<close>
- \<bar> "\<lambda>a. B" \<Rightarrow> \<open>fail\<close>
- \<bar> _ \<Rightarrow> \<open>-\<close>,
+ \<open>match (P) in B \<Rightarrow> fail
+ \<bar> "\<lambda>a. B" \<Rightarrow> fail
+ \<bar> _ \<Rightarrow> -,
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>)
@@ -139,7 +139,7 @@
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 (match asms in Y: "\<And>z a. A (z :: 'a) (a :: 'a) \<and> R" for R \<Rightarrow> fail \<bar> _ \<Rightarrow> -)
apply (rule asms[THEN conjunct1])
done
@@ -188,7 +188,7 @@
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>
- \<open>match H in "A \<and> C" and "A \<and> B" \<Rightarrow> \<open>fail\<close>\<close>
+ \<open>match H in "A \<and> C" and "A \<and> B" \<Rightarrow> fail\<close>
| simp add: X)
@@ -199,10 +199,10 @@
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>
+ \<open>match premises in H'':"\<And>x. A x \<and> B" \<Rightarrow> fail
+ \<bar> _ \<Rightarrow> -\<close>
+ ,match premises in H'':"\<And>x. A x \<and> B" \<Rightarrow> fail \<bar> _ \<Rightarrow> -\<close>)
+ apply (match premises in H:"\<And>x. A x \<and> B" \<Rightarrow> fail
\<bar> H':_ \<Rightarrow> \<open>rule H'[THEN conjunct2]\<close>)
done
@@ -214,7 +214,7 @@
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>
+ match premises (local) in "B \<and> C" \<Rightarrow> fail
\<bar> H:"C \<and> D" \<Rightarrow> \<open>rule H[THEN conjunct1]\<close>\<close>)
end
@@ -233,13 +233,13 @@
lemma
assumes A: "P \<and> Q"
shows "P"
- by ((match A in "P \<and> Q" \<Rightarrow> \<open>fail\<close> \<bar> "?H" \<Rightarrow> \<open>-\<close>) | simp add: A)
+ by ((match A in "P \<and> Q" \<Rightarrow> fail \<bar> "?H" \<Rightarrow> -) | simp add: A)
lemma
assumes A: "D \<and> C" "A \<and> B" "A \<longrightarrow> B"
shows "A"
apply ((match A in U: "P \<and> Q" (cut) and "P' \<longrightarrow> Q'" for P Q P' Q' \<Rightarrow>
- \<open>simp add: U\<close> \<bar> "?H" \<Rightarrow> \<open>-\<close>) | -)
+ \<open>simp add: U\<close> \<bar> "?H" \<Rightarrow> -) | -)
apply (simp add: A)
done
@@ -283,8 +283,8 @@
(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>)
+ \<bar> "True" \<Rightarrow> -
+ \<bar> "PROP ?P" \<Rightarrow> fail)
lemma
assumes asms: "A" "B"
@@ -460,9 +460,9 @@
subsection \<open>Proper context for method parameters\<close>
-method add_simp methods m uses f = (match f in H[simp]:_ \<Rightarrow> \<open>m\<close>)
+method add_simp methods m uses f = (match f in H[simp]:_ \<Rightarrow> m)
-method add_my_thms methods m uses f = (match f in H[my_thms_named]:_ \<Rightarrow> \<open>m\<close>)
+method add_my_thms methods m uses f = (match f in H[my_thms_named]:_ \<Rightarrow> m)
method rule_my_thms = (rule my_thms_named)
method rule_my_thms' declares my_thms_named = (rule my_thms_named)
@@ -472,9 +472,9 @@
shows
"(A \<or> B) \<and> A \<and> A \<and> A"
apply (intro conjI)
- apply (add_simp \<open>add_simp \<open>simp\<close> f: B\<close> f: A)
- apply (add_my_thms \<open>rule_my_thms\<close> f:A)
- apply (add_my_thms \<open>rule_my_thms'\<close> f:A)
+ apply (add_simp \<open>add_simp simp f: B\<close> f: A)
+ apply (add_my_thms rule_my_thms f:A)
+ apply (add_my_thms rule_my_thms' f:A)
apply (add_my_thms \<open>rule my_thms_named\<close> f:A)
done
@@ -483,7 +483,7 @@
method all_args for A B methods m1 m2 uses f1 f2 declares my_thms_named = fail
lemma True
- by (all_args True False \<open>-\<close> \<open>fail\<close> f1: TrueI f2: TrueI my_thms_named: TrueI | rule TrueI)
+ by (all_args True False - fail f1: TrueI f2: TrueI my_thms_named: TrueI | rule TrueI)
subsection \<open>Method name internalization test\<close>
--- a/src/HOL/Eisbach/match_method.ML Tue Dec 22 17:14:35 2015 +0100
+++ b/src/HOL/Eisbach/match_method.ML Tue Dec 22 17:41:46 2015 +0100
@@ -94,9 +94,9 @@
else
let val b = #1 (the opt_dyn)
in error ("Cannot bind fact name in term match" ^ Position.here (pos_of b)) end)) --
- Scan.lift (for_fixes -- (@{keyword "\<Rightarrow>"} |-- Parse.token Parse.cartouche))
- >> (fn ((ctxt, ts), (fixes, cartouche)) =>
- (case Token.get_value cartouche of
+ Scan.lift (for_fixes -- (@{keyword "\<Rightarrow>"} |-- Parse.token Parse.text))
+ >> (fn ((ctxt, ts), (fixes, body)) =>
+ (case Token.get_value body of
SOME (Token.Source src) =>
let
val text = Method_Closure.read ctxt src;
@@ -198,7 +198,7 @@
|> (fn ctxt => fold2 upd_ctxt binds pats ([], ctxt) |> apfst rev)
||> Proof_Context.restore_mode ctxt;
- val (text, src) = Method_Closure.read_closure_input ctxt6 (Token.input_of cartouche);
+ val (text, src) = Method_Closure.read_closure_input ctxt6 (Token.input_of body);
val morphism =
Variable.export_morphism ctxt6
@@ -239,7 +239,7 @@
val binds'' = (binds' ~~ match_args) ~~ pats';
val src' = map (Token.transform morphism) src;
- val _ = Token.assign (SOME (Token.Source src')) cartouche;
+ val _ = Token.assign (SOME (Token.Source src')) body;
in
(binds'', real_fixes', text)
end));
--- a/src/HOL/Eisbach/method_closure.ML Tue Dec 22 17:14:35 2015 +0100
+++ b/src/HOL/Eisbach/method_closure.ML Tue Dec 22 17:41:46 2015 +0100
@@ -90,7 +90,7 @@
val method_text =
- Args.context -- Scan.lift (Parse.token Parse.cartouche) >> (fn (ctxt, tok) =>
+ Args.context -- Scan.lift (Parse.token Parse.text) >> (fn (ctxt, tok) =>
(case Token.get_value tok of
SOME (Token.Source src) => read ctxt src
| _ =>