text:
(*
Copyright 2018

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
*)
theory readyqueues_push_back_mem
  imports tasks
begin

text \<open>Up to two locales per function in the binary.\<close>
locale readyqueues_push_back_function = tasks_context +
  fixes rsp\<^sub>0 rbp\<^sub>0 task a readyqueues_push_back_ret :: \<open>64 word\<close>
    and core_id :: \<open>32 word\<close>
    and v\<^sub>0 :: \<open>8 word\<close>
    and blocks :: \<open>(nat \<times> 64 word \<times> nat) set\<close>
  assumes seps: \<open>seps blocks\<close>
    and masters\<^sub>2:
      \<open>master blocks (a, 1) 0\<close>
      \<open>master blocks (rsp\<^sub>0, 8) 1\<close>
      \<open>master blocks (rsp\<^sub>0-8, 8) 2\<close>
      \<open>master blocks (rsp\<^sub>0-16, 8) 3\<close>
      \<open>master blocks (rsp\<^sub>0-28, 4) 4\<close>
      \<open>master blocks (rsp\<^sub>0-40, 8) 5\<close>
      \<open>master blocks (task + 41, 1) 6\<close> \<comment> \<open>\texttt{task->prio}\<close>
      \<open>master blocks (the (label_to_address assembly ''readyqueues'') + 24 + (ucast core_id + (ucast core_id << 3) << 6), 4) 7\<close>
    and ret_address: \<open>outside readyqueues_push_back_ret 464 649\<close> \<comment> \<open>Only works for non-recursive functions.\<close>
begin

text \<open>Need the exact format used in the below proofs, so doing this icky explicit simplification\<close>
lemma boffset_add_commute[simp]: \<open>x + boffset + y = boffset + (y + x)\<close>
  by simp
lemmas masters = masters\<^sub>2[simplified]
declare boffset_add_commute[simp del]

text \<open>
  The Floyd invariant expresses for some locations properties that are invariably true.
  Simply expresses that a byte in the memory remains untouched.
\<close>
definition pp_\<Theta> :: floyd_invar where
  \<open>pp_\<Theta> \<equiv> [
    \<comment> \<open>precondition\<close>
    boffset+464 \<mapsto> \<lambda>\<sigma>. regs \<sigma> rsp = rsp\<^sub>0
      \<and> regs \<sigma> rbp = rbp\<^sub>0
      \<and> \<langle>31,0\<rangle>regs \<sigma> rdi = core_id
      \<and> regs \<sigma> rsi = task
      \<and> \<sigma> \<turnstile> *[rsp\<^sub>0,8] = boffset+readyqueues_push_back_ret
      \<and> \<sigma> \<turnstile> *[a,1] = v\<^sub>0,
    boffset+555 \<mapsto> \<lambda>\<sigma>. regs \<sigma> rsp = rsp\<^sub>0-40
      \<and> regs \<sigma> rbp = rsp\<^sub>0-8
      \<and> \<sigma> \<turnstile> *[rsp\<^sub>0-8,8] = rbp\<^sub>0
      \<and> \<sigma> \<turnstile> *[rsp\<^sub>0-28,4] = core_id
      \<and> \<sigma> \<turnstile> *[rsp\<^sub>0-40,8] = task
      \<and> \<sigma> \<turnstile> *[rsp\<^sub>0,8] = boffset+readyqueues_push_back_ret
      \<and> \<sigma> \<turnstile> *[a,1] = v\<^sub>0,
    boffset+560 \<mapsto> \<lambda>\<sigma>. regs \<sigma> rsp = rsp\<^sub>0-40
      \<and> regs \<sigma> rbp = rsp\<^sub>0-8
      \<and> \<sigma> \<turnstile> *[rsp\<^sub>0-8,8] = rbp\<^sub>0
      \<and> \<sigma> \<turnstile> *[rsp\<^sub>0-28,4] = core_id
      \<and> \<sigma> \<turnstile> *[rsp\<^sub>0-40,8] = task
      \<and> \<sigma> \<turnstile> *[rsp\<^sub>0,8] = boffset+readyqueues_push_back_ret
      \<and> \<sigma> \<turnstile> *[a,1] = v\<^sub>0,
    \<comment> \<open>postcondition\<close>
    boffset+readyqueues_push_back_ret \<mapsto> \<lambda>\<sigma>. \<sigma> \<turnstile> *[a,1] = v\<^sub>0
      \<and> regs \<sigma> rsp = rsp\<^sub>0+8
      \<and> regs \<sigma> rbp = rbp\<^sub>0
  ]\<close>

text \<open>Adding some rules to the simplifier to simplify proofs.\<close>
schematic_goal pp_\<Theta>_zero[simp]:
  shows \<open>pp_\<Theta> boffset = ?x\<close>
  unfolding pp_\<Theta>_def
  by simp
schematic_goal pp_\<Theta>_numeral_l[simp]:
  shows \<open>pp_\<Theta> (n + boffset) = ?x\<close>
  unfolding pp_\<Theta>_def
  by simp
schematic_goal pp_\<Theta>_numeral_r[simp]:
  shows \<open>pp_\<Theta> (boffset + n) = ?x\<close>
  unfolding pp_\<Theta>_def
  by simp

end

locale readyqueues_push_back_function_calls = readyqueues_push_back_function +
  fixes task_list_push_back :: \<open>state \<Rightarrow> state\<close>
  assumes task_list_push_back_def: \<open>exec_instr assembly semantics tasks_flag_annotation (Unary (IS_8088 Call) (Immediate (ImmLabel ''task_list_push_back''))) 5 = task_list_push_back\<close>
    and task_list_push_back_incr: \<open>regs (task_list_push_back \<sigma>) rip = regs \<sigma> rip + 5\<close>
    and task_list_push_back555: \<open>the (pp_\<Theta> (boffset+555)) \<sigma> \<Longrightarrow> the (pp_\<Theta> (boffset+560)) (task_list_push_back \<sigma>)\<close>
begin

lemma rewrite_readyqueues_push_back_mem:
  \<open>is_std_invar readyqueues_push_back_ret (floyd.invar readyqueues_push_back_ret pp_\<Theta>)\<close>
  text \<open>Boilerplate code to start the VCG\<close>
  apply (rule floyd_invarI)
  apply (rewrite at \<open>floyd_vcs readyqueues_push_back_ret \<hole> _\<close> pp_\<Theta>_def)
  apply (intro floyd_vcsI)

  text \<open>Subgoal for rip = boffset+464\<close>
  subgoal premises prems for \<sigma>
    text \<open>Insert relevant knowledge\<close>
    apply (insert prems seps ret_address)
    text \<open>Apply VCG/symb.\ execution\<close>
    apply (restart_symbolic_execution?, (symbolic_execution masters: masters)+, (finish_symbolic_execution masters: masters)?)+
    done

  text \<open>Subgoal for rip = boffset+555\<close>
  subgoal premises prems for \<sigma>
    text \<open>Insert relevant knowledge\<close>
    apply (insert prems seps ret_address)
    text \<open>Discharge function call\<close>
    apply (rule wps_rls)
    apply (simp (no_asm_simp) add: lookup_table_def instr_index_def entry_size_def)
    apply (rewrite_one_let' add: assembly_def)
    apply (rewrite_one_let' add: task_list_push_back_def)
    apply (rule floyd_invarI'[of _ _ \<open>the (pp_\<Theta> (boffset+560))\<close>])
     apply (simp add: task_list_push_back_incr)
    using task_list_push_back555
    apply simp
    done

  text \<open>Subgoal for rip = boffset+560\<close>
  subgoal premises prems for \<sigma>
    text \<open>Insert relevant knowledge\<close>
    apply (insert prems seps ret_address)
    text \<open>Apply VCG/symb.\ execution\<close>
    apply (symbolic_execution masters: masters)+
    apply (finish_symbolic_execution masters: masters)
    done

  text \<open>Trivial ending subgoal.\<close>
  subgoal
    by simp
  done

end

end

author: ssrg-vt

repo: Luce-src

save_path: github-repos/isabelle/ssrg-vt-Luce-src


text:
theory VC4_to_mTSP_abs_old
  imports Main tsp.Misc tsp.Berge tsp.GraphExec
  "HOL-Data_Structures.Map_Specs" "HOL-Data_Structures.Set_Specs"
  tsp.CompleteGraph tsp.TravelingSalesman tsp.VertexCover
begin

(* OLD, NOT NEEDED; TODO: remove *)

(* ----- TODO ----- *)

text \<open>
({u,v},u,1) --- ({u,v},u,5) --- ({u,v},v,2)
     |                               |
({u,v},u,3) --- ({u,v},u,6) --- ({u,v},v,4)
     |                               |
({u,v},u,4) --- ({u,v},v,6) --- ({u,v},v,3)
     |                               |
({u,v},u,2) --- ({u,v},v,5) --- ({u,v},v,1)
\<close>

abbreviation "H\<^sub>e e \<equiv> (case e of uEdge u v \<Rightarrow>
  [((e,u,1::nat),[(e,u,3),(e,u,5)]),
  ((e,u,2),[(e,u,4),(e,v,5)]),
  ((e,u,3),[(e,u,1),(e,u,4),(e,u,6)]),
  ((e,u,4),[(e,u,2),(e,u,3),(e,v,6)]),
  ((e,u,5),[(e,u,1),(e,v,2)]),
  ((e,u,6),[(e,u,3),(e,v,4)]),
  ((e,v,1),[(e,v,3),(e,v,5)]),
  ((e,v,2),[(e,v,4),(e,u,5)]),
  ((e,v,3),[(e,v,1),(e,v,4),(e,v,6)]),
  ((e,v,4),[(e,v,2),(e,v,3),(e,u,6)]),
  ((e,v,5),[(e,v,1),(e,u,2)]),
  ((e,v,6),[(e,v,3),(e,u,4)])])"

abbreviation "Vs_H\<^sub>e e \<equiv> (case e of uEdge u v \<Rightarrow>
  [(e,u,1::nat),(e,u,2),(e,u,3),(e,u,4),(e,u,5),(e,u,6),
  (e,v,1),(e,v,2),(e,v,3),(e,v,4),(e,v,5),(e,v,6)])" \<comment> \<open>Vertices of a subgraph that corresponds to the edge \<open>e\<close>.\<close>

fun f_exec :: "'a graph_adj_list \<Rightarrow> ('a uedge \<times> 'a \<times> nat) graph_adj_list" where
  "f_exec G = (let V = concat (map Vs_H\<^sub>e (uedge_list G)) \<comment> \<open>Compute vertices of graph.\<close> in
    compl_graph_exec V) \<comment> \<open>Compute a complete graph for a given set of vertices.\<close>"

fun edge_in_He :: "'a graph_adj_list \<Rightarrow> ('a uedge \<times> 'a \<times> nat) uedge \<Rightarrow> bool" where \<comment> \<open>The function \<open>c\<close> gives the weights for the mTSP-instance \<open>f E\<close>.\<close>
  "edge_in_He G (uEdge (e,u,i) (f,v,j)) = undefined"

fun vertices_in_He :: "'a graph_adj_list \<Rightarrow> ('a uedge \<times> 'a \<times> nat) uedge \<Rightarrow> bool" where \<comment> \<open>The function \<open>c\<close> gives the weights for the mTSP-instance \<open>f E\<close>.\<close>
  "vertices_in_He G (uEdge (e,u,i) (f,v,j)) = undefined"

fun dist_in_He :: "'a uedge \<Rightarrow> ('a uedge \<times> 'a \<times> nat) \<Rightarrow> ('a uedge \<times> 'a \<times> nat) \<Rightarrow> int" where
  "dist_in_He e (e,u,i) (f,v,j) = min {length P | P. path (e,u,i) (H\<^sub>e e) (f,v,j)}" (* TODO: define path *)

