--- 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 \<Rightarrow> '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 \<Rightarrow> 'a sem"
where
--- 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 \<Rightarrow> '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 \<Rightarrow> 'a sem"
where
--- 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 \<Rightarrow> nat option)"
+type_synonym heap = "(nat \<Rightarrow> nat option)"
text{* @{text "Some"} means allocated, @{text "None"} means
free. Address @{text "0"} serves as the null reference. *}
--- 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 \<times> nat"
- edges = "edge list"
+type_synonym nodes = "node list"
+type_synonym edge = "nat \<times> nat"
+type_synonym edges = "edge list"
consts Roots :: "nat set"
--- 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
--- 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 \<times> 'a assn)"
+type_synonym 'a ann_com_op = "('a ann_com) option"
+type_synonym 'a ann_triple_op = "('a ann_com_op \<times> 'a assn)"
primrec com :: "'a ann_triple_op \<Rightarrow> 'a ann_com_op" where
"com (c, q) = c"
--- 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 \<Rightarrow>'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
--- 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 \<times> 'a set \<times> ('a \<times> 'a) set \<times> ('a \<times> 'a) set \<times> 'a set"
+type_synonym 'a par_rgformula =
+ "('a rgformula) list \<times> 'a set \<times> ('a \<times> 'a) set \<times> ('a \<times> 'a) set \<times> 'a set"
inductive
par_rghoare :: "('a rgformula) list \<Rightarrow> 'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set \<Rightarrow> bool"
--- 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) \<times> 'a"
+type_synonym 'a conf = "(('a com) option) \<times> 'a"
inductive_set
etran :: "('a conf \<times> 'a conf) set"
@@ -48,7 +48,7 @@
subsection {* Semantics of Parallel Programs *}
-types 'a par_conf = "('a par_com) \<times> 'a"
+type_synonym 'a par_conf = "('a par_com) \<times> 'a"
inductive_set
par_etran :: "('a par_conf \<times> '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)] \<in> cptn"
| CptnEnv: "(P, t)#xs \<in> cptn \<Longrightarrow> (P,s)#(P,t)#xs \<in> 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)] \<in> par_cptn"
| ParCptnEnv: "(P,t)#xs \<in> par_cptn \<Longrightarrow> (P,s)#(P,t)#xs \<in> par_cptn"
@@ -363,7 +363,8 @@
subsection {* Validity for Component Programs. *}
-types 'a rgformula = "'a com \<times> 'a set \<times> ('a \<times> 'a) set \<times> ('a \<times> 'a) set \<times> 'a set"
+type_synonym 'a rgformula =
+ "'a com \<times> 'a set \<times> ('a \<times> 'a) set \<times> ('a \<times> 'a) set \<times> 'a set"
definition assum :: "('a set \<times> ('a \<times> 'a) set) \<Rightarrow> ('a confs) set" where
"assum \<equiv> \<lambda>(pre, rely). {c. snd(c!0) \<in> pre \<and> (\<forall>i. Suc i<length c \<longrightarrow>
--- 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 \<Rightarrow> val"
- aexp = "state \<Rightarrow> val"
- bexp = "state \<Rightarrow> bool"
+type_synonym val = nat -- "or anything else, @{text nat} used in examples"
+type_synonym state = "loc \<Rightarrow> val"
+type_synonym aexp = "state \<Rightarrow> val"
+type_synonym bexp = "state \<Rightarrow> bool"
-- "arithmetic and boolean expressions are not modelled explicitly here,"
-- "they are just functions on states"
--- 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\<times>state)set"
+type_synonym com_den = "(state \<times> state) set"
definition
Gamma :: "[bexp,com_den] => (com_den => com_den)" where
--- 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
--- 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)
--- 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 \<times> instrs \<times> state"
+type_synonym config = "instrs \<times> instrs \<times> state"
inductive_set
--- 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
--- 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"
--- 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
--- 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
--- 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\<leftarrow>xs]"
-term "[e x y. x\<leftarrow>xs, y\<leftarrow>ys]"
-term "[(x,y,z). x<a, x>b]"
-term "[(x,y,z). x\<leftarrow>xs, x>b]"
-term "[(x,y,z). x<a, x\<leftarrow>xs]"
-term "[(x,y). Cons True x \<leftarrow> xs]"
-term "[(x,y,z). Cons x [] \<leftarrow> xs]"
-term "[(x,y,z). x<a, x>b, x=d]"
-term "[(x,y,z). x<a, x>b, y\<leftarrow>ys]"
-term "[(x,y,z). x<a, x\<leftarrow>xs,y>b]"
-term "[(x,y,z). x<a, x\<leftarrow>xs, y\<leftarrow>ys]"
-term "[(x,y,z). x\<leftarrow>xs, x>b, y<a]"
-term "[(x,y,z). x\<leftarrow>xs, x>b, y\<leftarrow>ys]"
-term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,y>x]"
-term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,z\<leftarrow>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\<leftarrow>xs]" "map (\<lambda>x. (x, y, z)) xs";
+ check "[e x y. x\<leftarrow>xs, y\<leftarrow>ys]" "concat (map (\<lambda>x. map (\<lambda>y. e x y) ys) xs)";
+ check "[(x,y,z). x<a, x>b]" "if x < a then if b < x then [(x, y, z)] else [] else []";
+ check "[(x,y,z). x\<leftarrow>xs, x>b]" "concat (map (\<lambda>x. if b < x then [(x, y, z)] else []) xs)";
+ check "[(x,y,z). x<a, x\<leftarrow>xs]" "if x < a then map (\<lambda>x. (x, y, z)) xs else []";
+ check "[(x,y). Cons True x \<leftarrow> xs]"
+ "concat (map (\<lambda>xa. case xa of [] \<Rightarrow> [] | True # x \<Rightarrow> [(x, y)] | False # x \<Rightarrow> []) xs)";
+ check "[(x,y,z). Cons x [] \<leftarrow> xs]"
+ "concat (map (\<lambda>xa. case xa of [] \<Rightarrow> [] | [x] \<Rightarrow> [(x, y, z)] | x # aa # lista \<Rightarrow> []) xs)";
+ check "[(x,y,z). x<a, x>b, x=d]"
+ "if x < a then if b < x then if x = d then [(x, y, z)] else [] else [] else []";
+ check "[(x,y,z). x<a, x>b, y\<leftarrow>ys]"
+ "if x < a then if b < x then map (\<lambda>y. (x, y, z)) ys else [] else []";
+ check "[(x,y,z). x<a, x\<leftarrow>xs,y>b]"
+ "if x < a then concat (map (\<lambda>x. if b < y then [(x, y, z)] else []) xs) else []";
+ check "[(x,y,z). x<a, x\<leftarrow>xs, y\<leftarrow>ys]"
+ "if x < a then concat (map (\<lambda>x. map (\<lambda>y. (x, y, z)) ys) xs) else []";
+ check "[(x,y,z). x\<leftarrow>xs, x>b, y<a]"
+ "concat (map (\<lambda>x. if b < x then if y < a then [(x, y, z)] else [] else []) xs)";
+ check "[(x,y,z). x\<leftarrow>xs, x>b, y\<leftarrow>ys]"
+ "concat (map (\<lambda>x. if b < x then map (\<lambda>y. (x, y, z)) ys else []) xs)";
+ check "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,y>x]"
+ "concat (map (\<lambda>x. concat (map (\<lambda>y. if x < y then [(x, y, z)] else []) ys)) xs)";
+ check "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,z\<leftarrow>zs]"
+ "concat (map (\<lambda>x. concat (map (\<lambda>y. map (\<lambda>z. (x, y, z)) zs) ys)) xs)"
+ end;
+*}
+
(*
term "[(x,y). x\<leftarrow>xs, let xx = x+x, y\<leftarrow>ys, y \<noteq> xx]"
*)
+
use "Tools/list_to_set_comprehension.ML"
simproc_setup list_to_set_comprehension ("set xs") = {* K List_to_Set_Comprehension.simproc *}
--- 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
--- 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;
--- 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
--- 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 ()))
--- 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; }
--- 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,