From: matitaweb Date: Thu, 8 Mar 2012 07:43:23 +0000 (+0000) Subject: commit by user ricciott X-Git-Tag: make_still_working~1872 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a95a1f6ca434470d5ba385557ab3de392fbbccc0;p=helm.git commit by user ricciott --- diff --git a/weblib/cr/lambda.ma b/weblib/cr/lambda.ma index 493f63304..f368613c7 100644 --- a/weblib/cr/lambda.ma +++ b/weblib/cr/lambda.ma @@ -661,6 +661,30 @@ definition body ≝ λx,M.match M with [ Abs M0 ⇒ a href="cic:/matita/cr/lambda/vopen.fix(0,0,2)"vopen/a M (xa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]) a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a | _ ⇒ M ]. +inductive dupfree (A:Type[0]) : a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A → Prop ≝ +| df_nil : dupfree A a title="nil" href="cic:/fakeuri.def(1)"[/a] +| df_cons : ∀x,xl.x a title="list not member" href="cic:/fakeuri.def(1)"∉/a xl → dupfree A xl → dupfree A (xa title="cons" href="cic:/fakeuri.def(1)":/a:xl). + +record df_list (A:Type[0]) : Type[0] ≝ { + list_of_dfl :> a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A; + dfl_dupfree : a href="cic:/matita/cr/lambda/dupfree.ind(1,0,1)"dupfree/a A list_of_dfl +}. + +(* ciascuno dei pre_tm utilizzati nella costruzione deve essere un ext_tm 0 *) +inductive tm : a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"pre_tm/a → Prop ≝ +| tm_Par : ∀xl:a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"df_list/a a href="cic:/matita/cr/lambda/X.dec"X/a.∀x.x a title="list member" href="cic:/fakeuri.def(1)"∈/a xl → tm (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a xl (a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"Par/a x)) +| tm_App : ∀xl:a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"df_list/a a href="cic:/matita/cr/lambda/X.dec"X/a.∀M1,M2:a href="cic:/matita/cr/lambda/ext_tm.ind(1,0,1)"ext_tm/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a.tm (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a xl M1) → tm (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a xl M2) → tm (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a xl (a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"App/a M1 M2)) +| tm_Lam : ∀xl:a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"df_list/a a href="cic:/matita/cr/lambda/X.dec"X/a.∀x.∀M:a href="cic:/matita/cr/lambda/ext_tm.ind(1,0,1)"ext_tm/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a.x a title="list not member" href="cic:/fakeuri.def(1)"∉/a xl → tm (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a (xa title="cons" href="cic:/fakeuri.def(1)":/a:xl) M) → tm (a href="cic:/matita/cr/lambda/Judg.def(5)"Judg/a xl (a href="cic:/matita/cr/lambda/Lam.def(5)"Lam/a x M)). + + +inductive tm2 : pre_tm → Prop ≝ +| tm2_Par : ∀xl:df_list X.∀x.x ∈ xl → tm2 (Judg xl (Par x)) +| tm2_App : ∀xl:df_list X.∀M1,M2.tm2 (Judg xl M1) → tm2 (Judg xl M2) → tm2 (Judg xl (App M1 M2)) +| tm2_Lam : ∀xl:df_list X.∀M,C.(∀x.x ∉ xl@C → tm2 (Judg (x::xl) (body x M))) → tm2 (Judg xl (Abs M)). + + + + inductive L (F:X → S_exp → Y) : S_exp → Prop \def | LPar : ∀x:X.L F (Par x) | LApp : ∀M,N:S_exp. (L F M) → (L F N) → L F (App M N)