fun c_exec :: "'a graph_adj_list \<Rightarrow> ('a uedge \<times> 'a \<times> nat) uedge \<Rightarrow> int" where \<comment> \<open>The function \<open>c\<close> gives the weights for the mTSP-instance \<open>f E\<close>.\<close>
  "c_exec G (uEdge (e,u,i) (f,v,j)) =
    (if edge_in_He G (uEdge (e,u,i) (f,v,j)) then 1
    else if vertices_in_He G (uEdge (e,u,i) (f,v,j)) then dist_in_He e (e,u,i) (f,v,j)
    else if u = v \<and> e \<noteq> f then 4
    else 5)"

fun split_list_at :: "'a list \<Rightarrow> 'a \<Rightarrow> ('a list \<times> 'a list) option" where
  "split_list_at [] y = None"
| "split_list_at (x#xs) y =
  (if x = y then Some ([],xs)
  else case split_list_at xs y of
    Some (xs\<^sub>1,xs\<^sub>2) \<Rightarrow> Some (x#xs\<^sub>1,xs\<^sub>2)
  | None \<Rightarrow> None)"

lemma "split_list_at xs y = Some (xs\<^sub>1,xs\<^sub>2) \<Longrightarrow> xs\<^sub>1 @ y#xs\<^sub>2 = xs"
  by (induction xs arbitrary: xs\<^sub>1 xs\<^sub>2) (auto split: if_splits option.splits)

fun rotate_tour_to :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list option" where
  "rotate_tour_to xs y = (case split_list_at xs y of
    Some (xs\<^sub>1,xs\<^sub>2) \<Rightarrow> Some (y#xs\<^sub>2 @ rev (butlast xs\<^sub>1) @ [y]) \<comment> \<open>x\<^sub>1,x\<^sub>2,\<dots>,x\<^sub>i,y,x\<^sub>i\<^sub>+\<^sub>1,\<dots>,x\<^sub>n,x\<^sub>1 \<mapsto> y,x\<^sub>i\<^sub>+\<^sub>1,\<dots>,x\<^sub>n,x\<^sub>1,x\<^sub>2,\<dots>,x\<^sub>i,y\<close>
  | None \<Rightarrow> None)"

lemma "rotate_tour_to xs y = Some xs' \<Longrightarrow> hd xs' = y"
  by (induction xs arbitrary: xs) (auto split: option.splits)

fun does_tour_contain_path :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
  "does_tour_contain_path T [] = True"
| "does_tour_contain_path T (v#P) = (case rotate_tour_to T v of
    Some T' \<Rightarrow> undefined
  | None \<Rightarrow> False)" (* TODO *)

fun g_exec :: "'a graph_adj_list \<Rightarrow> ('a uedge \<times> 'a \<times> nat) list \<Rightarrow> 'a set" where \<comment> \<open>The function \<open>g\<close> computes a VC4 solution, given a mTSP-solution.\<close>
  "g_exec G [] = {}"
| "g_exec G ((e,u,i)#T) =
  (if i = 1 \<or> i = 2 then {u} \<union> g_exec G (filter (\<lambda>(f,v,j). False)) T
  else undefined)"

section \<open>Properties of the Functions\<close>

lemma "Vs (uedges (f_exec G)) = {(uEdge u v,u,i) | u v i. {u,v} \<in> uedges G \<and> 1 \<le> i \<and> i \<le> 6}"
  sorry

lemma is_complete_exec: "is_complete (uedges (compl_graph_exec X))"
  sorry

lemma complete_f_exec: "is_complete (uedges (f_exec G))"
  apply (simp only: f_exec.simps Let_def)
  apply (rule is_complete_exec)
  sorry

section \<open>Reduction\<close>

abbreviation "c\<^sub>V\<^sub>C\<^sub>4 \<equiv> \<lambda>X. int (card X)" \<comment> \<open>Cost-function for the VC4 problem: cardinatlity of the vertex cover.\<close>

locale VC4_to_mTSP_abs1 =
  VC4: graph_adj_list Es +
  mTSP: metric_graph_adj_list Hs c for Es :: "'a graph_adj_list" and Hs :: "'b graph_adj_list" and c :: "'b \<times> 'b \<Rightarrow> int" +
  fixes g :: "'b list \<Rightarrow> 'a set"
    and OPT\<^sub>m\<^sub>T\<^sub>S\<^sub>P OPT\<^sub>V\<^sub>C\<^sub>4 and c\<^sub>m\<^sub>T\<^sub>S\<^sub>P :: "'b list \<Rightarrow> int"
  defines "c\<^sub>m\<^sub>T\<^sub>S\<^sub>P T \<equiv> cost_of_path (\<lambda>u v. c (u,v)) T" \<comment> \<open>Cost-function for the mTSP problem: cost of the Hamiltonian cycle.\<close>
  \<comment> \<open>Assumptions about the VC4 problem instance.\<close>
  assumes max_deg_leq_4: "\<And>v. v \<in> Vs VC4.E \<Longrightarrow> degree VC4.E v \<le> 4"
    and opt_vc4: "is_min_vc VC4.E OPT\<^sub>V\<^sub>C\<^sub>4"
    \<comment> \<open>Assumptions about the mTSP problem instance.\<close>
    and opt_mtsp: "is_tsp mTSP.E (\<lambda>u v. c (u,v)) OPT\<^sub>m\<^sub>T\<^sub>S\<^sub>P"
    \<comment> \<open>Assumptions about the relationship of the two graph-problem instances\<close>
    and cost_opt_mtsp_leq: "c\<^sub>m\<^sub>T\<^sub>S\<^sub>P OPT\<^sub>m\<^sub>T\<^sub>S\<^sub>P \<le> 15 * card VC4.E + c\<^sub>V\<^sub>C\<^sub>4 OPT\<^sub>V\<^sub>C\<^sub>4"
    and vc_of_tour: "\<And>T. is_hc mTSP.E T \<Longrightarrow> \<exists>k. c\<^sub>m\<^sub>T\<^sub>S\<^sub>P T = 15 * card VC4.E + k \<and> is_vc VC4.E (g T) \<and> c\<^sub>V\<^sub>C\<^sub>4 (g T) \<le> k"
begin

(* ----- 1st condition for a L-reduction ----- *)

lemma l_reduction1: "c\<^sub>m\<^sub>T\<^sub>S\<^sub>P OPT\<^sub>m\<^sub>T\<^sub>S\<^sub>P \<le> 61 * c\<^sub>V\<^sub>C\<^sub>4 OPT\<^sub>V\<^sub>C\<^sub>4"
proof -
  have "is_vc VC4.E OPT\<^sub>V\<^sub>C\<^sub>4"
    using opt_vc4 by (elim is_min_vcE)
  hence cardE_leq: "card VC4.E \<le> 4 * card OPT\<^sub>V\<^sub>C\<^sub>4"
    using max_deg_leq_4 by (auto intro: VC4.vc_card_E_leq_max_degree simp: numeral_eq_enat)
  thus ?thesis
    using cost_opt_mtsp_leq by (auto simp: c\<^sub>m\<^sub>T\<^sub>S\<^sub>P_def)
qed

(* ----- 2nd condition for a L-reduction ----- *)

lemma g_feasible_solution: "is_hc mTSP.E T \<Longrightarrow> is_vc VC4.E (g T)"
  using vc_of_tour by auto

lemma l_reduction2:
  assumes "is_hc mTSP.E T"
  shows "\<bar> c\<^sub>V\<^sub>C\<^sub>4 (g T) - c\<^sub>V\<^sub>C\<^sub>4 OPT\<^sub>V\<^sub>C\<^sub>4 \<bar> \<le> 1 * \<bar> c\<^sub>m\<^sub>T\<^sub>S\<^sub>P T - c\<^sub>m\<^sub>T\<^sub>S\<^sub>P OPT\<^sub>m\<^sub>T\<^sub>S\<^sub>P \<bar>"
proof -
  obtain k where cost_T: "c\<^sub>m\<^sub>T\<^sub>S\<^sub>P T = 15 * card VC4.E + k" and "is_vc VC4.E (g T)" "c\<^sub>V\<^sub>C\<^sub>4 (g T) \<le> k"
    using assms vc_of_tour by auto
  moreover hence opt_vc4_leq: "c\<^sub>V\<^sub>C\<^sub>4 OPT\<^sub>V\<^sub>C\<^sub>4 \<le> c\<^sub>V\<^sub>C\<^sub>4 (g T)"
    using opt_vc4 by (auto elim: is_min_vcE)
  ultimately show ?thesis
    using cost_T cost_opt_mtsp_leq by auto
qed

end

locale VC4_to_mTSP_abs2 =
  VC4: graph_adj_list Es for Es :: "'a graph_adj_list" +
  fixes OPT\<^sub>V\<^sub>C\<^sub>4
  assumes max_deg_leq_4: "\<And>v. v \<in> Vs VC4.E \<Longrightarrow> degree VC4.E v \<le> 4"
    and opt_vc4: "is_min_vc VC4.E OPT\<^sub>V\<^sub>C\<^sub>4"
begin

definition "Hs \<equiv> f_exec Es"

lemma irrefl_H: "v \<notin> ls_set (\<N> Hs v)"
  sorry

lemma sym_H: "u \<in> lset_set (\<N> Hs v) \<Longrightarrow> v \<in> lset_set (\<N> Hs u)"
  sorry

lemma graph_H: "graph_list_invar Hs"
  using irrefl_H sym_H by (auto intro: graph_list_invarI)

sublocale mTSP: graph_adj_list Hs
  using graph_H by unfold_locales

abbreviation "c\<^sub>m\<^sub>T\<^sub>S\<^sub>P \<equiv> \<lambda>T. cost_of_path (\<lambda>u v. c_exec Es (u,v)) T"

lemma complete_H: "is_complete mTSP.E"
  unfolding mTSP.E_def3 unfolding Hs_def by (rule complete_f_exec)

lemma costs_positive_dc: "c_exec Es e > 0"
  sorry

lemma tri_ineq_dc:
  "u \<in> Vs mTSP.E \<Longrightarrow> v \<in> Vs mTSP.E \<Longrightarrow> w \<in> Vs mTSP.E \<Longrightarrow> c_exec Es (u,w) \<le> c_exec Es (u,v) + c_exec Es (v,w)"
  sorry

sublocale mTSP': metric_graph_adj_list Hs "c_exec Es"
  using complete_H costs_positive_dc tri_ineq_dc by unfold_locales

definition "g T \<equiv> g_exec Es T"

lemma cost_opt_mtsp_leq:
  assumes opt_mtsp: "is_tsp mTSP.E (\<lambda>u v. c_exec Es (u,v)) OPT\<^sub>m\<^sub>T\<^sub>S\<^sub>P"
  shows "c\<^sub>m\<^sub>T\<^sub>S\<^sub>P OPT\<^sub>m\<^sub>T\<^sub>S\<^sub>P \<le> int (15 * card VC4.E) + int (card OPT\<^sub>V\<^sub>C\<^sub>4)"
  sorry

lemma vc_of_tour:
  assumes "is_hc mTSP.E T"
  shows "\<exists>k. c\<^sub>m\<^sub>T\<^sub>S\<^sub>P T = 15 * card VC4.E + k \<and> is_vc VC4.E (g T) \<and> c\<^sub>V\<^sub>C\<^sub>4 (g T) \<le> k"
  sorry

lemma l_reduction1:
  assumes "is_tsp mTSP.E (\<lambda>u v. c_exec Es (u,v)) OPT\<^sub>m\<^sub>T\<^sub>S\<^sub>P"
  shows "c\<^sub>m\<^sub>T\<^sub>S\<^sub>P OPT\<^sub>m\<^sub>T\<^sub>S\<^sub>P \<le> 61 * c\<^sub>V\<^sub>C\<^sub>4 OPT\<^sub>V\<^sub>C\<^sub>4"
  apply (rule VC4_to_mTSP_abs1.l_reduction1)
  using assms max_deg_leq_4 opt_vc4 cost_opt_mtsp_leq vc_of_tour
  apply unfold_locales
  apply auto
  sorry

