theory PileInd imports Main begin typedecl P typedecl A consts empty :: P consts push :: "A \ P \ P" inductive FP :: "P \ bool" where FPe : "FP empty" | Fpp : "FP p \ FP (push a p)" inductive L :: "P \ nat \ bool" where Lem : "L empty 0" | Lpu : "L p n \ L (push a p) (1+n)" lemma "\ p n. (L p n \ FP p)" apply (rule allI) apply (rule allI) apply (rule impI) apply (erule L.induct) apply (rule FPe) apply (rule Fpp) apply (assumption) done lemma "\ p. FP p \ (\ n. L p n)" apply (rule allI) apply (rule impI) apply (erule FP.induct) apply (rule exI) apply (rule Lem) apply (erule exE) apply (rule exI) apply (erule Lpu) done lemma "(\ p. L p 0 \ p=empty)" apply (rule allI) apply (rule impI) apply (subst (asm) L.simps) apply (erule disjE) apply (erule conjE) apply (assumption) apply (erule exE) apply (erule exE) apply (erule exE) apply (erule conjE) apply (erule conjE) apply (subst (asm) One_nat_def) apply (subst (asm) plus_nat.add_Suc) apply (subst (asm) Zero_not_Suc) apply (erule FalseE) done (* using [[simp_trace] apply (simp) *) (* non prouvable, pourquoi ? *) lemma "(\ p n. L p (1+n) \ p \ empty)" sorry lemma "\ p n. L p (1+n) \ (\ a q. p = push a q)" (* à compléter *) sorry end