equal
deleted
inserted
replaced
50 and step: "\<And>a b. phi a b \<Longrightarrow> |
50 and step: "\<And>a b. phi a b \<Longrightarrow> |
51 lab a = lab b \<and> |
51 lab a = lab b \<and> |
52 lengthh (sub a) = lengthh (sub b) \<and> |
52 lengthh (sub a) = lengthh (sub b) \<and> |
53 (\<forall>i < lengthh (sub a). phi (nthh (sub a) i) (nthh (sub b) i))" |
53 (\<forall>i < lengthh (sub a). phi (nthh (sub a) i) (nthh (sub b) i))" |
54 shows "x = y" |
54 shows "x = y" |
55 proof (rule mp[OF treeFI.dtor_coinduct, of phi, OF _ *]) |
55 proof (rule mp[OF treeFI.dtor_map_coinduct, of phi, OF _ *]) |
56 fix a b :: "'a treeFI" |
56 fix a b :: "'a treeFI" |
57 let ?zs = "zipp (sub a) (sub b)" |
57 let ?zs = "zipp (sub a) (sub b)" |
58 let ?z = "(lab a, ?zs)" |
58 let ?z = "(lab a, ?zs)" |
59 assume "phi a b" |
59 assume "phi a b" |
60 with step have step': "lab a = lab b" "lengthh (sub a) = lengthh (sub b)" |
60 with step have step': "lab a = lab b" "lengthh (sub a) = lengthh (sub b)" |