isahipster: 8ea06bbb50ecce681b2ad9da4545e279b4ce023c
1: theory MediumL
2: imports "../Listing"
3: "../Naturals"
4: (*"../Nat-prfs/ProofN"*)
5: (*BasicL*)
6: begin
7:
8: (** FIXME: = or \<noteq> will fail with our current tactic: no induction associated? different rule?
9: Cfr: we only have rules that induct on lists (except for the result type)
10: Should we start considering more rules not present in the conjecture? **)
11: lemma count01: "\<not> (eqN r t) \<Longrightarrow> count r (app ts (Cons t Nil)) = count r ts"
12: by hipster_induct_schemes (*
13: apply(induction ts)
14: apply(simp_all)
15: apply(induction rule: eqN.induct)
16: apply(simp_all)
17: done*)
18: lemma idNat : "eqN x x"
19: by hipster_induct_simp_metis
20:
21: lemma count02: "count t ts = n \<Longrightarrow> count t (Cons t ts) = S n"
22: (* apply(case_tac ts) (* OR: induciton ts on its own *)
23: by (simp_all add: identityNat) (*XXX: how come the simplifier cannot get itself to the conclusion eqN v v? *)
24: *)
25: by (hipster_induct_simp_metis idNat) (* requires ProofN: eqN x x *)
26:
27: lemma count03: "count t ts = n \<Longrightarrow> count t (app rs ts) = add (count t rs) n"
28: by (hipster_induct_simp_metis)
29:
30: lemma elem01: "elem t ts \<Longrightarrow> elem t (Cons r ts)"
31: by (metis elem.simps)
32: (* apply(induction ts) by (simp_all) *)
33: (*by (hipster_induct_simp_metis)*)
34:
35: lemma elem02: "elem t ts \<Longrightarrow> elem t (app ts rs)"
36: (* apply(induction ts) by (simp_all) *)
37: by (hipster_induct_simp_metis)
38:
39: lemma elem03: "elem t ts \<Longrightarrow> elem t (app rs ts)"
40: (* apply(induction rs) apply(simp_all) *)
41: by (hipster_induct_simp_metis)
42:
43: lemma inRev: "elem t ts \<Longrightarrow> elem t (rev ts)"
44: (*apply(induction ts) apply(simp_all) by (metis elem.simps(2) elem02 elem03)*)
45: by (hipster_induct_simp_metis elem02 elem03 elem.simps(2))
46:
47: lemma lastAfterCons: "ts \<noteq> Nil \<Longrightarrow> last ts = last (Cons t ts)"
48: by (metis List.exhaust Listing.last.simps(2))
49: (*by (hipster_induct_simp_metis)*)
50:
51: lemma lastElemIsLast: "last (app ts (Cons t Nil)) = t"
52: by (hipster_induct_schemes) (*
53: apply(induction ts rule: last.induct)
54: by (simp_all)
55: OR:
56: apply (induction ts rule: last.induct)
57: by (tactic {* Ind_Schemes_Tacs.routine_tac @{context} *}) *)
58:
59: lemma firstLast: "ts \<noteq> Nil \<Longrightarrow> head ts = last (rev ts)"
60: (* apply(induction ts) by (simp_all add: lastElemIsLast) *)
61: by (hipster_induct_simp_metis lastElemIsLast)
62: (* apply (induction ts rule: rev.induct)
63: apply(simp_all)
64: apply (induction ts rule: head.induct)
65: apply simp_all
66: XXX: strangely enough this brings the same subgoal twice... and does not get simplified *)
67:
68:
69: lemma addId[]: "add m Z = m"
70: by hipster_induct_simp_metis
71:
72: lemma addS2[]: "add n (S m) = S (add n m)"
73: by hipster_induct_simp_metis
74:
75: lemma setCountRev: "count t ts = count t (rev ts)"
76: by (hipster_induct_schemes count.simps rev.simps count03 addId addS2)
77: (* TODO: Ill-typed instantiation::: check types before inducting with a rule that does not correspond
78: HOWEVER: we cannot know in some cases immediately... XXX: how to extract which var's a rule inducts over? *)
79: (*apply(induction ts arbitrary: t) (* XXX: no need for rule: rev.induct ! *)
80: apply (simp_all) (* for some reason still won't do with hipster and these lemmas *)
81: apply(metis count.simps count03 addId addS2)*)
82:
83: lemma lenTake: "leq n (len ts) \<Longrightarrow> len (take n ts) = n" (* XXX: same as previous *)
84: by hipster_induct_schemes (*
85: apply(induction ts rule: take.induct)
86: apply(simp_all)
87: done*)
88:
89: lemma len0: "Z = len ts \<Longrightarrow> ts = Nil"
90: (* by (metis Nat.distinct(1) len.elims) However, we do not add Nat.distinct(1) *)
91: by (hipster_induct_simp_metis)
92:
93: declare [[show_types]]
94: declare [[show_sorts]]
95: declare [[show_consts]]
96:
97: lemma notLen0: "leq (S n) (len ts) \<Longrightarrow> ts \<noteq> Nil" (* FIXME: loops in Hipster \<Longrightarrow> timeout on simp too? *)
98: by (metis len.simps(1) leq.simps(2)) (* XXX: maybe we do not add .simps rules to routine tacs? *)
99: (* by hipster_induct_simp_metis
100: apply(induction ts)
101: by (simp_all)*)
102:
103: (* XXX: maybe start with innermost? *)
104: (* XXX2: Shall we add simps for conditions always? *)
105: lemma notEmptyDrop: "leq (S n) (len ts) \<Longrightarrow> (drop n ts) \<noteq> Nil"
106: by (hipster_induct_schemes leq.simps len.simps) (*
107: apply(induction ts rule: drop.induct) (* XXX: same as previous; NOTE: loops in struct-ind attempt *)
108: by (simp_all add: notLen0) *) (* notLen0 necessary! *)
109: lemma noLowerZ: "leq n Z \<Longrightarrow> n = Z" (* will fail with the rule stated *)
110: by hipster_induct_simp_metis (* tactic {* Tactic_Data.routine_tac @{context}*}) if lemma_az is in thy_expl*)
111:
112: lemma emptyDrop: "leq (len ts) n \<Longrightarrow> drop n ts = Nil"
113: by (hipster_induct_schemes noLowerZ len0 leq.simps len.simps) (* :S
114: apply(induction ts rule: drop.induct)
115: apply(simp_all)
116: apply(frule noLowerZ) (* XXX: why frule's is not done also by the simplifier? *)
117: by (simp_all add: len0)*)
118:
119: (* TODO: strategy: start with tailing call? nah, didn't matter: both take.induct and drop.induct get us there *)
120: lemma dropTake : "ts = app (take n ts) (drop n ts)" (* XXX: ill-instantiation again... *)
121: apply(induction ts)
122: apply(metis Nat.exhaust list.exhaust take.simps app.simps drop.simps) oops
123: (*apply(metis (full_types) Nat.exhaust list.exhaust take.simps app.simps drop.simps)
124: done
125: by hipster_induct_schemes*) (*
126: apply(induction ts rule: take.induct)
127: apply(case_tac n)
128: apply(simp_all)
129: (** conditional **)
130: done*)
131:
132: lemma dropNil: "drop n Nil = Nil" (* from BasicL *)
133: (*by (metis drop.simps Nat.exhaust)*)
134: by hipster_induct_simp_metis
135:
136: lemma auxLastDrop : "drop n ts \<noteq> Nil \<Longrightarrow> last (drop n ts) = last ts" (* XXX: needs schemes *)
137: by (hipster_induct_schemes lastAfterCons dropNil)
138:
139: lemma lastDrop : "leq (S n) (len ts) \<Longrightarrow> last (drop n ts) = last ts"
140: by (metis notEmptyDrop auxLastDrop)
141: (* by (hipster_induct_schemes notEmptyDrop lastAfterCons dropNil) *)
142: (* OR: instead of lastAfterCons, dropNil \<Rightarrow> auxLastDrop *)
143:
144: lemma takeMore: "leq (len ts) n \<Longrightarrow> take n ts = ts"
145: by (hipster_induct_schemes emptyDrop drop.simps) (*
146: apply(induction ts rule: take.induct)
147: apply(simp_all)
148: by (metis drop.simps emptyDrop) *)
149: (* by (hipster_induct_simp_metis appNil emptyDrop dropTake)
150: apply(induction ts rule: take.induct)
151: apply(simp_all)
152: apply(drule emptyDrop)
153: by (simp_all) *)
154:
155: lemma headTake: "lt Z n \<Longrightarrow> head (take n ts) = head ts" (* No ts \<noteq> Nil ... *)
156: by hipster_induct_schemes
157:
158: (*
159: lemma subId: "sub n Z = n" (* from ProofN *)
160: (* apply(hipster_induct_schemes add.simps) *)
161: by hipster_induct_simp_metis*)
162:
163: (* XXX: make sure we include helping lemmas \<Longrightarrow> they avoid errors + infinite running! (ill-instantiations... none) *)
164: lemma initAsTake: "init ts = take (sub (len ts) (S Z)) ts"
165: by (hipster_induct_schemes sub.simps Nat.exhaust) (*
166: apply(induction ts rule: init.induct)
167: apply simp_all
168: by (metis Nat.exhaust sub.simps)
169: apply(induction ts rule: init.induct)
170: by (simp_all add: subId) (* from ProofN *) *)
171:
172:
173: lemma zipNil: "rs = Nil \<Longrightarrow> zip rs ts = Nil" (* "\<not> notNil rs *) (* does not require condition "format" *)
174: by (tactic {* Simp_T.routine_tac @{context} *})
175: (*by (hipster_induct_simp_metis)*)
176:
177: (* XXX: we should do something about our conclusions in the induction? type of the Nil has a
178: _SCHEMATIC TYPE_ variable... *)
179: lemma zip2nil: "zip ts Nil = Nil"
180: by hipster_induct_simp_metis
181: (* by (metis Listing.zip.simps Listing.List.exhaust)*)
182:
183: lemma zipNilBis: "\<not> notNil ts \<Longrightarrow> zip rs ts = Nil"
184: by hipster_induct_schemes (* here: usage of notNil requires the induction? *)
185:
186: lemma zipNotNil: "notNil rs \<Longrightarrow> zip (Cons t ts) rs = Cons (t, head rs) (zip ts (tail rs))"
187: by hipster_induct_simp_metis (*
188: apply(case_tac rs)
189: apply(simp_all)
190: done*)
191:
192: lemma zipSingleton: "zip (Cons t Nil) (Cons r Nil) = Cons (t,r) Nil"
193: by simp
194:
195: (* XXX: if the condition is dropped, simplification alone (our Simp_Tacs.routine_tac) suffices, of course
196: But if induction is taken, the method cannot be applied and it fails...
197: Notably, if we have a condition and still use Nil instead of ts, we don't get "type unification"
198: for both Nil's despite the type of rev, apparently - or so it seems - *)
199: lemma revNil: "ts = Nil \<Longrightarrow> rev ts = Nil"
200: by hipster_induct_simp_metis
201:
202:
203:
204:
205: (*hipster rotate*)
206:
207: (*hipster rotate len*)
208:
209: value "(3,4)"
210: datatype 'a bitup = Bt 'a 'a
211: (*
212: datatype 'a ptree = Leaf 'a | Node "(('a bitup) ptree)"
213: datatype 'a nest = NilN | ConsN "('a \<times> ('a bitup) nest)"
214: datatype 'a bush = Ro | Bu "(('a bush) bush)"*)
215:
216: (*hipster rotate app*)
217:
218: thm rotate.induct
219: lemma rotSelf : "rotate n (app xs xs) = app (rotate n xs) (rotate n xs)"
220: apply(induction xs rule: rotate.induct)
221: apply(simp_all)
222: apply(case_tac n)
223: apply auto
224: oops
225:
226: end
227:
228:
Generated by git2html.