equal
deleted
inserted
replaced
99 lemma Nat_atleast_set_locs [rule_format, simp]: |
99 lemma Nat_atleast_set_locs [rule_format, simp]: |
100 "\<forall>s v. set_locs l s:v \<ge> n = (s:v \<ge> n)" |
100 "\<forall>s v. set_locs l s:v \<ge> n = (s:v \<ge> n)" |
101 apply (induct n) |
101 apply (induct n) |
102 by auto |
102 by auto |
103 |
103 |
104 lemma Nat_atleast_reset_locs [rule_format, simp]: |
104 lemma Nat_atleast_del_locs [rule_format, simp]: |
105 "\<forall>s v. reset_locs s:v \<ge> n = (s:v \<ge> n)" |
105 "\<forall>s v. del_locs s:v \<ge> n = (s:v \<ge> n)" |
106 apply (induct n) |
106 apply (induct n) |
107 by auto |
107 by auto |
108 |
108 |
109 lemma Nat_atleast_NullD [rule_format]: "s:Null \<ge> n \<longrightarrow> False" |
109 lemma Nat_atleast_NullD [rule_format]: "s:Null \<ge> n \<longrightarrow> False" |
110 apply (induct n) |
110 apply (induct n) |