equal
deleted
inserted
replaced
53 lemma dnat_flat: "ALL x y::dnat. x<<y --> x=UU | x=y" |
53 lemma dnat_flat: "ALL x y::dnat. x<<y --> x=UU | x=y" |
54 apply (rule allI) |
54 apply (rule allI) |
55 apply (induct_tac x rule: dnat.ind) |
55 apply (induct_tac x rule: dnat.ind) |
56 apply fast |
56 apply fast |
57 apply (rule allI) |
57 apply (rule allI) |
58 apply (rule_tac x = y in dnat.casedist) |
58 apply (case_tac y) |
59 apply simp |
59 apply simp |
60 apply simp |
60 apply simp |
61 apply simp |
61 apply simp |
62 apply (rule allI) |
62 apply (rule allI) |
63 apply (rule_tac x = y in dnat.casedist) |
63 apply (case_tac y) |
64 apply (fast intro!: UU_I) |
64 apply (fast intro!: UU_I) |
65 apply (thin_tac "ALL y. dnat << y --> dnat = UU | dnat = y") |
65 apply (thin_tac "ALL y. dnat << y --> dnat = UU | dnat = y") |
66 apply simp |
66 apply simp |
67 apply (simp (no_asm_simp)) |
67 apply (simp (no_asm_simp)) |
68 apply (drule_tac x="dnata" in spec) |
68 apply (drule_tac x="dnata" in spec) |