lemma g_feasible_solution:
  assumes "is_hc mTSP.E T"
  shows "is_vc VC4.E (g T)"
  using assms vc_of_tour by auto

lemma l_reduction2:
  assumes "is_tsp mTSP.E (\<lambda>u v. c_exec Es (u,v)) OPT\<^sub>m\<^sub>T\<^sub>S\<^sub>P"
      and "is_hc mTSP.E T"
  shows "\<bar> c\<^sub>V\<^sub>C\<^sub>4 (g T) - c\<^sub>V\<^sub>C\<^sub>4 OPT\<^sub>V\<^sub>C\<^sub>4 \<bar> \<le> 1 * \<bar> c\<^sub>m\<^sub>T\<^sub>S\<^sub>P T - c\<^sub>m\<^sub>T\<^sub>S\<^sub>P OPT\<^sub>m\<^sub>T\<^sub>S\<^sub>P \<bar>"
  apply (rule VC4_to_mTSP_abs1.l_reduction2)
  using assms max_deg_leq_4 opt_vc4 cost_opt_mtsp_leq vc_of_tour
  apply unfold_locales
  using assms apply auto
  done

end

abbreviation "uf_exec Es \<equiv> (uedges o f_exec) Es"

(* ----- 1st condition for a L-reduction ----- *)

lemma l_reduction1:
  assumes "\<And>v. v \<in> Vs (uedges Es) \<Longrightarrow> degree (uedges Es) v \<le> 4"
      and "is_min_vc (uedges Es) OPT\<^sub>V\<^sub>C\<^sub>4"
      and "is_tsp (uedges (f_exec Es)) (\<lambda>u v. c_exec Es (u,v)) OPT\<^sub>m\<^sub>T\<^sub>S\<^sub>P"
      and "is_hc (uedges (f_exec Es)) T"
  shows "cost_of_path (\<lambda>u v. c_exec Es (u,v)) OPT\<^sub>m\<^sub>T\<^sub>S\<^sub>P \<le> 61 * c\<^sub>V\<^sub>C\<^sub>4 OPT\<^sub>V\<^sub>C\<^sub>4"
  apply (rule VC4_to_mTSP_abs2.l_reduction1)
  using assms apply unfold_locales

  sorry

(* ----- 2nd condition for a L-reduction ----- *)

lemma g_feasible_solution:
  assumes "is_hc (uf_exec Es) T"
  shows "is_vc (uedges Es) (g_exec Es T)"
  sorry

lemma l_reduction2:
  assumes "is_min_vc (uedges Es) OPT\<^sub>V\<^sub>C\<^sub>4"
    and "is_tsp (uf_exec Es) (\<lambda>u v. c_exec Es (u,v)) OPT\<^sub>m\<^sub>T\<^sub>S\<^sub>P"
    and "is_hc (uf_exec Es) T"
  shows "\<bar> c\<^sub>V\<^sub>C\<^sub>4 (g_exec Es T) - c\<^sub>V\<^sub>C\<^sub>4 OPT\<^sub>V\<^sub>C\<^sub>4 \<bar> \<le> 1 * \<bar> cost_of_path (\<lambda>u v. c_exec Es (u,v)) T - cost_of_path (\<lambda>u v. c_exec Es (u,v)) OPT\<^sub>m\<^sub>T\<^sub>S\<^sub>P \<bar>"
  sorry

(* ----- TODO ----- *)

text \<open>
({u,v},u,1) --- ({u,v},u,5) --- ({u,v},v,2)
     |                               |
({u,v},u,3) --- ({u,v},u,6) --- ({u,v},v,4)
     |                               |
({u,v},u,4) --- ({u,v},v,6) --- ({u,v},v,3)
     |                               |
({u,v},u,2) --- ({u,v},v,5) --- ({u,v},v,1)
\<close>

definition "H\<^sub>e u v \<equiv> (let e = {u,v} in
  {{(e,u,1::nat),(e,u,3)},
  {(e,u,1),(e,u,5)},
  {(e,u,2),(e,u,4)},
  {(e,u,2),(e,v,5)},
  {(e,u,3),(e,u,4)},
  {(e,u,3),(e,u,6)},
  {(e,u,4),(e,v,6)},

  {(e,v,1::nat),(e,v,3)},
  {(e,v,1),(e,v,5)},
  {(e,v,2),(e,v,4)},
  {(e,v,2),(e,u,5)},
  {(e,v,3),(e,v,4)},
  {(e,v,3),(e,v,6)},
  {(e,v,4),(e,u,6)}})"

abbreviation "H E \<equiv> \<Union> {H\<^sub>e u v | u v. {u,v} \<in> E}"

definition "f E \<equiv> (let V\<^sub>H = Vs (H E) in complete_graph V\<^sub>H)"

locale VC4_to_mTSP_abs2 =
  graph_abs E for E :: "'a set set" +
  fixes f :: "'a set set \<Rightarrow> ('a set \<times> 'a \<times> nat) set set" \<comment> \<open>Given a VC4-instance, the function \<open>f\<close> constructs the graph for a mTSP-instance.\<close>
    and c :: "('a set \<times> 'a \<times> nat) set \<Rightarrow> nat" \<comment> \<open>The function \<open>c\<close> gives the weights for the mTSP-instance \<open>f E\<close>.\<close>
    and g :: "('a set \<times> 'a \<times> nat) list \<Rightarrow> 'a set" \<comment> \<open>The function \<open>g\<close> computes a VC4 solution, given a mTSP-solution.\<close>
  assumes fE_complete: "is_complete (f E)"
      and pos_costs: "\<And>e'. e' \<in> f E \<Longrightarrow> c e' \<ge> 0"
      and c_tri_ineq: "\<And>u v w. u \<in> Vs (f E) \<Longrightarrow> v \<in> Vs (f E) \<Longrightarrow> w \<in> Vs (f E)
        \<Longrightarrow> c {u,w} \<le> c {u,v} + c {v,w}"
      \<comment> \<open>Assumptions needed for the Reduction.\<close>
      and cost_1: "\<And>u v x y. {u,v} \<in> E \<Longrightarrow> {x,y} \<in> H\<^sub>e u v \<Longrightarrow> c {x,y} = 1"
      and cost_dist: "\<And>u v x y. {u,v} \<in> E \<Longrightarrow> x \<in> Vs (H\<^sub>e u v) \<Longrightarrow> y \<in> Vs (H\<^sub>e u v) \<Longrightarrow> {x,y} \<notin>  H\<^sub>e u v
        \<Longrightarrow> c {u',v'} = distH\<^sub>e u' v'" (* TODO: How to define distance measure? *)
      and cost_4: "\<And>e\<^sub>1 e\<^sub>2 v i j x y. x = (e\<^sub>1,v,i) \<Longrightarrow> x = (e\<^sub>2,v,j) \<Longrightarrow> c {x,y} = 4"
      and cost_5: "\<And>e\<^sub>1 e\<^sub>2 v i j x y. False \<Longrightarrow> c {x,y} = 5" (* TODO: How to easily formalize 'otherwise'? *)
begin

abbreviation "H \<equiv> f E"

abbreviation "c\<^sub>m\<^sub>T\<^sub>S\<^sub>P \<equiv> \<lambda>T. int (cost_of_path c T)"
abbreviation "c\<^sub>V\<^sub>C\<^sub>4 \<equiv> \<lambda>X. int (card X)"

lemma
  assumes "is_vc E X"
  obtains T where "is_hc H T" "cost_of_path c T = 15 * card E + card X"
  sorry
  (* TODO: How do I obtain a partition of E? \<rightarrow> executable graph model! *)

lemma
  assumes opt_vc: "is_min_vc E OPT\<^sub>V\<^sub>C"
      and opt_mtsp: "is_tsp H c OPT\<^sub>m\<^sub>T\<^sub>S\<^sub>P"
  shows "cost_of_path c OPT\<^sub>m\<^sub>T\<^sub>S\<^sub>P \<le> 15 * card E + card OPT\<^sub>V\<^sub>C"
  sorry

lemma
  assumes "is_hc H T"
  obtains u P v where "is_hp H u P v" "cost_of_path c P \<le> 0"
  sorry (* TODO: How do I formalize: contains a Hamiltonian path of each subgraph H\<^sub>e? *)

lemma
  assumes "is_hc H T" "cost_of_path c T = 15 * card E + k"
  obtains X where "is_vc E X" "card x = k"
  sorry

end

(* ----- 1st condition for a L-reduction ----- *)

lemma l_reduction1:
  assumes opt_vc: "is_min_vc E OPT\<^sub>V\<^sub>C"
      and opt_mtsp: "is_tsp H c OPT\<^sub>m\<^sub>T\<^sub>S\<^sub>P"
  shows "cost_of_path c OPT\<^sub>m\<^sub>T\<^sub>S\<^sub>P \<le> 61 * card OPT\<^sub>V\<^sub>C" (is "?c' OPT\<^sub>m\<^sub>T\<^sub>S\<^sub>P \<le> ?\<alpha> * ?c OPT\<^sub>V\<^sub>C")
  sorry

(* ----- 2nd condition for a L-reduction ----- *)

text \<open>The function \<open>g\<close> maps a feasible solution of mTSP to a feasible solution of VC4.\<close>
lemma
  assumes "is_hc H T"
  shows "is_vc E (g T)"
  sorry

lemma l_reduction2:
  assumes opt_vc: "is_min_vc E OPT\<^sub>V\<^sub>C"
      and opt_mtsp: "is_tsp H c OPT\<^sub>m\<^sub>T\<^sub>S\<^sub>P"
      and "is_hc H T"
  shows "\<bar> c\<^sub>m\<^sub>T\<^sub>S\<^sub>P (g T) - c\<^sub>m\<^sub>T\<^sub>S\<^sub>P OPT\<^sub>V\<^sub>C \<bar> \<le> 1 * \<bar> c\<^sub>m\<^sub>T\<^sub>S\<^sub>P T - c\<^sub>m\<^sub>T\<^sub>S\<^sub>P OPT\<^sub>m\<^sub>T\<^sub>S\<^sub>P \<bar>"
  sorry

end

end

author: kollerlukas

repo: tsp

save_path: github-repos/isabelle/kollerlukas-tsp


text:
(*****************************************************************************
 * Featherweight-OCL --- A Formal Semantics for UML-OCL Version OCL 2.5
 *                       for the OMG Standard.
 *                       http://www.brucker.ch/projects/hol-testgen/
 *
 * UML_Contracts.thy ---
 * This file is part of HOL-TestGen.
 *
 * Copyright (c) 2013-2015 Université Paris-Saclay, Univ. Paris-Sud, France
 *               2013-2015 IRT SystemX, France
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 ******************************************************************************)

theory UML_Contracts
imports UML_State
begin

text\<open>Modeling of an operation contract for an operation  with 2 arguments,
       (so depending on three parameters if one takes "self" into account).\<close>

