equal
deleted
inserted
replaced
168 (* a~:A, a:B *) |
168 (* a~:A, a:B *) |
169 by (Asm_full_simp_tac 1); |
169 by (Asm_full_simp_tac 1); |
170 by (rtac (Forall_Conc_impl RS mp) 1); |
170 by (rtac (Forall_Conc_impl RS mp) 1); |
171 by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1); |
171 by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1); |
172 (* a~:A,a~:B *) |
172 (* a~:A,a~:B *) |
173 by (Auto_tac()); |
173 by Auto_tac; |
174 qed"ForallAorB_mksch1"; |
174 qed"ForallAorB_mksch1"; |
175 |
175 |
176 bind_thm ("ForallAorB_mksch",ForallAorB_mksch1 RS spec RS spec RS mp); |
176 bind_thm ("ForallAorB_mksch",ForallAorB_mksch1 RS spec RS spec RS mp); |
177 |
177 |
178 goal thy "!!A B. compatible B A ==> \ |
178 goal thy "!!A B. compatible B A ==> \ |
393 |
393 |
394 goal thy "!! y.Finite y ==> ! z tr. Forall (%a.a:ext (A||B)) tr & \ |
394 goal thy "!! y.Finite y ==> ! z tr. Forall (%a.a:ext (A||B)) tr & \ |
395 \ y = z @@ mksch A B`tr`a`b\ |
395 \ y = z @@ mksch A B`tr`a`b\ |
396 \ --> Finite tr"; |
396 \ --> Finite tr"; |
397 by (etac Seq_Finite_ind 1); |
397 by (etac Seq_Finite_ind 1); |
398 by (Auto_tac()); |
398 by Auto_tac; |
399 by (Seq_case_simp_tac "tr" 1); |
399 by (Seq_case_simp_tac "tr" 1); |
400 (* tr = UU *) |
400 (* tr = UU *) |
401 by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc]) 1); |
401 by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc]) 1); |
402 (* tr = nil *) |
402 (* tr = nil *) |
403 by (Auto_tac()); |
403 by Auto_tac; |
404 (* tr = Conc *) |
404 (* tr = Conc *) |
405 ren "s ss" 1; |
405 ren "s ss" 1; |
406 |
406 |
407 by (case_tac "s:act A" 1); |
407 by (case_tac "s:act A" 1); |
408 by (case_tac "s:act B" 1); |
408 by (case_tac "s:act B" 1); |
417 addss (simpset() addsimps [externals_of_par]) ) 1); |
417 addss (simpset() addsimps [externals_of_par]) ) 1); |
418 (* main case *) |
418 (* main case *) |
419 by (Seq_case_simp_tac "tr" 1); |
419 by (Seq_case_simp_tac "tr" 1); |
420 (* tr = UU *) |
420 (* tr = UU *) |
421 by (asm_full_simp_tac (simpset() addsimps [Conc_Conc_eq]) 1); |
421 by (asm_full_simp_tac (simpset() addsimps [Conc_Conc_eq]) 1); |
422 by (Auto_tac()); |
422 by Auto_tac; |
423 (* tr = nil ok *) |
423 (* tr = nil ok *) |
424 (* tr = Conc *) |
424 (* tr = Conc *) |
425 by (Seq_case_simp_tac "z" 1); |
425 by (Seq_case_simp_tac "z" 1); |
426 (* z = UU ok *) |
426 (* z = UU ok *) |
427 (* z = nil *) |
427 (* z = nil *) |
450 |
450 |
451 |
451 |
452 |
452 |
453 goal thy "(x>>xs = y @@ z) = ((y=nil & x>>xs=z) | (? ys. y=x>>ys & xs=ys@@z))"; |
453 goal thy "(x>>xs = y @@ z) = ((y=nil & x>>xs=z) | (? ys. y=x>>ys & xs=ys@@z))"; |
454 by (Seq_case_simp_tac "y" 1); |
454 by (Seq_case_simp_tac "y" 1); |
455 by (Auto_tac()); |
455 by Auto_tac; |
456 qed"Conc_Conc_eq"; |
456 qed"Conc_Conc_eq"; |
457 |
457 |
458 goal thy "!! (y::'a Seq).Finite y ==> ~ y= x@@UU"; |
458 goal thy "!! (y::'a Seq).Finite y ==> ~ y= x@@UU"; |
459 by (etac Seq_Finite_ind 1); |
459 by (etac Seq_Finite_ind 1); |
460 by (Seq_case_simp_tac "x" 1); |
460 by (Seq_case_simp_tac "x" 1); |
461 by (Seq_case_simp_tac "x" 1); |
461 by (Seq_case_simp_tac "x" 1); |
462 by (Auto_tac()); |
462 by Auto_tac; |
463 qed"FiniteConcUU1"; |
463 qed"FiniteConcUU1"; |
464 |
464 |
465 goal thy "~ Finite ((x::'a Seq)@@UU)"; |
465 goal thy "~ Finite ((x::'a Seq)@@UU)"; |
466 by (rtac (FiniteConcUU1 COMP rev_contrapos) 1); |
466 by (rtac (FiniteConcUU1 COMP rev_contrapos) 1); |
467 by (Auto_tac()); |
467 by Auto_tac; |
468 qed"FiniteConcUU"; |
468 qed"FiniteConcUU"; |
469 |
469 |
470 finiteR_mksch |
470 finiteR_mksch |
471 "Finite (mksch A B`tr`x`y) --> Finite tr" |
471 "Finite (mksch A B`tr`x`y) --> Finite tr" |
472 *) |
472 *) |