From cd1ea2cc540bf000db797a497314028ce0fda0fa Mon Sep 17 00:00:00 2001 From: matitaweb Date: Wed, 16 Nov 2011 12:37:49 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter4.ma | 24 +++++++++++++++++------- 1 file changed, 17 insertions(+), 7 deletions(-) diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma index 272465561..76065b6db 100644 --- a/weblib/tutorial/chapter4.ma +++ b/weblib/tutorial/chapter4.ma @@ -178,16 +178,26 @@ lemma if_epsilon_true : ∀S.∀e:a href="cic:/matita/tutorial/chapter4/pre.def #S * #pi #b * [normalize #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/] cases b normalize // @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a qed. -definition lor ≝ λS:Alpha.λa,b:pre S.〈\fst a + \fst b,\snd a ∨ \snd b〉. +definition lor ≝ λS:a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"Alpha/a.λa,b:a href="cic:/matita/tutorial/chapter4/pre.def(1)"pre/a S.a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a a a title="por" href="cic:/fakeuri.def(1)"+/a a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a b,a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a a a title="boolean or" href="cic:/fakeuri.def(1)"∨/a a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a b〉. notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}. -interpretation "oplus" 'oplus a b = (lo ? a b). +interpretation "oplus" 'oplus a b = (lor ? a b). -ndefinition lc ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λa,b:pre S. - match a with [ mk_pair e1 b1 ⇒ - match b1 with - [ false ⇒ 〈e1 · \fst b, \snd b〉 - | true ⇒ 〈e1 · \fst (bcast ? (\fst b)),\snd b || \snd (bcast ? (\fst b))〉]]. +definition item_concat: ∀S:a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"Alpha/a.a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"pitem/a S → a href="cic:/matita/tutorial/chapter4/pre.def(1)"pre/a S → a href="cic:/matita/tutorial/chapter4/pre.def(1)"pre/a S ≝ + λS,i,e.a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai a title="pcat" href="cic:/fakeuri.def(1)"·/a a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e, a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a e〉. + +definition lcat: ∀S:Alpha.∀bcast:(∀S:Alpha.pre S →pre S).pre S → pre S → pre S + ≝ λS:Alpha.λbcast:∀S:Alpha.pre S → pre S.λe1,e2:pre S. + match e1 with [ mk_pair i1 b1 ⇒ e2]. + + match e1 with [ _ => e1]. + + match b1 with + [ false ⇒ e2 | _ => e1 ]]. + + | true ⇒ item_concat S i1 (bcast S e2) + ] +]. notation < "a ⊙ b" left associative with precedence 60 for @{'lc $op $a $b}. interpretation "lc" 'lc op a b = (lc ? op a b). -- 2.39.2