equal
deleted
inserted
replaced
71 (*---------------------------------------------------------------------------- |
71 (*---------------------------------------------------------------------------- |
72 * Wellfoundedness of lexicographic combinations |
72 * Wellfoundedness of lexicographic combinations |
73 *---------------------------------------------------------------------------*) |
73 *---------------------------------------------------------------------------*) |
74 |
74 |
75 val [wfa,wfb] = goalw thy [wf_def,lex_prod_def] |
75 val [wfa,wfb] = goalw thy [wf_def,lex_prod_def] |
76 "[| wf(ra); wf(rb) |] ==> wf(ra**rb)"; |
76 "[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)"; |
77 by (EVERY1 [rtac allI,rtac impI]); |
77 by (EVERY1 [rtac allI,rtac impI]); |
78 by (simp_tac (HOL_basic_ss addsimps [split_paired_All]) 1); |
78 by (simp_tac (HOL_basic_ss addsimps [split_paired_All]) 1); |
79 by (rtac (wfa RS spec RS mp) 1); |
79 by (rtac (wfa RS spec RS mp) 1); |
80 by (EVERY1 [rtac allI,rtac impI]); |
80 by (EVERY1 [rtac allI,rtac impI]); |
81 by (rtac (wfb RS spec RS mp) 1); |
81 by (rtac (wfb RS spec RS mp) 1); |
85 |
85 |
86 (*--------------------------------------------------------------------------- |
86 (*--------------------------------------------------------------------------- |
87 * Transitivity of WF combinators. |
87 * Transitivity of WF combinators. |
88 *---------------------------------------------------------------------------*) |
88 *---------------------------------------------------------------------------*) |
89 Goalw [trans_def, lex_prod_def] |
89 Goalw [trans_def, lex_prod_def] |
90 "!!R1 R2. [| trans R1; trans R2 |] ==> trans (R1 ** R2)"; |
90 "!!R1 R2. [| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)"; |
91 by (Simp_tac 1); |
91 by (Simp_tac 1); |
92 by (Blast_tac 1); |
92 by (Blast_tac 1); |
93 qed "trans_lex_prod"; |
93 qed "trans_lex_prod"; |
94 AddSIs [trans_lex_prod]; |
94 AddSIs [trans_lex_prod]; |
95 |
95 |