strengthen lemma
authorAndreas Lochbihler
Tue Dec 01 12:27:16 2015 +0100 (2015-12-01)
changeset 61764ac6e5de1a50b
parent 61759 49353865e539
child 61765 13ca8f4f6907
strengthen lemma
src/HOL/Library/Transitive_Closure_Table.thy
     1.1 --- a/src/HOL/Library/Transitive_Closure_Table.thy	Mon Nov 30 19:12:08 2015 +0100
     1.2 +++ b/src/HOL/Library/Transitive_Closure_Table.thy	Tue Dec 01 12:27:16 2015 +0100
     1.3 @@ -93,14 +93,14 @@
     1.4  
     1.5  lemma rtrancl_path_distinct:
     1.6    assumes xy: "rtrancl_path r x xs y"
     1.7 -  obtains xs' where "rtrancl_path r x xs' y" and "distinct (x # xs')"
     1.8 +  obtains xs' where "rtrancl_path r x xs' y" and "distinct (x # xs')" and "set xs' \<subseteq> set xs"
     1.9    using xy
    1.10  proof (induct xs rule: measure_induct_rule [of length])
    1.11    case (less xs)
    1.12    show ?case
    1.13    proof (cases "distinct (x # xs)")
    1.14      case True
    1.15 -    with \<open>rtrancl_path r x xs y\<close> show ?thesis by (rule less)
    1.16 +    with \<open>rtrancl_path r x xs y\<close> show ?thesis by (rule less) simp
    1.17    next
    1.18      case False
    1.19      then have "\<exists>as bs cs a. x # xs = as @ [a] @ bs @ [a] @ cs"
    1.20 @@ -112,11 +112,11 @@
    1.21        case Nil
    1.22        with xxs have x: "x = a" and xs: "xs = bs @ a # cs"
    1.23          by auto
    1.24 -      from x xs \<open>rtrancl_path r x xs y\<close> have cs: "rtrancl_path r x cs y"
    1.25 +      from x xs \<open>rtrancl_path r x xs y\<close> have cs: "rtrancl_path r x cs y" "set cs \<subseteq> set xs"
    1.26          by (auto elim: rtrancl_path_appendE)
    1.27        from xs have "length cs < length xs" by simp
    1.28        then show ?thesis
    1.29 -        by (rule less(1)) (iprover intro: cs less(2))+
    1.30 +        by (rule less(1))(blast intro: cs less(2) order_trans del: subsetI)+
    1.31      next
    1.32        case (Cons d ds)
    1.33        with xxs have xs: "xs = ds @ a # (bs @ [a] @ cs)"
    1.34 @@ -127,9 +127,10 @@
    1.35        from ay have "rtrancl_path r a cs y" by (auto elim: rtrancl_path_appendE)
    1.36        with xa have xy: "rtrancl_path r x ((ds @ [a]) @ cs) y"
    1.37          by (rule rtrancl_path_trans)
    1.38 +      from xs have set: "set ((ds @ [a]) @ cs) \<subseteq> set xs" by auto
    1.39        from xs have "length ((ds @ [a]) @ cs) < length xs" by simp
    1.40        then show ?thesis
    1.41 -        by (rule less(1)) (iprover intro: xy less(2))+
    1.42 +        by (rule less(1))(blast intro: xy less(2) set[THEN subsetD])+
    1.43      qed
    1.44    qed
    1.45  qed