src/HOL/Library/Transitive_Closure_Table.thy
 changeset 35423 6ef9525a5727 parent 34912 c04747153bcf child 36176 3fe7e97ccca8
equal 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"`