section ‹CFG› theory CFG imports BasicDefs begin subsection ‹The abstract CFG› subsubsection ‹Locale fixes and assumptions› locale CFG = fixes sourcenode :: "'edge ⇒ 'node" fixes targetnode :: "'edge ⇒ 'node" fixes kind :: "'edge ⇒ ('var,'val,'ret,'pname) edge_kind" fixes valid_edge :: "'edge ⇒ bool" fixes Entry::"'node" ("'('_Entry'_')") fixes get_proc::"'node ⇒ 'pname" fixes get_return_edges::"'edge ⇒ 'edge set" fixes procs::"('pname × 'var list × 'var list) list" fixes Main::"'pname" assumes Entry_target [dest]: "⟦valid_edge a; targetnode a = (_Entry_)⟧ ⟹ False" and get_proc_Entry:"get_proc (_Entry_) = Main" and Entry_no_call_source: "⟦valid_edge a; kind a = Q:r↪⇘p⇙fs; sourcenode a = (_Entry_)⟧ ⟹ False" and edge_det: "⟦valid_edge a; valid_edge a'; sourcenode a = sourcenode a'; targetnode a = targetnode a'⟧ ⟹ a = a'" and Main_no_call_target:"⟦valid_edge a; kind a = Q:r↪⇘Main⇙f⟧ ⟹ False" and Main_no_return_source:"⟦valid_edge a; kind a = Q'↩⇘Main⇙f'⟧ ⟹ False" and callee_in_procs: "⟦valid_edge a; kind a = Q:r↪⇘p⇙fs⟧ ⟹ ∃ins outs. (p,ins,outs) ∈ set procs" and get_proc_intra:"⟦valid_edge a; intra_kind(kind a)⟧ ⟹ get_proc (sourcenode a) = get_proc (targetnode a)" and get_proc_call: "⟦valid_edge a; kind a = Q:r↪⇘p⇙fs⟧ ⟹ get_proc (targetnode a) = p" and get_proc_return: "⟦valid_edge a; kind a = Q'↩⇘p⇙f'⟧ ⟹ get_proc (sourcenode a) = p" and call_edges_only:"⟦valid_edge a; kind a = Q:r↪⇘p⇙fs⟧ ⟹ ∀a'. valid_edge a' ∧ targetnode a' = targetnode a ⟶ (∃Qx rx fsx. kind a' = Qx:rx↪⇘p⇙fsx)" and return_edges_only:"⟦valid_edge a; kind a = Q'↩⇘p⇙f'⟧ ⟹ ∀a'. valid_edge a' ∧ sourcenode a' = sourcenode a ⟶ (∃Qx fx. kind a' = Qx↩⇘p⇙fx)" and get_return_edge_call: "⟦valid_edge a; kind a = Q:r↪⇘p⇙fs⟧ ⟹ get_return_edges a ≠ {}" and get_return_edges_valid: "⟦valid_edge a; a' ∈ get_return_edges a⟧ ⟹ valid_edge a'" and only_call_get_return_edges: "⟦valid_edge a; a' ∈ get_return_edges a⟧ ⟹ ∃Q r p fs. kind a = Q:r↪⇘p⇙fs" and call_return_edges: "⟦valid_edge a; kind a = Q:r↪⇘p⇙fs; a' ∈ get_return_edges a⟧ ⟹ ∃Q' f'. kind a' = Q'↩⇘p⇙f'" and return_needs_call: "⟦valid_edge a; kind a = Q'↩⇘p⇙f'⟧ ⟹ ∃!a'. valid_edge a' ∧ (∃Q r fs. kind a' = Q:r↪⇘p⇙fs) ∧ a ∈ get_return_edges a'" and intra_proc_additional_edge: "⟦valid_edge a; a' ∈ get_return_edges a⟧ ⟹ ∃a''. valid_edge a'' ∧ sourcenode a'' = targetnode a ∧ targetnode a'' = sourcenode a' ∧ kind a'' = (λcf. False)⇩_{√}" and call_return_node_edge: "⟦valid_edge a; a' ∈ get_return_edges a⟧ ⟹ ∃a''. valid_edge a'' ∧ sourcenode a'' = sourcenode a ∧ targetnode a'' = targetnode a' ∧ kind a'' = (λcf. False)⇩_{√}" and call_only_one_intra_edge: "⟦valid_edge a; kind a = Q:r↪⇘p⇙fs⟧ ⟹ ∃!a'. valid_edge a' ∧ sourcenode a' = sourcenode a ∧ intra_kind(kind a')" and return_only_one_intra_edge: "⟦valid_edge a; kind a = Q'↩⇘p⇙f'⟧ ⟹ ∃!a'. valid_edge a' ∧ targetnode a' = targetnode a ∧ intra_kind(kind a')" and same_proc_call_unique_target: "⟦valid_edge a; valid_edge a'; kind a = Q⇩_{1}:r⇩_{1}↪⇘p⇙fs⇩_{1}; kind a' = Q⇩_{2}:r⇩_{2}↪⇘p⇙fs⇩_{2}⟧ ⟹ targetnode a = targetnode a'" and unique_callers:"distinct_fst procs" and distinct_formal_ins:"(p,ins,outs) ∈ set procs ⟹ distinct ins" and distinct_formal_outs:"(p,ins,outs) ∈ set procs ⟹ distinct outs" begin lemma get_proc_get_return_edge: assumes "valid_edge a" and "a' ∈ get_return_edges a" shows "get_proc (sourcenode a) = get_proc (targetnode a')" proof - from assms obtain ax where "valid_edge ax" and "sourcenode a = sourcenode ax" and "targetnode a' = targetnode ax" and "intra_kind(kind ax)" by(auto dest:call_return_node_edge simp:intra_kind_def) thus ?thesis by(fastforce intro:get_proc_intra) qed lemma call_intra_edge_False: assumes "valid_edge a" and "kind a = Q:r↪⇘p⇙fs" and "valid_edge a'" and "sourcenode a = sourcenode a'" and "intra_kind(kind a')" shows "kind a' = (λcf. False)⇩_{√}" proof - from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› obtain ax where "ax ∈ get_return_edges a" by(fastforce dest:get_return_edge_call) with ‹valid_edge a› obtain a'' where "valid_edge a''" and "sourcenode a'' = sourcenode a" and "kind a'' = (λcf. False)⇩_{√}" by(fastforce dest:call_return_node_edge) from ‹kind a'' = (λcf. False)⇩_{√}› have "intra_kind(kind a'')" by(simp add:intra_kind_def) with assms ‹valid_edge a''› ‹sourcenode a'' = sourcenode a› ‹kind a'' = (λcf. False)⇩_{√}› show ?thesis by(fastforce dest:call_only_one_intra_edge) qed lemma formal_in_THE: "⟦valid_edge a; kind a = Q:r↪⇘p⇙fs; (p,ins,outs) ∈ set procs⟧ ⟹ (THE ins. ∃outs. (p,ins,outs) ∈ set procs) = ins" by(fastforce dest:distinct_fst_isin_same_fst intro:unique_callers) lemma formal_out_THE: "⟦valid_edge a; kind a = Q↩⇘p⇙f; (p,ins,outs) ∈ set procs⟧ ⟹ (THE outs. ∃ins. (p,ins,outs) ∈ set procs) = outs" by(fastforce dest:distinct_fst_isin_same_fst intro:unique_callers) subsubsection ‹Transfer and predicate functions› fun params :: "(('var ⇀ 'val) ⇀ 'val) list ⇒ ('var ⇀ 'val) ⇒ 'val option list" where "params [] cf = []" | "params (f#fs) cf = (f cf)#params fs cf" lemma params_nth: "i < length fs ⟹ (params fs cf)!i = (fs!i) cf" by(induct fs arbitrary:i,auto,case_tac i,auto) lemma [simp]:"length (params fs cf) = length fs" by(induct fs) auto fun transfer :: "('var,'val,'ret,'pname) edge_kind ⇒ (('var ⇀ 'val) × 'ret) list ⇒ (('var ⇀ 'val) × 'ret) list" where "transfer (⇑f) (cf#cfs) = (f (fst cf),snd cf)#cfs" | "transfer (Q)⇩_{√}(cf#cfs) = (cf#cfs)" | "transfer (Q:r↪⇘p⇙fs) (cf#cfs) = (let ins = THE ins. ∃outs. (p,ins,outs) ∈ set procs in (Map.empty(ins [:=] params fs (fst cf)),r)#cf#cfs)" | "transfer (Q↩⇘p⇙f )(cf#cfs) = (case cfs of [] ⇒ [] | cf'#cfs' ⇒ (f (fst cf) (fst cf'),snd cf')#cfs')" | "transfer et [] = []" fun transfers :: "('var,'val,'ret,'pname) edge_kind list ⇒ (('var ⇀ 'val) × 'ret) list ⇒ (('var ⇀ 'val) × 'ret) list" where "transfers [] s = s" | "transfers (et#ets) s = transfers ets (transfer et s)" fun pred :: "('var,'val,'ret,'pname) edge_kind ⇒ (('var ⇀ 'val) × 'ret) list ⇒ bool" where "pred (⇑f) (cf#cfs) = True" | "pred (Q)⇩_{√}(cf#cfs) = Q (fst cf)" | "pred (Q:r↪⇘p⇙fs) (cf#cfs) = Q (fst cf,r)" | "pred (Q↩⇘p⇙f) (cf#cfs) = (Q cf ∧ cfs ≠ [])" | "pred et [] = False" fun preds :: "('var,'val,'ret,'pname) edge_kind list ⇒ (('var ⇀ 'val) × 'ret) list ⇒ bool" where "preds [] s = True" | "preds (et#ets) s = (pred et s ∧ preds ets (transfer et s))" lemma transfers_split: "(transfers (ets@ets') s) = (transfers ets' (transfers ets s))" by(induct ets arbitrary:s) auto lemma preds_split: "(preds (ets@ets') s) = (preds ets s ∧ preds ets' (transfers ets s))" by(induct ets arbitrary:s) auto abbreviation state_val :: "(('var ⇀ 'val) × 'ret) list ⇒ 'var ⇀ 'val" where "state_val s V ≡ (fst (hd s)) V" subsubsection ‹‹valid_node›› definition valid_node :: "'node ⇒ bool" where "valid_node n ≡ (∃a. valid_edge a ∧ (n = sourcenode a ∨ n = targetnode a))" lemma [simp]: "valid_edge a ⟹ valid_node (sourcenode a)" by(fastforce simp:valid_node_def) lemma [simp]: "valid_edge a ⟹ valid_node (targetnode a)" by(fastforce simp:valid_node_def) subsection ‹CFG paths› inductive path :: "'node ⇒ 'edge list ⇒ 'node ⇒ bool" ("_ -_→* _" [51,0,0] 80) where empty_path:"valid_node n ⟹ n -[]→* n" | Cons_path: "⟦n'' -as→* n'; valid_edge a; sourcenode a = n; targetnode a = n''⟧ ⟹ n -a#as→* n'" lemma path_valid_node: assumes "n -as→* n'" shows "valid_node n" and "valid_node n'" using ‹n -as→* n'› by(induct rule:path.induct,auto) lemma empty_path_nodes [dest]:"n -[]→* n' ⟹ n = n'" by(fastforce elim:path.cases) lemma path_valid_edges:"n -as→* n' ⟹ ∀a ∈ set as. valid_edge a" by(induct rule:path.induct) auto lemma path_edge:"valid_edge a ⟹ sourcenode a -[a]→* targetnode a" by(fastforce intro:Cons_path empty_path) lemma path_Append:"⟦n -as→* n''; n'' -as'→* n'⟧ ⟹ n -as@as'→* n'" by(induct rule:path.induct,auto intro:Cons_path) lemma path_split: assumes "n -as@a#as'→* n'" shows "n -as→* sourcenode a" and "valid_edge a" and "targetnode a -as'→* n'" using ‹n -as@a#as'→* n'› proof(induct as arbitrary:n) case Nil case 1 thus ?case by(fastforce elim:path.cases intro:empty_path) next case Nil case 2 thus ?case by(fastforce elim:path.cases intro:path_edge) next case Nil case 3 thus ?case by(fastforce elim:path.cases) next case (Cons ax asx) note IH1 = ‹⋀n. n -asx@a#as'→* n' ⟹ n -asx→* sourcenode a› note IH2 = ‹⋀n. n -asx@a#as'→* n' ⟹ valid_edge a› note IH3 = ‹⋀n. n -asx@a#as'→* n' ⟹ targetnode a -as'→* n'› { case 1 hence "sourcenode ax = n" and "targetnode ax -asx@a#as'→* n'" and "valid_edge ax" by(auto elim:path.cases) from IH1[OF ‹ targetnode ax -asx@a#as'→* n'›] have "targetnode ax -asx→* sourcenode a" . with ‹sourcenode ax = n› ‹valid_edge ax› show ?case by(fastforce intro:Cons_path) next case 2 hence "targetnode ax -asx@a#as'→* n'" by(auto elim:path.cases) from IH2[OF this] show ?case . next case 3 hence "targetnode ax -asx@a#as'→* n'" by(auto elim:path.cases) from IH3[OF this] show ?case . } qed lemma path_split_Cons: assumes "n -as→* n'" and "as ≠ []" obtains a' as' where "as = a'#as'" and "n = sourcenode a'" and "valid_edge a'" and "targetnode a' -as'→* n'" proof(atomize_elim) from ‹as ≠ []› obtain a' as' where "as = a'#as'" by(cases as) auto with ‹n -as→* n'› have "n -[]@a'#as'→* n'" by simp hence "n -[]→* sourcenode a'" and "valid_edge a'" and "targetnode a' -as'→* n'" by(rule path_split)+ from ‹n -[]→* sourcenode a'› have "n = sourcenode a'" by fast with ‹as = a'#as'› ‹valid_edge a'› ‹targetnode a' -as'→* n'› show "∃a' as'. as = a'#as' ∧ n = sourcenode a' ∧ valid_edge a' ∧ targetnode a' -as'→* n'" by fastforce qed lemma path_split_snoc: assumes "n -as→* n'" and "as ≠ []" obtains a' as' where "as = as'@[a']" and "n -as'→* sourcenode a'" and "valid_edge a'" and "n' = targetnode a'" proof(atomize_elim) from ‹as ≠ []› obtain a' as' where "as = as'@[a']" by(cases as rule:rev_cases) auto with ‹n -as→* n'› have "n -as'@a'#[]→* n'" by simp hence "n -as'→* sourcenode a'" and "valid_edge a'" and "targetnode a' -[]→* n'" by(rule path_split)+ from ‹targetnode a' -[]→* n'› have "n' = targetnode a'" by fast with ‹as = as'@[a']› ‹valid_edge a'› ‹n -as'→* sourcenode a'› show "∃as' a'. as = as'@[a'] ∧ n -as'→* sourcenode a' ∧ valid_edge a' ∧ n' = targetnode a'" by fastforce qed lemma path_split_second: assumes "n -as@a#as'→* n'" shows "sourcenode a -a#as'→* n'" proof - from ‹n -as@a#as'→* n'› have "valid_edge a" and "targetnode a -as'→* n'" by(auto intro:path_split) thus ?thesis by(fastforce intro:Cons_path) qed lemma path_Entry_Cons: assumes "(_Entry_) -as→* n'" and "n' ≠ (_Entry_)" obtains n a where "sourcenode a = (_Entry_)" and "targetnode a = n" and "n -tl as→* n'" and "valid_edge a" and "a = hd as" proof(atomize_elim) from ‹(_Entry_) -as→* n'› ‹n' ≠ (_Entry_)› have "as ≠ []" by(cases as,auto elim:path.cases) with ‹(_Entry_) -as→* n'› obtain a' as' where "as = a'#as'" and "(_Entry_) = sourcenode a'" and "valid_edge a'" and "targetnode a' -as'→* n'" by(erule path_split_Cons) thus "∃a n. sourcenode a = (_Entry_) ∧ targetnode a = n ∧ n -tl as→* n' ∧ valid_edge a ∧ a = hd as" by fastforce qed lemma path_det: "⟦n -as→* n'; n -as→* n''⟧ ⟹ n' = n''" proof(induct as arbitrary:n) case Nil thus ?case by(auto elim:path.cases) next case (Cons a' as') note IH = ‹⋀n. ⟦n -as'→* n'; n -as'→* n''⟧ ⟹ n' = n''› from ‹n -a'#as'→* n'› have "targetnode a' -as'→* n'" by(fastforce elim:path_split_Cons) from ‹n -a'#as'→* n''› have "targetnode a' -as'→* n''" by(fastforce elim:path_split_Cons) from IH[OF ‹targetnode a' -as'→* n'› this] show ?thesis . qed definition sourcenodes :: "'edge list ⇒ 'node list" where "sourcenodes xs ≡ map sourcenode xs" definition kinds :: "'edge list ⇒ ('var,'val,'ret,'pname) edge_kind list" where "kinds xs ≡ map kind xs" definition targetnodes :: "'edge list ⇒ 'node list" where "targetnodes xs ≡ map targetnode xs" lemma path_sourcenode: "⟦n -as→* n'; as ≠ []⟧ ⟹ hd (sourcenodes as) = n" by(fastforce elim:path_split_Cons simp:sourcenodes_def) lemma path_targetnode: "⟦n -as→* n'; as ≠ []⟧ ⟹ last (targetnodes as) = n'" by(fastforce elim:path_split_snoc simp:targetnodes_def) lemma sourcenodes_is_n_Cons_butlast_targetnodes: "⟦n -as→* n'; as ≠ []⟧ ⟹ sourcenodes as = n#(butlast (targetnodes as))" proof(induct as arbitrary:n) case Nil thus ?case by simp next case (Cons a' as') note IH = ‹⋀n. ⟦n -as'→* n'; as' ≠ []⟧ ⟹ sourcenodes as' = n#(butlast (targetnodes as'))› from ‹n -a'#as'→* n'› have "n = sourcenode a'" and "targetnode a' -as'→* n'" by(auto elim:path_split_Cons) show ?case proof(cases "as' = []") case True with ‹targetnode a' -as'→* n'› have "targetnode a' = n'" by fast with True ‹n = sourcenode a'› show ?thesis by(simp add:sourcenodes_def targetnodes_def) next case False from IH[OF ‹targetnode a' -as'→* n'› this] have "sourcenodes as' = targetnode a' # butlast (targetnodes as')" . with ‹n = sourcenode a'› False show ?thesis by(simp add:sourcenodes_def targetnodes_def) qed qed lemma targetnodes_is_tl_sourcenodes_App_n': "⟦n -as→* n'; as ≠ []⟧ ⟹ targetnodes as = (tl (sourcenodes as))@[n']" proof(induct as arbitrary:n' rule:rev_induct) case Nil thus ?case by simp next case (snoc a' as') note IH = ‹⋀n'. ⟦n -as'→* n'; as' ≠ []⟧ ⟹ targetnodes as' = tl (sourcenodes as') @ [n']› from ‹n -as'@[a']→* n'› have "n -as'→* sourcenode a'" and "n' = targetnode a'" by(auto elim:path_split_snoc) show ?case proof(cases "as' = []") case True with ‹n -as'→* sourcenode a'› have "n = sourcenode a'" by fast with True ‹n' = targetnode a'› show ?thesis by(simp add:sourcenodes_def targetnodes_def) next case False from IH[OF ‹n -as'→* sourcenode a'› this] have "targetnodes as' = tl (sourcenodes as')@[sourcenode a']" . with ‹n' = targetnode a'› False show ?thesis by(simp add:sourcenodes_def targetnodes_def) qed qed subsubsection ‹Intraprocedural paths› definition intra_path :: "'node ⇒ 'edge list ⇒ 'node ⇒ bool" ("_ -_→⇩_{ι}* _" [51,0,0] 80) where "n -as→⇩_{ι}* n' ≡ n -as→* n' ∧ (∀a ∈ set as. intra_kind(kind a))" lemma intra_path_get_procs: assumes "n -as→⇩_{ι}* n'" shows "get_proc n = get_proc n'" proof - from ‹n -as→⇩_{ι}* n'› have "n -as→* n'" and "∀a ∈ set as. intra_kind(kind a)" by(simp_all add:intra_path_def) thus ?thesis proof(induct as arbitrary:n) case Nil thus ?case by fastforce next case (Cons a' as') note IH = ‹⋀n. ⟦n -as'→* n'; ∀a∈set as'. intra_kind (kind a)⟧ ⟹ get_proc n = get_proc n'› from ‹∀a∈set (a'#as'). intra_kind (kind a)› have "intra_kind(kind a')" and "∀a∈set as'. intra_kind (kind a)" by simp_all from ‹n -a'#as'→* n'› have "sourcenode a' = n" and "valid_edge a'" and "targetnode a' -as'→* n'" by(auto elim:path.cases) from IH[OF ‹targetnode a' -as'→* n'› ‹∀a∈set as'. intra_kind (kind a)›] have "get_proc (targetnode a') = get_proc n'" . from ‹valid_edge a'› ‹intra_kind(kind a')› have "get_proc (sourcenode a') = get_proc (targetnode a')" by(rule get_proc_intra) with ‹sourcenode a' = n› ‹get_proc (targetnode a') = get_proc n'› show ?case by simp qed qed lemma intra_path_Append: "⟦n -as→⇩_{ι}* n''; n'' -as'→⇩_{ι}* n'⟧ ⟹ n -as@as'→⇩_{ι}* n'" by(fastforce intro:path_Append simp:intra_path_def) lemma get_proc_get_return_edges: assumes "valid_edge a" and "a' ∈ get_return_edges a" shows "get_proc(targetnode a) = get_proc(sourcenode a')" proof - from ‹valid_edge a› ‹a' ∈ get_return_edges a› obtain a'' where "valid_edge a''" and "sourcenode a'' = targetnode a" and "targetnode a'' = sourcenode a'" and "kind a'' = (λcf. False)⇩_{√}" by(fastforce dest:intra_proc_additional_edge) from ‹valid_edge a''› ‹kind a'' = (λcf. False)⇩_{√}› have "get_proc(sourcenode a'') = get_proc(targetnode a'')" by(fastforce intro:get_proc_intra simp:intra_kind_def) with ‹sourcenode a'' = targetnode a› ‹targetnode a'' = sourcenode a'› show ?thesis by simp qed subsubsection ‹Valid paths› declare conj_cong[fundef_cong] fun valid_path_aux :: "'edge list ⇒ 'edge list ⇒ bool" where "valid_path_aux cs [] ⟷ True" | "valid_path_aux cs (a#as) ⟷ (case (kind a) of Q:r↪⇘p⇙fs ⇒ valid_path_aux (a#cs) as | Q↩⇘p⇙f ⇒ case cs of [] ⇒ valid_path_aux [] as | c'#cs' ⇒ a ∈ get_return_edges c' ∧ valid_path_aux cs' as | _ ⇒ valid_path_aux cs as)" lemma vpa_induct [consumes 1,case_names vpa_empty vpa_intra vpa_Call vpa_ReturnEmpty vpa_ReturnCons]: assumes major: "valid_path_aux xs ys" and rules: "⋀cs. P cs []" "⋀cs a as. ⟦intra_kind(kind a); valid_path_aux cs as; P cs as⟧ ⟹ P cs (a#as)" "⋀cs a as Q r p fs. ⟦kind a = Q:r↪⇘p⇙fs; valid_path_aux (a#cs) as; P (a#cs) as⟧ ⟹ P cs (a#as)" "⋀cs a as Q p f. ⟦kind a = Q↩⇘p⇙f; cs = []; valid_path_aux [] as; P [] as⟧ ⟹ P cs (a#as)" "⋀cs a as Q p f c' cs' . ⟦kind a = Q↩⇘p⇙f; cs = c'#cs'; valid_path_aux cs' as; a ∈ get_return_edges c'; P cs' as⟧ ⟹ P cs (a#as)" shows "P xs ys" using major apply(induct ys arbitrary: xs) by(auto intro:rules split:edge_kind.split_asm list.split_asm simp:intra_kind_def) lemma valid_path_aux_intra_path: "∀a ∈ set as. intra_kind(kind a) ⟹ valid_path_aux cs as" by(induct as,auto simp:intra_kind_def) lemma valid_path_aux_callstack_prefix: "valid_path_aux (cs@cs') as ⟹ valid_path_aux cs as" proof(induct "cs@cs'" as arbitrary:cs cs' rule:vpa_induct) case vpa_empty thus ?case by simp next case (vpa_intra a as) hence "valid_path_aux cs as" by simp with ‹intra_kind (kind a)› show ?case by(cases "kind a",auto simp:intra_kind_def) next case (vpa_Call a as Q r p fs cs'' cs') note IH = ‹⋀xs ys. a#cs''@cs' = xs@ys ⟹ valid_path_aux xs as› have "a#cs''@cs' = (a#cs'')@cs'" by simp from IH[OF this] have "valid_path_aux (a#cs'') as" . with ‹kind a = Q:r↪⇘p⇙fs› show ?case by simp next case (vpa_ReturnEmpty a as Q p f cs'' cs') hence "valid_path_aux cs'' as" by simp with ‹kind a = Q↩⇘p⇙f› ‹cs''@cs' = []› show ?case by simp next case (vpa_ReturnCons a as Q p f c' cs' csx csx') note IH = ‹⋀xs ys. cs' = xs@ys ⟹ valid_path_aux xs as› from ‹csx@csx' = c'#cs'› have "csx = [] ∧ csx' = c'#cs' ∨ (∃zs. csx = c'#zs ∧ zs@csx' = cs')" by(simp add:append_eq_Cons_conv) thus ?case proof assume "csx = [] ∧ csx' = c'#cs'" hence "csx = []" and "csx' = c'#cs'" by simp_all from ‹csx' = c'#cs'› have "cs' = []@tl csx'" by simp from IH[OF this] have "valid_path_aux [] as" . with ‹csx = []› ‹kind a = Q↩⇘p⇙f› show ?thesis by simp next assume "∃zs. csx = c'#zs ∧ zs@csx' = cs'" then obtain zs where "csx = c'#zs" and "cs' = zs@csx'" by auto from IH[OF ‹cs' = zs@csx'›] have "valid_path_aux zs as" . with ‹csx = c'#zs› ‹kind a = Q↩⇘p⇙f› ‹a ∈ get_return_edges c'› show ?thesis by simp qed qed fun upd_cs :: "'edge list ⇒ 'edge list ⇒ 'edge list" where "upd_cs cs [] = cs" | "upd_cs cs (a#as) = (case (kind a) of Q:r↪⇘p⇙fs ⇒ upd_cs (a#cs) as | Q↩⇘p⇙f ⇒ case cs of [] ⇒ upd_cs cs as | c'#cs' ⇒ upd_cs cs' as | _ ⇒ upd_cs cs as)" lemma upd_cs_empty [dest]: "upd_cs cs [] = [] ⟹ cs = []" by(cases cs) auto lemma upd_cs_intra_path: "∀a ∈ set as. intra_kind(kind a) ⟹ upd_cs cs as = cs" by(induct as,auto simp:intra_kind_def) lemma upd_cs_Append: "⟦upd_cs cs as = cs'; upd_cs cs' as' = cs''⟧ ⟹ upd_cs cs (as@as') = cs''" by(induct as arbitrary:cs,auto split:edge_kind.split list.split) lemma upd_cs_empty_split: assumes "upd_cs cs as = []" and "cs ≠ []" and "as ≠ []" obtains xs ys where "as = xs@ys" and "xs ≠ []" and "upd_cs cs xs = []" and "∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs xs' ≠ []" and "upd_cs [] ys = []" proof(atomize_elim) from ‹upd_cs cs as = []› ‹cs ≠ []› ‹as ≠ []› show "∃xs ys. as = xs@ys ∧ xs ≠ [] ∧ upd_cs cs xs = [] ∧ (∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs xs' ≠ []) ∧ upd_cs [] ys = []" proof(induct as arbitrary:cs) case Nil thus ?case by simp next case (Cons a' as') note IH = ‹⋀cs. ⟦upd_cs cs as' = []; cs ≠ []; as' ≠ []⟧ ⟹ ∃xs ys. as' = xs@ys ∧ xs ≠ [] ∧ upd_cs cs xs = [] ∧ (∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs xs' ≠ []) ∧ upd_cs [] ys = []› show ?case proof(cases "kind a'" rule:edge_kind_cases) case Intra with ‹upd_cs cs (a'#as') = []› have "upd_cs cs as' = []" by(fastforce simp:intra_kind_def) with ‹cs ≠ []› have "as' ≠ []" by fastforce from IH[OF ‹upd_cs cs as' = []› ‹cs ≠ []› this] obtain xs ys where "as' = xs@ys" and "xs ≠ []" and "upd_cs cs xs = []" and "upd_cs [] ys = []" and "∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs xs' ≠ []" by blast from ‹upd_cs cs xs = []› Intra have "upd_cs cs (a'#xs) = []" by(fastforce simp:intra_kind_def) from ‹∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs xs' ≠ []› ‹xs ≠ []› Intra have "∀xs' ys'. a'#xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs xs' ≠ []" apply auto apply(case_tac xs') apply(auto simp:intra_kind_def) by(erule_tac x="[]" in allE,fastforce)+ with ‹as' = xs@ys› ‹upd_cs cs (a'#xs) = []› ‹upd_cs [] ys = []› show ?thesis apply(rule_tac x="a'#xs" in exI) by fastforce next case (Call Q p f) with ‹upd_cs cs (a'#as') = []› have "upd_cs (a'#cs) as' = []" by simp with ‹cs ≠ []› have "as' ≠ []" by fastforce from IH[OF ‹upd_cs (a'#cs) as' = []› _ this] obtain xs ys where "as' = xs@ys" and "xs ≠ []" and "upd_cs (a'#cs) xs = []" and "upd_cs [] ys = []" and "∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs (a'#cs) xs' ≠ []" by blast from ‹upd_cs (a'#cs) xs = []› Call have "upd_cs cs (a'#xs) = []" by simp from ‹∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs (a'#cs) xs' ≠ []› ‹xs ≠ []› ‹cs ≠ []› Call have "∀xs' ys'. a'#xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs xs' ≠ []" by auto(case_tac xs',auto) with ‹as' = xs@ys› ‹upd_cs cs (a'#xs) = []› ‹upd_cs [] ys = []› show ?thesis apply(rule_tac x="a'#xs" in exI) by fastforce next case (Return Q p f) with ‹upd_cs cs (a'#as') = []› ‹cs ≠ []› obtain c' cs' where "cs = c'#cs'" and "upd_cs cs' as' = []" by(cases cs) auto show ?thesis proof(cases "cs' = []") case True with ‹cs = c'#cs'› ‹upd_cs cs' as' = []› Return show ?thesis apply(rule_tac x="[a']" in exI) apply clarsimp by(case_tac xs') auto next case False with ‹upd_cs cs' as' = []› have "as' ≠ []" by fastforce from IH[OF ‹upd_cs cs' as' = []› False this] obtain xs ys where "as' = xs@ys" and "xs ≠ []" and "upd_cs cs' xs = []" and "upd_cs [] ys = []" and "∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs' xs' ≠ []" by blast from ‹upd_cs cs' xs = []› ‹cs = c'#cs'› Return have "upd_cs cs (a'#xs) = []" by simp from ‹∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs' xs' ≠ []› ‹xs ≠ []› ‹cs = c'#cs'› Return have "∀xs' ys'. a'#xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs xs' ≠ []" by auto(case_tac xs',auto) with ‹as' = xs@ys› ‹upd_cs cs (a'#xs) = []› ‹upd_cs [] ys = []› show ?thesis apply(rule_tac x="a'#xs" in exI) by fastforce qed qed qed qed lemma upd_cs_snoc_Return_Cons: assumes "kind a = Q↩⇘p⇙f" shows "upd_cs cs as = c'#cs' ⟹ upd_cs cs (as@[a]) = cs'" proof(induct as arbitrary:cs) case Nil with ‹kind a = Q↩⇘p⇙f› have "upd_cs cs [a] = cs'" by simp thus ?case by simp next case (Cons a' as') note IH = ‹⋀cs. upd_cs cs as' = c'#cs' ⟹ upd_cs cs (as'@[a]) = cs'› show ?case proof(cases "kind a'" rule:edge_kind_cases) case Intra with ‹upd_cs cs (a'#as') = c'#cs'› have "upd_cs cs as' = c'#cs'" by(fastforce simp:intra_kind_def) from IH[OF this] have "upd_cs cs (as'@[a]) = cs'" . with Intra show ?thesis by(fastforce simp:intra_kind_def) next case Call with ‹upd_cs cs (a'#as') = c'#cs'› have "upd_cs (a'#cs) as' = c'#cs'" by simp from IH[OF this] have "upd_cs (a'#cs) (as'@[a]) = cs'" . with Call show ?thesis by simp next case Return show ?thesis proof(cases cs) case Nil with ‹upd_cs cs (a'#as') = c'#cs'› Return have "upd_cs cs as' = c'#cs'" by simp from IH[OF this] have "upd_cs cs (as'@[a]) = cs'" . with Nil Return show ?thesis by simp next case (Cons cx csx) with ‹upd_cs cs (a'#as') = c'#cs'› Return have "upd_cs csx as' = c'#cs'" by simp from IH[OF this] have "upd_cs csx (as'@[a]) = cs'" . with Cons Return show ?thesis by simp qed qed qed lemma upd_cs_snoc_Call: assumes "kind a = Q:r↪⇘p⇙fs" shows "upd_cs cs (as@[a]) = a#(upd_cs cs as)" proof(induct as arbitrary:cs) case Nil with ‹kind a = Q:r↪⇘p⇙fs› show ?case by simp next case (Cons a' as') note IH = ‹⋀cs. upd_cs cs (as'@[a]) = a#upd_cs cs as'› show ?case proof(cases "kind a'" rule:edge_kind_cases) case Intra with IH[of cs] show ?thesis by(fastforce simp:intra_kind_def) next case Call with IH[of "a'#cs"] show ?thesis by simp next case Return show ?thesis proof(cases cs) case Nil with IH[of "[]"] Return show ?thesis by simp next case (Cons cx csx) with IH[of csx] Return show ?thesis by simp qed qed qed lemma valid_path_aux_split: assumes "valid_path_aux cs (as@as')" shows "valid_path_aux cs as" and "valid_path_aux (upd_cs cs as) as'" using ‹valid_path_aux cs (as@as')› proof(induct cs "as@as'" arbitrary:as as' rule:vpa_induct) case (vpa_intra cs a as as'') note IH1 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_aux cs xs› note IH2 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_aux (upd_cs cs xs) ys› { case 1 from vpa_intra have "as'' = [] ∧ a#as = as' ∨ (∃xs. a#xs = as'' ∧ as = xs@as')" by(simp add:Cons_eq_append_conv) thus ?case proof assume "as'' = [] ∧ a#as = as'" thus ?thesis by simp next assume "∃xs. a#xs = as'' ∧ as = xs@as'" then obtain xs where "a#xs = as''" and "as = xs@as'" by auto from IH1[OF ‹as = xs@as'›] have "valid_path_aux cs xs" . with ‹a#xs = as''› ‹intra_kind (kind a)› show ?thesis by(fastforce simp:intra_kind_def) qed next case 2 from vpa_intra have "as'' = [] ∧ a#as = as' ∨ (∃xs. a#xs = as'' ∧ as = xs@as')" by(simp add:Cons_eq_append_conv) thus ?case proof assume "as'' = [] ∧ a#as = as'" hence "as = []@tl as'" by(cases as') auto from IH2[OF this] have "valid_path_aux (upd_cs cs []) (tl as')" by simp with ‹as'' = [] ∧ a#as = as'› ‹intra_kind (kind a)› show ?thesis by(fastforce simp:intra_kind_def) next assume "∃xs. a#xs = as'' ∧ as = xs@as'" then obtain xs where "a#xs = as''" and "as = xs@as'" by auto from IH2[OF ‹as = xs@as'›] have "valid_path_aux (upd_cs cs xs) as'" . from ‹a#xs = as''› ‹intra_kind (kind a)› have "upd_cs cs xs = upd_cs cs as''" by(fastforce simp:intra_kind_def) with ‹valid_path_aux (upd_cs cs xs) as'› show ?thesis by simp qed } next case (vpa_Call cs a as Q r p fs as'') note IH1 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_aux (a#cs) xs› note IH2 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_aux (upd_cs (a#cs) xs) ys› { case 1 from vpa_Call have "as'' = [] ∧ a#as = as' ∨ (∃xs. a#xs = as'' ∧ as = xs@as')" by(simp add:Cons_eq_append_conv) thus ?case proof assume "as'' = [] ∧ a#as = as'" thus ?thesis by simp next assume "∃xs. a#xs = as'' ∧ as = xs@as'" then obtain xs where "a#xs = as''" and "as = xs@as'" by auto from IH1[OF ‹as = xs@as'›] have "valid_path_aux (a#cs) xs" . with ‹a#xs = as''›[THEN sym] ‹kind a = Q:r↪⇘p⇙fs› show ?thesis by simp qed next case 2 from vpa_Call have "as'' = [] ∧ a#as = as' ∨ (∃xs. a#xs = as'' ∧ as = xs@as')" by(simp add:Cons_eq_append_conv) thus ?case proof assume "as'' = [] ∧ a#as = as'" hence "as = []@tl as'" by(cases as') auto from IH2[OF this] have "valid_path_aux (upd_cs (a#cs) []) (tl as')" . with ‹as'' = [] ∧ a#as = as'› ‹kind a = Q:r↪⇘p⇙fs› show ?thesis by clarsimp next assume "∃xs. a#xs = as'' ∧ as = xs@as'" then obtain xs where "a#xs = as''" and "as = xs@as'" by auto from IH2[OF ‹as = xs@as'›] have "valid_path_aux (upd_cs (a # cs) xs) as'" . with ‹a#xs = as''›[THEN sym] ‹kind a = Q:r↪⇘p⇙fs› show ?thesis by simp qed } next case (vpa_ReturnEmpty cs a as Q p f as'') note IH1 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_aux [] xs› note IH2 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_aux (upd_cs [] xs) ys› { case 1 from vpa_ReturnEmpty have "as'' = [] ∧ a#as = as' ∨ (∃xs. a#xs = as'' ∧ as = xs@as')" by(simp add:Cons_eq_append_conv) thus ?case proof assume "as'' = [] ∧ a#as = as'" thus ?thesis by simp next assume "∃xs. a#xs = as'' ∧ as = xs@as'" then obtain xs where "a#xs = as''" and "as = xs@as'" by auto from IH1[OF ‹as = xs@as'›] have "valid_path_aux [] xs" . with ‹a#xs = as''›[THEN sym] ‹kind a = Q↩⇘p⇙f› ‹cs = []› show ?thesis by simp qed next case 2 from vpa_ReturnEmpty have "as'' = [] ∧ a#as = as' ∨ (∃xs. a#xs = as'' ∧ as = xs@as')" by(simp add:Cons_eq_append_conv) thus ?case proof assume "as'' = [] ∧ a#as = as'" hence "as = []@tl as'" by(cases as') auto from IH2[OF this] have "valid_path_aux [] (tl as')" by simp with ‹as'' = [] ∧ a#as = as'› ‹kind a = Q↩⇘p⇙f› ‹cs = []› show ?thesis by fastforce next assume "∃xs. a#xs = as'' ∧ as = xs@as'" then obtain xs where "a#xs = as''" and "as = xs@as'" by auto from IH2[OF ‹as = xs@as'›] have "valid_path_aux (upd_cs [] xs) as'" . from ‹a#xs = as''›[THEN sym] ‹kind a = Q↩⇘p⇙f› ‹cs = []› have "upd_cs [] xs = upd_cs cs as''" by simp with ‹valid_path_aux (upd_cs [] xs) as'› show ?thesis by simp qed } next case (vpa_ReturnCons cs a as Q p f c' cs' as'') note IH1 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_aux cs' xs› note IH2 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_aux (upd_cs cs' xs) ys› { case 1 from vpa_ReturnCons have "as'' = [] ∧ a#as = as' ∨ (∃xs. a#xs = as'' ∧ as = xs@as')" by(simp add:Cons_eq_append_conv) thus ?case proof assume "as'' = [] ∧ a#as = as'" thus ?thesis by simp next assume "∃xs. a#xs = as'' ∧ as = xs@as'" then obtain xs where "a#xs = as''" and "as = xs@as'" by auto from IH1[OF ‹as = xs@as'›] have "valid_path_aux cs' xs" . with ‹a#xs = as''›[THEN sym] ‹kind a = Q↩⇘p⇙f› ‹cs = c'#cs'› ‹a ∈ get_return_edges c'› show ?thesis by simp qed next case 2 from vpa_ReturnCons have "as'' = [] ∧ a#as = as' ∨ (∃xs. a#xs = as'' ∧ as = xs@as')" by(simp add:Cons_eq_append_conv) thus ?case proof assume "as'' = [] ∧ a#as = as'" hence "as = []@tl as'" by(cases as') auto from IH2[OF this] have "valid_path_aux (upd_cs cs' []) (tl as')" . with ‹as'' = [] ∧ a#as = as'› ‹kind a = Q↩⇘p⇙f› ‹cs = c'#cs'› ‹a ∈ get_return_edges c'› show ?thesis by fastforce next assume "∃xs. a#xs = as'' ∧ as = xs@as'" then obtain xs where "a#xs = as''" and "as = xs@as'" by auto from IH2[OF ‹as = xs@as'›] have "valid_path_aux (upd_cs cs' xs) as'" . from ‹a#xs = as''›[THEN sym] ‹kind a = Q↩⇘p⇙f› ‹cs = c'#cs'› have "upd_cs cs' xs = upd_cs cs as''" by simp with ‹valid_path_aux (upd_cs cs' xs) as'› show ?thesis by simp qed } qed simp_all lemma valid_path_aux_Append: "⟦valid_path_aux cs as; valid_path_aux (upd_cs cs as) as'⟧ ⟹ valid_path_aux cs (as@as')" by(induct rule:vpa_induct,auto simp:intra_kind_def) lemma vpa_snoc_Call: assumes "kind a = Q:r↪⇘p⇙fs" shows "valid_path_aux cs as ⟹ valid_path_aux cs (as@[a])" proof(induct rule:vpa_induct) case (vpa_empty cs) from ‹kind a = Q:r↪⇘p⇙fs› have "valid_path_aux cs [a]" by simp thus ?case by simp next case (vpa_intra cs a' as') from ‹valid_path_aux cs (as'@[a])› ‹intra_kind (kind a')› have "valid_path_aux cs (a'#(as'@[a]))" by(fastforce simp:intra_kind_def) thus ?case by simp next case (vpa_Call cs a' as' Q' r' p' fs') from ‹valid_path_aux (a'#cs) (as'@[a])› ‹kind a' = Q':r'↪⇘p'⇙fs'› have "valid_path_aux cs (a'#(as'@[a]))" by simp thus ?case by simp next case (vpa_ReturnEmpty cs a' as' Q' p' f') from ‹valid_path_aux [] (as'@[a])› ‹kind a' = Q'↩⇘p'⇙f'› ‹cs = []› have "valid_path_aux cs (a'#(as'@[a]))" by simp thus ?case by simp next case (vpa_ReturnCons cs a' as' Q' p' f' c' cs') from ‹valid_path_aux cs' (as'@[a])› ‹kind a' = Q'↩⇘p'⇙f'› ‹cs = c'#cs'› ‹a' ∈ get_return_edges c'› have "valid_path_aux cs (a'#(as'@[a]))" by simp thus ?case by simp qed definition valid_path :: "'edge list ⇒ bool" where "valid_path as ≡ valid_path_aux [] as" lemma valid_path_aux_valid_path: "valid_path_aux cs as ⟹ valid_path as" by(fastforce intro:valid_path_aux_callstack_prefix simp:valid_path_def) lemma valid_path_split: assumes "valid_path (as@as')" shows "valid_path as" and "valid_path as'" using ‹valid_path (as@as')› apply(auto simp:valid_path_def) apply(erule valid_path_aux_split) apply(drule valid_path_aux_split(2)) by(fastforce intro:valid_path_aux_callstack_prefix) definition valid_path' :: "'node ⇒ 'edge list ⇒ 'node ⇒ bool" ("_ -_→⇩_{√}* _" [51,0,0] 80) where vp_def:"n -as→⇩_{√}* n' ≡ n -as→* n' ∧ valid_path as" lemma intra_path_vp: assumes "n -as→⇩_{ι}* n'" shows "n -as→⇩_{√}* n'" proof - from ‹n -as→⇩_{ι}* n'› have "n -as→* n'" and "∀a ∈ set as. intra_kind(kind a)" by(simp_all add:intra_path_def) from ‹∀a ∈ set as. intra_kind(kind a)› have "valid_path_aux [] as" by(rule valid_path_aux_intra_path) thus ?thesis using ‹n -as→* n'› by(simp add:vp_def valid_path_def) qed lemma vp_split_Cons: assumes "n -as→⇩_{√}* n'" and "as ≠ []" obtains a' as' where "as = a'#as'" and "n = sourcenode a'" and "valid_edge a'" and "targetnode a' -as'→⇩_{√}* n'" proof(atomize_elim) from ‹n -as→⇩_{√}* n'› ‹as ≠ []› obtain a' as' where "as = a'#as'" and "n = sourcenode a'" and "valid_edge a'" and "targetnode a' -as'→* n'" by(fastforce elim:path_split_Cons simp:vp_def) from ‹n -as→⇩_{√}* n'› have "valid_path as" by(simp add:vp_def) from ‹as = a'#as'› have "as = [a']@as'" by simp with ‹valid_path as› have "valid_path ([a']@as')" by simp hence "valid_path as'" by(rule valid_path_split) with ‹targetnode a' -as'→* n'› have "targetnode a' -as'→⇩_{√}* n'" by(simp add:vp_def) with ‹as = a'#as'› ‹n = sourcenode a'› ‹valid_edge a'› show "∃a' as'. as = a'#as' ∧ n = sourcenode a' ∧ valid_edge a' ∧ targetnode a' -as'→⇩_{√}* n'" by blast qed lemma vp_split_snoc: assumes "n -as→⇩_{√}* n'" and "as ≠ []" obtains a' as' where "as = as'@[a']" and "n -as'→⇩_{√}* sourcenode a'" and "valid_edge a'" and "n' = targetnode a'" proof(atomize_elim) from ‹n -as→⇩_{√}* n'› ‹as ≠ []› obtain a' as' where "as = as'@[a']" and "n -as'→* sourcenode a'" and "valid_edge a'" and "n' = targetnode a'" by(clarsimp simp:vp_def)(erule path_split_snoc,auto) from ‹n -as→⇩_{√}* n'› ‹as = as'@[a']› have "valid_path (as'@[a'])" by(simp add:vp_def) hence "valid_path as'" by(rule valid_path_split) with ‹n -as'→* sourcenode a'› have "n -as'→⇩_{√}* sourcenode a'" by(simp add:vp_def) with ‹as = as'@[a']› ‹valid_edge a'› ‹n' = targetnode a'› show "∃as' a'. as = as'@[a'] ∧ n -as'→⇩_{√}* sourcenode a' ∧ valid_edge a' ∧ n' = targetnode a'" by blast qed lemma vp_split: assumes "n -as@a#as'→⇩_{√}* n'" shows "n -as→⇩_{√}* sourcenode a" and "valid_edge a" and "targetnode a -as'→⇩_{√}* n'" proof - from ‹n -as@a#as'→⇩_{√}* n'› have "n -as→* sourcenode a" and "valid_edge a" and "targetnode a -as'→* n'" by(auto intro:path_split simp:vp_def) from ‹n -as@a#as'→⇩_{√}* n'› have "valid_path (as@a#as')" by(simp add:vp_def) hence "valid_path as" and "valid_path (a#as')" by(auto intro:valid_path_split) from ‹valid_path (a#as')› have "valid_path ([a]@as')" by simp hence "valid_path as'" by(rule valid_path_split) with ‹n -as→* sourcenode a› ‹valid_path as› ‹valid_edge a› ‹targetnode a -as'→* n'› show "n -as→⇩_{√}* sourcenode a" "valid_edge a" "targetnode a -as'→⇩_{√}* n'" by(auto simp:vp_def) qed lemma vp_split_second: assumes "n -as@a#as'→⇩_{√}* n'" shows "sourcenode a -a#as'→⇩_{√}* n'" proof - from ‹n -as@a#as'→⇩_{√}* n'› have "sourcenode a -a#as'→* n'" by(fastforce elim:path_split_second simp:vp_def) from ‹n -as@a#as'→⇩_{√}* n'› have "valid_path (as@a#as')" by(simp add:vp_def) hence "valid_path (a#as')" by(rule valid_path_split) with ‹sourcenode a -a#as'→* n'› show ?thesis by(simp add:vp_def) qed function valid_path_rev_aux :: "'edge list ⇒ 'edge list ⇒ bool" where "valid_path_rev_aux cs [] ⟷ True" | "valid_path_rev_aux cs (as@[a]) ⟷ (case (kind a) of Q↩⇘p⇙f ⇒ valid_path_rev_aux (a#cs) as | Q:r↪⇘p⇙fs ⇒ case cs of [] ⇒ valid_path_rev_aux [] as | c'#cs' ⇒ c' ∈ get_return_edges a ∧ valid_path_rev_aux cs' as | _ ⇒ valid_path_rev_aux cs as)" by auto(case_tac b rule:rev_cases,auto) termination by lexicographic_order lemma vpra_induct [consumes 1,case_names vpra_empty vpra_intra vpra_Return vpra_CallEmpty vpra_CallCons]: assumes major: "valid_path_rev_aux xs ys" and rules: "⋀cs. P cs []" "⋀cs a as. ⟦intra_kind(kind a); valid_path_rev_aux cs as; P cs as⟧ ⟹ P cs (as@[a])" "⋀cs a as Q p f. ⟦kind a = Q↩⇘p⇙f; valid_path_rev_aux (a#cs) as; P (a#cs) as⟧ ⟹ P cs (as@[a])" "⋀cs a as Q r p fs. ⟦kind a = Q:r↪⇘p⇙fs; cs = []; valid_path_rev_aux [] as; P [] as⟧ ⟹ P cs (as@[a])" "⋀cs a as Q r p fs c' cs'. ⟦kind a = Q:r↪⇘p⇙fs; cs = c'#cs'; valid_path_rev_aux cs' as; c' ∈ get_return_edges a; P cs' as⟧ ⟹ P cs (as@[a])" shows "P xs ys" using major apply(induct ys arbitrary:xs rule:rev_induct) by(auto intro:rules split:edge_kind.split_asm list.split_asm simp:intra_kind_def) lemma vpra_callstack_prefix: "valid_path_rev_aux (cs@cs') as ⟹ valid_path_rev_aux cs as" proof(induct "cs@cs'" as arbitrary:cs cs' rule:vpra_induct) case vpra_empty thus ?case by simp next case (vpra_intra a as) hence "valid_path_rev_aux cs as" by simp with ‹intra_kind (kind a)› show ?case by(fastforce simp:intra_kind_def) next case (vpra_Return a as Q p f) note IH = ‹⋀ds ds'. a#cs@cs' = ds@ds' ⟹ valid_path_rev_aux ds as› have "a#cs@cs' = (a#cs)@cs'" by simp from IH[OF this] have "valid_path_rev_aux (a#cs) as" . with ‹kind a = Q↩⇘p⇙f› show ?case by simp next case (vpra_CallEmpty a as Q r p fs) hence "valid_path_rev_aux cs as" by simp with ‹kind a = Q:r↪⇘p⇙fs› ‹cs@cs' = []› show ?case by simp next case (vpra_CallCons a as Q r p fs c' csx) note IH = ‹⋀cs cs'. csx = cs@cs' ⟹ valid_path_rev_aux cs as› from ‹cs@cs' = c'#csx› have "(cs = [] ∧ cs' = c'#csx) ∨ (∃zs. cs = c'#zs ∧ zs@cs' = csx)" by(simp add:append_eq_Cons_conv) thus ?case proof assume "cs = [] ∧ cs' = c'#csx" hence "cs = []" and "cs' = c'#csx" by simp_all from ‹cs' = c'#csx› have "csx = []@tl cs'" by simp from IH[OF this] have "valid_path_rev_aux [] as" . with ‹cs = []› ‹kind a = Q:r↪⇘p⇙fs› show ?thesis by simp next assume "∃zs. cs = c'#zs ∧ zs@cs' = csx" then obtain zs where "cs = c'#zs" and "csx = zs@cs'" by auto from IH[OF ‹csx = zs@cs'›] have "valid_path_rev_aux zs as" . with ‹cs = c'#zs› ‹kind a = Q:r↪⇘p⇙fs› ‹c' ∈ get_return_edges a› show ?thesis by simp qed qed function upd_rev_cs :: "'edge list ⇒ 'edge list ⇒ 'edge list" where "upd_rev_cs cs [] = cs" | "upd_rev_cs cs (as@[a]) = (case (kind a) of Q↩⇘p⇙f ⇒ upd_rev_cs (a#cs) as | Q:r↪⇘p⇙fs ⇒ case cs of [] ⇒ upd_rev_cs cs as | c'#cs' ⇒ upd_rev_cs cs' as | _ ⇒ upd_rev_cs cs as)" by auto(case_tac b rule:rev_cases,auto) termination by lexicographic_order lemma upd_rev_cs_empty [dest]: "upd_rev_cs cs [] = [] ⟹ cs = []" by(cases cs) auto lemma valid_path_rev_aux_split: assumes "valid_path_rev_aux cs (as@as')" shows "valid_path_rev_aux cs as'" and "valid_path_rev_aux (upd_rev_cs cs as') as" using ‹valid_path_rev_aux cs (as@as')› proof(induct cs "as@as'" arbitrary:as as' rule:vpra_induct) case (vpra_intra cs a as as'') note IH1 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_rev_aux cs ys› note IH2 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_rev_aux (upd_rev_cs cs ys) xs› { case 1 from vpra_intra have "as' = [] ∧ as@[a] = as'' ∨ (∃xs. as = as''@xs ∧ xs@[a] = as')" by(cases as' rule:rev_cases) auto thus ?case proof assume "as' = [] ∧ as@[a] = as''" thus ?thesis by simp next assume "∃xs. as = as''@xs ∧ xs@[a] = as'" then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto from IH1[OF ‹as = as''@xs›] have "valid_path_rev_aux cs xs" . with ‹xs@[a] = as'› ‹intra_kind (kind a)› show ?thesis by(fastforce simp:intra_kind_def) qed next case 2 from vpra_intra have "as' = [] ∧ as@[a] = as'' ∨ (∃xs. as = as''@xs ∧ xs@[a] = as')" by(cases as' rule:rev_cases) auto thus ?case proof assume "as' = [] ∧ as@[a] = as''" hence "as = butlast as''@[]" by(cases as) auto from IH2[OF this] have "valid_path_rev_aux (upd_rev_cs cs []) (butlast as'')" . with ‹as' = [] ∧ as@[a] = as''› ‹intra_kind (kind a)› show ?thesis by(fastforce simp:intra_kind_def) next assume "∃xs. as = as''@xs ∧ xs@[a] = as'" then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto from IH2[OF ‹as = as''@xs›] have "valid_path_rev_aux (upd_rev_cs cs xs) as''" . from ‹xs@[a] = as'› ‹intra_kind (kind a)› have "upd_rev_cs cs xs = upd_rev_cs cs as'" by(fastforce simp:intra_kind_def) with ‹valid_path_rev_aux (upd_rev_cs cs xs) as''› show ?thesis by simp qed } next case (vpra_Return cs a as Q p f as'') note IH1 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_rev_aux (a#cs) ys› note IH2 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_rev_aux (upd_rev_cs (a#cs) ys) xs› { case 1 from vpra_Return have "as' = [] ∧ as@[a] = as'' ∨ (∃xs. as = as''@xs ∧ xs@[a] = as')" by(cases as' rule:rev_cases) auto thus ?case proof assume "as' = [] ∧ as@[a] = as''" thus ?thesis by simp next assume "∃xs. as = as''@xs ∧ xs@[a] = as'" then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto from IH1[OF ‹as = as''@xs›] have "valid_path_rev_aux (a#cs) xs" . with ‹xs@[a] = as'› ‹kind a = Q↩⇘p⇙f› show ?thesis by fastforce qed next case 2 from vpra_Return have "as' = [] ∧ as@[a] = as'' ∨ (∃xs. as = as''@xs ∧ xs@[a] = as')" by(cases as' rule:rev_cases) auto thus ?case proof assume "as' = [] ∧ as@[a] = as''" hence "as = butlast as''@[]" by(cases as) auto from IH2[OF this] have "valid_path_rev_aux (upd_rev_cs (a#cs) []) (butlast as'')" . with ‹as' = [] ∧ as@[a] = as''› ‹kind a = Q↩⇘p⇙f› show ?thesis by fastforce next assume "∃xs. as = as''@xs ∧ xs@[a] = as'" then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto from IH2[OF ‹as = as''@xs›] have "valid_path_rev_aux (upd_rev_cs (a#cs) xs) as''" . from ‹xs@[a] = as'› ‹kind a = Q↩⇘p⇙f› have "upd_rev_cs (a#cs) xs = upd_rev_cs cs as'" by fastforce with ‹valid_path_rev_aux (upd_rev_cs (a#cs) xs) as''› show ?thesis by simp qed } next case (vpra_CallEmpty cs a as Q r p fs as'') note IH1 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_rev_aux [] ys› note IH2 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_rev_aux (upd_rev_cs [] ys) xs› { case 1 from vpra_CallEmpty have "as' = [] ∧ as@[a] = as'' ∨ (∃xs. as = as''@xs ∧ xs@[a] = as')" by(cases as' rule:rev_cases) auto thus ?case proof assume "as' = [] ∧ as@[a] = as''" thus ?thesis by simp next assume "∃xs. as = as''@xs ∧ xs@[a] = as'" then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto from IH1[OF ‹as = as''@xs›] have "valid_path_rev_aux [] xs" . with ‹xs@[a] = as'› ‹kind a = Q:r↪⇘p⇙fs› ‹cs = []› show ?thesis by fastforce qed next case 2 from vpra_CallEmpty have "as' = [] ∧ as@[a] = as'' ∨ (∃xs. as = as''@xs ∧ xs@[a] = as')" by(cases as' rule:rev_cases) auto thus ?case proof assume "as' = [] ∧ as@[a] = as''" hence "as = butlast as''@[]" by(cases as) auto from IH2[OF this] have "valid_path_rev_aux (upd_rev_cs [] []) (butlast as'')" . with ‹as' = [] ∧ as@[a] = as''› ‹kind a = Q:r↪⇘p⇙fs› ‹cs = []› show ?thesis by fastforce next assume "∃xs. as = as''@xs ∧ xs@[a] = as'" then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto from IH2[OF ‹as = as''@xs›] have "valid_path_rev_aux (upd_rev_cs [] xs) as''" . with ‹xs@[a] = as'› ‹kind a = Q:r↪⇘p⇙fs› ‹cs = []› show ?thesis by fastforce qed } next case (vpra_CallCons cs a as Q r p fs c' cs' as'') note IH1 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_rev_aux cs' ys› note IH2 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_rev_aux (upd_rev_cs cs' ys) xs› { case 1 from vpra_CallCons have "as' = [] ∧ as@[a] = as'' ∨ (∃xs. as = as''@xs ∧ xs@[a] = as')" by(cases as' rule:rev_cases) auto thus ?case proof assume "as' = [] ∧ as@[a] = as''" thus ?thesis by simp next assume "∃xs. as = as''@xs ∧ xs@[a] = as'" then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto from IH1[OF ‹as = as''@xs›] have "valid_path_rev_aux cs' xs" . with ‹xs@[a] = as'› ‹kind a = Q:r↪⇘p⇙fs› ‹cs = c' # cs'› ‹c' ∈ get_return_edges a› show ?thesis by fastforce qed next case 2 from vpra_CallCons have "as' = [] ∧ as@[a] = as'' ∨ (∃xs. as = as''@xs ∧ xs@[a] = as')" by(cases as' rule:rev_cases) auto thus ?case proof assume "as' = [] ∧ as@[a] = as''" hence "as = butlast as''@[]" by(cases as) auto from IH2[OF this] have "valid_path_rev_aux (upd_rev_cs cs' []) (butlast as'')" . with ‹as' = [] ∧ as@[a] = as''› ‹kind a = Q:r↪⇘p⇙fs› ‹cs = c' # cs'› ‹c' ∈ get_return_edges a› show ?thesis by fastforce next assume "∃xs. as = as''@xs ∧ xs@[a] = as'" then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto from IH2[OF ‹as = as''@xs›] have "valid_path_rev_aux (upd_rev_cs cs' xs) as''" . with ‹xs@[a] = as'› ‹kind a = Q:r↪⇘p⇙fs› ‹cs = c' # cs'› ‹c' ∈ get_return_edges a› show ?thesis by fastforce qed } qed simp_all lemma valid_path_rev_aux_Append: "⟦valid_path_rev_aux cs as'; valid_path_rev_aux (upd_rev_cs cs as') as⟧ ⟹ valid_path_rev_aux cs (as@as')" by(induct rule:vpra_induct, auto simp:intra_kind_def simp del:append_assoc simp:append_assoc[THEN sym]) lemma vpra_Cons_intra: assumes "intra_kind(kind a)" shows "valid_path_rev_aux cs as ⟹ valid_path_rev_aux cs (a#as)" proof(induct rule:vpra_induct) case (vpra_empty cs) have "valid_path_rev_aux cs []" by simp with ‹intra_kind(kind a)› have "valid_path_rev_aux cs ([]@[a])" by(simp only:valid_path_rev_aux.simps intra_kind_def,fastforce) thus ?case by simp qed(simp only:append_Cons[THEN sym] valid_path_rev_aux.simps intra_kind_def,fastforce)+ lemma vpra_Cons_Return: assumes "kind a = Q↩⇘p⇙f" shows "valid_path_rev_aux cs as ⟹ valid_path_rev_aux cs (a#as)" proof(induct rule:vpra_induct) case (vpra_empty cs) from ‹kind a = Q↩⇘p⇙f› have "valid_path_rev_aux cs ([]@[a])" by(simp only:valid_path_rev_aux.simps,clarsimp) thus ?case by simp next case (vpra_intra cs a' as') from ‹valid_path_rev_aux cs (a#as')› ‹intra_kind (kind a')› have "valid_path_rev_aux cs ((a#as')@[a'])" by(simp only:valid_path_rev_aux.simps,fastforce simp:intra_kind_def) thus ?case by simp next case (vpra_Return cs a' as' Q' p' f') from ‹valid_path_rev_aux (a'#cs) (a#as')› ‹kind a' = Q'↩⇘p'⇙f'› have "valid_path_rev_aux cs ((a#as')@[a'])" by(simp only:valid_path_rev_aux.simps,clarsimp) thus ?case by simp next case (vpra_CallEmpty cs a' as' Q' r' p' fs') from ‹valid_path_rev_aux [] (a#as')› ‹kind a' = Q':r'↪⇘p'⇙fs'› ‹cs = []› have "valid_path_rev_aux cs ((a#as')@[a'])" by(simp only:valid_path_rev_aux.simps,clarsimp) thus ?case by simp next case (vpra_CallCons cs a' as' Q' r' p' fs' c' cs') from ‹valid_path_rev_aux cs' (a#as')› ‹kind a' = Q':r'↪⇘p'⇙fs'› ‹cs = c'#cs'› ‹c' ∈ get_return_edges a'› have "valid_path_rev_aux cs ((a#as')@[a'])" by(simp only:valid_path_rev_aux.simps,clarsimp) thus ?case by simp qed (*<*) lemmas append_Cons_rev = append_Cons[THEN sym] declare append_Cons [simp del] append_Cons_rev [simp] (*>*) lemma upd_rev_cs_Cons_intra: assumes "intra_kind(kind a)" shows "upd_rev_cs cs (a#as) = upd_rev_cs cs as" proof(induct as arbitrary:cs rule:rev_induct) case Nil from ‹intra_kind (kind a)› have "upd_rev_cs cs ([]@[a]) = upd_rev_cs cs []" by(simp only:upd_rev_cs.simps,auto simp:intra_kind_def) thus ?case by simp next case (snoc a' as') note IH = ‹⋀cs. upd_rev_cs cs (a#as') = upd_rev_cs cs as'› show ?case proof(cases "kind a'" rule:edge_kind_cases) case Intra from IH have "upd_rev_cs cs (a#as') = upd_rev_cs cs as'" . with Intra have "upd_rev_cs cs ((a#as')@[a']) = upd_rev_cs cs (as'@[a'])" by(fastforce simp:intra_kind_def) thus ?thesis by simp next case Return from IH have "upd_rev_cs (a'#cs) (a#as') = upd_rev_cs (a'#cs) as'" .