# HG changeset patch # User bulwahn # Date 1301552883 -7200 # Node ID 5cb4a2f4f2a40fa15598a2f58c2138996b3778bf # Parent c7b6d8d9922edfcf9eaf0cade9f0af5569895ba9# Parent d0be2722ce9f360a582df76003bc084268f056e0 merged diff -r c7b6d8d9922e -r 5cb4a2f4f2a4 src/HOL/Hoare/Hoare_Logic.thy --- a/src/HOL/Hoare/Hoare_Logic.thy Wed Mar 30 19:09:57 2011 +0200 +++ b/src/HOL/Hoare/Hoare_Logic.thy Thu Mar 31 08:28:03 2011 +0200 @@ -13,9 +13,8 @@ uses ("hoare_syntax.ML") ("hoare_tac.ML") begin -types - 'a bexp = "'a set" - 'a assn = "'a set" +type_synonym 'a bexp = "'a set" +type_synonym 'a assn = "'a set" datatype 'a com = Basic "'a \ 'a" @@ -25,7 +24,7 @@ abbreviation annskip ("SKIP") where "SKIP == Basic id" -types 'a sem = "'a => 'a => bool" +type_synonym 'a sem = "'a => 'a => bool" inductive Sem :: "'a com \ 'a sem" where diff -r c7b6d8d9922e -r 5cb4a2f4f2a4 src/HOL/Hoare/Hoare_Logic_Abort.thy --- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Wed Mar 30 19:09:57 2011 +0200 +++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Thu Mar 31 08:28:03 2011 +0200 @@ -10,9 +10,8 @@ uses ("hoare_syntax.ML") ("hoare_tac.ML") begin -types - 'a bexp = "'a set" - 'a assn = "'a set" +type_synonym 'a bexp = "'a set" +type_synonym 'a assn = "'a set" datatype 'a com = Basic "'a \ 'a" @@ -23,7 +22,7 @@ abbreviation annskip ("SKIP") where "SKIP == Basic id" -types 'a sem = "'a option => 'a option => bool" +type_synonym 'a sem = "'a option => 'a option => bool" inductive Sem :: "'a com \ 'a sem" where diff -r c7b6d8d9922e -r 5cb4a2f4f2a4 src/HOL/Hoare/SepLogHeap.thy --- a/src/HOL/Hoare/SepLogHeap.thy Wed Mar 30 19:09:57 2011 +0200 +++ b/src/HOL/Hoare/SepLogHeap.thy Thu Mar 31 08:28:03 2011 +0200 @@ -10,7 +10,7 @@ imports Main begin -types heap = "(nat \ nat option)" +type_synonym heap = "(nat \ nat option)" text{* @{text "Some"} means allocated, @{text "None"} means free. Address @{text "0"} serves as the null reference. *} diff -r c7b6d8d9922e -r 5cb4a2f4f2a4 src/HOL/Hoare_Parallel/Graph.thy --- a/src/HOL/Hoare_Parallel/Graph.thy Wed Mar 30 19:09:57 2011 +0200 +++ b/src/HOL/Hoare_Parallel/Graph.thy Thu Mar 31 08:28:03 2011 +0200 @@ -6,10 +6,9 @@ datatype node = Black | White -types - nodes = "node list" - edge = "nat \ nat" - edges = "edge list" +type_synonym nodes = "node list" +type_synonym edge = "nat \ nat" +type_synonym edges = "edge list" consts Roots :: "nat set" diff -r c7b6d8d9922e -r 5cb4a2f4f2a4 src/HOL/Hoare_Parallel/OG_Com.thy --- a/src/HOL/Hoare_Parallel/OG_Com.thy Wed Mar 30 19:09:57 2011 +0200 +++ b/src/HOL/Hoare_Parallel/OG_Com.thy Thu Mar 31 08:28:03 2011 +0200 @@ -7,9 +7,8 @@ text {* Type abbreviations for boolean expressions and assertions: *} -types - 'a bexp = "'a set" - 'a assn = "'a set" +type_synonym 'a bexp = "'a set" +type_synonym 'a assn = "'a set" text {* The syntax of commands is defined by two mutually recursive datatypes: @{text "'a ann_com"} for annotated commands and @{text "'a diff -r c7b6d8d9922e -r 5cb4a2f4f2a4 src/HOL/Hoare_Parallel/OG_Tran.thy --- a/src/HOL/Hoare_Parallel/OG_Tran.thy Wed Mar 30 19:09:57 2011 +0200 +++ b/src/HOL/Hoare_Parallel/OG_Tran.thy Thu Mar 31 08:28:03 2011 +0200 @@ -3,9 +3,8 @@ theory OG_Tran imports OG_Com begin -types - 'a ann_com_op = "('a ann_com) option" - 'a ann_triple_op = "('a ann_com_op \ 'a assn)" +type_synonym 'a ann_com_op = "('a ann_com) option" +type_synonym 'a ann_triple_op = "('a ann_com_op \ 'a assn)" primrec com :: "'a ann_triple_op \ 'a ann_com_op" where "com (c, q) = c" diff -r c7b6d8d9922e -r 5cb4a2f4f2a4 src/HOL/Hoare_Parallel/RG_Com.thy --- a/src/HOL/Hoare_Parallel/RG_Com.thy Wed Mar 30 19:09:57 2011 +0200 +++ b/src/HOL/Hoare_Parallel/RG_Com.thy Thu Mar 31 08:28:03 2011 +0200 @@ -10,8 +10,7 @@ of states. Syntax of commands @{text com} and parallel commands @{text par_com}. *} -types - 'a bexp = "'a set" +type_synonym 'a bexp = "'a set" datatype 'a com = Basic "'a \'a" @@ -20,6 +19,6 @@ | While "'a bexp" "'a com" | Await "'a bexp" "'a com" -types 'a par_com = "(('a com) option) list" +type_synonym 'a par_com = "'a com option list" end \ No newline at end of file diff -r c7b6d8d9922e -r 5cb4a2f4f2a4 src/HOL/Hoare_Parallel/RG_Hoare.thy --- a/src/HOL/Hoare_Parallel/RG_Hoare.thy Wed Mar 30 19:09:57 2011 +0200 +++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy Thu Mar 31 08:28:03 2011 +0200 @@ -55,7 +55,8 @@ subsection {* Proof System for Parallel Programs *} -types 'a par_rgformula = "('a rgformula) list \ 'a set \ ('a \ 'a) set \ ('a \ 'a) set \ 'a set" +type_synonym 'a par_rgformula = + "('a rgformula) list \ 'a set \ ('a \ 'a) set \ ('a \ 'a) set \ 'a set" inductive par_rghoare :: "('a rgformula) list \ 'a set \ ('a \ 'a) set \ ('a \ 'a) set \ 'a set \ bool" diff -r c7b6d8d9922e -r 5cb4a2f4f2a4 src/HOL/Hoare_Parallel/RG_Tran.thy --- a/src/HOL/Hoare_Parallel/RG_Tran.thy Wed Mar 30 19:09:57 2011 +0200 +++ b/src/HOL/Hoare_Parallel/RG_Tran.thy Thu Mar 31 08:28:03 2011 +0200 @@ -8,7 +8,7 @@ subsubsection {* Environment transitions *} -types 'a conf = "(('a com) option) \ 'a" +type_synonym 'a conf = "(('a com) option) \ 'a" inductive_set etran :: "('a conf \ 'a conf) set" @@ -48,7 +48,7 @@ subsection {* Semantics of Parallel Programs *} -types 'a par_conf = "('a par_com) \ 'a" +type_synonym 'a par_conf = "('a par_com) \ 'a" inductive_set par_etran :: "('a par_conf \ 'a par_conf) set" @@ -73,9 +73,9 @@ subsubsection {* Sequential computations *} -types 'a confs = "('a conf) list" +type_synonym 'a confs = "'a conf list" -inductive_set cptn :: "('a confs) set" +inductive_set cptn :: "'a confs set" where CptnOne: "[(P,s)] \ cptn" | CptnEnv: "(P, t)#xs \ cptn \ (P,s)#(P,t)#xs \ cptn" @@ -86,9 +86,9 @@ subsubsection {* Parallel computations *} -types 'a par_confs = "('a par_conf) list" +type_synonym 'a par_confs = "'a par_conf list" -inductive_set par_cptn :: "('a par_confs) set" +inductive_set par_cptn :: "'a par_confs set" where ParCptnOne: "[(P,s)] \ par_cptn" | ParCptnEnv: "(P,t)#xs \ par_cptn \ (P,s)#(P,t)#xs \ par_cptn" @@ -363,7 +363,8 @@ subsection {* Validity for Component Programs. *} -types 'a rgformula = "'a com \ 'a set \ ('a \ 'a) set \ ('a \ 'a) set \ 'a set" +type_synonym 'a rgformula = + "'a com \ 'a set \ ('a \ 'a) set \ ('a \ 'a) set \ 'a set" definition assum :: "('a set \ ('a \ 'a) set) \ ('a confs) set" where "assum \ \(pre, rely). {c. snd(c!0) \ pre \ (\i. Suc i diff -r c7b6d8d9922e -r 5cb4a2f4f2a4 src/HOL/IMP/Com.thy --- a/src/HOL/IMP/Com.thy Wed Mar 30 19:09:57 2011 +0200 +++ b/src/HOL/IMP/Com.thy Thu Mar 31 08:28:03 2011 +0200 @@ -11,11 +11,10 @@ -- "an unspecified (arbitrary) type of locations (adresses/names) for variables" -types - val = nat -- "or anything else, @{text nat} used in examples" - state = "loc \ val" - aexp = "state \ val" - bexp = "state \ bool" +type_synonym val = nat -- "or anything else, @{text nat} used in examples" +type_synonym state = "loc \ val" +type_synonym aexp = "state \ val" +type_synonym bexp = "state \ bool" -- "arithmetic and boolean expressions are not modelled explicitly here," -- "they are just functions on states" diff -r c7b6d8d9922e -r 5cb4a2f4f2a4 src/HOL/IMP/Denotation.thy --- a/src/HOL/IMP/Denotation.thy Wed Mar 30 19:09:57 2011 +0200 +++ b/src/HOL/IMP/Denotation.thy Thu Mar 31 08:28:03 2011 +0200 @@ -6,7 +6,7 @@ theory Denotation imports Natural begin -types com_den = "(state\state)set" +type_synonym com_den = "(state \ state) set" definition Gamma :: "[bexp,com_den] => (com_den => com_den)" where diff -r c7b6d8d9922e -r 5cb4a2f4f2a4 src/HOL/IMP/Expr.thy --- a/src/HOL/IMP/Expr.thy Wed Mar 30 19:09:57 2011 +0200 +++ b/src/HOL/IMP/Expr.thy Thu Mar 31 08:28:03 2011 +0200 @@ -14,8 +14,7 @@ subsection "Arithmetic expressions" typedecl loc -types - state = "loc => nat" +type_synonym state = "loc => nat" datatype aexp = N nat diff -r c7b6d8d9922e -r 5cb4a2f4f2a4 src/HOL/IMP/Hoare.thy --- a/src/HOL/IMP/Hoare.thy Wed Mar 30 19:09:57 2011 +0200 +++ b/src/HOL/IMP/Hoare.thy Thu Mar 31 08:28:03 2011 +0200 @@ -6,7 +6,7 @@ theory Hoare imports Natural begin -types assn = "state => bool" +type_synonym assn = "state => bool" inductive hoare :: "assn => com => assn => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50) diff -r c7b6d8d9922e -r 5cb4a2f4f2a4 src/HOL/IMP/Machines.thy --- a/src/HOL/IMP/Machines.thy Wed Mar 30 19:09:57 2011 +0200 +++ b/src/HOL/IMP/Machines.thy Thu Mar 31 08:28:03 2011 +0200 @@ -14,7 +14,7 @@ text {* There are only three instructions: *} datatype instr = SET loc aexp | JMPF bexp nat | JMPB nat -types instrs = "instr list" +type_synonym instrs = "instr list" subsection "M0 with PC" @@ -47,7 +47,7 @@ an operational (small step) semantics: *} -types config = "instrs \ instrs \ state" +type_synonym config = "instrs \ instrs \ state" inductive_set diff -r c7b6d8d9922e -r 5cb4a2f4f2a4 src/HOL/IMPP/Com.thy --- a/src/HOL/IMPP/Com.thy Wed Mar 30 19:09:57 2011 +0200 +++ b/src/HOL/IMPP/Com.thy Thu Mar 31 08:28:03 2011 +0200 @@ -8,8 +8,9 @@ imports Main begin -types val = nat (* for the meta theory, this may be anything, but with - current Isabelle, types cannot be refined later *) +type_synonym val = nat + (* for the meta theory, this may be anything, but types cannot be refined later *) + typedecl glb typedecl loc @@ -18,15 +19,15 @@ Res :: loc datatype vname = Glb glb | Loc loc -types globs = "glb => val" - locals = "loc => val" +type_synonym globs = "glb => val" +type_synonym locals = "loc => val" datatype state = st globs locals (* for the meta theory, the following would be sufficient: typedecl state consts st :: "[globs , locals] => state" *) -types aexp = "state => val" - bexp = "state => bool" +type_synonym aexp = "state => val" +type_synonym bexp = "state => bool" typedecl pname diff -r c7b6d8d9922e -r 5cb4a2f4f2a4 src/HOL/IMPP/Hoare.thy --- a/src/HOL/IMPP/Hoare.thy Wed Mar 30 19:09:57 2011 +0200 +++ b/src/HOL/IMPP/Hoare.thy Thu Mar 31 08:28:03 2011 +0200 @@ -16,7 +16,7 @@ vs. simultaneous recursion in call rule *} -types 'a assn = "'a => state => bool" +type_synonym 'a assn = "'a => state => bool" translations (type) "'a assn" <= (type) "'a => state => bool" diff -r c7b6d8d9922e -r 5cb4a2f4f2a4 src/HOL/IOA/Asig.thy --- a/src/HOL/IOA/Asig.thy Wed Mar 30 19:09:57 2011 +0200 +++ b/src/HOL/IOA/Asig.thy Thu Mar 31 08:28:03 2011 +0200 @@ -9,7 +9,7 @@ imports Main begin -types +type_synonym 'a signature = "('a set * 'a set * 'a set)" consts diff -r c7b6d8d9922e -r 5cb4a2f4f2a4 src/HOL/IOA/IOA.thy --- a/src/HOL/IOA/IOA.thy Wed Mar 30 19:09:57 2011 +0200 +++ b/src/HOL/IOA/IOA.thy Thu Mar 31 08:28:03 2011 +0200 @@ -9,12 +9,11 @@ imports Asig begin -types - 'a seq = "nat => 'a" - 'a oseq = "nat => 'a option" - ('a,'b)execution = "'a oseq * 'b seq" - ('a,'s)transition = "('s * 'a * 's)" - ('a,'s)ioa = "'a signature * 's set * ('a,'s)transition set" +type_synonym 'a seq = "nat => 'a" +type_synonym 'a oseq = "nat => 'a option" +type_synonym ('a, 'b) execution = "'a oseq * 'b seq" +type_synonym ('a, 's) transition = "('s * 'a * 's)" +type_synonym ('a,'s) ioa = "'a signature * 's set * ('a, 's) transition set" consts diff -r c7b6d8d9922e -r 5cb4a2f4f2a4 src/HOL/List.thy --- a/src/HOL/List.thy Wed Mar 30 19:09:57 2011 +0200 +++ b/src/HOL/List.thy Thu Mar 31 08:28:03 2011 +0200 @@ -426,26 +426,45 @@ in [(@{syntax_const "_listcompr"}, lc_tr)] end *} -term "[(x,y,z). b]" -term "[(x,y,z). x\xs]" -term "[e x y. x\xs, y\ys]" -term "[(x,y,z). xb]" -term "[(x,y,z). x\xs, x>b]" -term "[(x,y,z). xxs]" -term "[(x,y). Cons True x \ xs]" -term "[(x,y,z). Cons x [] \ xs]" -term "[(x,y,z). xb, x=d]" -term "[(x,y,z). xb, y\ys]" -term "[(x,y,z). xxs,y>b]" -term "[(x,y,z). xxs, y\ys]" -term "[(x,y,z). x\xs, x>b, yxs, x>b, y\ys]" -term "[(x,y,z). x\xs, y\ys,y>x]" -term "[(x,y,z). x\xs, y\ys,z\zs]" +ML {* + let + val read = Syntax.read_term @{context}; + fun check s1 s2 = read s1 aconv read s2 orelse error ("Check failed: " ^ quote s1); + in + check "[(x,y,z). b]" "if b then [(x, y, z)] else []"; + check "[(x,y,z). x\xs]" "map (\x. (x, y, z)) xs"; + check "[e x y. x\xs, y\ys]" "concat (map (\x. map (\y. e x y) ys) xs)"; + check "[(x,y,z). xb]" "if x < a then if b < x then [(x, y, z)] else [] else []"; + check "[(x,y,z). x\xs, x>b]" "concat (map (\x. if b < x then [(x, y, z)] else []) xs)"; + check "[(x,y,z). xxs]" "if x < a then map (\x. (x, y, z)) xs else []"; + check "[(x,y). Cons True x \ xs]" + "concat (map (\xa. case xa of [] \ [] | True # x \ [(x, y)] | False # x \ []) xs)"; + check "[(x,y,z). Cons x [] \ xs]" + "concat (map (\xa. case xa of [] \ [] | [x] \ [(x, y, z)] | x # aa # lista \ []) xs)"; + check "[(x,y,z). xb, x=d]" + "if x < a then if b < x then if x = d then [(x, y, z)] else [] else [] else []"; + check "[(x,y,z). xb, y\ys]" + "if x < a then if b < x then map (\y. (x, y, z)) ys else [] else []"; + check "[(x,y,z). xxs,y>b]" + "if x < a then concat (map (\x. if b < y then [(x, y, z)] else []) xs) else []"; + check "[(x,y,z). xxs, y\ys]" + "if x < a then concat (map (\x. map (\y. (x, y, z)) ys) xs) else []"; + check "[(x,y,z). x\xs, x>b, yx. if b < x then if y < a then [(x, y, z)] else [] else []) xs)"; + check "[(x,y,z). x\xs, x>b, y\ys]" + "concat (map (\x. if b < x then map (\y. (x, y, z)) ys else []) xs)"; + check "[(x,y,z). x\xs, y\ys,y>x]" + "concat (map (\x. concat (map (\y. if x < y then [(x, y, z)] else []) ys)) xs)"; + check "[(x,y,z). x\xs, y\ys,z\zs]" + "concat (map (\x. concat (map (\y. map (\z. (x, y, z)) zs) ys)) xs)" + end; +*} + (* term "[(x,y). x\xs, let xx = x+x, y\ys, y \ xx]" *) + use "Tools/list_to_set_comprehension.ML" simproc_setup list_to_set_comprehension ("set xs") = {* K List_to_Set_Comprehension.simproc *} diff -r c7b6d8d9922e -r 5cb4a2f4f2a4 src/HOL/Tools/list_to_set_comprehension.ML --- a/src/HOL/Tools/list_to_set_comprehension.ML Wed Mar 30 19:09:57 2011 +0200 +++ b/src/HOL/Tools/list_to_set_comprehension.ML Thu Mar 31 08:28:03 2011 +0200 @@ -8,7 +8,7 @@ signature LIST_TO_SET_COMPREHENSION = sig val simproc : simpset -> cterm -> thm option -end; +end structure List_to_Set_Comprehension : LIST_TO_SET_COMPREHENSION = struct @@ -16,66 +16,69 @@ (* conversion *) fun all_exists_conv cv ctxt ct = - case Thm.term_of ct of - Const(@{const_name HOL.Ex}, _) $ Abs(_, _, _) => + (case Thm.term_of ct of + Const (@{const_name HOL.Ex}, _) $ Abs _ => Conv.arg_conv (Conv.abs_conv (all_exists_conv cv o #2) ctxt) ct - | _ => cv ctxt ct + | _ => cv ctxt ct) fun all_but_last_exists_conv cv ctxt ct = - case Thm.term_of ct of + (case Thm.term_of ct of Const (@{const_name HOL.Ex}, _) $ Abs (_, _, Const (@{const_name HOL.Ex}, _) $ _) => Conv.arg_conv (Conv.abs_conv (all_but_last_exists_conv cv o #2) ctxt) ct - | _ => cv ctxt ct + | _ => cv ctxt ct) fun Collect_conv cv ctxt ct = (case Thm.term_of ct of Const (@{const_name Set.Collect}, _) $ Abs _ => Conv.arg_conv (Conv.abs_conv cv ctxt) ct - | _ => raise CTERM ("Collect_conv", [ct])); + | _ => raise CTERM ("Collect_conv", [ct])) fun Trueprop_conv cv ct = (case Thm.term_of ct of Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct - | _ => raise CTERM ("Trueprop_conv", [ct])); + | _ => raise CTERM ("Trueprop_conv", [ct])) fun eq_conv cv1 cv2 ct = (case Thm.term_of ct of Const (@{const_name HOL.eq}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct - | _ => raise CTERM ("eq_conv", [ct])); + | _ => raise CTERM ("eq_conv", [ct])) fun conj_conv cv1 cv2 ct = (case Thm.term_of ct of Const (@{const_name HOL.conj}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct - | _ => raise CTERM ("conj_conv", [ct])); + | _ => raise CTERM ("conj_conv", [ct])) fun rewr_conv' th = Conv.rewr_conv (mk_meta_eq th) - -fun conjunct_assoc_conv ct = Conv.try_conv - ((rewr_conv' @{thm conj_assoc}) then_conv conj_conv Conv.all_conv conjunct_assoc_conv) ct - -fun right_hand_set_comprehension_conv conv ctxt = Trueprop_conv (eq_conv Conv.all_conv - (Collect_conv (all_exists_conv conv o #2) ctxt)) + +fun conjunct_assoc_conv ct = + Conv.try_conv + (rewr_conv' @{thm conj_assoc} then_conv conj_conv Conv.all_conv conjunct_assoc_conv) ct + +fun right_hand_set_comprehension_conv conv ctxt = + Trueprop_conv (eq_conv Conv.all_conv + (Collect_conv (all_exists_conv conv o #2) ctxt)) + (* term abstraction of list comprehension patterns *) - + datatype termlets = If | Case of (typ * int) fun simproc ss redex = let val ctxt = Simplifier.the_context ss - val thy = ProofContext.theory_of ctxt + val thy = ProofContext.theory_of ctxt val set_Nil_I = @{thm trans} OF [@{thm set.simps(1)}, @{thm empty_def}] val set_singleton = @{lemma "set [a] = {x. x = a}" by simp} val inst_Collect_mem_eq = @{lemma "set A = {x. x : set A}" by simp} - val del_refl_eq = @{lemma "(t = t & P) == P" by simp} + val del_refl_eq = @{lemma "(t = t & P) == P" by simp} fun mk_set T = Const (@{const_name List.set}, HOLogic.listT T --> HOLogic.mk_setT T) fun dest_set (Const (@{const_name List.set}, _) $ xs) = xs fun dest_singleton_list (Const (@{const_name List.Cons}, _) - $ t $ (Const (@{const_name List.Nil}, _))) = t + $ t $ (Const (@{const_name List.Nil}, _))) = t | dest_singleton_list t = raise TERM ("dest_singleton_list", [t]) (* We check that one case returns a singleton list and all other cases - return [], and return the index of the one singleton list case *) + return [], and return the index of the one singleton list case *) fun possible_index_of_singleton_case cases = - let + let fun check (i, case_t) s = (case strip_abs_body case_t of (Const (@{const_name List.Nil}, _)) => s @@ -88,112 +91,132 @@ let val (case_const, args) = strip_comb case_term in - case try dest_Const case_const of - SOME (c, T) => (case Datatype_Data.info_of_case thy c of - SOME _ => (case possible_index_of_singleton_case (fst (split_last args)) of - SOME i => - let - val (Ts, _) = strip_type T - val T' = List.last Ts - in SOME (List.last args, T', i, nth args i) end + (case try dest_Const case_const of + SOME (c, T) => + (case Datatype_Data.info_of_case thy c of + SOME _ => + (case possible_index_of_singleton_case (fst (split_last args)) of + SOME i => + let + val (Ts, _) = strip_type T + val T' = List.last Ts + in SOME (List.last args, T', i, nth args i) end + | NONE => NONE) | NONE => NONE) - | NONE => NONE) - | NONE => NONE + | NONE => NONE) end (* returns condition continuing term option *) fun dest_if (Const (@{const_name If}, _) $ cond $ then_t $ Const (@{const_name Nil}, _)) = - SOME (cond, then_t) + SOME (cond, then_t) | dest_if _ = NONE - fun tac _ [] = - rtac set_singleton 1 ORELSE rtac inst_Collect_mem_eq 1 - | tac ctxt (If :: cont) = - Splitter.split_tac [@{thm split_if}] 1 - THEN rtac @{thm conjI} 1 - THEN rtac @{thm impI} 1 - THEN Subgoal.FOCUS (fn {prems, context, ...} => - CONVERSION (right_hand_set_comprehension_conv (K - (conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_TrueI})) Conv.all_conv - then_conv rewr_conv' @{thm simp_thms(22)})) context) 1) ctxt 1 - THEN tac ctxt cont - THEN rtac @{thm impI} 1 - THEN Subgoal.FOCUS (fn {prems, context, ...} => - CONVERSION (right_hand_set_comprehension_conv (K - (conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_FalseI})) Conv.all_conv - then_conv rewr_conv' @{thm simp_thms(24)})) context) 1) ctxt 1 - THEN rtac set_Nil_I 1 - | tac ctxt (Case (T, i) :: cont) = - let - val info = Datatype.the_info thy (fst (dest_Type T)) - in - (* do case distinction *) - Splitter.split_tac [#split info] 1 - THEN EVERY (map_index (fn (i', case_rewrite) => - (if i' < length (#case_rewrites info) - 1 then rtac @{thm conjI} 1 else all_tac) - THEN REPEAT_DETERM (rtac @{thm allI} 1) + fun tac _ [] = rtac set_singleton 1 ORELSE rtac inst_Collect_mem_eq 1 + | tac ctxt (If :: cont) = + Splitter.split_tac [@{thm split_if}] 1 + THEN rtac @{thm conjI} 1 + THEN rtac @{thm impI} 1 + THEN Subgoal.FOCUS (fn {prems, context, ...} => + CONVERSION (right_hand_set_comprehension_conv (K + (conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_TrueI})) Conv.all_conv + then_conv + rewr_conv' @{lemma "(True & P) = P" by simp})) context) 1) ctxt 1 + THEN tac ctxt cont THEN rtac @{thm impI} 1 - THEN (if i' = i then - (* continue recursively *) - Subgoal.FOCUS (fn {prems, context, ...} => - CONVERSION (Thm.eta_conversion then_conv right_hand_set_comprehension_conv (K - ((conj_conv - (eq_conv Conv.all_conv (rewr_conv' (List.last prems)) - then_conv (Conv.try_conv (Conv.rewrs_conv (map mk_meta_eq (#inject info))))) Conv.all_conv) - then_conv (Conv.try_conv (Conv.rewr_conv del_refl_eq)) - then_conv conjunct_assoc_conv)) context - then_conv (Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) => - Conv.repeat_conv (all_but_last_exists_conv (K (rewr_conv' @{thm simp_thms(39)})) ctxt)) context)))) 1) ctxt 1 - THEN tac ctxt cont - else - Subgoal.FOCUS (fn {prems, context, ...} => - CONVERSION ((right_hand_set_comprehension_conv (K - (conj_conv - ((eq_conv Conv.all_conv - (rewr_conv' (List.last prems))) - then_conv (Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) (#distinct info)))) Conv.all_conv - then_conv (rewr_conv' @{thm simp_thms(24)}))) context) - then_conv (Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) => - Conv.repeat_conv (Conv.bottom_conv (K (rewr_conv' @{thm simp_thms(36)})) ctxt)) context)))) 1) ctxt 1 - THEN rtac set_Nil_I 1)) (#case_rewrites info)) - end + THEN Subgoal.FOCUS (fn {prems, context, ...} => + CONVERSION (right_hand_set_comprehension_conv (K + (conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_FalseI})) Conv.all_conv + then_conv rewr_conv' @{lemma "(False & P) = False" by simp})) context) 1) ctxt 1 + THEN rtac set_Nil_I 1 + | tac ctxt (Case (T, i) :: cont) = + let + val info = Datatype.the_info thy (fst (dest_Type T)) + in + (* do case distinction *) + Splitter.split_tac [#split info] 1 + THEN EVERY (map_index (fn (i', case_rewrite) => + (if i' < length (#case_rewrites info) - 1 then rtac @{thm conjI} 1 else all_tac) + THEN REPEAT_DETERM (rtac @{thm allI} 1) + THEN rtac @{thm impI} 1 + THEN (if i' = i then + (* continue recursively *) + Subgoal.FOCUS (fn {prems, context, ...} => + CONVERSION (Thm.eta_conversion then_conv right_hand_set_comprehension_conv (K + ((conj_conv + (eq_conv Conv.all_conv (rewr_conv' (List.last prems)) then_conv + (Conv.try_conv (Conv.rewrs_conv (map mk_meta_eq (#inject info))))) + Conv.all_conv) + then_conv (Conv.try_conv (Conv.rewr_conv del_refl_eq)) + then_conv conjunct_assoc_conv)) context + then_conv (Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) => + Conv.repeat_conv + (all_but_last_exists_conv + (K (rewr_conv' + @{lemma "(EX x. x = t & P x) = P t" by simp})) ctxt)) context)))) 1) ctxt 1 + THEN tac ctxt cont + else + Subgoal.FOCUS (fn {prems, context, ...} => + CONVERSION + (right_hand_set_comprehension_conv (K + (conj_conv + ((eq_conv Conv.all_conv + (rewr_conv' (List.last prems))) then_conv + (Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) (#distinct info)))) + Conv.all_conv then_conv + (rewr_conv' @{lemma "(False & P) = False" by simp}))) context then_conv + Trueprop_conv + (eq_conv Conv.all_conv + (Collect_conv (fn (_, ctxt) => + Conv.repeat_conv + (Conv.bottom_conv + (K (rewr_conv' + @{lemma "(EX x. P) = P" by simp})) ctxt)) context))) 1) ctxt 1 + THEN rtac set_Nil_I 1)) (#case_rewrites info)) + end fun make_inner_eqs bound_vs Tis eqs t = - case dest_case t of + (case dest_case t of SOME (x, T, i, cont) => let val (vs, body) = strip_abs (Pattern.eta_long (map snd bound_vs) cont) val x' = incr_boundvars (length vs) x val eqs' = map (incr_boundvars (length vs)) eqs val (constr_name, _) = nth (the (Datatype_Data.get_constrs thy (fst (dest_Type T)))) i - val constr_t = list_comb (Const (constr_name, map snd vs ---> T), map Bound (((length vs) - 1) downto 0)) + val constr_t = + list_comb + (Const (constr_name, map snd vs ---> T), map Bound (((length vs) - 1) downto 0)) val constr_eq = Const (@{const_name HOL.eq}, T --> T --> @{typ bool}) $ constr_t $ x' in make_inner_eqs (rev vs @ bound_vs) (Case (T, i) :: Tis) (constr_eq :: eqs') body end | NONE => - case dest_if t of - SOME (condition, cont) => make_inner_eqs bound_vs (If :: Tis) (condition :: eqs) cont - | NONE => - if eqs = [] then NONE (* no rewriting, nothing to be done *) - else - let - val Type (@{type_name List.list}, [rT]) = fastype_of1 (map snd bound_vs, t) - val pat_eq = - case try dest_singleton_list t of - SOME t' => Const (@{const_name HOL.eq}, rT --> rT --> @{typ bool}) - $ Bound (length bound_vs) $ t' - | NONE => Const (@{const_name Set.member}, rT --> HOLogic.mk_setT rT --> @{typ bool}) - $ Bound (length bound_vs) $ (mk_set rT $ t) - val reverse_bounds = curry subst_bounds - ((map Bound ((length bound_vs - 1) downto 0)) @ [Bound (length bound_vs)]) - val eqs' = map reverse_bounds eqs - val pat_eq' = reverse_bounds pat_eq - val inner_t = fold (fn (v, T) => fn t => HOLogic.exists_const T $ absdummy (T, t)) - (rev bound_vs) (fold (curry HOLogic.mk_conj) eqs' pat_eq') - val lhs = term_of redex - val rhs = HOLogic.mk_Collect ("x", rT, inner_t) - val rewrite_rule_t = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) - in - SOME ((Goal.prove ctxt [] [] rewrite_rule_t (fn {context, ...} => tac context (rev Tis))) RS @{thm eq_reflection}) - end + (case dest_if t of + SOME (condition, cont) => make_inner_eqs bound_vs (If :: Tis) (condition :: eqs) cont + | NONE => + if eqs = [] then NONE (* no rewriting, nothing to be done *) + else + let + val Type (@{type_name List.list}, [rT]) = fastype_of1 (map snd bound_vs, t) + val pat_eq = + (case try dest_singleton_list t of + SOME t' => + Const (@{const_name HOL.eq}, rT --> rT --> @{typ bool}) $ + Bound (length bound_vs) $ t' + | NONE => + Const (@{const_name Set.member}, rT --> HOLogic.mk_setT rT --> @{typ bool}) $ + Bound (length bound_vs) $ (mk_set rT $ t)) + val reverse_bounds = curry subst_bounds + ((map Bound ((length bound_vs - 1) downto 0)) @ [Bound (length bound_vs)]) + val eqs' = map reverse_bounds eqs + val pat_eq' = reverse_bounds pat_eq + val inner_t = + fold (fn (v, T) => fn t => HOLogic.exists_const T $ absdummy (T, t)) + (rev bound_vs) (fold (curry HOLogic.mk_conj) eqs' pat_eq') + val lhs = term_of redex + val rhs = HOLogic.mk_Collect ("x", rT, inner_t) + val rewrite_rule_t = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) + in + SOME + ((Goal.prove ctxt [] [] rewrite_rule_t + (fn {context, ...} => tac context (rev Tis))) RS @{thm eq_reflection}) + end)) in make_inner_eqs [] [] [] (dest_set (term_of redex)) end diff -r c7b6d8d9922e -r 5cb4a2f4f2a4 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Wed Mar 30 19:09:57 2011 +0200 +++ b/src/Pure/Isar/proof_context.ML Thu Mar 31 08:28:03 2011 +0200 @@ -670,9 +670,11 @@ get_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt false a))) handle ERROR _ => (false, Consts.intern (consts_of ctxt) a)), get_free = intern_skolem ctxt (Variable.def_type ctxt false), - markup_const = Name_Space.markup_entry (const_space ctxt), - markup_free = fn x => Markup.name x Markup.free, - markup_var = fn xi => Markup.name (Term.string_of_vname xi) Markup.var}; + markup_const = fn x => [Name_Space.markup_entry (const_space ctxt) x], + markup_free = fn x => + [if can Name.dest_skolem x then Markup.skolem else Markup.free] @ + (if not (Variable.is_body ctxt) orelse Variable.is_fixed ctxt x then [] else [Markup.hilite]), + markup_var = fn xi => [Markup.name (Term.string_of_vname xi) Markup.var]}; val decode_term = Syntax.decode_term o term_context; diff -r c7b6d8d9922e -r 5cb4a2f4f2a4 src/Pure/Syntax/type_ext.ML --- a/src/Pure/Syntax/type_ext.ML Wed Mar 30 19:09:57 2011 +0200 +++ b/src/Pure/Syntax/type_ext.ML Thu Mar 31 08:28:03 2011 +0200 @@ -130,15 +130,15 @@ (* decode_term -- transform parse tree into raw term *) fun markup_bound def id = - Markup.properties [(if def then Markup.defN else Markup.refN, id)] Markup.bound; + [Markup.properties [(if def then Markup.defN else Markup.refN, id)] Markup.bound]; type term_context = {get_sort: (indexname * sort) list -> indexname -> sort, get_const: string -> bool * string, get_free: string -> string option, - markup_const: string -> Markup.T, - markup_free: string -> Markup.T, - markup_var: indexname -> Markup.T}; + markup_const: string -> Markup.T list, + markup_free: string -> Markup.T list, + markup_var: indexname -> Markup.T list}; fun decode_term (term_context: term_context) tm = let @@ -148,8 +148,8 @@ val reports = Unsynchronized.ref ([]: (Position.T * Markup.T) list); fun report [] _ _ = () | report ps markup x = - let val m = markup x - in Unsynchronized.change reports (fold (fn p => cons (p, m)) ps) end; + let val ms = markup x + in Unsynchronized.change reports (fold (fn p => fold (fn m => cons (p, m)) ms) ps) end; fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) = (case decode_position typ of diff -r c7b6d8d9922e -r 5cb4a2f4f2a4 src/Pure/System/session.ML --- a/src/Pure/System/session.ML Wed Mar 30 19:09:57 2011 +0200 +++ b/src/Pure/System/session.ML Thu Mar 31 08:28:03 2011 +0200 @@ -103,10 +103,13 @@ let val start = Timing.start (); val _ = use root; + val timing = Timing.result start; + val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing) + |> Real.fmt (StringCvt.FIX (SOME 2)); val _ = Output.raw_stderr ("Timing " ^ item ^ " (" ^ string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^ - Timing.message (Timing.result start) ^ ")\n"); + Timing.message timing ^ ", factor " ^ factor ^ ")\n"); in () end else use root; finish ())) diff -r c7b6d8d9922e -r 5cb4a2f4f2a4 src/Tools/jEdit/dist-template/etc/isabelle-jedit.css --- a/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css Wed Mar 30 19:09:57 2011 +0200 +++ b/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css Thu Mar 31 08:28:03 2011 +0200 @@ -9,7 +9,7 @@ .report { display: none; } -.hilite { background-color: #FFFACD; } +.hilite { background-color: #FFCC66; } .keyword { font-weight: bold; color: #009966; } .operator { font-weight: bold; } diff -r c7b6d8d9922e -r 5cb4a2f4f2a4 src/Tools/jEdit/src/jedit/isabelle_markup.scala --- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala Wed Mar 30 19:09:57 2011 +0200 +++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala Thu Mar 31 08:28:03 2011 +0200 @@ -26,6 +26,7 @@ val warning_color = new Color(255, 140, 0) val error_color = new Color(178, 34, 34) val bad_color = new Color(255, 106, 106, 100) + val hilite_color = new Color(255, 204, 102, 100) class Icon(val priority: Int, val icon: javax.swing.Icon) { @@ -100,6 +101,7 @@ val background1: Markup_Tree.Select[Color] = { case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color + case Text.Info(_, XML.Elem(Markup(Markup.HILITE, _), _)) => hilite_color } val background2: Markup_Tree.Select[Color] = @@ -154,7 +156,7 @@ Markup.TFREE -> NULL, Markup.FREE -> MARKUP, Markup.TVAR -> NULL, - Markup.SKOLEM -> NULL, + Markup.SKOLEM -> COMMENT2, Markup.BOUND -> LABEL, Markup.VAR -> NULL, Markup.NUM -> DIGIT,