# HG changeset patch # User paulson # Date 1430404439 -3600 # Node ID 1d218c3e84e2d894972cc57fa47d8221d36c8e2c # Parent 645058aa9d6ff2158cf4478eaa9a6893d822a5d1# Parent ccf9241af2170deb8cae0c63855df98f61fb124a Merge diff -r 645058aa9d6f -r 1d218c3e84e2 src/HOL/List.thy --- a/src/HOL/List.thy Thu Apr 30 15:28:01 2015 +0100 +++ b/src/HOL/List.thy Thu Apr 30 15:33:59 2015 +0100 @@ -539,19 +539,19 @@ fun all_exists_conv cv ctxt ct = (case Thm.term_of ct of - Const (@{const_name HOL.Ex}, _) $ Abs _ => + Const (@{const_name Ex}, _) $ Abs _ => Conv.arg_conv (Conv.abs_conv (all_exists_conv cv o #2) ctxt) ct | _ => cv ctxt ct) fun all_but_last_exists_conv cv ctxt ct = (case Thm.term_of ct of - Const (@{const_name HOL.Ex}, _) $ Abs (_, _, Const (@{const_name HOL.Ex}, _) $ _) => + Const (@{const_name Ex}, _) $ Abs (_, _, Const (@{const_name Ex}, _) $ _) => Conv.arg_conv (Conv.abs_conv (all_but_last_exists_conv cv o #2) 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 + Const (@{const_name Collect}, _) $ Abs _ => Conv.arg_conv (Conv.abs_conv cv ctxt) ct | _ => raise CTERM ("Collect_conv", [ct])) fun rewr_conv' th = Conv.rewr_conv (mk_meta_eq th) @@ -567,18 +567,17 @@ (* term abstraction of list comprehension patterns *) -datatype termlets = If | Case of (typ * int) +datatype termlets = If | Case of typ * int fun simproc ctxt redex = let - val set_Nil_I = @{thm trans} OF [@{thm list.set(1)}, @{thm empty_def}] + val set_Nil_I = @{lemma "set [] = {x. False}" by (simp add: empty_def [symmetric])} 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} - 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 + val del_refl_eq = @{lemma "(t = t \ P) \ P" by simp} + fun mk_set T = Const (@{const_name set}, HOLogic.listT T --> HOLogic.mk_setT T) + fun dest_set (Const (@{const_name set}, _) $ xs) = xs + fun dest_singleton_list (Const (@{const_name Cons}, _) $ t $ (Const (@{const_name 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 *) @@ -586,7 +585,7 @@ let fun check (i, case_t) s = (case strip_abs_body case_t of - (Const (@{const_name List.Nil}, _)) => s + (Const (@{const_name Nil}, _)) => s | _ => (case s of SOME NONE => SOME (SOME i) | _ => NONE)) in fold_index check cases (SOME NONE) |> the_default NONE @@ -624,13 +623,13 @@ CONVERSION (right_hand_set_comprehension_conv (K (HOLogic.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 + rewr_conv' @{lemma "(True \ P) = P" by simp})) 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 (HOLogic.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_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 @@ -657,7 +656,7 @@ 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 + @{lemma "(\x. x = t \ P x) = P t" by simp})) ctxt)) context)))) 1) ctxt 1 THEN tac ctxt cont else Subgoal.FOCUS (fn {prems, context, ...} => @@ -668,14 +667,14 @@ (rewr_conv' (List.last prems))) then_conv (Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) distincts))) Conv.all_conv then_conv - (rewr_conv' @{lemma "(False & P) = False" by simp}))) context then_conv + (rewr_conv' @{lemma "(False \ P) = False" by simp}))) context then_conv HOLogic.Trueprop_conv (HOLogic.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 + @{lemma "(\x. P) = P" by simp})) ctxt)) context))) 1) ctxt 1 THEN rtac set_Nil_I 1)) case_thms) end fun make_inner_eqs bound_vs Tis eqs t = @@ -699,7 +698,7 @@ 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 Type (@{type_name list}, [rT]) = fastype_of1 (map snd bound_vs, t) val pat_eq = (case try dest_singleton_list t of SOME t' => diff -r 645058aa9d6f -r 1d218c3e84e2 src/HOL/Proofs/ex/XML_Data.thy --- a/src/HOL/Proofs/ex/XML_Data.thy Thu Apr 30 15:28:01 2015 +0100 +++ b/src/HOL/Proofs/ex/XML_Data.thy Thu Apr 30 15:33:59 2015 +0100 @@ -57,9 +57,9 @@ text {* Some fairly large proof: *} ML_val {* - val xml = export_proof @{thm Int.times_int.abs_eq}; + val xml = export_proof @{thm abs_less_iff}; val thm = import_proof thy1 xml; - @{assert} (size (YXML.string_of_body xml) > 50000000); + @{assert} (size (YXML.string_of_body xml) > 1000000); *} end