src/HOL/List.thy
changeset 69215 ab94035ba6ea
parent 69203 a5c0d61ce5db
child 69275 9bbd5497befd
equal deleted inserted replaced
69214:74455459973d 69215:ab94035ba6ea
   917         val neq_len = HOLogic.mk_Trueprop (HOLogic.Not $ eq_len);
   917         val neq_len = HOLogic.mk_Trueprop (HOLogic.Not $ eq_len);
   918         val thm = Goal.prove ctxt [] [] neq_len
   918         val thm = Goal.prove ctxt [] [] neq_len
   919           (K (simp_tac (put_simpset ss ctxt) 1));
   919           (K (simp_tac (put_simpset ss ctxt) 1));
   920       in SOME (thm RS @{thm neq_if_length_neq}) end
   920       in SOME (thm RS @{thm neq_if_length_neq}) end
   921   in
   921   in
   922     if m < n andalso submultiset (aconv) (ls,rs) orelse
   922     if m < n andalso submultiset (op aconv) (ls,rs) orelse
   923        n < m andalso submultiset (aconv) (rs,ls)
   923        n < m andalso submultiset (op aconv) (rs,ls)
   924     then prove_neq() else NONE
   924     then prove_neq() else NONE
   925   end;
   925   end;
   926 in K list_neq end;
   926 in K list_neq end
   927 \<close>
   927 \<close>
   928 
   928 
   929 
   929 
   930 subsubsection \<open>\<open>@\<close> -- append\<close>
   930 subsubsection \<open>\<open>@\<close> -- append\<close>
   931 
   931 
  1072       in
  1072       in
  1073         if list1 lastl andalso list1 lastr then rearr @{thm append1_eq_conv}
  1073         if list1 lastl andalso list1 lastr then rearr @{thm append1_eq_conv}
  1074         else if lastl aconv lastr then rearr @{thm append_same_eq}
  1074         else if lastl aconv lastr then rearr @{thm append_same_eq}
  1075         else NONE
  1075         else NONE
  1076       end;
  1076       end;
  1077   in fn _ => fn ctxt => fn ct => list_eq ctxt (Thm.term_of ct) end;
  1077   in fn _ => fn ctxt => fn ct => list_eq ctxt (Thm.term_of ct) end
  1078 \<close>
  1078 \<close>
  1079 
  1079 
  1080 
  1080 
  1081 subsubsection \<open>@{const map}\<close>
  1081 subsubsection \<open>@{const map}\<close>
  1082 
  1082