# HG changeset patch # User wenzelm # Date 1354041780 -3600 # Node ID 9a65279b5d27c8933675e815ca3371cab751b7d3 # Parent 491c5c81c2e804a7b3067dddce9ea44110729740# Parent 4df875d326ee5d36461684ce7020de0868c20f74 merged diff -r 491c5c81c2e8 -r 9a65279b5d27 src/HOL/Decision_Procs/MIR.thy --- a/src/HOL/Decision_Procs/MIR.thy Tue Nov 27 19:31:11 2012 +0100 +++ b/src/HOL/Decision_Procs/MIR.thy Tue Nov 27 19:43:00 2012 +0100 @@ -5010,7 +5010,7 @@ from alluopairs_set1[where xs="?U"] have UpU: "set ?Up \ (set ?U \ set ?U)" by simp from \_l[OF lq] have U_l: "\ (t,n) \ set ?U. numbound0 t \ n > 0" . from U_l UpU - have Up_: "\ ((t,n),(s,m)) \ set ?Up. numbound0 t \ n> 0 \ numbound0 s \ m > 0" by auto + have "\ ((t,n),(s,m)) \ set ?Up. numbound0 t \ n> 0 \ numbound0 s \ m > 0" by auto hence Snb: "\ (t,n) \ set ?S. numbound0 t \ n > 0 " by (auto simp add: mult_pos_pos) have Y_l: "\ (t,n) \ set ?Y. numbound0 t \ n > 0" diff -r 491c5c81c2e8 -r 9a65279b5d27 src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Tue Nov 27 19:31:11 2012 +0100 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Tue Nov 27 19:43:00 2012 +0100 @@ -996,9 +996,9 @@ thus ?thesis apply- apply(rule that[of q]) unfolding True by auto next case False note p = division_ofD[OF assms(1)] have *:"\k\p. \q. q division_of {a..b} \ k\q" proof case goal1 - guess c using p(4)[OF goal1] .. then guess d .. note cd_ = this - have *:"{c..d} \ {a..b}" "{c..d} \ {}" using p(2,3)[OF goal1, unfolded cd_] using assms(2) by auto - guess q apply(rule partial_division_extend_1[OF *]) . thus ?case unfolding cd_ by auto qed + guess c using p(4)[OF goal1] .. then guess d .. note "cd" = this + have *:"{c..d} \ {a..b}" "{c..d} \ {}" using p(2,3)[OF goal1, unfolded "cd"] using assms(2) by auto + guess q apply(rule partial_division_extend_1[OF *]) . thus ?case unfolding "cd" by auto qed guess q using bchoice[OF *] .. note q = conjunctD2[OF this[rule_format]] have "\x. x\p \ \d. d division_of \(q x - {x})" apply(rule,rule_tac p="q x" in division_of_subset) proof- fix x assume x:"x\p" show "q x division_of \q x" apply-apply(rule division_ofI) diff -r 491c5c81c2e8 -r 9a65279b5d27 src/HOL/Proofs/Lambda/StrongNorm.thy --- a/src/HOL/Proofs/Lambda/StrongNorm.thy Tue Nov 27 19:31:11 2012 +0100 +++ b/src/HOL/Proofs/Lambda/StrongNorm.thy Tue Nov 27 19:43:00 2012 +0100 @@ -102,7 +102,7 @@ assume uIT: "IT u" assume uT: "e \ u : T" { - case (Var rs n e_ T'_ u_ i_) + case (Var rs n e1 T'1 u1 i1) assume nT: "e\i:T\ \ Var n \\ rs : T'" let ?ty = "\t. \T'. e\i:T\ \ t : T'" let ?R = "\t. \e T' u i. @@ -210,13 +210,13 @@ with False show ?thesis by (auto simp add: subst_Var) qed next - case (Lambda r e_ T'_ u_ i_) + case (Lambda r e1 T'1 u1 i1) assume "e\i:T\ \ Abs r : T'" and "\e T' u i. PROP ?Q r e T' u i T" with uIT uT show "IT (Abs r[u/i])" by fastforce next - case (Beta r a as e_ T'_ u_ i_) + case (Beta r a as e1 T'1 u1 i1) assume T: "e\i:T\ \ Abs r \ a \\ as : T'" assume SI1: "\e T' u i. PROP ?Q (r[a/0] \\ as) e T' u i T" assume SI2: "\e T' u i. PROP ?Q a e T' u i T" diff -r 491c5c81c2e8 -r 9a65279b5d27 src/HOL/Proofs/Lambda/WeakNorm.thy --- a/src/HOL/Proofs/Lambda/WeakNorm.thy Tue Nov 27 19:31:11 2012 +0100 +++ b/src/HOL/Proofs/Lambda/WeakNorm.thy Tue Nov 27 19:43:00 2012 +0100 @@ -76,7 +76,7 @@ proof induct fix e T' u i assume uNF: "NF u" and uT: "e \ u : T" { - case (App ts x e_ T'_ u_ i_) + case (App ts x e1 T'1 u1 i1) assume "e\i:T\ \ Var x \\ ts : T'" then obtain Us where varT: "e\i:T\ \ Var x : Us \ T'" @@ -187,7 +187,7 @@ qed qed next - case (Abs r e_ T'_ u_ i_) + case (Abs r e1 T'1 u1 i1) assume absT: "e\i:T\ \ Abs r : T'" then obtain R S where "e\0:R\\Suc i:T\ \ r : S" by (rule abs_typeE) simp moreover have "NF (lift u 0)" using `NF u` by (rule lift_NF) diff -r 491c5c81c2e8 -r 9a65279b5d27 src/Pure/General/symbol.ML --- a/src/Pure/General/symbol.ML Tue Nov 27 19:31:11 2012 +0100 +++ b/src/Pure/General/symbol.ML Tue Nov 27 19:43:00 2012 +0100 @@ -46,6 +46,7 @@ val decode: symbol -> sym datatype kind = Letter | Digit | Quasi | Blank | Other val kind: symbol -> kind + val is_letter_symbol: symbol -> bool val is_letter: symbol -> bool val is_digit: symbol -> bool val is_quasi: symbol -> bool @@ -236,8 +237,6 @@ (* standard symbol kinds *) -datatype kind = Letter | Digit | Quasi | Blank | Other; - local val letter_symbols = Symtab.make_set [ @@ -383,16 +382,22 @@ "\\<^isup>" ]; in - fun kind s = - if is_ascii_letter s then Letter - else if is_ascii_digit s then Digit - else if is_ascii_quasi s then Quasi - else if is_ascii_blank s then Blank - else if is_char s then Other - else if Symtab.defined letter_symbols s then Letter - else Other; + +val is_letter_symbol = Symtab.defined letter_symbols; + end; +datatype kind = Letter | Digit | Quasi | Blank | Other; + +fun kind s = + if is_ascii_letter s then Letter + else if is_ascii_digit s then Digit + else if is_ascii_quasi s then Quasi + else if is_ascii_blank s then Blank + else if is_char s then Other + else if is_letter_symbol s then Letter + else Other; + fun is_letter s = kind s = Letter; fun is_digit s = kind s = Digit; fun is_quasi s = kind s = Quasi; @@ -513,7 +518,8 @@ (* bump string -- treat as base 26 or base 1 numbers *) -fun symbolic_end (_ :: "\\<^isub>" :: _) = true +fun symbolic_end (_ :: "\\<^sub>" :: _) = true + | symbolic_end (_ :: "\\<^isub>" :: _) = true | symbolic_end (_ :: "\\<^isup>" :: _) = true | symbolic_end (s :: _) = is_symbolic s | symbolic_end [] = false; diff -r 491c5c81c2e8 -r 9a65279b5d27 src/Pure/General/symbol_pos.ML --- a/src/Pure/General/symbol_pos.ML Tue Nov 27 19:31:11 2012 +0100 +++ b/src/Pure/General/symbol_pos.ML Tue Nov 27 19:43:00 2012 +0100 @@ -37,8 +37,8 @@ val range: T list -> Position.range val implode_range: Position.T -> Position.T -> T list -> text * Position.range val explode: text * Position.T -> T list + val scan_new_ident: T list -> T list * T list val scan_ident: T list -> T list * T list - val is_ident: T list -> bool val is_identifier: string -> bool end; @@ -214,6 +214,40 @@ (* identifiers *) +local + +val latin = Symbol.is_ascii_letter; +val digit = Symbol.is_ascii_digit; +fun underscore s = s = "_"; +fun prime s = s = "'"; +fun script s = s = "\\<^sub>" orelse s = "\\<^isub>" orelse s = "\\<^isup>"; +fun special_letter s = Symbol.is_letter_symbol s andalso not (script s); + +val scan_plain = Scan.one ((latin orf digit orf prime) o symbol) >> single; +val scan_digit = Scan.one (digit o symbol) >> single; +val scan_prime = Scan.one (prime o symbol) >> single; + +val scan_script = + Scan.one (script o symbol) -- Scan.one ((latin orf digit orf special_letter) o symbol) + >> (fn (x, y) => [x, y]); + +val scan_ident_part1 = + Scan.one (latin o symbol) ::: (Scan.repeat (scan_plain || scan_script) >> flat) || + Scan.one (special_letter o symbol) ::: + (Scan.repeat (scan_digit || scan_prime || scan_script) >> flat); + +val scan_ident_part2 = + Scan.repeat1 (scan_plain || scan_script) >> flat || + scan_ident_part1; + +in + +val scan_new_ident = + scan_ident_part1 @@@ + (Scan.repeat (Scan.many1 (underscore o symbol) @@@ scan_ident_part2) >> flat); + +end; + val scan_ident = Scan.one (Symbol.is_letter o symbol) ::: Scan.many (Symbol.is_letdig o symbol); diff -r 491c5c81c2e8 -r 9a65279b5d27 src/Pure/Syntax/lexicon.ML --- a/src/Pure/Syntax/lexicon.ML Tue Nov 27 19:31:11 2012 +0100 +++ b/src/Pure/Syntax/lexicon.ML Tue Nov 27 19:43:00 2012 +0100 @@ -293,6 +293,7 @@ fun idxname cs ds = (implode (rev cs), nat 0 ds); fun chop_idx [] ds = idxname [] ds + | chop_idx (cs as (_ :: "\\<^sub>" :: _)) ds = idxname cs ds | chop_idx (cs as (_ :: "\\<^isub>" :: _)) ds = idxname cs ds | chop_idx (cs as (_ :: "\\<^isup>" :: _)) ds = idxname cs ds | chop_idx (c :: cs) ds = diff -r 491c5c81c2e8 -r 9a65279b5d27 src/Pure/term.ML --- a/src/Pure/term.ML Tue Nov 27 19:31:11 2012 +0100 +++ b/src/Pure/term.ML Tue Nov 27 19:43:00 2012 +0100 @@ -981,7 +981,8 @@ val idx = string_of_int i; val dot = (case rev (Symbol.explode x) of - _ :: "\\<^isub>" :: _ => false + _ :: "\\<^sub>" :: _ => false + | _ :: "\\<^isub>" :: _ => false | _ :: "\\<^isup>" :: _ => false | c :: _ => Symbol.is_digit c | _ => true);