locale contract_scheme =
   fixes f_\<upsilon>
   fixes f_lam
   fixes f   :: "('\<AA>,'\<alpha>0::null)val \<Rightarrow>
                 'b \<Rightarrow>
                  ('\<AA>,'res::null)val"
   fixes PRE
   fixes POST
   assumes def_scheme': "f self x \<equiv>  (\<lambda> \<tau>. SOME res. let res = \<lambda> _. res in
                                           if (\<tau> \<Turnstile> (\<delta> self)) \<and> f_\<upsilon> x \<tau>
                                           then (\<tau> \<Turnstile> PRE self x) \<and>
                                                (\<tau> \<Turnstile> POST self x res)
                                           else \<tau> \<Turnstile> res \<triangleq> invalid)"
   assumes all_post': "\<forall> \<sigma> \<sigma>' \<sigma>''. ((\<sigma>,\<sigma>') \<Turnstile> PRE self x) = ((\<sigma>,\<sigma>'') \<Turnstile> PRE self x)"
           (* PRE is really a pre-condition semantically,
              i.e. it does not depend on the post-state. ... *)
   assumes cp\<^sub>P\<^sub>R\<^sub>E': "PRE (self) x \<tau> = PRE (\<lambda> _. self \<tau>) (f_lam x \<tau>) \<tau> "
           (* this interface is preferable than :
              assumes "cp self' \<Longrightarrow> cp a1' \<Longrightarrow> cp a2' \<Longrightarrow> cp (\<lambda>X. PRE (self' X) (a1' X) (a2' X) )"
              which is too polymorphic. *)
   assumes cp\<^sub>P\<^sub>O\<^sub>S\<^sub>T':"POST (self) x (res) \<tau> = POST (\<lambda> _. self \<tau>) (f_lam x \<tau>) (\<lambda> _. res \<tau>) \<tau>"
   assumes f_\<upsilon>_val: "\<And>a1. f_\<upsilon> (f_lam a1 \<tau>) \<tau> = f_\<upsilon> a1 \<tau>"
begin
   lemma strict0 [simp]: "f invalid X = invalid"
   by(rule ext, rename_tac "\<tau>", simp add: def_scheme' StrongEq_def OclValid_def false_def true_def)

   lemma nullstrict0[simp]: "f null X = invalid"
   by(rule ext, rename_tac "\<tau>", simp add: def_scheme' StrongEq_def OclValid_def false_def true_def)

   lemma cp0 : "f self a1 \<tau> = f (\<lambda> _. self \<tau>) (f_lam a1 \<tau>) \<tau>"
   proof -
      have A: "(\<tau> \<Turnstile> \<delta> (\<lambda>_. self \<tau>)) = (\<tau> \<Turnstile> \<delta> self)" by(simp add: OclValid_def cp_defined[symmetric])
      have B: "f_\<upsilon> (f_lam a1 \<tau>) \<tau> = f_\<upsilon> a1 \<tau>" by (rule f_\<upsilon>_val)
      have D: "(\<tau> \<Turnstile> PRE (\<lambda>_. self \<tau>) (f_lam a1 \<tau>)) = ( \<tau> \<Turnstile> PRE self a1 )"
                                                 by(simp add: OclValid_def cp\<^sub>P\<^sub>R\<^sub>E'[symmetric])
      show ?thesis
        apply(auto simp: def_scheme' A B D)
        apply(simp add: OclValid_def)
        by(subst cp\<^sub>P\<^sub>O\<^sub>S\<^sub>T', simp)
      qed

   theorem unfold' :
      assumes context_ok:    "cp E"
      and args_def_or_valid: "(\<tau> \<Turnstile> \<delta> self) \<and> f_\<upsilon> a1 \<tau>"
      and pre_satisfied:     "\<tau> \<Turnstile> PRE self a1"
      and post_satisfiable:  " \<exists>res. (\<tau> \<Turnstile> POST self a1 (\<lambda> _. res))"
      and sat_for_sols_post: "(\<And>res. \<tau> \<Turnstile> POST self a1 (\<lambda> _. res)  \<Longrightarrow> \<tau> \<Turnstile> E (\<lambda> _. res))"
      shows                  "\<tau> \<Turnstile> E(f self a1)"
   proof -
      have cp0: "\<And> X \<tau>. E X \<tau> = E (\<lambda>_. X \<tau>) \<tau>" by(insert context_ok[simplified cp_def], auto)
      show ?thesis
         apply(simp add: OclValid_def, subst cp0, fold OclValid_def)
         apply(simp add:def_scheme' args_def_or_valid pre_satisfied)
         apply(insert post_satisfiable, elim exE)
         apply(rule Hilbert_Choice.someI2, assumption)
         by(rule sat_for_sols_post, simp)
   qed

   lemma unfold2' :
      assumes context_ok:      "cp E"
      and args_def_or_valid:   "(\<tau> \<Turnstile> \<delta> self) \<and> (f_\<upsilon> a1 \<tau>)"
      and pre_satisfied:       "\<tau> \<Turnstile> PRE self a1"
      and postsplit_satisfied: "\<tau> \<Turnstile> POST' self a1" (* split constraint holds on post-state *)
      and post_decomposable  : "\<And> res. (POST self a1 res) =
                                       ((POST' self a1)  and (res \<triangleq> (BODY self a1)))"
      shows "(\<tau> \<Turnstile> E(f self a1)) = (\<tau> \<Turnstile> E(BODY self a1))"
   proof -
      have cp0: "\<And> X \<tau>. E X \<tau> = E (\<lambda>_. X \<tau>) \<tau>" by(insert context_ok[simplified cp_def], auto)
      show ?thesis
         apply(simp add: OclValid_def, subst cp0, fold OclValid_def)
         apply(simp add:def_scheme' args_def_or_valid pre_satisfied
                        post_decomposable postsplit_satisfied foundation10')
         apply(subst some_equality)
         apply(simp add: OclValid_def StrongEq_def true_def)+
         by(subst (2) cp0, rule refl)
   qed
end

locale contract0 =
   fixes f   :: "('\<AA>,'\<alpha>0::null)val \<Rightarrow>
                  ('\<AA>,'res::null)val"
   fixes PRE
   fixes POST
   assumes def_scheme: "f self \<equiv>  (\<lambda> \<tau>. SOME res. let res = \<lambda> _. res in
                                        if (\<tau> \<Turnstile> (\<delta> self))
                                        then (\<tau> \<Turnstile> PRE self) \<and>
                                             (\<tau> \<Turnstile> POST self res)
                                        else \<tau> \<Turnstile> res \<triangleq> invalid)"
   assumes all_post: "\<forall> \<sigma> \<sigma>' \<sigma>''. ((\<sigma>,\<sigma>') \<Turnstile> PRE self) = ((\<sigma>,\<sigma>'') \<Turnstile> PRE self)"
           (* PRE is really a pre-condition semantically,
              i.e. it does not depend on the post-state. ... *)
   assumes cp\<^sub>P\<^sub>R\<^sub>E: "PRE (self)  \<tau> = PRE (\<lambda> _. self \<tau>) \<tau> "
           (* this interface is preferable than :
              assumes "cp self' \<Longrightarrow> cp a1' \<Longrightarrow> cp a2' \<Longrightarrow> cp (\<lambda>X. PRE (self' X) (a1' X) (a2' X) )"
              which is too polymorphic. *)
   assumes cp\<^sub>P\<^sub>O\<^sub>S\<^sub>T:"POST (self) (res) \<tau> = POST (\<lambda> _. self \<tau>) (\<lambda> _. res \<tau>) \<tau>"

sublocale contract0 < contract_scheme "\<lambda>_ _. True" "\<lambda>x _. x" "\<lambda>x _. f x" "\<lambda>x _. PRE x" "\<lambda>x _. POST x"
 apply(unfold_locales)
     apply(simp add: def_scheme, rule all_post, rule cp\<^sub>P\<^sub>R\<^sub>E, rule cp\<^sub>P\<^sub>O\<^sub>S\<^sub>T)
by simp

context contract0
begin
   lemma cp_pre: "cp self' \<Longrightarrow>  cp (\<lambda>X. PRE (self' X)  )"
   by(rule_tac f=PRE in cpI1, auto intro: cp\<^sub>P\<^sub>R\<^sub>E)

   lemma cp_post: "cp self' \<Longrightarrow> cp res'  \<Longrightarrow> cp (\<lambda>X. POST (self' X) (res' X))"
   by(rule_tac f=POST in cpI2, auto intro: cp\<^sub>P\<^sub>O\<^sub>S\<^sub>T)

   lemma cp [simp]:  "cp self' \<Longrightarrow>  cp res' \<Longrightarrow> cp (\<lambda>X. f (self' X) )"
      by(rule_tac f=f in cpI1, auto intro:cp0)

   lemmas unfold = unfold'[simplified]

   lemma unfold2 :
      assumes                  "cp E"
      and                      "(\<tau> \<Turnstile> \<delta> self)"
      and                      "\<tau> \<Turnstile> PRE self"
      and                      "\<tau> \<Turnstile> POST' self" (* split constraint holds on post-state *)
      and                      "\<And> res. (POST self res) =
                                       ((POST' self)  and (res \<triangleq> (BODY self)))"
      shows "(\<tau> \<Turnstile> E(f self)) = (\<tau> \<Turnstile> E(BODY self))"
        apply(rule unfold2'[simplified])
      by((rule assms)+)

end

locale contract1 =
   fixes f   :: "('\<AA>,'\<alpha>0::null)val \<Rightarrow>
                  ('\<AA>,'\<alpha>1::null)val \<Rightarrow>
                  ('\<AA>,'res::null)val"
   fixes PRE
   fixes POST
   assumes def_scheme: "f self a1 \<equiv>
                               (\<lambda> \<tau>. SOME res. let res = \<lambda> _. res in
                                     if (\<tau> \<Turnstile> (\<delta> self)) \<and>  (\<tau> \<Turnstile> \<upsilon> a1)
                                     then (\<tau> \<Turnstile> PRE self a1) \<and>
                                          (\<tau> \<Turnstile> POST self a1 res)
                                     else \<tau> \<Turnstile> res \<triangleq> invalid) "
   assumes all_post: "\<forall> \<sigma> \<sigma>' \<sigma>''.  ((\<sigma>,\<sigma>') \<Turnstile> PRE self a1) = ((\<sigma>,\<sigma>'') \<Turnstile> PRE self a1)"
           (* PRE is really a pre-condition semantically,
              i.e. it does not depend on the post-state. ... *)
   assumes cp\<^sub>P\<^sub>R\<^sub>E: "PRE (self) (a1)  \<tau> = PRE (\<lambda> _. self \<tau>) (\<lambda> _. a1 \<tau>) \<tau> "
           (* this interface is preferable than :
              assumes "cp self' \<Longrightarrow> cp a1' \<Longrightarrow> cp a2' \<Longrightarrow> cp (\<lambda>X. PRE (self' X) (a1' X) (a2' X) )"
              which is too polymorphic. *)
   assumes cp\<^sub>P\<^sub>O\<^sub>S\<^sub>T:"POST (self) (a1) (res) \<tau> = POST (\<lambda> _. self \<tau>)(\<lambda> _. a1 \<tau>) (\<lambda> _. res \<tau>) \<tau>"

sublocale contract1 < contract_scheme "\<lambda>a1 \<tau>. (\<tau> \<Turnstile> \<upsilon> a1)" "\<lambda>a1 \<tau>. (\<lambda> _. a1 \<tau>)"
 apply(unfold_locales)
     apply(rule def_scheme, rule all_post, rule cp\<^sub>P\<^sub>R\<^sub>E, rule cp\<^sub>P\<^sub>O\<^sub>S\<^sub>T)
by(simp add: OclValid_def cp_valid[symmetric])

context contract1
begin
   lemma strict1[simp]: "f self invalid = invalid"
   by(rule ext, rename_tac "\<tau>", simp add: def_scheme StrongEq_def OclValid_def false_def true_def)

   lemma defined_mono : "\<tau> \<Turnstile>\<upsilon>(f Y Z) \<Longrightarrow> (\<tau> \<Turnstile>\<delta> Y) \<and> (\<tau> \<Turnstile>\<upsilon> Z)"
   by(auto simp: valid_def bot_fun_def invalid_def
                 def_scheme StrongEq_def OclValid_def false_def true_def
           split: if_split_asm)

   lemma cp_pre: "cp self' \<Longrightarrow> cp a1' \<Longrightarrow>  cp (\<lambda>X. PRE (self' X) (a1' X)  )"
   by(rule_tac f=PRE in cpI2, auto intro: cp\<^sub>P\<^sub>R\<^sub>E)

   lemma cp_post: "cp self' \<Longrightarrow> cp a1' \<Longrightarrow> cp res'
                   \<Longrightarrow> cp (\<lambda>X. POST (self' X) (a1' X) (res' X))"
   by(rule_tac f=POST in cpI3, auto intro: cp\<^sub>P\<^sub>O\<^sub>S\<^sub>T)

   lemma cp [simp]:  "cp self' \<Longrightarrow> cp a1' \<Longrightarrow>  cp res' \<Longrightarrow> cp (\<lambda>X. f (self' X) (a1' X))"
      by(rule_tac f=f in cpI2, auto intro:cp0)

   lemmas unfold = unfold'
   lemmas unfold2 = unfold2'
end

locale contract2 =
   fixes f   :: "('\<AA>,'\<alpha>0::null)val \<Rightarrow>
                  ('\<AA>,'\<alpha>1::null)val \<Rightarrow> ('\<AA>,'\<alpha>2::null)val \<Rightarrow>
                  ('\<AA>,'res::null)val"
   fixes PRE
   fixes POST
   assumes def_scheme: "f self a1 a2 \<equiv>
                               (\<lambda> \<tau>. SOME res. let res = \<lambda> _. res in
                                     if (\<tau> \<Turnstile> (\<delta> self)) \<and>  (\<tau> \<Turnstile> \<upsilon> a1) \<and>  (\<tau> \<Turnstile> \<upsilon> a2)
                                     then (\<tau> \<Turnstile> PRE self a1 a2) \<and>
                                          (\<tau> \<Turnstile> POST self a1 a2 res)
                                     else \<tau> \<Turnstile> res \<triangleq> invalid) "
   assumes all_post: "\<forall> \<sigma> \<sigma>' \<sigma>''.  ((\<sigma>,\<sigma>') \<Turnstile> PRE self a1 a2) = ((\<sigma>,\<sigma>'') \<Turnstile> PRE self a1 a2)"
           (* PRE is really a pre-condition semantically,
              i.e. it does not depend on the post-state. ... *)
   assumes cp\<^sub>P\<^sub>R\<^sub>E: "PRE (self) (a1) (a2) \<tau> = PRE (\<lambda> _. self \<tau>) (\<lambda> _. a1 \<tau>) (\<lambda> _. a2 \<tau>) \<tau> "
           (* this interface is preferable than :
              assumes "cp self' \<Longrightarrow> cp a1' \<Longrightarrow> cp a2' \<Longrightarrow> cp (\<lambda>X. PRE (self' X) (a1' X) (a2' X) )"
              which is too polymorphic. *)
   assumes cp\<^sub>P\<^sub>O\<^sub>S\<^sub>T:"\<And>res. POST (self) (a1) (a2) (res) \<tau> =
                         POST (\<lambda> _. self \<tau>)(\<lambda> _. a1 \<tau>)(\<lambda> _. a2 \<tau>) (\<lambda> _. res \<tau>) \<tau>"

sublocale contract2 < contract_scheme "\<lambda>(a1,a2) \<tau>. (\<tau> \<Turnstile> \<upsilon> a1) \<and> (\<tau> \<Turnstile> \<upsilon> a2)"
                                      "\<lambda>(a1,a2) \<tau>. (\<lambda> _.a1 \<tau>, \<lambda> _.a2 \<tau>)"
                                      "(\<lambda>x (a,b). f x a b)"
                                      "(\<lambda>x (a,b). PRE x a b)"
                                      "(\<lambda>x (a,b). POST x a b)"
 apply(unfold_locales)
     apply(auto simp add: def_scheme)
        apply (metis all_post, metis all_post)
      apply(subst cp\<^sub>P\<^sub>R\<^sub>E, simp)
     apply(subst cp\<^sub>P\<^sub>O\<^sub>S\<^sub>T, simp)
by(simp_all add: OclValid_def cp_valid[symmetric])

context contract2
begin
   lemma strict0'[simp] : "f invalid X Y = invalid"
   by(insert strict0[of "(X,Y)"], simp)

   lemma nullstrict0'[simp]: "f null X Y = invalid"
   by(insert nullstrict0[of "(X,Y)"], simp)

   lemma strict1[simp]: "f self invalid Y = invalid"
   by(rule ext, rename_tac "\<tau>", simp add: def_scheme StrongEq_def OclValid_def false_def true_def)

   lemma strict2[simp]: "f self X invalid = invalid"
   by(rule ext, rename_tac "\<tau>", simp add: def_scheme StrongEq_def OclValid_def false_def true_def)

   lemma defined_mono : "\<tau> \<Turnstile>\<upsilon>(f X Y Z) \<Longrightarrow> (\<tau> \<Turnstile>\<delta> X) \<and> (\<tau> \<Turnstile>\<upsilon> Y) \<and> (\<tau> \<Turnstile>\<upsilon> Z)"
   by(auto simp: valid_def bot_fun_def invalid_def
                 def_scheme StrongEq_def OclValid_def false_def true_def
           split: if_split_asm)

   lemma cp_pre: "cp self' \<Longrightarrow> cp a1' \<Longrightarrow> cp a2' \<Longrightarrow> cp (\<lambda>X. PRE (self' X) (a1' X) (a2' X) )"
   by(rule_tac f=PRE in cpI3, auto intro: cp\<^sub>P\<^sub>R\<^sub>E)

   lemma cp_post: "cp self' \<Longrightarrow> cp a1' \<Longrightarrow> cp a2' \<Longrightarrow> cp res'
                   \<Longrightarrow> cp (\<lambda>X. POST (self' X) (a1' X) (a2' X) (res' X))"
   by(rule_tac f=POST in cpI4, auto intro: cp\<^sub>P\<^sub>O\<^sub>S\<^sub>T)

   lemma cp0' : "f self a1 a2 \<tau> = f (\<lambda> _. self \<tau>) (\<lambda> _. a1 \<tau>) (\<lambda> _. a2 \<tau>) \<tau>"
   by (rule cp0[of _ "(a1,a2)", simplified])

   lemma cp [simp]:  "cp self' \<Longrightarrow> cp a1' \<Longrightarrow> cp a2' \<Longrightarrow> cp res'
                       \<Longrightarrow> cp (\<lambda>X. f (self' X) (a1' X) (a2' X))"
      by(rule_tac f=f in cpI3, auto intro:cp0')

   theorem unfold :
      assumes                "cp E"
      and                    "(\<tau> \<Turnstile> \<delta> self) \<and> (\<tau> \<Turnstile> \<upsilon> a1) \<and>  (\<tau> \<Turnstile> \<upsilon> a2)"
      and                    "\<tau> \<Turnstile> PRE self a1 a2"
      and                    " \<exists>res. (\<tau> \<Turnstile> POST self a1 a2 (\<lambda> _. res))"
      and                    "(\<And>res. \<tau> \<Turnstile> POST self a1 a2 (\<lambda> _. res)  \<Longrightarrow> \<tau> \<Turnstile> E (\<lambda> _. res))"
      shows                  "\<tau> \<Turnstile> E(f self a1 a2)"
      apply(rule unfold'[of _ _ _ "(a1, a2)", simplified])
      by((rule assms)+)

   lemma unfold2 :
      assumes                  "cp E"
      and                      "(\<tau> \<Turnstile> \<delta> self) \<and> (\<tau> \<Turnstile> \<upsilon> a1) \<and>  (\<tau> \<Turnstile> \<upsilon> a2)"
      and                      "\<tau> \<Turnstile> PRE self a1 a2"
      and                      "\<tau> \<Turnstile> POST' self a1 a2" (* split constraint holds on post-state *)
      and                      "\<And> res. (POST self a1 a2 res) =
                                       ((POST' self a1 a2)  and (res \<triangleq> (BODY self a1 a2)))"
      shows "(\<tau> \<Turnstile> E(f self a1 a2)) = (\<tau> \<Turnstile> E(BODY self a1 a2))"
      apply(rule unfold2'[of _ _ _ "(a1, a2)", simplified])
      by((rule assms)+)
end

locale contract3 =
   fixes f   :: "('\<AA>,'\<alpha>0::null)val \<Rightarrow>
                  ('\<AA>,'\<alpha>1::null)val \<Rightarrow>
                  ('\<AA>,'\<alpha>2::null)val \<Rightarrow>
                  ('\<AA>,'\<alpha>3::null)val \<Rightarrow>
                  ('\<AA>,'res::null)val"
   fixes PRE
   fixes POST
   assumes def_scheme: "f self a1 a2 a3 \<equiv>
                               (\<lambda> \<tau>. SOME res. let res = \<lambda> _. res in
                                     if (\<tau> \<Turnstile> (\<delta> self)) \<and>  (\<tau> \<Turnstile> \<upsilon> a1) \<and>  (\<tau> \<Turnstile> \<upsilon> a2) \<and>  (\<tau> \<Turnstile> \<upsilon> a3)
                                     then (\<tau> \<Turnstile> PRE self a1 a2 a3) \<and>
                                          (\<tau> \<Turnstile> POST self a1 a2 a3 res)
                                     else \<tau> \<Turnstile> res \<triangleq> invalid) "
   assumes all_post: "\<forall> \<sigma> \<sigma>' \<sigma>''.  ((\<sigma>,\<sigma>') \<Turnstile> PRE self a1 a2 a3) = ((\<sigma>,\<sigma>'') \<Turnstile> PRE self a1 a2 a3)"
           (* PRE is really a pre-condition semantically,
              i.e. it does not depend on the post-state. ... *)
   assumes cp\<^sub>P\<^sub>R\<^sub>E: "PRE (self) (a1) (a2) (a3) \<tau> = PRE (\<lambda> _. self \<tau>) (\<lambda> _. a1 \<tau>) (\<lambda> _. a2 \<tau>) (\<lambda> _. a3 \<tau>) \<tau> "
           (* this interface is preferable than :
              assumes "cp self' \<Longrightarrow> cp a1' \<Longrightarrow> cp a2' \<Longrightarrow> cp a3' \<Longrightarrow> cp (\<lambda>X. PRE (self' X) (a1' X) (a2' X) (a3' X) )"
              which is too polymorphic. *)
   assumes cp\<^sub>P\<^sub>O\<^sub>S\<^sub>T:"\<And>res. POST (self) (a1) (a2) (a3) (res) \<tau> =
                         POST (\<lambda> _. self \<tau>)(\<lambda> _. a1 \<tau>)(\<lambda> _. a2 \<tau>)(\<lambda> _. a3 \<tau>) (\<lambda> _. res \<tau>) \<tau>"

sublocale contract3 < contract_scheme "\<lambda>(a1,a2,a3) \<tau>. (\<tau> \<Turnstile> \<upsilon> a1) \<and> (\<tau> \<Turnstile> \<upsilon> a2)\<and> (\<tau> \<Turnstile> \<upsilon> a3)"
                                      "\<lambda>(a1,a2,a3) \<tau>. (\<lambda> _.a1 \<tau>, \<lambda> _.a2 \<tau>, \<lambda> _.a3 \<tau>)"
                                      "(\<lambda>x (a,b,c). f x a b c)"
                                      "(\<lambda>x (a,b,c). PRE x a b c)"
                                      "(\<lambda>x (a,b,c). POST x a b c)"
 apply(unfold_locales)
     apply(auto simp add: def_scheme)
        apply (metis all_post, metis all_post)
      apply(subst cp\<^sub>P\<^sub>R\<^sub>E, simp)
     apply(subst cp\<^sub>P\<^sub>O\<^sub>S\<^sub>T, simp)
by(simp_all add: OclValid_def cp_valid[symmetric])

context contract3
begin
   lemma strict0'[simp] : "f invalid X Y Z = invalid"
   by(rule ext, rename_tac "\<tau>", simp add: def_scheme StrongEq_def OclValid_def false_def true_def)

   lemma nullstrict0'[simp]: "f null X Y Z = invalid"
   by(rule ext, rename_tac "\<tau>", simp add: def_scheme StrongEq_def OclValid_def false_def true_def)

   lemma strict1[simp]: "f self invalid Y Z = invalid"
   by(rule ext, rename_tac "\<tau>", simp add: def_scheme StrongEq_def OclValid_def false_def true_def)

   lemma strict2[simp]: "f self X invalid Z = invalid"
   by(rule ext, rename_tac "\<tau>", simp add: def_scheme StrongEq_def OclValid_def false_def true_def)

   lemma defined_mono : "\<tau> \<Turnstile>\<upsilon>(f W X Y Z) \<Longrightarrow> (\<tau> \<Turnstile>\<delta> W) \<and> (\<tau> \<Turnstile>\<upsilon> X) \<and> (\<tau> \<Turnstile>\<upsilon> Y) \<and> (\<tau> \<Turnstile>\<upsilon> Z)"
   by(auto simp: valid_def bot_fun_def invalid_def
                 def_scheme StrongEq_def OclValid_def false_def true_def
           split: if_split_asm)

   lemma cp_pre: "cp self' \<Longrightarrow> cp a1' \<Longrightarrow> cp a2'\<Longrightarrow> cp a3'
                  \<Longrightarrow> cp (\<lambda>X. PRE (self' X) (a1' X) (a2' X) (a3' X) )"
   by(rule_tac f=PRE in cpI4, auto intro: cp\<^sub>P\<^sub>R\<^sub>E)

   lemma cp_post: "cp self' \<Longrightarrow> cp a1' \<Longrightarrow> cp a2' \<Longrightarrow> cp a3' \<Longrightarrow> cp res'
                   \<Longrightarrow> cp (\<lambda>X. POST (self' X) (a1' X) (a2' X) (a3' X)  (res' X))"
   by(rule_tac f=POST in cpI5, auto intro: cp\<^sub>P\<^sub>O\<^sub>S\<^sub>T)

   lemma cp0' : "f self a1 a2 a3 \<tau> = f (\<lambda> _. self \<tau>) (\<lambda> _. a1 \<tau>) (\<lambda> _. a2 \<tau>) (\<lambda> _. a3 \<tau>) \<tau>"
   by (rule cp0[of _ "(a1,a2,a3)", simplified])

   lemma cp [simp]:  "cp self' \<Longrightarrow> cp a1' \<Longrightarrow> cp a2' \<Longrightarrow> cp a3' \<Longrightarrow> cp res'
                       \<Longrightarrow> cp (\<lambda>X. f (self' X) (a1' X) (a2' X) (a3' X))"
      by(rule_tac f=f in cpI4, auto intro:cp0')

   theorem unfold :
      assumes                "cp E"
      and                    "(\<tau> \<Turnstile> \<delta> self) \<and> (\<tau> \<Turnstile> \<upsilon> a1) \<and>  (\<tau> \<Turnstile> \<upsilon> a2) \<and>  (\<tau> \<Turnstile> \<upsilon> a3)"
      and                    "\<tau> \<Turnstile> PRE self a1 a2 a3"
      and                    " \<exists>res. (\<tau> \<Turnstile> POST self a1 a2 a3 (\<lambda> _. res))"
      and                    "(\<And>res. \<tau> \<Turnstile> POST self a1 a2 a3 (\<lambda> _. res)  \<Longrightarrow> \<tau> \<Turnstile> E (\<lambda> _. res))"
      shows                  "\<tau> \<Turnstile> E(f self a1 a2 a3)"
      apply(rule unfold'[of _ _ _ "(a1, a2, a3)", simplified])
      by((rule assms)+)

   lemma unfold2 :
      assumes                  "cp E"
      and                      "(\<tau> \<Turnstile> \<delta> self) \<and> (\<tau> \<Turnstile> \<upsilon> a1) \<and>  (\<tau> \<Turnstile> \<upsilon> a2) \<and>  (\<tau> \<Turnstile> \<upsilon> a3)"
      and                      "\<tau> \<Turnstile> PRE self a1 a2 a3"
      and                      "\<tau> \<Turnstile> POST' self a1 a2 a3" (* split constraint holds on post-state *)
      and                      "\<And> res. (POST self a1 a2 a3 res) =
                                       ((POST' self a1 a2 a3)  and (res \<triangleq> (BODY self a1 a2 a3)))"
      shows "(\<tau> \<Turnstile> E(f self a1 a2 a3)) = (\<tau> \<Turnstile> E(BODY self a1 a2 a3))"
      apply(rule unfold2'[of _ _ _ "(a1, a2, a3)", simplified])
      by((rule assms)+)
end

end

repo: PSL


text:
theory Number_Theory_Aux imports
  "HOL-Number_Theory.Cong"
  "HOL-Number_Theory.Residues"
begin

lemma bezw_inverse:
  assumes "gcd (e :: nat) (N ::nat) = 1"
  shows "[nat e * nat ((fst (bezw e N)) mod N) = 1] (mod nat N)"
proof-
  have "(fst (bezw e N) * e + snd (bezw e N) * N) mod N = 1 mod N"
    by (metis assms bezw_aux zmod_int)
  hence "(fst (bezw e N) mod N * e mod N) = 1 mod N"
    by (simp add: mod_mult_right_eq mult.commute)
  hence cong_eq: "[(fst (bezw e N) mod N * e) = 1] (mod N)"
    by (metis of_nat_1 zmod_int cong_def)
  hence "[nat (fst (bezw e N) mod N) * e = 1] (mod N)"
  proof -
    { assume "int (nat (fst (bezw e N) mod int N)) \<noteq> fst (bezw e N) mod int N"
      have "N = 0 \<longrightarrow> 0 \<le> fst (bezw e N) mod int N"
        by fastforce
      then have "int (nat (fst (bezw e N) mod int N)) = fst (bezw e N) mod int N"
        by fastforce }
    then have "[int (nat (fst (bezw e N) mod int N) * e) = int 1] (mod int N)"
      by (metis cong_eq of_nat_1 of_nat_mult)
    then show ?thesis
      using cong_int_iff by blast
  qed
  then show ?thesis by(simp add: mult.commute)
qed

lemma inverse:
  assumes "gcd x (q::nat) = 1"
    and "q > 0"
  shows "[x * (fst (bezw x q)) = 1] (mod q)"
proof-
  have int_eq: "fst (bezw  x q) * x + snd (bezw x q) * int q = 1"
    by (metis assms(1) bezw_aux of_nat_1)
  hence int_eq': "(fst (bezw  x q) * x + snd (bezw x q) * int q) mod q = 1 mod q"
    by (metis of_nat_1 zmod_int)
  hence "(fst (bezw x q) * x) mod q = 1 mod q"
    by simp
  hence "[(fst (bezw x q)) * x  = 1] (mod q)"
    using cong_def int_eq int_eq' by metis
  then show ?thesis by(simp add: mult.commute)
qed

lemma prod_not_prime:
  assumes "prime (x::nat)"
    and "prime y"
    and "x > 2"
    and "y > 2"
  shows "\<not> prime ((x-1)*(y-1))"
  by (metis assms One_nat_def Suc_diff_1 nat_neq_iff numeral_2_eq_2 prime_gt_0_nat prime_product)

lemma ex_inverse:
  assumes coprime: "coprime (e :: nat) ((P-1)*(Q-1))"
    and "prime P"
    and "prime Q"
    and "P \<noteq> Q"
  shows "\<exists> d. [e*d = 1] (mod (P-1)) \<and> d \<noteq> 0"
proof-
  have "coprime e (P-1)"
    using assms(1) by simp
  then obtain d where d: "[e*d = 1] (mod (P-1))"
    using cong_solve_coprime_nat by auto
  then show ?thesis by (metis cong_0_1_nat cong_1 mult_0_right zero_neq_one)
qed

lemma ex_k1_k2:
  assumes coprime: "coprime (e :: nat) ((P-1)*(Q-1))"
    and "[e*d = 1] (mod (P-1))"
  shows "\<exists> k1 k2. e*d + k1*(P-1) = 1 + k2*(P-1)"
  by (metis assms(2) cong_iff_lin_nat)

lemma ex_k_mod:
  assumes coprime: "coprime (e :: nat) ((P-1)*(Q-1))"
    and "P \<noteq> Q"
    and "prime P"
    and "prime Q"
    and "d \<noteq> 0"
    and " [e*d = 1] (mod (P-1))"
  shows "\<exists> k. e*d = 1 + k*(P-1)"
proof-
  have "e > 0"
    using assms(1) assms(2) prime_gt_0_nat by fastforce
  then have "e*d \<ge> 1" using assms by simp
  then obtain k where k: "e*d = 1 + k*(P-1)"
    using assms(6) cong_to_1'_nat by auto
  then show ?thesis
    by simp
qed

lemma fermat_little:
  assumes "prime (P :: nat)"
  shows "[x^P = x] (mod P)"
proof(cases "P dvd x")
  case True
  hence "x mod P = 0" by simp
  moreover have "x ^ P mod P = 0"
    by (simp add: True assms prime_dvd_power_nat_iff prime_gt_0_nat)
  ultimately show ?thesis
    by (simp add: cong_def)
next
  case False
  hence "[x ^ (P - 1) = 1] (mod P)"
    using fermat_theorem assms by blast
  then show ?thesis
    by (metis assms cong_def diff_diff_cancel diff_is_0_eq' diff_zero mod_mult_right_eq power_eq_if power_one_right prime_ge_1_nat zero_le_one)
qed

end


text:
theory int_add_inv_right
imports Main
        "$HIPSTER_HOME/IsaHipster"
begin

datatype Nat = Zero | Succ "Nat"

datatype Z = P "Nat" | N "Nat"

fun zero :: "Z" where
"zero = P Zero"

fun plus2 :: "Nat => Nat => Nat" where
"plus2 (Zero) y = y"
| "plus2 (Succ n) y = Succ (plus2 n y)"

fun neg :: "Z => Z" where
"neg (P (Zero)) = P Zero"
| "neg (P (Succ n)) = N n"
| "neg (N m) = P (Succ m)"

fun minus :: "Nat => Nat => Z" where
"minus (Zero) (Zero) = P Zero"
| "minus (Zero) (Succ n) = N n"
| "minus (Succ m) (Zero) = P (Succ m)"
| "minus (Succ m) (Succ o) = minus m o"

fun plus :: "Z => Z => Z" where
"plus (P m) (P n) = P (plus2 m n)"
| "plus (P m) (N o) = minus m (Succ o)"
| "plus (N m2) (P n2) = minus n2 (Succ m2)"
| "plus (N m2) (N n3) = N (Succ (plus2 m2 n3))"

(*hipster zero plus2 neg minus plus *)

theorem x0 :
  "!! (x :: Z) . (plus x (neg x)) = zero"
  by (tactic \<open>Subgoal.FOCUS_PARAMS (K (Tactic_Data.hard_tac @{context})) @{context} 1\<close>)

end

author: moajohansson

repo: IsaHipster


text:
(*  Title:      HOL/Auth/flash_data_cub_lemma_on_inv__109.thy
    Author:     Yongjian Li and Kaiqiang Duan, State Key Lab of Computer Science, Institute of Software, Chinese Academy of Sciences
    Copyright    2016 State Key Lab of Computer Science, Institute of Software, Chinese Academy of Sciences
*)

header{*The flash_data_cub Protocol Case Study*}

theory flash_data_cub_lemma_on_inv__109 imports flash_data_cub_base
begin
section{*All lemmas on causal relation between inv__109 and some rule r*}
lemma n_PI_Local_Get_GetVsinv__109:
assumes a1: "(r=n_PI_Local_Get_Get  )" and
a2: "(f=inv__109  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_PI_Local_GetX_GetX__part__0Vsinv__109:
assumes a1: "(r=n_PI_Local_GetX_GetX__part__0  )" and
a2: "(f=inv__109  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
  have "?P3 s"
  apply (cut_tac a1 a2 , simp, rule_tac x="(neg (andForm (eqn (IVar (Field (Field (Ident ''Sta'') ''Dir'') ''ShrVld'')) (Const true)) (eqn (IVar (Field (Field (Ident ''Sta'') ''Dir'') ''Dirty'')) (Const true))))" in exI, auto) done
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_PI_Local_GetX_GetX__part__1Vsinv__109:
assumes a1: "(r=n_PI_Local_GetX_GetX__part__1  )" and
a2: "(f=inv__109  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
  have "?P3 s"
  apply (cut_tac a1 a2 , simp, rule_tac x="(neg (andForm (eqn (IVar (Field (Field (Ident ''Sta'') ''Dir'') ''ShrVld'')) (Const true)) (eqn (IVar (Field (Field (Ident ''Sta'') ''Dir'') ''Dirty'')) (Const true))))" in exI, auto) done
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_PI_Local_GetX_PutX_HeadVld__part__0Vsinv__109:
assumes a1: "(r=n_PI_Local_GetX_PutX_HeadVld__part__0 N )" and
a2: "(f=inv__109  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_PI_Local_GetX_PutX_HeadVld__part__1Vsinv__109:
assumes a1: "(r=n_PI_Local_GetX_PutX_HeadVld__part__1 N )" and
a2: "(f=inv__109  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Nak_HomeVsinv__109:
assumes a1: "(r=n_NI_Nak_Home  )" and
a2: "(f=inv__109  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Local_Get_Put_HeadVsinv__109:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_Get_Put_Head N src)" and
a2: "(f=inv__109  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_Get_Put_Head N src" apply fastforce done
  have "?P3 s"
  apply (cut_tac a1 a2 , simp, rule_tac x="(neg (andForm (eqn (IVar (Field (Field (Ident ''Sta'') ''Dir'') ''Pending'')) (Const false)) (eqn (IVar (Field (Field (Ident ''Sta'') ''HomeUniMsg'') ''Cmd'')) (Const UNI_GetX))))" in exI, auto) done
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Remote_Get_Nak_HomeVsinv__109:
assumes a1: "(\<exists> dst. dst\<le>N\<and>r=n_NI_Remote_Get_Nak_Home  dst)" and
a2: "(f=inv__109  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain dst where a1:"dst\<le>N\<and>r=n_NI_Remote_Get_Nak_Home  dst" apply fastforce done
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Remote_Get_Put_HomeVsinv__109:
assumes a1: "(\<exists> dst. dst\<le>N\<and>r=n_NI_Remote_Get_Put_Home  dst)" and
a2: "(f=inv__109  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain dst where a1:"dst\<le>N\<and>r=n_NI_Remote_Get_Put_Home  dst" apply fastforce done
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Local_GetX_PutX_1Vsinv__109:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_1 N src)" and
a2: "(f=inv__109  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_PutX_1 N src" apply fastforce done
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Local_GetX_PutX_2Vsinv__109:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_2 N src)" and
a2: "(f=inv__109  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_PutX_2 N src" apply fastforce done
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Local_GetX_PutX_3Vsinv__109:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_3 N src)" and
a2: "(f=inv__109  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_PutX_3 N src" apply fastforce done
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Local_GetX_PutX_4Vsinv__109:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_4 N src)" and
a2: "(f=inv__109  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_PutX_4 N src" apply fastforce done
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Local_GetX_PutX_5Vsinv__109:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_5 N src)" and
a2: "(f=inv__109  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_PutX_5 N src" apply fastforce done
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Local_GetX_PutX_6Vsinv__109:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_6 N src)" and
a2: "(f=inv__109  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_PutX_6 N src" apply fastforce done
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Local_GetX_PutX_7__part__0Vsinv__109:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_7__part__0 N src)" and
a2: "(f=inv__109  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_PutX_7__part__0 N src" apply fastforce done
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Local_GetX_PutX_7__part__1Vsinv__109:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_7__part__1 N src)" and
a2: "(f=inv__109  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_PutX_7__part__1 N src" apply fastforce done
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Local_GetX_PutX_7_NODE_Get__part__0Vsinv__109:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_7_NODE_Get__part__0 N src)" and
a2: "(f=inv__109  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_PutX_7_NODE_Get__part__0 N src" apply fastforce done
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Local_GetX_PutX_7_NODE_Get__part__1Vsinv__109:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_7_NODE_Get__part__1 N src)" and
a2: "(f=inv__109  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_PutX_7_NODE_Get__part__1 N src" apply fastforce done
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Local_GetX_PutX_8_HomeVsinv__109:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_8_Home N src)" and
a2: "(f=inv__109  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_PutX_8_Home N src" apply fastforce done
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Local_GetX_PutX_8_Home_NODE_GetVsinv__109:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_8_Home_NODE_Get N src)" and
a2: "(f=inv__109  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_PutX_8_Home_NODE_Get N src" apply fastforce done
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Local_GetX_PutX_8Vsinv__109:
assumes a1: "(\<exists> src pp. src\<le>N\<and>pp\<le>N\<and>src~=pp\<and>r=n_NI_Local_GetX_PutX_8 N src pp)" and
a2: "(f=inv__109  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src pp where a1:"src\<le>N\<and>pp\<le>N\<and>src~=pp\<and>r=n_NI_Local_GetX_PutX_8 N src pp" apply fastforce done
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Local_GetX_PutX_8_NODE_GetVsinv__109:
assumes a1: "(\<exists> src pp. src\<le>N\<and>pp\<le>N\<and>src~=pp\<and>r=n_NI_Local_GetX_PutX_8_NODE_Get N src pp)" and
a2: "(f=inv__109  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src pp where a1:"src\<le>N\<and>pp\<le>N\<and>src~=pp\<and>r=n_NI_Local_GetX_PutX_8_NODE_Get N src pp" apply fastforce done
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Local_GetX_PutX_9__part__0Vsinv__109:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_9__part__0 N src)" and
a2: "(f=inv__109  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_PutX_9__part__0 N src" apply fastforce done
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Local_GetX_PutX_9__part__1Vsinv__109:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_9__part__1 N src)" and
a2: "(f=inv__109  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_PutX_9__part__1 N src" apply fastforce done
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Local_GetX_PutX_10_HomeVsinv__109:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_10_Home N src)" and
a2: "(f=inv__109  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_PutX_10_Home N src" apply fastforce done
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Local_GetX_PutX_10Vsinv__109:
assumes a1: "(\<exists> src pp. src\<le>N\<and>pp\<le>N\<and>src~=pp\<and>r=n_NI_Local_GetX_PutX_10 N src pp)" and
a2: "(f=inv__109  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src pp where a1:"src\<le>N\<and>pp\<le>N\<and>src~=pp\<and>r=n_NI_Local_GetX_PutX_10 N src pp" apply fastforce done
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Local_GetX_PutX_11Vsinv__109:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_11 N src)" and
a2: "(f=inv__109  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_PutX_11 N src" apply fastforce done
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Remote_GetX_Nak_HomeVsinv__109:
assumes a1: "(\<exists> dst. dst\<le>N\<and>r=n_NI_Remote_GetX_Nak_Home  dst)" and
a2: "(f=inv__109  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain dst where a1:"dst\<le>N\<and>r=n_NI_Remote_GetX_Nak_Home  dst" apply fastforce done
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Remote_GetX_PutX_HomeVsinv__109:
assumes a1: "(\<exists> dst. dst\<le>N\<and>r=n_NI_Remote_GetX_PutX_Home  dst)" and
a2: "(f=inv__109  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain dst where a1:"dst\<le>N\<and>r=n_NI_Remote_GetX_PutX_Home  dst" apply fastforce done
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Local_PutVsinv__109:
assumes a1: "(r=n_NI_Local_Put  )" and
a2: "(f=inv__109  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Local_PutXAcksDoneVsinv__109:
assumes a1: "(r=n_NI_Local_PutXAcksDone  )" and
a2: "(f=inv__109  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_ShWbVsinv__109:
assumes a1: "(r=n_NI_ShWb N )" and
a2: "(f=inv__109  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
  have "?P3 s"
  apply (cut_tac a1 a2 , simp, rule_tac x="(neg (andForm (eqn (IVar (Field (Field (Ident ''Sta'') ''ShWbMsg'') ''Cmd'')) (Const SHWB_ShWb)) (eqn (IVar (Field (Field (Ident ''Sta'') ''HomeUniMsg'') ''Cmd'')) (Const UNI_GetX))))" in exI, auto) done
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Local_Get_Get__part__1Vsinv__109:
  assumes a1: "\<exists> src. src\<le>N\<and>r=n_NI_Local_Get_Get__part__1  src" and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_PI_Remote_GetVsinv__109:
  assumes a1: "\<exists> src. src\<le>N\<and>r=n_PI_Remote_Get  src" and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_PI_Local_GetX_PutX__part__0Vsinv__109:
  assumes a1: "r=n_PI_Local_GetX_PutX__part__0  " and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_WbVsinv__109:
  assumes a1: "r=n_NI_Wb  " and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_StoreVsinv__109:
  assumes a1: "\<exists> src data. src\<le>N\<and>data\<le>N\<and>r=n_Store  src data" and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_Local_GetX_GetX__part__1Vsinv__109:
  assumes a1: "\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_GetX__part__1  src" and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_InvAck_3Vsinv__109:
  assumes a1: "\<exists> src. src\<le>N\<and>r=n_NI_InvAck_3 N src" and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_InvAck_1Vsinv__109:
  assumes a1: "\<exists> src. src\<le>N\<and>r=n_NI_InvAck_1 N src" and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_PI_Remote_ReplaceVsinv__109:
  assumes a1: "\<exists> src. src\<le>N\<and>r=n_PI_Remote_Replace  src" and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_Store_HomeVsinv__109:
  assumes a1: "\<exists> data. data\<le>N\<and>r=n_Store_Home  data" and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_PI_Local_ReplaceVsinv__109:
  assumes a1: "r=n_PI_Local_Replace  " and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_Local_GetX_Nak__part__1Vsinv__109:
  assumes a1: "\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_Nak__part__1  src" and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_Local_Get_Nak__part__1Vsinv__109:
  assumes a1: "\<exists> src. src\<le>N\<and>r=n_NI_Local_Get_Nak__part__1  src" and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_Local_Get_Get__part__0Vsinv__109:
  assumes a1: "\<exists> src. src\<le>N\<and>r=n_NI_Local_Get_Get__part__0  src" and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_InvAck_existsVsinv__109:
  assumes a1: "\<exists> src pp. src\<le>N\<and>pp\<le>N\<and>src~=pp\<and>r=n_NI_InvAck_exists  src pp" and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_Local_GetX_Nak__part__2Vsinv__109:
  assumes a1: "\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_Nak__part__2  src" and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_PI_Remote_PutXVsinv__109:
  assumes a1: "\<exists> dst. dst\<le>N\<and>r=n_PI_Remote_PutX  dst" and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_InvVsinv__109:
  assumes a1: "\<exists> dst. dst\<le>N\<and>r=n_NI_Inv  dst" and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_PI_Local_PutXVsinv__109:
  assumes a1: "r=n_PI_Local_PutX  " and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_Local_Get_Nak__part__2Vsinv__109:
  assumes a1: "\<exists> src. src\<le>N\<and>r=n_NI_Local_Get_Nak__part__2  src" and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_Local_GetX_GetX__part__0Vsinv__109:
  assumes a1: "\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_GetX__part__0  src" and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_PI_Local_Get_PutVsinv__109:
  assumes a1: "r=n_PI_Local_Get_Put  " and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_ReplaceVsinv__109:
  assumes a1: "\<exists> src. src\<le>N\<and>r=n_NI_Replace  src" and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_Remote_GetX_NakVsinv__109:
  assumes a1: "\<exists> src dst. src\<le>N\<and>dst\<le>N\<and>src~=dst\<and>r=n_NI_Remote_GetX_Nak  src dst" and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_NakVsinv__109:
  assumes a1: "\<exists> dst. dst\<le>N\<and>r=n_NI_Nak  dst" and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_PI_Remote_GetXVsinv__109:
  assumes a1: "\<exists> src. src\<le>N\<and>r=n_PI_Remote_GetX  src" and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_PI_Local_GetX_PutX__part__1Vsinv__109:
  assumes a1: "r=n_PI_Local_GetX_PutX__part__1  " and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_Remote_PutXVsinv__109:
  assumes a1: "\<exists> dst. dst\<le>N\<and>r=n_NI_Remote_PutX  dst" and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_Remote_PutVsinv__109:
  assumes a1: "\<exists> dst. dst\<le>N\<and>r=n_NI_Remote_Put  dst" and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_Local_Get_PutVsinv__109:
  assumes a1: "\<exists> src. src\<le>N\<and>r=n_NI_Local_Get_Put  src" and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_Local_GetX_Nak__part__0Vsinv__109:
  assumes a1: "\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_Nak__part__0  src" and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_InvAck_exists_HomeVsinv__109:
  assumes a1: "\<exists> src. src\<le>N\<and>r=n_NI_InvAck_exists_Home  src" and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_Replace_HomeVsinv__109:
  assumes a1: "r=n_NI_Replace_Home  " and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_Remote_GetX_PutXVsinv__109:
  assumes a1: "\<exists> src dst. src\<le>N\<and>dst\<le>N\<and>src~=dst\<and>r=n_NI_Remote_GetX_PutX  src dst" and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_Remote_Get_NakVsinv__109:
  assumes a1: "\<exists> src dst. src\<le>N\<and>dst\<le>N\<and>src~=dst\<and>r=n_NI_Remote_Get_Nak  src dst" and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_Nak_ClearVsinv__109:
  assumes a1: "r=n_NI_Nak_Clear  " and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_Local_Get_Put_DirtyVsinv__109:
  assumes a1: "\<exists> src. src\<le>N\<and>r=n_NI_Local_Get_Put_Dirty  src" and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_Local_Get_Nak__part__0Vsinv__109:
  assumes a1: "\<exists> src. src\<le>N\<and>r=n_NI_Local_Get_Nak__part__0  src" and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_Remote_Get_PutVsinv__109:
  assumes a1: "\<exists> src dst. src\<le>N\<and>dst\<le>N\<and>src~=dst\<and>r=n_NI_Remote_Get_Put  src dst" and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_InvAck_2Vsinv__109:
  assumes a1: "\<exists> src. src\<le>N\<and>r=n_NI_InvAck_2 N src" and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_FAckVsinv__109:
  assumes a1: "r=n_NI_FAck  " and
  a2: "(f=inv__109  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

end

repo: newParaVerifier


text:
theory T21
imports Main
begin
lemma "(
(\<forall> x::nat. \<forall> y::nat. meet(x, y) = meet(y, x)) &
(\<forall> x::nat. \<forall> y::nat. join(x, y) = join(y, x)) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. meet(x, meet(y, z)) = meet(meet(x, y), z)) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. join(x, join(y, z)) = join(join(x, y), z)) &
(\<forall> x::nat. \<forall> y::nat. meet(x, join(x, y)) = x) &
(\<forall> x::nat. \<forall> y::nat. join(x, meet(x, y)) = x) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. mult(x, join(y, z)) = join(mult(x, y), mult(x, z))) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. mult(join(x, y), z) = join(mult(x, z), mult(y, z))) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. meet(x, over(join(mult(x, y), z), y)) = x) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. meet(y, undr(x, join(mult(x, y), z))) = y) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. join(mult(over(x, y), y), x) = x) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. join(mult(y, undr(y, x)), x) = x) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. undr(x, join(y, z)) = join(undr(x, y), undr(x, z))) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. over(join(x, y), z) = join(over(x, z), over(y, z))) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. over(x, meet(y, z)) = join(over(x, y), over(x, z))) &
(\<forall> x::nat. \<forall> y::nat. invo(join(x, y)) = meet(invo(x), invo(y))) &
(\<forall> x::nat. \<forall> y::nat. invo(meet(x, y)) = join(invo(x), invo(y))) &
(\<forall> x::nat. invo(invo(x)) = x)
) \<longrightarrow>
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. mult(x, meet(y, z)) = meet(mult(x, y), mult(x, z)))
"
nitpick[card nat=4,timeout=86400]
oops
end

author: inpefess

repo: residuated-binars


text:
(*
Copyright 2018

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
*)
theory vring_size_opt_mem
  imports virtio_ring_opt
begin

text \<open>Up to two locales per function in the binary.\<close>
locale vring_size_function = virtio_ring_opt_context +
  fixes rsp\<^sub>0 rbp\<^sub>0 a vring_size_opt_ret :: \<open>64 word\<close>
    and v\<^sub>0 :: \<open>8 word\<close>
    and blocks :: \<open>(nat \<times> 64 word \<times> nat) set\<close>
  assumes seps: \<open>seps blocks\<close>
    and masters:
      \<open>master blocks (a, 1) 0\<close>
      \<open>master blocks (rsp\<^sub>0, 8) 1\<close>
    and ret_address: \<open>outside vring_size_opt_ret 46 63\<close> \<comment> \<open>Only works for non-recursive functions.\<close>
begin

text \<open>
  The Floyd invariant expresses for some locations properties that are invariably true.
  Simply expresses that a byte in the memory remains untouched.
\<close>
definition pp_\<Theta> :: floyd_invar where
  \<open>pp_\<Theta> \<equiv> [
    \<comment> \<open>precondition\<close>
    boffset+46 \<mapsto> \<lambda>\<sigma>. regs \<sigma> rsp = rsp\<^sub>0
      \<and> regs \<sigma> rbp = rbp\<^sub>0
      \<and> \<sigma> \<turnstile> *[rsp\<^sub>0,8] = boffset+vring_size_opt_ret
      \<and> \<sigma> \<turnstile> *[a,1] = v\<^sub>0,
    \<comment> \<open>postcondition\<close>
    boffset+vring_size_opt_ret \<mapsto> \<lambda>\<sigma>. \<sigma> \<turnstile> *[a,1] = v\<^sub>0
      \<and> regs \<sigma> rsp = rsp\<^sub>0+8
      \<and> regs \<sigma> rbp = rbp\<^sub>0
  ]\<close>

text \<open>Adding some rules to the simplifier to simplify proofs.\<close>
schematic_goal pp_\<Theta>_zero[simp]:
  \<open>pp_\<Theta> boffset = ?x\<close>
  unfolding pp_\<Theta>_def
  by simp
schematic_goal pp_\<Theta>_numeral_l[simp]:
  \<open>pp_\<Theta> (n + boffset) = ?x\<close>
  unfolding pp_\<Theta>_def
  by simp
schematic_goal pp_\<Theta>_numeral_r[simp]:
  \<open>pp_\<Theta> (boffset + n) = ?x\<close>
  unfolding pp_\<Theta>_def
  by simp

lemma rewrite_vring_size_opt_mem:
  \<open>is_std_invar vring_size_opt_ret (floyd.invar vring_size_opt_ret pp_\<Theta>)\<close>
  text \<open>Boilerplate code to start the VCG\<close>
  apply (rule floyd_invarI)
  apply (rewrite at \<open>floyd_vcs vring_size_opt_ret \<hole> _\<close> pp_\<Theta>_def)
  apply (intro floyd_vcsI)

  text \<open>Subgoal for rip = boffset+46\<close>
  subgoal premises prems for \<sigma>
    text \<open>Insert relevant knowledge\<close>
    apply (insert prems seps ret_address)
    text \<open>Apply VCG/symb.\ execution\<close>
    apply (restart_symbolic_execution?, (symbolic_execution masters: masters)+, (finish_symbolic_execution masters: masters)?)+
    done

  text \<open>Trivial ending subgoal.\<close>
  subgoal
    by simp
  done

end

end


text:
(*  Title:      HOL/Auth/n_german_lemma_inv__20_on_rules.thy
    Author:     Yongjian Li and Kaiqiang Duan, State Key Lab of Computer Science, Institute of Software, Chinese Academy of Sciences
    Copyright    2016 State Key Lab of Computer Science, Institute of Software, Chinese Academy of Sciences
*)

header{*The n_german Protocol Case Study*}

theory n_german_lemma_inv__20_on_rules imports n_german_lemma_on_inv__20
begin
section{*All lemmas on causal relation between inv__20*}
lemma lemma_inv__20_on_rules:
  assumes b1: "r \<in> rules N" and b2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__20  p__Inv4)"
  shows "invHoldForRule s f r (invariants N)"
  proof -
  have c1: "(\<exists> j. j\<le>N\<and>r=n_SendReqS  j)\<or>
    (\<exists> i. i\<le>N\<and>r=n_SendReqEI  i)\<or>
    (\<exists> i. i\<le>N\<and>r=n_SendReqES  i)\<or>
    (\<exists> i. i\<le>N\<and>r=n_RecvReq N i)\<or>
    (\<exists> i. i\<le>N\<and>r=n_SendInvE  i)\<or>
    (\<exists> i. i\<le>N\<and>r=n_SendInvS  i)\<or>
    (\<exists> i. i\<le>N\<and>r=n_SendInvAck  i)\<or>
    (\<exists> i. i\<le>N\<and>r=n_RecvInvAck  i)\<or>
    (\<exists> i. i\<le>N\<and>r=n_SendGntS  i)\<or>
    (\<exists> i. i\<le>N\<and>r=n_SendGntE N i)\<or>
    (\<exists> i. i\<le>N\<and>r=n_RecvGntS  i)\<or>
    (\<exists> i. i\<le>N\<and>r=n_RecvGntE  i)\<or>
    (\<exists> i d. i\<le>N\<and>d\<le>N\<and>r=n_Store  i d)"
  apply (cut_tac b1, auto) done
    moreover {
      assume d1: "(\<exists> j. j\<le>N\<and>r=n_SendReqS  j)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_SendReqSVsinv__20) done
    }

    moreover {
      assume d1: "(\<exists> i. i\<le>N\<and>r=n_SendReqEI  i)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_SendReqEIVsinv__20) done
    }

    moreover {
      assume d1: "(\<exists> i. i\<le>N\<and>r=n_SendReqES  i)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_SendReqESVsinv__20) done
    }

    moreover {
      assume d1: "(\<exists> i. i\<le>N\<and>r=n_RecvReq N i)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_RecvReqVsinv__20) done
    }

    moreover {
      assume d1: "(\<exists> i. i\<le>N\<and>r=n_SendInvE  i)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_SendInvEVsinv__20) done
    }

    moreover {
      assume d1: "(\<exists> i. i\<le>N\<and>r=n_SendInvS  i)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_SendInvSVsinv__20) done
    }

    moreover {
      assume d1: "(\<exists> i. i\<le>N\<and>r=n_SendInvAck  i)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_SendInvAckVsinv__20) done
    }

    moreover {
      assume d1: "(\<exists> i. i\<le>N\<and>r=n_RecvInvAck  i)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_RecvInvAckVsinv__20) done
    }

    moreover {
      assume d1: "(\<exists> i. i\<le>N\<and>r=n_SendGntS  i)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_SendGntSVsinv__20) done
    }

    moreover {
      assume d1: "(\<exists> i. i\<le>N\<and>r=n_SendGntE N i)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_SendGntEVsinv__20) done
    }

    moreover {
      assume d1: "(\<exists> i. i\<le>N\<and>r=n_RecvGntS  i)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_RecvGntSVsinv__20) done
    }

    moreover {
      assume d1: "(\<exists> i. i\<le>N\<and>r=n_RecvGntE  i)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_RecvGntEVsinv__20) done
    }

    moreover {
      assume d1: "(\<exists> i d. i\<le>N\<and>d\<le>N\<and>r=n_Store  i d)"
      have "invHoldForRule s f r (invariants N)"
      apply (cut_tac b2 d1, metis n_StoreVsinv__20) done
    }

  ultimately show "invHoldForRule s f r (invariants N)"
  by satx
qed

end

author: paraVerifier

repo: paraVerifier