summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

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" |