diff options
Diffstat (limited to 'theories/Wellfounded/Disjoint_Union.v')
-rw-r--r-- | theories/Wellfounded/Disjoint_Union.v | 54 |
1 files changed, 54 insertions, 0 deletions
diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v new file mode 100644 index 000000000..162a31e83 --- /dev/null +++ b/theories/Wellfounded/Disjoint_Union.v @@ -0,0 +1,54 @@ + +(* $Id$ *) + +(****************************************************************************) +(* Cristina Cornes *) +(* *) +(* From : Constructing Recursion Operators in Type Theory *) +(* L. Paulson JSC (1986) 2, 325-355 *) +(****************************************************************************) + +Require Relation_Operators. + +Section Wf_Disjoint_Union. +Variable A,B:Set. +Variable leA: A->A->Prop. +Variable leB: B->B->Prop. + +Syntactic Definition Le_AsB := (le_AsB A B leA leB). + +Lemma acc_A_sum: (x:A)(Acc A leA x)->(Acc A+B Le_AsB (inl A B x)). +Proof. + Induction 1;Intros. + Apply Acc_intro;Intros. + Inversion_clear H2. + Auto with sets. +Qed. + +Lemma acc_B_sum: (well_founded A leA) ->(x:B)(Acc B leB x) + ->(Acc A+B Le_AsB (inr A B x)). +Proof. + Induction 2;Intros. + Apply Acc_intro;Intros. + Inversion_clear H3;Auto with sets. + Apply acc_A_sum;Auto with sets. +Save. + + +Lemma wf_disjoint_sum: + (well_founded A leA) + -> (well_founded B leB) -> (well_founded A+B Le_AsB). +Proof. + Intros. + Unfold well_founded . + Induction a. + Intro. + Apply (acc_A_sum y). + Apply (H y). + + Intro. + Apply (acc_B_sum H y). + Apply (H0 y). +Qed. + +End Wf_Disjoint_Union. |