src/HOL/Library/Transitive_Closure_Table.thy
changeset 35423 6ef9525a5727
parent 34912 c04747153bcf
child 36176 3fe7e97ccca8
equal deleted inserted replaced
35422:e74b6f3b950c 35423:6ef9525a5727
   105       by iprover
   105       by iprover
   106     show ?thesis
   106     show ?thesis
   107     proof (cases as)
   107     proof (cases as)
   108       case Nil
   108       case Nil
   109       with xxs have x: "x = a" and xs: "xs = bs @ a # cs"
   109       with xxs have x: "x = a" and xs: "xs = bs @ a # cs"
   110 	by auto
   110         by auto
   111       from x xs `rtrancl_path r x xs y` have cs: "rtrancl_path r x cs y"
   111       from x xs `rtrancl_path r x xs y` have cs: "rtrancl_path r x cs y"
   112 	by (auto elim: rtrancl_path_appendE)
   112         by (auto elim: rtrancl_path_appendE)
   113       from xs have "length cs < length xs" by simp
   113       from xs have "length cs < length xs" by simp
   114       then show ?thesis
   114       then show ?thesis
   115 	by (rule less(1)) (iprover intro: cs less(2))+
   115         by (rule less(1)) (iprover intro: cs less(2))+
   116     next
   116     next
   117       case (Cons d ds)
   117       case (Cons d ds)
   118       with xxs have xs: "xs = ds @ a # (bs @ [a] @ cs)"
   118       with xxs have xs: "xs = ds @ a # (bs @ [a] @ cs)"
   119 	by auto
   119         by auto
   120       with `rtrancl_path r x xs y` obtain xa: "rtrancl_path r x (ds @ [a]) a"
   120       with `rtrancl_path r x xs y` obtain xa: "rtrancl_path r x (ds @ [a]) a"
   121         and ay: "rtrancl_path r a (bs @ a # cs) y"
   121         and ay: "rtrancl_path r a (bs @ a # cs) y"
   122 	by (auto elim: rtrancl_path_appendE)
   122         by (auto elim: rtrancl_path_appendE)
   123       from ay have "rtrancl_path r a cs y" by (auto elim: rtrancl_path_appendE)
   123       from ay have "rtrancl_path r a cs y" by (auto elim: rtrancl_path_appendE)
   124       with xa have xy: "rtrancl_path r x ((ds @ [a]) @ cs) y"
   124       with xa have xy: "rtrancl_path r x ((ds @ [a]) @ cs) y"
   125 	by (rule rtrancl_path_trans)
   125         by (rule rtrancl_path_trans)
   126       from xs have "length ((ds @ [a]) @ cs) < length xs" by simp
   126       from xs have "length ((ds @ [a]) @ cs) < length xs" by simp
   127       then show ?thesis
   127       then show ?thesis
   128 	by (rule less(1)) (iprover intro: xy less(2))+
   128         by (rule less(1)) (iprover intro: xy less(2))+
   129     qed
   129     qed
   130   qed
   130   qed
   131 qed
   131 qed
   132 
   132 
   133 inductive rtrancl_tab :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
   133 inductive rtrancl_tab :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"