src/HOLCF/IOA/NTP/Impl.thy
changeset 28839 32d498cf7595
parent 28265 7e14443f2dd6
child 35174 e15040ae75d7
equal deleted inserted replaced
28838:d5db6dfcb34a 28839:32d498cf7595
   218   txt {* 3 *}
   218   txt {* 3 *}
   219   apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
   219   apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
   220     (@{thm raw_inv1} RS @{thm invariantE})] 1 *})
   220     (@{thm raw_inv1} RS @{thm invariantE})] 1 *})
   221 
   221 
   222   apply (tactic "tac2 1")
   222   apply (tactic "tac2 1")
   223   apply (tactic {* fold_tac [rewrite_rule [@{thm Packet.hdr_def}]
   223   apply (tactic {* fold_goals_tac [rewrite_rule [@{thm Packet.hdr_def}]
   224     (@{thm Impl.hdr_sum_def})] *})
   224     (@{thm Impl.hdr_sum_def})] *})
   225   apply arith
   225   apply arith
   226 
   226 
   227   txt {* 2 *}
   227   txt {* 2 *}
   228   apply (tactic "tac2 1")
   228   apply (tactic "tac2 1")
   236   apply (tactic "tac2 1")
   236   apply (tactic "tac2 1")
   237   apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
   237   apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
   238                                (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1 *})
   238                                (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1 *})
   239   apply (intro strip)
   239   apply (intro strip)
   240   apply (erule conjE)+
   240   apply (erule conjE)+
   241   apply (tactic {* fold_tac  [rewrite_rule [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})] *})
   241   apply (tactic {* fold_goals_tac [rewrite_rule [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})] *})
   242   apply simp
   242   apply simp
   243 
   243 
   244   done
   244   done
   245 
   245 
   246 
   246