src/HOL/IOA/NTP/Correctness.ML
changeset 1465 5d7a7e439cec
parent 1342 f6651b6b0482
child 1894 c2c8279d40f0
equal deleted inserted replaced
1464:a608f83e3421 1465:5d7a7e439cec
    68 goalw Correctness.thy [Spec.ioa_def, Solve.is_weak_pmap_def]
    68 goalw Correctness.thy [Spec.ioa_def, Solve.is_weak_pmap_def]
    69   "is_weak_pmap hom (restrict impl_ioa (externals spec_sig)) spec_ioa";
    69   "is_weak_pmap hom (restrict impl_ioa (externals spec_sig)) spec_ioa";
    70 by(simp_tac (!simpset addsimps 
    70 by(simp_tac (!simpset addsimps 
    71     [Correctness.hom_def,
    71     [Correctness.hom_def,
    72      cancel_restrict,externals_lemma]) 1);
    72      cancel_restrict,externals_lemma]) 1);
    73 br conjI 1;
    73 by (rtac conjI 1);
    74 by(simp_tac ss' 1);
    74 by(simp_tac ss' 1);
    75 br ballI 1;
    75 by (rtac ballI 1);
    76 bd CollectD 1;
    76 by (dtac CollectD 1);
    77 by(asm_simp_tac (!simpset addsimps sels) 1);
    77 by(asm_simp_tac (!simpset addsimps sels) 1);
    78 by(REPEAT(rtac allI 1));
    78 by(REPEAT(rtac allI 1));
    79 br imp_conj_lemma 1;   (* from lemmas.ML *)
    79 by (rtac imp_conj_lemma 1);   (* from lemmas.ML *)
    80 
    80 
    81 by(Action.action.induct_tac "a"  1);
    81 by(Action.action.induct_tac "a"  1);
    82 by(asm_simp_tac (ss' setloop (split_tac [expand_if])) 1);
    82 by(asm_simp_tac (ss' setloop (split_tac [expand_if])) 1);
    83 by(forward_tac [inv4] 1);
    83 by(forward_tac [inv4] 1);
    84 by(asm_full_simp_tac (!simpset addsimps 
    84 by(asm_full_simp_tac (!simpset addsimps 
    92 by(simp_tac ss' 1);
    92 by(simp_tac ss' 1);
    93 
    93 
    94 by(asm_simp_tac ss' 1);
    94 by(asm_simp_tac ss' 1);
    95 by(forward_tac [inv4] 1);
    95 by(forward_tac [inv4] 1);
    96 by(forward_tac [inv2] 1);
    96 by(forward_tac [inv2] 1);
    97 be disjE 1;
    97 by (etac disjE 1);
    98 by(Asm_simp_tac 1);
    98 by(Asm_simp_tac 1);
    99 by(asm_full_simp_tac (!simpset addsimps [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1);
    99 by(asm_full_simp_tac (!simpset addsimps [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1);
   100 
   100 
   101 by(asm_simp_tac ss' 1);
   101 by(asm_simp_tac ss' 1);
   102 by(forward_tac [inv2] 1);
   102 by(forward_tac [inv2] 1);
   103 be disjE 1;
   103 by (etac disjE 1);
   104 
   104 
   105 by(forward_tac [inv3] 1);
   105 by(forward_tac [inv3] 1);
   106 by(case_tac "sq(sen(s))=[]" 1);
   106 by(case_tac "sq(sen(s))=[]" 1);
   107 
   107 
   108 by(asm_full_simp_tac ss' 1);
   108 by(asm_full_simp_tac ss' 1);