equal
deleted
inserted
replaced
82 text {* shows applicability of the induction hypothesis of the following Lemma 1 *} |
82 text {* shows applicability of the induction hypothesis of the following Lemma 1 *} |
83 lemma last_ind_on_first: |
83 lemma last_ind_on_first: |
84 "l ~= [] ==> hd (reverse (reduce (a # l))) = hd (reverse (reduce l))" |
84 "l ~= [] ==> hd (reverse (reduce (a # l))) = hd (reverse (reduce l))" |
85 apply simp |
85 apply simp |
86 apply (tactic {* auto_tac (map_simpset (fn _ => |
86 apply (tactic {* auto_tac (map_simpset (fn _ => |
87 HOL_ss addsplits [@{thm list.split}] |
87 HOL_ss |
88 addsimps (@{thms reverse.simps} @ [@{thm hd_append}, @{thm rev_red_not_nil}])) @{context}) *}) |
88 addsimps (@{thms reverse.simps} @ [@{thm hd_append}, @{thm rev_red_not_nil}]) |
|
89 |> Splitter.add_split @{thm list.split}) @{context}) *}) |
89 done |
90 done |
90 |
91 |
91 text {* Main Lemma 1 for @{text "S_pkt"} in showing that reduce is refinement. *} |
92 text {* Main Lemma 1 for @{text "S_pkt"} in showing that reduce is refinement. *} |
92 lemma reduce_hd: |
93 lemma reduce_hd: |
93 "if x=hd(reverse(reduce(l))) & reduce(l)~=[] then |
94 "if x=hd(reverse(reduce(l))) & reduce(l)~=[] then |