text:
section {*L\_ATS\_Simulation\_Configuration\_WeakDET*}
theory
  L_ATS_Simulation_Configuration_WeakDET

imports
  L_ATS_Simulation_Configuration_Weak

begin

locale ATS_Simulation_Configuration_WeakDET =
  LR :
  ATS_Simulation_Configuration_Weak
  "TSstructure1 :: 'TSstructure1 \<Rightarrow> bool"
  "configurations1 :: 'TSstructure1 \<Rightarrow> 'conf1 set"
  "initial_configurations1 :: 'TSstructure1 \<Rightarrow> 'conf1 set"
  "step_labels1 :: 'TSstructure1 \<Rightarrow> 'label1 set"
  "step_relation1 :: 'TSstructure1 \<Rightarrow> 'conf1 \<Rightarrow> 'label1 \<Rightarrow> 'conf1 \<Rightarrow> bool"
  "effects1 :: 'TSstructure1 \<Rightarrow> 'event1 set"
  "marking_condition1 :: 'TSstructure1 \<Rightarrow> ('label1,'conf1)derivation \<Rightarrow> bool"
  "marked_effect1 :: 'TSstructure1 \<Rightarrow> ('label1,'conf1)derivation \<Rightarrow> 'event1 set"
  "unmarked_effect1 :: 'TSstructure1 \<Rightarrow> ('label1,'conf1)derivation \<Rightarrow> 'event1 set"
  "TSstructure2 :: 'TSstructure2 \<Rightarrow> bool"
  "configurations2 :: 'TSstructure2 \<Rightarrow> 'conf2 set"
  "initial_configurations2 :: 'TSstructure2 \<Rightarrow> 'conf2 set"
  "step_labels2 :: 'TSstructure2 \<Rightarrow> 'label2 set"
  "step_relation2 :: 'TSstructure2 \<Rightarrow> 'conf2 \<Rightarrow> 'label2 \<Rightarrow> 'conf2 \<Rightarrow> bool"
  "effects2 :: 'TSstructure2 \<Rightarrow> 'event2 set"
  "marking_condition2 :: 'TSstructure2 \<Rightarrow> ('label2,'conf2)derivation \<Rightarrow> bool"
  "marked_effect2 :: 'TSstructure2 \<Rightarrow> ('label2,'conf2)derivation \<Rightarrow> 'event2 set"
  "unmarked_effect2 :: 'TSstructure2 \<Rightarrow> ('label2,'conf2)derivation \<Rightarrow> 'event2 set"
  "relation_configurationLR :: 'TSstructure1 \<Rightarrow> 'TSstructure2 \<Rightarrow> 'conf1 \<Rightarrow> 'conf2 \<Rightarrow> bool"
  "relation_initial_configurationLR :: 'TSstructure1 \<Rightarrow> 'TSstructure2 \<Rightarrow> 'conf1 \<Rightarrow> 'conf2 \<Rightarrow> bool"
  "relation_effectLR :: 'TSstructure1 \<Rightarrow> 'TSstructure2 \<Rightarrow> 'event1 \<Rightarrow> 'event2 \<Rightarrow> bool"
  "relation_TSstructureLR :: 'TSstructure1 \<Rightarrow> 'TSstructure2 \<Rightarrow> bool"
  "relation_initial_simulationLRLR :: 'TSstructure1 \<Rightarrow> 'TSstructure2 \<Rightarrow> 'conf1 \<Rightarrow> (nat \<Rightarrow> ('label2, 'conf2) derivation_configuration option) \<Rightarrow> bool"
  "relation_step_simulationLRLR :: 'TSstructure1 \<Rightarrow> 'TSstructure2 \<Rightarrow> 'conf1 \<Rightarrow> 'label1 \<Rightarrow> 'conf1 \<Rightarrow> 'conf2 \<Rightarrow> (nat \<Rightarrow> ('label2, 'conf2) derivation_configuration option) \<Rightarrow> bool"
  +
  RL :
  ATS_Simulation_Configuration_Weak
  "TSstructure2 :: 'TSstructure2 \<Rightarrow> bool"
  "configurations2 :: 'TSstructure2 \<Rightarrow> 'conf2 set"
  "initial_configurations2 :: 'TSstructure2 \<Rightarrow> 'conf2 set"
  "step_labels2 :: 'TSstructure2 \<Rightarrow> 'label2 set"
  "step_relation2 :: 'TSstructure2 \<Rightarrow> 'conf2 \<Rightarrow> 'label2 \<Rightarrow> 'conf2 \<Rightarrow> bool"
  "effects2 :: 'TSstructure2 \<Rightarrow> 'event2 set"
  "marking_condition2 :: 'TSstructure2 \<Rightarrow> ('label2,'conf2)derivation \<Rightarrow> bool"
  "marked_effect2 :: 'TSstructure2 \<Rightarrow> ('label2,'conf2)derivation \<Rightarrow> 'event2 set"
  "unmarked_effect2 :: 'TSstructure2 \<Rightarrow> ('label2,'conf2)derivation \<Rightarrow> 'event2 set"
  "TSstructure1 :: 'TSstructure1 \<Rightarrow> bool"
  "configurations1 :: 'TSstructure1 \<Rightarrow> 'conf1 set"
  "initial_configurations1 :: 'TSstructure1 \<Rightarrow> 'conf1 set"
  "step_labels1 :: 'TSstructure1 \<Rightarrow> 'label1 set"
  "step_relation1 :: 'TSstructure1 \<Rightarrow> 'conf1 \<Rightarrow> 'label1 \<Rightarrow> 'conf1 \<Rightarrow> bool"
  "effects1 :: 'TSstructure1 \<Rightarrow> 'event1 set"
  "marking_condition1 :: 'TSstructure1 \<Rightarrow> ('label1,'conf1)derivation \<Rightarrow> bool"
  "marked_effect1 :: 'TSstructure1 \<Rightarrow> ('label1,'conf1)derivation \<Rightarrow> 'event1 set"
  "unmarked_effect1 :: 'TSstructure1 \<Rightarrow> ('label1,'conf1)derivation \<Rightarrow> 'event1 set"
  "relation_configurationRL :: 'TSstructure2 \<Rightarrow> 'TSstructure1 \<Rightarrow> 'conf2 \<Rightarrow> 'conf1 \<Rightarrow> bool"
  "relation_initial_configurationRL :: 'TSstructure2 \<Rightarrow> 'TSstructure1 \<Rightarrow> 'conf2 \<Rightarrow> 'conf1 \<Rightarrow> bool"
  "relation_effectRL :: 'TSstructure2 \<Rightarrow> 'TSstructure1 \<Rightarrow> 'event2 \<Rightarrow> 'event1 \<Rightarrow> bool"
  "relation_TSstructureRL :: 'TSstructure2 \<Rightarrow> 'TSstructure1 \<Rightarrow> bool"
  "relation_initial_simulationLRRL :: 'TSstructure2 \<Rightarrow> 'TSstructure1 \<Rightarrow> 'conf2 \<Rightarrow> (nat \<Rightarrow> ('label1, 'conf1) derivation_configuration option) \<Rightarrow> bool"
  "relation_step_simulationLRRL :: 'TSstructure2 \<Rightarrow> 'TSstructure1 \<Rightarrow> 'conf2 \<Rightarrow> 'label2 \<Rightarrow> 'conf2 \<Rightarrow> 'conf1 \<Rightarrow> (nat \<Rightarrow> ('label1, 'conf1) derivation_configuration option) \<Rightarrow> bool"
  for
    TSstructure1 configurations1 initial_configurations1 step_labels1 step_relation1 effects1 marking_condition1 marked_effect1 unmarked_effect1 TSstructure2 configurations2 initial_configurations2 step_labels2 step_relation2 effects2 marking_condition2 marked_effect2 unmarked_effect2 relation_configurationLR relation_initial_configurationLR relation_effectLR relation_TSstructureLR relation_initial_simulationLRLR relation_step_simulationLRLR relation_configurationRL relation_initial_configurationRL relation_effectRL relation_TSstructureRL relation_initial_simulationLRRL relation_step_simulationLRRL
    +

fixes label_relation :: "'TSstructure1 \<Rightarrow> 'TSstructure2 \<Rightarrow> 'label1 \<Rightarrow> 'label2 \<Rightarrow> bool"

assumes AX_backwards_determinism: "
  relation_TSstructureRL G2 G1
  \<Longrightarrow> LR.GL.is_forward_edge_deterministic_accessible G1
  \<Longrightarrow> step_relation2 G2 cnR en1 cnR1
  \<Longrightarrow> step_relation2 G2 cnR en2 cnR2
  \<Longrightarrow> maximum_of_domain dR nR
  \<Longrightarrow> LR.GR.derivation_initial G2 dR
  \<Longrightarrow> dR nR = Some (pair enR cnR)
  \<Longrightarrow> LR.GL.derivation_initial G1 dL
  \<Longrightarrow> maximum_of_domain dL nL
  \<Longrightarrow> relation_initial_configurationRL G2 G1 c0R c0L
  \<Longrightarrow> relation_configurationRL G2 G1 cnR cnL
  \<Longrightarrow> dR 0 = Some (pair None c0R)
  \<Longrightarrow> dL 0 = Some (pair None c0L)
  \<Longrightarrow> dL nL = Some (pair enL cnL)
  \<Longrightarrow> LR.GL.derivation G1 dL1
  \<Longrightarrow> LR.GL.derivation G1 dL2
  \<Longrightarrow> LR.GL.belongs G1 dL1
  \<Longrightarrow> LR.GL.belongs G1 dL2
  \<Longrightarrow> relation_step_simulationLRRL G2 G1 cnR en1 cnR1 cnL dL1
  \<Longrightarrow> relation_step_simulationLRRL G2 G1 cnR en2 cnR2 cnL dL2
  \<Longrightarrow> maximum_of_domain dL1 nL1
  \<Longrightarrow> relation_configurationRL G2 G1 cnR1 cnL1
  \<Longrightarrow> maximum_of_domain dL2 nL2
  \<Longrightarrow> relation_configurationRL G2 G1 cnR2 cnL2
  \<Longrightarrow> dL1 0 = Some (pair None cnL)
  \<Longrightarrow> dL2 0 = Some (pair None cnL)
  \<Longrightarrow> dL1 nL1 = Some (pair enL1 cnL1)
  \<Longrightarrow> dL2 nL2 = Some (pair enL2 cnL2)
  \<Longrightarrow> en1 = en2"

context ATS_Simulation_Configuration_WeakDET begin

theorem is_forward_edge_deterministic_accessible_is_preserved: "
  relation_TSstructureRL G2 G1
  \<Longrightarrow> LR.GL.is_forward_edge_deterministic_accessible G1
  \<Longrightarrow> LR.GR.is_forward_edge_deterministic_accessible G2"
  apply(simp add: LR.GR.is_forward_edge_deterministic_accessible_def)
  apply(clarsimp)
  apply(rename_tac c c1 c2 e1 e2)(*strict*)
  apply(simp add: LR.GR.get_accessible_configurations_def)
  apply(clarsimp)
  apply(rename_tac c c1 c2 e1 e2 d i)(*strict*)
  apply(simp add: get_configuration_def)
  apply(case_tac "d i")
   apply(rename_tac c c1 c2 e1 e2 d i)(*strict*)
   apply(force)
  apply(rename_tac c c1 c2 e1 e2 d i a)(*strict*)
  apply(clarsimp)
  apply(case_tac a)
  apply(rename_tac c c1 c2 e1 e2 d i a option b)(*strict*)
  apply(clarsimp)
  apply(rename_tac c c1 c2 e1 e2 d i option)(*strict*)
  apply(rename_tac e)
  apply(rename_tac c c1 c2 e1 e2 d i e)(*strict*)
  apply(rename_tac cnR cnR1 cnR2 en1 en2 d i enR)
  apply(rename_tac cnR cnR1 cnR2 en1 en2 d i enR)(*strict*)
  apply(subgoal_tac "\<exists>dR nR. maximum_of_domain dR nR \<and> ATS.derivation_initial initial_configurations2 step_relation2 G2 dR \<and> dR nR = Some (pair enR cnR)")
   apply(rename_tac cnR cnR1 cnR2 en1 en2 d i enR)(*strict*)
   prefer 2
   apply(rule_tac
      x="derivation_take d i"
      in exI)
   apply(rule_tac
      x="i"
      in exI)
   apply(rule conjI)
    apply(rename_tac cnR cnR1 cnR2 en1 en2 d i enR)(*strict*)
    apply(rule maximum_of_domain_derivation_take)
    apply(force)
   apply(rename_tac cnR cnR1 cnR2 en1 en2 d i enR)(*strict*)
   apply(rule conjI)
    apply(rename_tac cnR cnR1 cnR2 en1 en2 d i enR)(*strict*)
    apply(rule LR.GR.derivation_take_preserves_derivation_initial)
    apply(force)
   apply(rename_tac cnR cnR1 cnR2 en1 en2 d i enR)(*strict*)
   apply(simp add: derivation_take_def)
  apply(rename_tac cnR cnR1 cnR2 en1 en2 d i enR)(*strict*)
  apply(clarsimp)
  apply(rename_tac cnR cnR1 cnR2 en1 en2 d i enR dR nR)(*strict*)
  apply(thin_tac "ATS.derivation_initial initial_configurations2 step_relation2 G2 d")
  apply(thin_tac "d i = Some (pair enR cnR)")
  apply(clarsimp)
  apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR)(*strict*)
  apply(subgoal_tac "\<exists>d2 n2. LR.GL.derivation_initial G1 d2 \<and> maximum_of_domain d2 n2 \<and> relation_initial_configurationRL G2 G1 (the (get_configuration (dR 0))) (the (get_configuration (d2 0))) \<and> relation_configurationRL G2 G1 cnR (the (get_configuration (d2 n2)))")
   apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR)(*strict*)
   prefer 2
   apply(rule RL.ATS_Simulation_Configuration_Weak_simulation_derivation_exists)
     apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR)(*strict*)
     apply(force)
    apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR)(*strict*)
    apply(force)
   apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR)(*strict*)
   apply(force)
  apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR)(*strict*)
  apply(clarsimp)
  apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR d2 n2)(*strict*)
  apply(simp add: get_configuration_def)
  apply(subgoal_tac "\<exists>c. dR 0 = Some (pair None c)")
   apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR d2 n2)(*strict*)
   prefer 2
   apply (metis LR.GR.derivation_initial_is_derivation LR.GR.some_position_has_details_at_0)
  apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR d2 n2)(*strict*)
  apply(subgoal_tac "\<exists>c. d2 0 = Some (pair None c)")
   apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR d2 n2)(*strict*)
   prefer 2
   apply (metis LR.GL.derivation_initial_is_derivation LR.GL.some_position_has_details_at_0)
  apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR d2 n2)(*strict*)
  apply(clarsimp)
  apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR d2 n2 c ca)(*strict*)
  apply(subgoal_tac "\<exists>e c. d2 n2 = Some (pair e c)")
   apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR d2 n2 c ca)(*strict*)
   prefer 2
   apply(rule LR.GL.some_position_has_details_before_max_dom)
     apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR d2 n2 c ca)(*strict*)
     apply(rule LR.GL.derivation_initial_is_derivation)
     apply(force)
    apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR d2 n2 c ca)(*strict*)
    apply(force)
   apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR d2 n2 c ca)(*strict*)
   apply(force)
  apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR d2 n2 c ca)(*strict*)
  apply(clarsimp)
  apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR d2 n2 c ca e cb)(*strict*)
  apply(rename_tac dL nL c0R c0L enL cnL)
  apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR dL nL c0R c0L enL cnL)(*strict*)
  apply(subgoal_tac "\<exists>d2 n. LR.GL.derivation G1 d2 \<and> LR.GL.belongs G1 d2 \<and> the(get_configuration(d2 0)) = cnL \<and> relation_step_simulationLRRL G2 G1 cnR en1 cnR1 cnL d2 \<and> maximum_of_domain d2 n \<and> relation_configurationRL G2 G1 cnR1 (the(get_configuration(d2 n)))")
   apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR dL nL c0R c0L enL cnL)(*strict*)
   apply(subgoal_tac "\<exists>d2 n. LR.GL.derivation G1 d2 \<and> LR.GL.belongs G1 d2 \<and> the(get_configuration(d2 0)) = cnL \<and> relation_step_simulationLRRL G2 G1 cnR en2 cnR2 cnL d2 \<and> maximum_of_domain d2 n \<and> relation_configurationRL G2 G1 cnR2 (the(get_configuration(d2 n)))")
    apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR dL nL c0R c0L enL cnL)(*strict*)
    apply(clarsimp)
    apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR dL nL c0R c0L enL d2 d2a n na)(*strict*)
    apply(simp add: get_configuration_def)
    apply(subgoal_tac "\<exists>c. d2 0 = Some (pair None c)")
     apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR dL nL c0R c0L enL d2 d2a n na)(*strict*)
     prefer 2
     apply (metis LR.GL.some_position_has_details_at_0)
    apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR dL nL c0R c0L enL d2 d2a n na)(*strict*)
    apply(clarsimp)
    apply(subgoal_tac "\<exists>c. d2a 0 = Some (pair None c)")
     apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR dL nL c0R c0L enL d2 d2a n na)(*strict*)
     prefer 2
     apply (metis LR.GL.some_position_has_details_at_0)
    apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR dL nL c0R c0L enL d2 d2a n na)(*strict*)
    apply(clarsimp)
    apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR dL nL c0R c0L enL d2 d2a n na c)(*strict*)
    apply(subgoal_tac "\<exists>e c. d2 n = Some (pair e c)")
     apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR dL nL c0R c0L enL d2 d2a n na c)(*strict*)
     prefer 2
     apply(rule LR.GL.some_position_has_details_before_max_dom)
       apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR dL nL c0R c0L enL d2 d2a n na c)(*strict*)
       apply(force)
      apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR dL nL c0R c0L enL d2 d2a n na c)(*strict*)
      apply(force)
     apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR dL nL c0R c0L enL d2 d2a n na c)(*strict*)
     apply(force)
    apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR dL nL c0R c0L enL d2 d2a n na c)(*strict*)
    apply(subgoal_tac "\<exists>e c. d2a na = Some (pair e c)")
     apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR dL nL c0R c0L enL d2 d2a n na c)(*strict*)
     prefer 2
     apply(rule LR.GL.some_position_has_details_before_max_dom)
       apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR dL nL c0R c0L enL d2 d2a n na c)(*strict*)
       apply(force)
      apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR dL nL c0R c0L enL d2 d2a n na c)(*strict*)
      apply(force)
     apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR dL nL c0R c0L enL d2 d2a n na c)(*strict*)
     apply(force)
    apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR dL nL c0R c0L enL d2 d2a n na c)(*strict*)
    apply(clarsimp)
    apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR dL nL c0R c0L enL d2 d2a n na c e ea ca cb)(*strict*)
    apply(rename_tac dL1 dL2 nL1 nL2 cnL enL1 enL2 cnL1 cnL2)
    apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR dL nL c0R c0L enL dL1 dL2 nL1 nL2 cnL enL1 enL2 cnL1 cnL2)(*strict*)
    prefer 2
    apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR dL nL c0R c0L enL cnL)(*strict*)
    apply(rule RL.AX_relation_step_simulation)
       apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR dL nL c0R c0L enL cnL)(*strict*)
       apply(force)
      apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR dL nL c0R c0L enL cnL)(*strict*)
      apply(force)
     apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR dL nL c0R c0L enL cnL)(*strict*)
     apply (metis LR.GR.belongs_configurations LR.GR.derivation_initial_belongs LR.GR.AX_step_relation_preserves_belongsE RL.AX_TSstructure_relation_TSstructure1_belongs)
    apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR dL nL c0R c0L enL cnL)(*strict*)
    apply(force)
   apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR dL nL c0R c0L enL dL1 dL2 nL1 nL2 cnL enL1 enL2 cnL1 cnL2)(*strict*)
   prefer 2
   apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR dL nL c0R c0L enL cnL)(*strict*)
   apply(rule RL.AX_relation_step_simulation)
      apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR dL nL c0R c0L enL cnL)(*strict*)
      apply(force)
     apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR dL nL c0R c0L enL cnL)(*strict*)
     apply(force)
    apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR dL nL c0R c0L enL cnL)(*strict*)
    apply (metis LR.GR.belongs_configurations LR.GR.derivation_initial_belongs LR.GR.AX_step_relation_preserves_belongsE RL.AX_TSstructure_relation_TSstructure1_belongs)
   apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR dL nL c0R c0L enL cnL)(*strict*)
   apply(force)
  apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR dL nL c0R c0L enL dL1 dL2 nL1 nL2 cnL enL1 enL2 cnL1 cnL2)(*strict*)
  apply(rule_tac
      ?G1.0="G1"
      and dR="dR"
      and ?dL1.0="dL1"
      and ?dL2.0="dL2"
      in AX_backwards_determinism)
                      apply(rename_tac cnR cnR1 cnR2 en1 en2 enR dR nR dL nL c0R c0L enL dL1 dL2 nL1 nL2 cnL enL1 enL2 cnL1 cnL2)(*strict*)
                      apply(force)+
  done

end

end

author: ControllerSynthesis

repo: Isabelle


text:
(*  Title:      HOL/Factorial.thy
    Author:     Jacques D. Fleuriot
    Author:     Lawrence C Paulson
    Author:     Jeremy Avigad
    Author:     Chaitanya Mangla
    Author:     Manuel Eberl
*)

section \<open>Factorial Function, Rising Factorials\<close>

theory Factorial
  imports Groups_List
begin

subsection \<open>Factorial Function\<close>

context semiring_char_0
begin

definition fact :: "nat \<Rightarrow> 'a"
  where fact_prod: "fact n = of_nat (\<Prod>{1..n})"

lemma fact_prod_Suc: "fact n = of_nat (prod Suc {0..<n})"
  unfolding fact_prod using atLeast0LessThan prod.atLeast1_atMost_eq by auto

lemma fact_prod_rev: "fact n = of_nat (\<Prod>i = 0..<n. n - i)"
proof -
  have "prod Suc {0..<n} = \<Prod>{1..n}"
    by (simp add: atLeast0LessThan prod.atLeast1_atMost_eq)
  then have "prod Suc {0..<n} = prod ((-) (n + 1)) {1..n}"
    using prod.atLeastAtMost_rev [of "\<lambda>i. i" 1 n] by presburger
  then show ?thesis
    unfolding fact_prod_Suc by (simp add: atLeast0LessThan prod.atLeast1_atMost_eq)
qed

lemma fact_0 [simp]: "fact 0 = 1"
  by (simp add: fact_prod)

lemma fact_1 [simp]: "fact 1 = 1"
  by (simp add: fact_prod)

lemma fact_Suc_0 [simp]: "fact (Suc 0) = 1"
  by (simp add: fact_prod)

lemma fact_Suc [simp]: "fact (Suc n) = of_nat (Suc n) * fact n"
  by (simp add: fact_prod atLeastAtMostSuc_conv algebra_simps)

lemma fact_2 [simp]: "fact 2 = 2"
  by (simp add: numeral_2_eq_2)

lemma fact_split: "k \<le> n \<Longrightarrow> fact n = of_nat (prod Suc {n - k..<n}) * fact (n - k)"
  by (simp add: fact_prod_Suc prod.union_disjoint [symmetric]
    ivl_disj_un ac_simps of_nat_mult [symmetric])

end

lemma of_nat_fact [simp]: "of_nat (fact n) = fact n"
  by (simp add: fact_prod)

lemma of_int_fact [simp]: "of_int (fact n) = fact n"
  by (simp only: fact_prod of_int_of_nat_eq)

lemma fact_reduce: "n > 0 \<Longrightarrow> fact n = of_nat n * fact (n - 1)"
  by (cases n) auto

lemma fact_nonzero [simp]: "fact n \<noteq> (0::'a::{semiring_char_0,semiring_no_zero_divisors})"
  using of_nat_0_neq by (induct n) auto

lemma fact_mono_nat: "m \<le> n \<Longrightarrow> fact m \<le> (fact n :: nat)"
  by (induct n) (auto simp: le_Suc_eq)

lemma fact_in_Nats: "fact n \<in> \<nat>"
  by (induct n) auto

lemma fact_in_Ints: "fact n \<in> \<int>"
  by (induct n) auto

context
  assumes "SORT_CONSTRAINT('a::linordered_semidom)"
begin

lemma fact_mono: "m \<le> n \<Longrightarrow> fact m \<le> (fact n :: 'a)"
  by (metis of_nat_fact of_nat_le_iff fact_mono_nat)

lemma fact_ge_1 [simp]: "fact n \<ge> (1 :: 'a)"
  by (metis le0 fact_0 fact_mono)

lemma fact_gt_zero [simp]: "fact n > (0 :: 'a)"
  using fact_ge_1 less_le_trans zero_less_one by blast

lemma fact_ge_zero [simp]: "fact n \<ge> (0 :: 'a)"
  by (simp add: less_imp_le)

lemma fact_not_neg [simp]: "\<not> fact n < (0 :: 'a)"
  by (simp add: not_less_iff_gr_or_eq)

lemma fact_le_power: "fact n \<le> (of_nat (n^n) :: 'a)"
proof (induct n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  then have *: "fact n \<le> (of_nat (Suc n ^ n) ::'a)"
    by (rule order_trans) (simp add: power_mono del: of_nat_power)
  have "fact (Suc n) = (of_nat (Suc n) * fact n ::'a)"
    by (simp add: algebra_simps)
  also have "\<dots> \<le> of_nat (Suc n) * of_nat (Suc n ^ n)"
    by (simp add: * ordered_comm_semiring_class.comm_mult_left_mono del: of_nat_power)
  also have "\<dots> \<le> of_nat (Suc n ^ Suc n)"
    by (metis of_nat_mult order_refl power_Suc)
  finally show ?case .
qed

end

lemma fact_less_mono_nat: "0 < m \<Longrightarrow> m < n \<Longrightarrow> fact m < (fact n :: nat)"
  by (induct n) (auto simp: less_Suc_eq)

lemma fact_less_mono: "0 < m \<Longrightarrow> m < n \<Longrightarrow> fact m < (fact n :: 'a::linordered_semidom)"
  by (metis of_nat_fact of_nat_less_iff fact_less_mono_nat)

lemma fact_ge_Suc_0_nat [simp]: "fact n \<ge> Suc 0"
  by (metis One_nat_def fact_ge_1)

lemma dvd_fact: "1 \<le> m \<Longrightarrow> m \<le> n \<Longrightarrow> m dvd fact n"
  by (induct n) (auto simp: dvdI le_Suc_eq)

lemma fact_ge_self: "fact n \<ge> n"
  by (cases "n = 0") (simp_all add: dvd_imp_le dvd_fact)

lemma fact_dvd: "n \<le> m \<Longrightarrow> fact n dvd (fact m :: 'a::linordered_semidom)"
  by (induct m) (auto simp: le_Suc_eq)

lemma fact_mod: "m \<le> n \<Longrightarrow> fact n mod (fact m :: 'a::{semidom_modulo, linordered_semidom}) = 0"
  by (simp add: mod_eq_0_iff_dvd fact_dvd)

lemma fact_eq_fact_times:
  assumes "m \<ge> n"
  shows "fact m = fact n * \<Prod>{Suc n..m}"
  unfolding fact_prod
  by (metis add.commute assms le_add1 le_add_diff_inverse of_nat_id plus_1_eq_Suc prod.ub_add_nat)

lemma fact_div_fact:
  assumes "m \<ge> n"
  shows "fact m div fact n = \<Prod>{n + 1..m}"
  by (simp add: fact_eq_fact_times [OF assms])

lemma fact_num_eq_if: "fact m = (if m = 0 then 1 else of_nat m * fact (m - 1))"
  by (cases m) auto

lemma fact_div_fact_le_pow:
  assumes "r \<le> n"
  shows "fact n div fact (n - r) \<le> n ^ r"
proof -
  have "r \<le> n \<Longrightarrow> \<Prod>{n - r..n} = (n - r) * \<Prod>{Suc (n - r)..n}" for r
    by (subst prod.insert[symmetric]) (auto simp: atLeastAtMost_insertL)
  with assms show ?thesis
    by (induct r rule: nat.induct) (auto simp add: fact_div_fact Suc_diff_Suc mult_le_mono)
qed

lemma prod_Suc_fact: "prod Suc {0..<n} = fact n"
  by (simp add: fact_prod_Suc)

lemma prod_Suc_Suc_fact: "prod Suc {Suc 0..<n} = fact n"
proof (cases "n = 0")
  case True
  then show ?thesis by simp
next
  case False
  have "prod Suc {Suc 0..<n} = Suc 0 * prod Suc {Suc 0..<n}"
    by simp
  also have "\<dots> = prod Suc (insert 0 {Suc 0..<n})"
    by simp
  also have "insert 0 {Suc 0..<n} = {0..<n}"
    using False by auto
  finally show ?thesis
    by (simp add: fact_prod_Suc)
qed

lemma fact_numeral: "fact (numeral k) = numeral k * fact (pred_numeral k)"
  \<comment> \<open>Evaluation for specific numerals\<close>
  by (metis fact_Suc numeral_eq_Suc of_nat_numeral)

subsection \<open>Pochhammer's symbol: generalized rising factorial\<close>

text \<open>See \<^url>\<open>https://en.wikipedia.org/wiki/Pochhammer_symbol\<close>.\<close>

context comm_semiring_1
begin

definition pochhammer :: "'a \<Rightarrow> nat \<Rightarrow> 'a"
  where pochhammer_prod: "pochhammer a n = prod (\<lambda>i. a + of_nat i) {0..<n}"

lemma pochhammer_prod_rev: "pochhammer a n = prod (\<lambda>i. a + of_nat (n - i)) {1..n}"
  using prod.atLeastLessThan_rev_at_least_Suc_atMost [of "\<lambda>i. a + of_nat i" 0 n]
  by (simp add: pochhammer_prod)

lemma pochhammer_Suc_prod: "pochhammer a (Suc n) = prod (\<lambda>i. a + of_nat i) {0..n}"
  by (simp add: pochhammer_prod atLeastLessThanSuc_atLeastAtMost)

lemma pochhammer_Suc_prod_rev: "pochhammer a (Suc n) = prod (\<lambda>i. a + of_nat (n - i)) {0..n}"
  using prod.atLeast_Suc_atMost_Suc_shift
  by (simp add: pochhammer_prod_rev prod.atLeast_Suc_atMost_Suc_shift del: prod.cl_ivl_Suc)

lemma pochhammer_0 [simp]: "pochhammer a 0 = 1"
  by (simp add: pochhammer_prod)

lemma pochhammer_1 [simp]: "pochhammer a 1 = a"
  by (simp add: pochhammer_prod lessThan_Suc)

lemma pochhammer_Suc0 [simp]: "pochhammer a (Suc 0) = a"
  by (simp add: pochhammer_prod lessThan_Suc)

lemma pochhammer_Suc: "pochhammer a (Suc n) = pochhammer a n * (a + of_nat n)"
  by (simp add: pochhammer_prod atLeast0_lessThan_Suc ac_simps)

end

lemma pochhammer_nonneg:
  fixes x :: "'a :: linordered_semidom"
  shows "x > 0 \<Longrightarrow> pochhammer x n \<ge> 0"
  by (induction n) (auto simp: pochhammer_Suc intro!: mult_nonneg_nonneg add_nonneg_nonneg)

lemma pochhammer_pos:
  fixes x :: "'a :: linordered_semidom"
  shows "x > 0 \<Longrightarrow> pochhammer x n > 0"
  by (induction n) (auto simp: pochhammer_Suc intro!: mult_pos_pos add_pos_nonneg)

context comm_semiring_1
begin

lemma pochhammer_of_nat: "pochhammer (of_nat x) n = of_nat (pochhammer x n)"
  by (simp add: pochhammer_prod Factorial.pochhammer_prod)

end

context comm_ring_1
begin

lemma pochhammer_of_int: "pochhammer (of_int x) n = of_int (pochhammer x n)"
  by (simp add: pochhammer_prod Factorial.pochhammer_prod)

end

lemma pochhammer_rec: "pochhammer a (Suc n) = a * pochhammer (a + 1) n"
  by (simp add: pochhammer_prod prod.atLeast0_lessThan_Suc_shift ac_simps del: prod.op_ivl_Suc)

lemma pochhammer_rec': "pochhammer z (Suc n) = (z + of_nat n) * pochhammer z n"
  by (simp add: pochhammer_prod prod.atLeast0_lessThan_Suc ac_simps)

lemma pochhammer_fact: "fact n = pochhammer 1 n"
  by (simp add: pochhammer_prod fact_prod_Suc)

lemma pochhammer_of_nat_eq_0_lemma: "k > n \<Longrightarrow> pochhammer (- (of_nat n :: 'a:: idom)) k = 0"
  by (auto simp add: pochhammer_prod)

lemma pochhammer_of_nat_eq_0_lemma':
  assumes kn: "k \<le> n"
  shows "pochhammer (- (of_nat n :: 'a::{idom,ring_char_0})) k \<noteq> 0"
proof (cases k)
  case 0
  then show ?thesis by simp
next
  case (Suc h)
  then show ?thesis
    apply (simp add: pochhammer_Suc_prod)
    using Suc kn
    apply (auto simp add: algebra_simps)
    done
qed

lemma pochhammer_of_nat_eq_0_iff:
  "pochhammer (- (of_nat n :: 'a::{idom,ring_char_0})) k = 0 \<longleftrightarrow> k > n"
  (is "?l = ?r")
  using pochhammer_of_nat_eq_0_lemma[of n k, where ?'a='a]
    pochhammer_of_nat_eq_0_lemma'[of k n, where ?'a = 'a]
  by (auto simp add: not_le[symmetric])

lemma pochhammer_0_left:
  "pochhammer 0 n = (if n = 0 then 1 else 0)"
  by (induction n) (simp_all add: pochhammer_rec)

lemma pochhammer_eq_0_iff: "pochhammer a n = (0::'a::field_char_0) \<longleftrightarrow> (\<exists>k < n. a = - of_nat k)"
  by (auto simp add: pochhammer_prod eq_neg_iff_add_eq_0)

lemma pochhammer_eq_0_mono:
  "pochhammer a n = (0::'a::field_char_0) \<Longrightarrow> m \<ge> n \<Longrightarrow> pochhammer a m = 0"
  unfolding pochhammer_eq_0_iff by auto

lemma pochhammer_neq_0_mono:
  "pochhammer a m \<noteq> (0::'a::field_char_0) \<Longrightarrow> m \<ge> n \<Longrightarrow> pochhammer a n \<noteq> 0"
  unfolding pochhammer_eq_0_iff by auto

lemma pochhammer_minus:
  "pochhammer (- b) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (b - of_nat k + 1) k"
proof (cases k)
  case 0
  then show ?thesis by simp
next
  case (Suc h)
  have eq: "((- 1) ^ Suc h :: 'a) = (\<Prod>i = 0..h. - 1)"
    using prod_constant [where A="{0.. h}" and y="- 1 :: 'a"]
    by auto
  with Suc show ?thesis
    using pochhammer_Suc_prod_rev [of "b - of_nat k + 1"]
    by (auto simp add: pochhammer_Suc_prod prod.distrib [symmetric] eq of_nat_diff simp del: prod_constant)
qed

lemma pochhammer_minus':
  "pochhammer (b - of_nat k + 1) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (- b) k"
  by (simp add: pochhammer_minus)

lemma pochhammer_same: "pochhammer (- of_nat n) n =
    ((- 1) ^ n :: 'a::{semiring_char_0,comm_ring_1,semiring_no_zero_divisors}) * fact n"
  unfolding pochhammer_minus
  by (simp add: of_nat_diff pochhammer_fact)

lemma pochhammer_product': "pochhammer z (n + m) = pochhammer z n * pochhammer (z + of_nat n) m"
proof (induct n arbitrary: z)
  case 0
  then show ?case by simp
next
  case (Suc n z)
  have "pochhammer z (Suc n) * pochhammer (z + of_nat (Suc n)) m =
      z * (pochhammer (z + 1) n * pochhammer (z + 1 + of_nat n) m)"
    by (simp add: pochhammer_rec ac_simps)
  also note Suc[symmetric]
  also have "z * pochhammer (z + 1) (n + m) = pochhammer z (Suc (n + m))"
    by (subst pochhammer_rec) simp
  finally show ?case
    by simp
qed

lemma pochhammer_product:
  "m \<le> n \<Longrightarrow> pochhammer z n = pochhammer z m * pochhammer (z + of_nat m) (n - m)"
  using pochhammer_product'[of z m "n - m"] by simp

lemma pochhammer_times_pochhammer_half:
  fixes z :: "'a::field_char_0"
  shows "pochhammer z (Suc n) * pochhammer (z + 1/2) (Suc n) = (\<Prod>k=0..2*n+1. z + of_nat k / 2)"
proof (induct n)
  case 0
  then show ?case
    by (simp add: atLeast0_atMost_Suc)
next
  case (Suc n)
  define n' where "n' = Suc n"
  have "pochhammer z (Suc n') * pochhammer (z + 1 / 2) (Suc n') =
      (pochhammer z n' * pochhammer (z + 1 / 2) n') * ((z + of_nat n') * (z + 1/2 + of_nat n'))"
    (is "_ = _ * ?A")
    by (simp_all add: pochhammer_rec' mult_ac)
  also have "?A = (z + of_nat (Suc (2 * n + 1)) / 2) * (z + of_nat (Suc (Suc (2 * n + 1))) / 2)"
    (is "_ = ?B")
    by (simp add: field_simps n'_def)
  also note Suc[folded n'_def]
  also have "(\<Prod>k=0..2 * n + 1. z + of_nat k / 2) * ?B = (\<Prod>k=0..2 * Suc n + 1. z + of_nat k / 2)"
    by (simp add: atLeast0_atMost_Suc)
  finally show ?case
    by (simp add: n'_def)
qed

lemma pochhammer_double:
  fixes z :: "'a::field_char_0"
  shows "pochhammer (2 * z) (2 * n) = of_nat (2^(2*n)) * pochhammer z n * pochhammer (z+1/2) n"
proof (induct n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  have "pochhammer (2 * z) (2 * (Suc n)) = pochhammer (2 * z) (2 * n) *
      (2 * (z + of_nat n)) * (2 * (z + of_nat n) + 1)"
    by (simp add: pochhammer_rec' ac_simps)
  also note Suc
  also have "of_nat (2 ^ (2 * n)) * pochhammer z n * pochhammer (z + 1/2) n *
        (2 * (z + of_nat n)) * (2 * (z + of_nat n) + 1) =
      of_nat (2 ^ (2 * (Suc n))) * pochhammer z (Suc n) * pochhammer (z + 1/2) (Suc n)"
    by (simp add: field_simps pochhammer_rec')
  finally show ?case .
qed

lemma fact_double:
  "fact (2 * n) = (2 ^ (2 * n) * pochhammer (1 / 2) n * fact n :: 'a::field_char_0)"
  using pochhammer_double[of "1/2::'a" n] by (simp add: pochhammer_fact)

lemma pochhammer_absorb_comp: "(r - of_nat k) * pochhammer (- r) k = r * pochhammer (-r + 1) k"
  (is "?lhs = ?rhs")
  for r :: "'a::comm_ring_1"
proof -
  have "?lhs = - pochhammer (- r) (Suc k)"
    by (subst pochhammer_rec') (simp add: algebra_simps)
  also have "\<dots> = ?rhs"
    by (subst pochhammer_rec) simp
  finally show ?thesis .
qed

subsection \<open>Misc\<close>

lemma fact_code [code]:
  "fact n = (of_nat (fold_atLeastAtMost_nat ((*)) 2 n 1) :: 'a::semiring_char_0)"
proof -
  have "fact n = (of_nat (\<Prod>{1..n}) :: 'a)"
    by (simp add: fact_prod)
  also have "\<Prod>{1..n} = \<Prod>{2..n}"
    by (intro prod.mono_neutral_right) auto
  also have "\<dots> = fold_atLeastAtMost_nat ((*)) 2 n 1"
    by (simp add: prod_atLeastAtMost_code)
  finally show ?thesis .
qed

lemma pochhammer_code [code]:
  "pochhammer a n =
    (if n = 0 then 1
     else fold_atLeastAtMost_nat (\<lambda>n acc. (a + of_nat n) * acc) 0 (n - 1) 1)"
  by (cases n)
    (simp_all add: pochhammer_prod prod_atLeastAtMost_code [symmetric]
      atLeastLessThanSuc_atLeastAtMost)

lemma mult_less_iff1: "0 < z \<Longrightarrow> x * z < y * z \<longleftrightarrow> x < y"
  for x y z :: "'a::linordered_idom"
  by simp

lemma mult_le_cancel_iff1: "0 < z \<Longrightarrow> x * z \<le> y * z \<longleftrightarrow> x \<le> y"
  for x y z :: "'a::linordered_idom"
  by simp

lemma mult_le_cancel_iff2: "0 < z \<Longrightarrow> z * x \<le> z * y \<longleftrightarrow> x \<le> y"
  for x y z :: "'a::linordered_idom"
  by simp

end

repo: isabelle


text:
theory Submission
  imports Defs
begin

inductive path :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" for E where
  trivial: "path E [x]" |
  cont: "E a x \<Longrightarrow> path E (x#xs) \<Longrightarrow> path E (a#x#xs)"

lemma path_reverse: "path E (a#x#xs) \<Longrightarrow> (E a x \<and> path E (x#xs))"
  using Submission.path.cases by blast

lemma mono_path[simp]:
  assumes mono: "\<forall>a b. E a b \<longrightarrow> (f::'a \<Rightarrow> nat) a \<le> f b"
    and "path E (s # xs @ [t])"
  shows "f s \<le> f t"
  using assms proof(induction xs arbitrary: s t)
  case Nil
  then show ?case using path_reverse by fastforce
next
  case (Cons a xs)
  then have "E s a" using path_reverse
    by force
  then have "f s \<le> f a"
    using mono by blast
  moreover
  from Cons.prems Cons.IH have "f a \<le> f t" using path_reverse
    by force
  ultimately
  have "f s \<le> f t"
    using le_trans by blast
  thus ?case .
qed

theorem no_cycle:
  assumes mono: "\<forall>a b. E a b \<longrightarrow> (f::'a \<Rightarrow> nat) a \<le> f b"
      and fv_less: "\<forall>w. E v w \<longrightarrow> f v < f w"
  shows "\<not> (\<exists>xs. path E (v # xs @ [v]))"
proof
  assume path_ex:"\<exists>xs. path E (v # xs @ [v])"
  then obtain xs where p: "path E (v # xs @ [v])"
    by blast
  with fv_less have not_nil: "xs \<noteq> Nil" using path_reverse
    by fastforce
  then have "\<exists>x xs'. xs = x#xs'"
    using neq_Nil_conv by fastforce
  then obtain x xs' where split_xs: "xs = x#xs'"
    by blast
  from fv_less have "\<forall>x \<in> set xs. E v x \<longrightarrow> f v < f x"
    by blast
  with split_xs have "f v < f x"
    using p path_reverse by fastforce
  moreover
  from p have "path E (x # xs' @ [v])" using path_reverse split_xs
    by fastforce
  with mono have "f x \<le> f v" using mono_path
    by simp
  ultimately
  show False
    by linarith
qed

value "lval (Let ''x'' (N 5) (Let ''y'' (V ''x'') (Plus (V ''x'') (Plus (V ''y'') (V ''x''))))) <> = 15"

paragraph \<open>Step 1\<close>

fun replace :: "lexp \<Rightarrow> vname \<Rightarrow> lexp \<Rightarrow> lexp" where
  "replace e x (Let u a b) = Let u (replace e x a) (replace e x b)" |
  "replace e x (Plus a b) = (if e = Plus a b then V x else Plus (replace e x a) (replace e x b))" |
  "replace e x a = a"

paragraph \<open>Step 2\<close>

theorem lval_upd_state_same:
  "x \<notin> vars_of a \<Longrightarrow> lval a (s(x := v)) = lval a s"
  proof(induction a arbitrary: s)
    case (N x)
    then show ?case
      by simp
  next
    case (V x)
    then show ?case
      by simp
  next
    case (Plus a b)
    then show ?case
      by simp
  next
    case (Let n a b)
    then have n_noteq_x: "n \<noteq> x"
      by auto
    then obtain s' where s'_def: "s' = s(n := lval a s)"
      by blast
    have "lval (Let n a b) (s(x := v)) = lval b (s(x := v,n := lval a (s(x := v))))"
      by fastforce
    also have "... = lval b (s(x := v,n := lval a s))"
      using local.Let.IH(1) local.Let.prems by fastforce
    also have "... = lval b (s'(x := v))"
      using n_noteq_x s'_def by (simp add: fun_upd_twist)
    also have "... = lval b s'"
      using local.Let.IH(2) local.Let.prems by fastforce
    also have "... = lval b (s(n := lval a s))"
      using s'_def by simp
    also have "... = lval (Let n a b) s"
      by simp
    finally show ?case .
  qed

paragraph \<open>Step 3\<close>

theorem lval_replace:
  assumes "x \<notin> vars_of a"
      and "bounds_of a \<inter> vars_of e = {}"
    shows "lval (replace e x a) (s(x := lval e s)) = lval a s"
using assms proof(induction a arbitrary: x e s)
  case (N x)
  then show ?case by simp
next
  case (V x)
  then show ?case by simp
next
  case (Plus e1 e2)
  then show ?case
  proof(cases "e=Plus e1 e2")
    case True
    then show ?thesis
      by simp
  next
    case False
    from Plus.prems have x_not_in_sub: "x \<notin> vars_of e1" "x \<notin> vars_of e2"
      by simp+
    from Plus.prems have sub_dist_from_e: "bounds_of e1 \<inter> vars_of e = {}" "bounds_of e2 \<inter> vars_of e = {}"
      by auto
    from False have "replace e x (Plus e1 e2) = Plus (replace e x e1) (replace e x e2)"
      by simp
    then have "lval (replace e x (Plus e1 e2)) (s(x := lval e s))
      = lval (replace e x e1) (s(x := lval e s)) + lval (replace e x e2) (s(x := lval e s))"
      by simp
    also have "... = lval e1 s + lval e2 s"
      using Plus.IH Plus.prems x_not_in_sub sub_dist_from_e
      by presburger
    also have "... = lval (Plus e1 e2) s"
      by simp
    finally show ?thesis .
  qed
next
  case (Let u l r)
  from Let.prems(1) have x_not_in_sub: "x \<notin> vars_of l" "x \<notin> vars_of r"
    by auto
  from Let.prems(2) have sub_dist_from_e :
    "bounds_of l \<inter> vars_of e = {}"
    "bounds_of r \<inter> vars_of e = {}"
    by auto
  have u_not_x: "u \<noteq> x"
    using local.Let.prems(1) by fastforce
  then obtain s' where s'_def: "s' = s(u := lval l s)"
    by simp
  have
    "lval (replace e x (Let u l r)) (s(x := lval e s))
    = lval (Let u (replace e x l) (replace e x r)) (s(x := lval e s))"
    by simp
  also have
    "... = lval (replace e x r) (s(x := lval e s, u := lval (replace e x l) (s(x := lval e s))))"
    by simp
  also from Let.prems have "... = lval (replace e x r) (s(x := lval e s, u := lval l s))"
    using Let.IH(1) x_not_in_sub sub_dist_from_e
    by presburger
  also from u_not_x have "... = lval (replace e x r) (s(u := lval l s, x := lval e s))"
    by (simp add: fun_upd_twist)
  also from s'_def have "... = lval (replace e x r) (s'(x := lval e s'))"
    using Let.prems(2)
    by (simp add: lval_upd_state_same)
  also have "... = lval r s'"
    using Let.IH(2) x_not_in_sub sub_dist_from_e
    by blast
  also have "... = lval r (s(u := lval l s))"
    by (simp add: s'_def)
  also have "... = lval (Let u l r) s"
    by simp
  finally show ?case .
qed

paragraph \<open>Step 4\<close>

fun issubexp :: "lexp \<Rightarrow> lexp \<Rightarrow> bool" where
  "issubexp e (N x) = (e = N x)" |
  "issubexp e (V x) = (e = V x)" |
  "issubexp e (Plus a b) = (if e = Plus a b then True else issubexp e a \<or> issubexp e b)" |
  "issubexp e (Let x a b) = (if e = Let x a b then True else issubexp e a \<or> issubexp e b)"

fun reorder :: "lexp list \<Rightarrow> lexp list \<Rightarrow> lexp list" where
  "reorder [] acc = acc" |
  "reorder (x#xs) acc = (if x \<in> set acc then reorder xs acc else (if \<exists>e \<in> set acc. issubexp x e then reorder xs (acc@[x]) else reorder xs (x#acc)))"

definition linearize :: "lexp \<Rightarrow> lexp" where
 "linearize e = (let
     exps = reorder (duplicates  (collect e)) [];
     names = invent_names (length exps);
     m = zip exps names
   in fold (\<lambda>(a, x) e. Let x a (replace a x e)) m e)"

value "linearize (Plus (Plus (Plus (V ''a'') (N 3)) (N 4)) (Plus (V ''a'') (N 3)))
= Let ''v'' (Plus (V ''a'') (N 3)) (Plus (Plus (V ''v'') (N 4)) (V ''v''))"

value "linearize (Plus (Plus (Plus (V ''a'') (N 3)) (N 4)) (Plus (Plus (V ''a'') (N 3)) (N 4)))
= Let ''v'' (Plus (V ''a'') (N 3)) (Let ''vv'' (Plus (V ''v'') (N 4)) (Plus (V ''vv'') (V ''vv'')))"

paragraph \<open>(Bonus) Step 5\<close> (* incomplete *)

lemma reorder_distinct_gen: "distinct ys \<Longrightarrow> distinct (reorder xs ys)"
  by(induction xs ys rule: reorder.induct, auto)

lemma reorder_distinct: "distinct (reorder xs [])"
  using reorder_distinct_gen by simp

lemma lval_let_same:
  assumes "x \<notin> vars_of e"
      and "bounds_of e \<inter> vars_of a = {}"
    shows "lval (Let x a (replace a x e)) s = lval e s"
using assms proof(induction e arbitrary: x a s)
  case (N x)
  then show ?case by simp
next
  case (V x)
  then show ?case by simp
next
  case (Plus e1 e2)
  have "lval (Let x a (replace a x (Plus e1 e2))) s = lval (replace a x (Plus e1 e2)) (s(x := lval a s))"
    by auto
  also from Plus.prems have "... = lval (Plus e1 e2) s"
    using lval_replace[of "x" "Plus e1 e2" "a" "s"]
    by simp
  then show ?case
    using calculation by presburger
next
  case (Let x1a e1 e2)
  have "lval (Let x a (replace a x (Let x1a e1 e2))) s = lval (replace a x (Let x1a  e1 e2)) (s(x := lval a s))"
    by auto
  then show ?case sorry
qed

lemma move_linearize_in_plus: (* this one is missing *)
  assumes "\<forall>x. x \<in> vars_of (Plus a b) \<longrightarrow> CHR ''v'' \<notin> set x"
      and "bounds_of (Plus a b) = {}"
    shows "lval (linearize (Plus a b)) s = lval (linearize a) s + lval (linearize b) s"
using assms proof(induction a arbitrary: b s)
  case (N x)
  then show ?case
    sorry
next
  case (V x)
  then show ?case sorry
next
  case (Plus a1 a2)
  then show ?case sorry
next
  case (Let x1a a1 a2)
  then show ?case sorry
qed

lemma linearize_correct:
  assumes "\<forall>x. x \<in> vars_of e \<longrightarrow> CHR ''v'' \<notin> set x"
      and "bounds_of e = {}"
    shows "lval (linearize e) s = lval e s"
using assms proof(induction e arbitrary: s)
  case (N x)
  then show ?case
    using linearize_def by simp
next
  case (V x)
  then show ?case
  using linearize_def by simp
next
  case (Plus a b)
  then have "lval (linearize (Plus a b)) s = lval (linearize a) s + lval (linearize b) s"
    using move_linearize_in_plus by simp
  also from Plus.IH Plus.prems have "... =  lval b s + lval a s"
    by force
  also have "... = lval (Plus a b) s"
    by simp
  finally show ?case .
next
  case (Let x1a e1 e2)
  then have "lval (linearize e) s = lval (linearize b) (s(x := lval (linearize a) s))"
    using assms by auto
  then show ?case
    using Let.prems(2) by auto
qed

end

author: MaximilianAnzinger


text:
(*  Title:      HOL/Auth/n_german_lemma_on_inv__33.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_on_inv__33 imports n_german_base
begin
section{*All lemmas on causal relation between inv__33 and some rule r*}
lemma n_SendInvEVsinv__33:
assumes a1: "(\<exists> i. i\<le>N\<and>r=n_SendInvE  i)" and
a2: "(\<exists> p__Inv3 p__Inv4. p__Inv3\<le>N\<and>p__Inv4\<le>N\<and>p__Inv3~=p__Inv4\<and>f=inv__33  p__Inv3 p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain i where a1:"i\<le>N\<and>r=n_SendInvE  i" apply fastforce done
from a2 obtain p__Inv3 p__Inv4 where a2:"p__Inv3\<le>N\<and>p__Inv4\<le>N\<and>p__Inv3~=p__Inv4\<and>f=inv__33  p__Inv3 p__Inv4" apply fastforce done
have "(i=p__Inv4)\<or>(i=p__Inv3)\<or>(i~=p__Inv3\<and>i~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(i=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(i=p__Inv3)"
  have "?P3 s"
  apply (cut_tac a1 a2 b1, simp, rule_tac x="(neg (andForm (eqn (IVar (Para (Ident ''InvSet'') p__Inv3)) (Const true)) (eqn (IVar (Field (Para (Ident ''Chan2'') p__Inv4) ''Cmd'')) (Const GntE))))" in exI, auto) done
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(i~=p__Inv3\<and>i~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_SendInvSVsinv__33:
assumes a1: "(\<exists> i. i\<le>N\<and>r=n_SendInvS  i)" and
a2: "(\<exists> p__Inv3 p__Inv4. p__Inv3\<le>N\<and>p__Inv4\<le>N\<and>p__Inv3~=p__Inv4\<and>f=inv__33  p__Inv3 p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain i where a1:"i\<le>N\<and>r=n_SendInvS  i" apply fastforce done
from a2 obtain p__Inv3 p__Inv4 where a2:"p__Inv3\<le>N\<and>p__Inv4\<le>N\<and>p__Inv3~=p__Inv4\<and>f=inv__33  p__Inv3 p__Inv4" apply fastforce done
have "(i=p__Inv4)\<or>(i=p__Inv3)\<or>(i~=p__Inv3\<and>i~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(i=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(i=p__Inv3)"
  have "?P3 s"
  apply (cut_tac a1 a2 b1, simp, rule_tac x="(neg (andForm (eqn (IVar (Para (Ident ''InvSet'') p__Inv3)) (Const true)) (eqn (IVar (Field (Para (Ident ''Chan2'') p__Inv4) ''Cmd'')) (Const GntE))))" in exI, auto) done
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(i~=p__Inv3\<and>i~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_SendInvAckVsinv__33:
assumes a1: "(\<exists> i. i\<le>N\<and>r=n_SendInvAck  i)" and
a2: "(\<exists> p__Inv3 p__Inv4. p__Inv3\<le>N\<and>p__Inv4\<le>N\<and>p__Inv3~=p__Inv4\<and>f=inv__33  p__Inv3 p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain i where a1:"i\<le>N\<and>r=n_SendInvAck  i" apply fastforce done
from a2 obtain p__Inv3 p__Inv4 where a2:"p__Inv3\<le>N\<and>p__Inv4\<le>N\<and>p__Inv3~=p__Inv4\<and>f=inv__33  p__Inv3 p__Inv4" apply fastforce done
have "(i=p__Inv4)\<or>(i=p__Inv3)\<or>(i~=p__Inv3\<and>i~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(i=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(i=p__Inv3)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(i~=p__Inv3\<and>i~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_SendGntSVsinv__33:
assumes a1: "(\<exists> i. i\<le>N\<and>r=n_SendGntS  i)" and
a2: "(\<exists> p__Inv3 p__Inv4. p__Inv3\<le>N\<and>p__Inv4\<le>N\<and>p__Inv3~=p__Inv4\<and>f=inv__33  p__Inv3 p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain i where a1:"i\<le>N\<and>r=n_SendGntS  i" apply fastforce done
from a2 obtain p__Inv3 p__Inv4 where a2:"p__Inv3\<le>N\<and>p__Inv4\<le>N\<and>p__Inv3~=p__Inv4\<and>f=inv__33  p__Inv3 p__Inv4" apply fastforce done
have "(i=p__Inv4)\<or>(i=p__Inv3)\<or>(i~=p__Inv3\<and>i~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(i=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(i=p__Inv3)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(i~=p__Inv3\<and>i~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_SendGntEVsinv__33:
assumes a1: "(\<exists> i. i\<le>N\<and>r=n_SendGntE N i)" and
a2: "(\<exists> p__Inv3 p__Inv4. p__Inv3\<le>N\<and>p__Inv4\<le>N\<and>p__Inv3~=p__Inv4\<and>f=inv__33  p__Inv3 p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain i where a1:"i\<le>N\<and>r=n_SendGntE N i" apply fastforce done
from a2 obtain p__Inv3 p__Inv4 where a2:"p__Inv3\<le>N\<and>p__Inv4\<le>N\<and>p__Inv3~=p__Inv4\<and>f=inv__33  p__Inv3 p__Inv4" apply fastforce done
have "(i=p__Inv4)\<or>(i=p__Inv3)\<or>(i~=p__Inv3\<and>i~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(i=p__Inv4)"
  have "?P3 s"
  apply (cut_tac a1 a2 b1, simp, rule_tac x="(neg (andForm (eqn (IVar (Field (Para (Ident ''Chan2'') p__Inv3) ''Cmd'')) (Const Inv)) (eqn (IVar (Para (Ident ''ShrSet'') p__Inv3)) (Const false))))" in exI, auto) done
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(i=p__Inv3)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(i~=p__Inv3\<and>i~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_RecvGntSVsinv__33:
assumes a1: "(\<exists> i. i\<le>N\<and>r=n_RecvGntS  i)" and
a2: "(\<exists> p__Inv3 p__Inv4. p__Inv3\<le>N\<and>p__Inv4\<le>N\<and>p__Inv3~=p__Inv4\<and>f=inv__33  p__Inv3 p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain i where a1:"i\<le>N\<and>r=n_RecvGntS  i" apply fastforce done
from a2 obtain p__Inv3 p__Inv4 where a2:"p__Inv3\<le>N\<and>p__Inv4\<le>N\<and>p__Inv3~=p__Inv4\<and>f=inv__33  p__Inv3 p__Inv4" apply fastforce done
have "(i=p__Inv4)\<or>(i=p__Inv3)\<or>(i~=p__Inv3\<and>i~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(i=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(i=p__Inv3)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(i~=p__Inv3\<and>i~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_RecvGntEVsinv__33:
assumes a1: "(\<exists> i. i\<le>N\<and>r=n_RecvGntE  i)" and
a2: "(\<exists> p__Inv3 p__Inv4. p__Inv3\<le>N\<and>p__Inv4\<le>N\<and>p__Inv3~=p__Inv4\<and>f=inv__33  p__Inv3 p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain i where a1:"i\<le>N\<and>r=n_RecvGntE  i" apply fastforce done
from a2 obtain p__Inv3 p__Inv4 where a2:"p__Inv3\<le>N\<and>p__Inv4\<le>N\<and>p__Inv3~=p__Inv4\<and>f=inv__33  p__Inv3 p__Inv4" apply fastforce done
have "(i=p__Inv4)\<or>(i=p__Inv3)\<or>(i~=p__Inv3\<and>i~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(i=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(i=p__Inv3)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(i~=p__Inv3\<and>i~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_StoreVsinv__33:
  assumes a1: "\<exists> i d. i\<le>N\<and>d\<le>N\<and>r=n_Store  i d" and
  a2: "(\<exists> p__Inv3 p__Inv4. p__Inv3\<le>N\<and>p__Inv4\<le>N\<and>p__Inv3~=p__Inv4\<and>f=inv__33  p__Inv3 p__Inv4)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_SendReqESVsinv__33:
  assumes a1: "\<exists> i. i\<le>N\<and>r=n_SendReqES  i" and
  a2: "(\<exists> p__Inv3 p__Inv4. p__Inv3\<le>N\<and>p__Inv4\<le>N\<and>p__Inv3~=p__Inv4\<and>f=inv__33  p__Inv3 p__Inv4)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_RecvInvAckVsinv__33:
  assumes a1: "\<exists> i. i\<le>N\<and>r=n_RecvInvAck  i" and
  a2: "(\<exists> p__Inv3 p__Inv4. p__Inv3\<le>N\<and>p__Inv4\<le>N\<and>p__Inv3~=p__Inv4\<and>f=inv__33  p__Inv3 p__Inv4)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_RecvReqVsinv__33:
  assumes a1: "\<exists> i. i\<le>N\<and>r=n_RecvReq N i" and
  a2: "(\<exists> p__Inv3 p__Inv4. p__Inv3\<le>N\<and>p__Inv4\<le>N\<and>p__Inv3~=p__Inv4\<and>f=inv__33  p__Inv3 p__Inv4)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_SendReqSVsinv__33:
  assumes a1: "\<exists> j. j\<le>N\<and>r=n_SendReqS  j" and
  a2: "(\<exists> p__Inv3 p__Inv4. p__Inv3\<le>N\<and>p__Inv4\<le>N\<and>p__Inv3~=p__Inv4\<and>f=inv__33  p__Inv3 p__Inv4)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_SendReqEIVsinv__33:
  assumes a1: "\<exists> i. i\<le>N\<and>r=n_SendReqEI  i" and
  a2: "(\<exists> p__Inv3 p__Inv4. p__Inv3\<le>N\<and>p__Inv4\<le>N\<and>p__Inv3~=p__Inv4\<and>f=inv__33  p__Inv3 p__Inv4)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

end

author: paraVerifier

repo: paraVerifier


text:
(*  Title:      HOL/HOLCF/IMP/HoareEx.thy
    Author:     Tobias Nipkow, TUM
    Copyright   1997 TUM
*)

section "Correctness of Hoare by Fixpoint Reasoning"

theory HoareEx imports Denotational begin

text \<open>
  An example from the HOLCF paper by Müller, Nipkow, Oheimb, Slotosch
  @{cite MuellerNvOS99}.  It demonstrates fixpoint reasoning by showing
  the correctness of the Hoare rule for while-loops.
\<close>

type_synonym assn = "state \<Rightarrow> bool"

definition
  hoare_valid :: "[assn, com, assn] \<Rightarrow> bool"  ("|= {(1_)}/ (_)/ {(1_)}" 50) where
  "|= {P} c {Q} = (\<forall>s t. P s \<and> D c\<cdot>(Discr s) = Def t \<longrightarrow> Q t)"

lemma WHILE_rule_sound:
    "|= {A} c {A} \<Longrightarrow> |= {A} WHILE b DO c {\<lambda>s. A s \<and> \<not> bval b s}"
  apply (unfold hoare_valid_def)
  apply (simp (no_asm))
  apply (rule fix_ind)
    apply (simp (no_asm)) \<comment> \<open>simplifier with enhanced \<open>adm\<close>-tactic\<close>
   apply (simp (no_asm))
  apply (simp (no_asm))
  apply blast
  done

end

author: m-fleury

repo: isabelle-emacs


text:
(* Property from Case-Analysis for Rippling and Inductive Proof,
   Moa Johansson, Lucas Dixon and Alan Bundy, ITP 2010.
   This Isabelle theory is produced using the TIP tool offered at the following website:
     https://github.com/tip-org/tools
   This file was originally provided as part of TIP benchmark at the following website:
     https://github.com/tip-org/benchmarks
   Yutaka Nagashima at CIIRC, CTU changed the TIP output theory file slightly
   to make it compatible with Isabelle2017.
   Some proofs were added by Yutaka Nagashima.*)
  theory TIP_prop_68
imports "../../Test_Base"
begin

datatype 'a list = nil2 | cons2 "'a" "'a list"

datatype Nat = Z | S "Nat"

fun x :: "Nat => Nat => bool" where
"x (Z) (Z) = True"
| "x (Z) (S z2) = False"
| "x (S x2) (Z) = False"
| "x (S x2) (S y2) = x x2 y2"

fun len :: "'a list => Nat" where
"len (nil2) = Z"
| "len (cons2 z xs) = S (len xs)"

fun delete :: "Nat => Nat list => Nat list" where
"delete y (nil2) = nil2"
| "delete y (cons2 z2 xs) =
     (if x y z2 then delete y xs else cons2 z2 (delete y xs))"

fun t2 :: "Nat => Nat => bool" where
"t2 (Z) z = True"
| "t2 (S z2) (Z) = False"
| "t2 (S z2) (S x2) = t2 z2 x2"

theorem property0 :
  "t2 (len (delete n xs)) (len xs)"
  oops

end

repo: PSL


text:
theory Planar_Subdivision
imports
  Graph_Genus
  Reachablen
  Permutations_2
begin

section \<open>Combinatorial Planarity and Subdivisions\<close>

locale subdiv1_contr = subdiv_step +
  fixes HM
  assumes H_map: "digraph_map H HM"
  assumes edge_rev_conv: "edge_rev HM = rev_H"

sublocale subdiv1_contr \<subseteq> H: digraph_map H HM
  rewrites "edge_rev HM = rev_H" by (intro H_map edge_rev_conv)+

sublocale subdiv1_contr \<subseteq> G: fin_digraph G
  by unfold_locales (auto simp: arcs_G verts_G)

context subdiv1_contr begin

  definition GM :: "'b pre_map" where
    "GM \<equiv>
      \<lparr> edge_rev = rev_G
      , edge_succ = perm_swap uw uv (perm_swap vw vu (fold perm_rem [wu, wv] (edge_succ HM)))
      \<rparr>"

  lemma edge_rev_GM:  "edge_rev GM = rev_G"
    by (simp add: GM_def)

  lemma edge_succ_GM: "edge_succ GM = perm_swap uw uv (perm_swap vw (rev_G uv) (fold perm_rem [wu, wv] (edge_succ HM)))"
    by (simp add: GM_def)

  lemma rev_H_eq_rev_G:
    assumes "x \<in> arcs G - {uv,vu}" shows "rev_H x = rev_G x"
  proof -
    have "perm_restrict rev_H (arcs G) = perm_restrict rev_G (arcs H)"
      using subdiv_step by (auto simp: subdivision_step_def)
    with assms show ?thesis
      unfolding arcs_H by (auto simp: perm_restrict_def fun_eq_iff split: if_splits)
  qed

  lemma edge_succ_permutes: "edge_succ GM permutes arcs G"
  proof -
    have "arcs H \<subseteq> (vw \<rightleftharpoons>\<^sub>F rev_G uv) ` (uw \<rightleftharpoons>\<^sub>F uv) ` arcs G \<union> {wv} \<union> {wu}"
      using subdiv_distinct_arcs in_arcs_G
      by (auto simp: arcs_H in_funswapid_image_iff transpose_def split: if_splits)
    then have "perm_swap uw uv (perm_swap vw (rev_G uv) (perm_rem (wv) (perm_rem (wu) (edge_succ HM)))) permutes arcs G"
      by (blast intro: perm_rem_permutes perm_swap_permutes2 permutes_subset H.edge_succ_permutes)
    then show ?thesis by (auto simp: edge_succ_GM)
  qed

  lemma out_arcs_empty:
    assumes "x \<in> verts G"
    shows "out_arcs G x = {} \<longleftrightarrow> out_arcs H x = {}"
  proof
    assume A: "out_arcs H x = {}"
    have tail_eqI: "\<And>a. tail H a = tail G a" by (simp only: tail_eq)

    { fix a assume "a \<in> out_arcs G x"
      moreover have "a \<in> arcs H \<Longrightarrow> a \<noteq> uv" "a \<in> arcs H \<Longrightarrow> a \<noteq> vu"
        using not_in_arcs_H by auto
      ultimately have "(uw \<rightleftharpoons>\<^sub>F uv) ((vw \<rightleftharpoons>\<^sub>F vu) a) \<in> out_arcs H x"
        using subdiv_distinct_arcs in_arcs_H not_in_arcs_H
        by (auto simp: arcs_G intro: tail_eqI)
    }
    then show "out_arcs G x = {}"
      using A by (auto simp del: in_out_arcs_conv)
  next
    assume A: "out_arcs G x = {}"
    have tail_eqI: "\<And>a. tail H a = tail G a" by (simp only: tail_eq)

    { fix a assume "a \<in> out_arcs H x"
      moreover have "x \<noteq> w" using assms not_in_verts_G by blast
      ultimately have "(uw \<rightleftharpoons>\<^sub>F uv) ((vw \<rightleftharpoons>\<^sub>F vu) a) \<in> out_arcs G x"
        using subdiv_distinct_arcs in_arcs_G not_in_arcs_G
        by (auto simp: arcs_H ) (auto simp: transpose_def intro: tail_eqI[symmetric])
    }
    then show "out_arcs H x = {}"
      using A by (auto simp del: in_out_arcs_conv)
  qed

  lemma cyclic_on_edge_succ:
    assumes "x \<in> verts G" "out_arcs G x \<noteq> {}"
    shows "cyclic_on (edge_succ GM) (out_arcs G x)"
  proof -
    have oa_Gx: "out_arcs G x = (uw \<rightleftharpoons>\<^sub>F uv) ` (vw \<rightleftharpoons>\<^sub>F vu) ` (out_arcs H x - {wu} - {wv})"
      using subdiv_distinct_arcs not_in_arcs_G in_arcs_G
      by (auto simp: in_funswapid_image_iff arcs_H transpose_def tail_eq[symmetric] split: if_splits)

    have "cyclic_on (perm_swap uw uv (perm_swap vw (rev_G uv) (perm_rem (wv) (perm_rem (wu) (edge_succ HM))))) (out_arcs G x)"
      unfolding oa_Gx
    proof (intro cyclic_on_perm_swap cyclic_on_perm_rem)
      show "cyclic_on (edge_succ HM) (out_arcs H x)"
        using assms by (auto simp: out_arcs_empty verts_H intro: H.edge_succ_cyclic)
      show "bij (edge_succ HM)" by (simp add: H.bij_edge_succ)
      show "bij (perm_rem (wu) (edge_succ HM))" by (simp add: H.bij_edge_succ)

      have "x \<noteq> w" using assms not_in_verts_G by auto
      then have "wu \<notin> out_arcs H x" "wv \<notin> out_arcs H x"
        by (auto simp: arc_to_ends_def)
      then show "out_arcs H x - {wu} \<noteq> {wv}" "out_arcs H x \<noteq> {wu}"
        by blast+
    qed
    then show ?thesis by (simp add: edge_succ_GM)
  qed

  lemma digraph_map_GM:
    shows "digraph_map G GM"
    by unfold_locales (auto simp: edge_rev_GM G.arev_dom edge_succ_permutes cyclic_on_edge_succ verts_G)

end

sublocale subdiv1_contr \<subseteq> GM: digraph_map G GM by (rule digraph_map_GM)

context subdiv1_contr begin

  lemma reachableGD:
    assumes "x \<rightarrow>\<^sup>*\<^bsub>G\<^esub> y" shows "x \<rightarrow>\<^sup>*\<^bsub>H\<^esub> y"
    using assms
  proof induct
    case base then show ?case by (auto simp: verts_H)
  next
    case (step x z)
    moreover
    have "u \<rightarrow>\<^sup>*\<^bsub>H\<^esub> v" "v \<rightarrow>\<^sup>*\<^bsub>H\<^esub> u" using adj_with_w by auto
    moreover
    { assume A: "(x,z) \<noteq> (u,v)" "(x,z) \<noteq> (v,u)"
      from \<open>x \<rightarrow>\<^bsub>G\<^esub> z\<close> obtain a where "a \<in> arcs G" "tail G a = x" "head G a = z"
        by auto
      with A have "a \<in> arcs H" "arc_to_ends H a = (x,z)" "tail H a = x" "head G a = z"
        by (auto simp: arcs_H tail_eq head_eq arc_to_ends_def fun_eq_iff)
      then have "x \<rightarrow>\<^bsub>H\<^esub> z" by (auto simp: arcs_ends_def intro: rev_image_eqI)
    }
    ultimately
    show ?case by (auto intro: H.reachable_trans)
  qed

  definition proj_verts_H :: "'a \<Rightarrow> 'a" where
    "proj_verts_H x \<equiv> if x = w then u else x"

  lemma proj_verts_H_in_G: "x \<in> verts H \<Longrightarrow> proj_verts_H x \<in> verts G"
    using in_verts_G by (auto simp: proj_verts_H_def verts_H)

  lemma dominatesHD:
    assumes "x \<rightarrow>\<^bsub>H\<^esub> y" shows "proj_verts_H x \<rightarrow>\<^sup>*\<^bsub>G\<^esub> proj_verts_H y"
  proof -
    have X1: "\<And>a. (w, y) = arc_to_ends G a \<Longrightarrow> a \<notin> arcs G"
      by (metis G.adj_in_verts(1) G.dominatesI not_in_verts_G)
    have X2: "\<And>a. (x, w) = arc_to_ends G a \<Longrightarrow> a \<notin> arcs G"
      by (metis G.adj_in_verts(2) G.dominatesI not_in_verts_G)
    show ?thesis
      using assms subdiv_ate_H_rev subdiv_ate in_verts_G
      by (auto simp: arcs_ends_def arcs_H arc_to_ends_eq proj_verts_H_def G_reach dest: X1 X2)
  qed

  lemma reachableHD:
    assumes reach:"x \<rightarrow>\<^sup>*\<^bsub>H\<^esub> y" shows "proj_verts_H x \<rightarrow>\<^sup>*\<^bsub>G\<^esub> proj_verts_H y"
    using assms by induct (blast intro: proj_verts_H_in_G G.reachable_trans dominatesHD)+

  lemma H_reach_conv: "\<And>x y. x \<rightarrow>\<^sup>*\<^bsub>H\<^esub> y \<longleftrightarrow> proj_verts_H x \<rightarrow>\<^sup>*\<^bsub>G\<^esub> proj_verts_H y"
    using w_reach by (auto simp: reachableHD)
      (auto simp: proj_verts_H_def verts_H split: if_splits dest: reachableGD intro: H.reachable_trans)

  lemma sccs_eq: "G.sccs_verts = (`) proj_verts_H ` H.sccs_verts" (is "?L = ?R")
  proof (intro set_eqI iffI)
    fix S assume "S \<in> ?L"
    then have "w \<notin> S" using G.sccs_verts_subsets not_in_verts_G by blast
    then have S_eq: "proj_verts_H ` proj_verts_H -` S = S"
        by (auto simp: proj_verts_H_def intro: range_eqI)
    then have "proj_verts_H -` S \<noteq> {}" using \<open>S \<in> ?L\<close> by safe (auto simp: G.sccs_verts_def)
    with \<open>S \<in> ?L\<close> have "proj_verts_H -` S \<in> H.sccs_verts"
      by (auto simp: G.in_sccs_verts_conv_reachable H.in_sccs_verts_conv_reachable H_reach_conv)
    then have "proj_verts_H ` proj_verts_H -` S \<in> (`) proj_verts_H ` H.sccs_verts" by (rule imageI)
    then show "S \<in> ?R" by (simp only: S_eq)
  next
    fix S assume "S \<in> ?R"
    have X: "\<And>v x. v \<notin> proj_verts_H ` x \<Longrightarrow> v = w \<or> (\<exists>y. v = proj_verts_H y \<and> y \<notin> x)"
      by (auto simp: proj_verts_H_def split: if_splits)
    from \<open>S \<in> ?R\<close> show "S \<in> ?L"
      using not_in_verts_G by (fastforce simp: G.reachable_in_verts G.in_sccs_verts_conv_reachable
        H.in_sccs_verts_conv_reachable H_reach_conv dest: X)
  qed

  lemma inj_on_proj_verts_H: "inj_on ((`) proj_verts_H) (pre_digraph.sccs_verts H)"
  proof (rule inj_onI)
    fix S T assume A: "S \<in> H.sccs_verts" "T \<in> H.sccs_verts" "proj_verts_H ` S = proj_verts_H ` T"
    have "\<And>x. w \<notin> x \<Longrightarrow> proj_verts_H ` x = x" by (auto simp: proj_verts_H_def)
    with A have "S \<noteq> T \<Longrightarrow> S \<inter> T \<noteq> {}"
      by (metis H.in_sccs_verts_conv_reachable Int_iff empty_iff image_eqI proj_verts_H_def w_reach(1,2))
    then show "S = T" using H.sccs_verts_disjoint[OF A(1,2)] by metis
  qed

  lemma card_sccs_verts: "card G.sccs_verts = card H.sccs_verts"
    unfolding sccs_eq by (intro card_image inj_on_proj_verts_H)

  lemma card_sccs_eq: "card G.sccs = card H.sccs"
    using card_sccs_verts G.inj_on_verts_sccs H.inj_on_verts_sccs
    by (auto simp: G.sccs_verts_conv H.sccs_verts_conv card_image)

  lemma isolated_verts_eq: "G.isolated_verts = H.isolated_verts"
    by (auto simp: G.isolated_verts_def H.isolated_verts_def verts_H out_arcs_w dest: out_arcs_empty)

  lemma card_verts: "card (verts H) = card (verts G) + 1"
    unfolding verts_H using not_in_verts_G by auto

  lemma card_arcs: "card (arcs H) = card (arcs G) + 2"
    unfolding arcs_H using not_in_arcs_G subdiv_distinct_arcs in_arcs_G by (auto simp: card_insert_if)

  lemma edge_succ_wu: "edge_succ HM wu = wv"
    using out_arcs_w out_degree_w edge_succ_permutes H.edge_succ_cyclic[of w]
    by (auto elim: eq_on_cyclic_on_iff1[where x="wu"] simp: verts_H out_degree_def)

  lemma edge_succ_wv: "edge_succ HM wv = wu"
    using out_arcs_w out_degree_w edge_succ_permutes H.edge_succ_cyclic[of w]
    by (auto elim: eq_on_cyclic_on_iff1[where x="wv"] simp: verts_H out_degree_def)

  lemmas edge_succ_w = edge_succ_wu edge_succ_wv

  lemma H_face_cycle_succ:
      "H.face_cycle_succ uw = wv"
      "H.face_cycle_succ vw = wu"
    unfolding H.face_cycle_succ_def by (auto simp: edge_succ_w)

  lemma H_edge_succ_tail_eqD:
    assumes "edge_succ HM a = b" shows "tail H a = tail H b"
    using assms H.tail_edge_succ[of a] by auto

  lemma YYY:
    "(wu \<rightleftharpoons>\<^sub>F wv) (edge_succ HM vw) = (edge_succ HM vw)"
    "(wu \<rightleftharpoons>\<^sub>F wv) (edge_succ HM uw) = (edge_succ HM uw)"
    using H.edge_succ_cyclic[of w] subdiv_distinct_verts0
    by (auto simp: Transposition.transpose_def dest: H_edge_succ_tail_eqD)

  text \<open>Project arcs of @{term H} to corresponding arcs of @{term G}\<close>
  definition proj_arcs_H :: "'b \<Rightarrow> 'b" where
    "proj_arcs_H x \<equiv>
      if x = uw \<or> x = wv then uv
      else if x = vw \<or> x = wu then vu
      else x"

  text \<open>Project arcs of @{term G} to corresponding arcs of @{term H}\<close>
  definition proj_arcs_G :: "'b \<Rightarrow> 'b" where
    "proj_arcs_G x \<equiv>
      if x = uv then uw
      else if x = vu then vw
      else x"

  lemma proj_arcs_H_simps[simp]:
      "proj_arcs_H uw = uv"
      "proj_arcs_H wv = uv"
      "proj_arcs_H vw = vu"
      "proj_arcs_H wu = vu"
      "x \<notin> {uw,vw,wu,wv} \<Longrightarrow> proj_arcs_H x = x"
      "a \<in> arcs G \<Longrightarrow> proj_arcs_H a = a"
    using subdiv_distinct_arcs not_in_arcs_G by (auto simp: proj_arcs_H_def)

  lemma proj_arcs_H_in_arcs_G: "a \<in> arcs H \<Longrightarrow> proj_arcs_H a \<in> arcs G"
    using subdiv_distinct_arcs in_arcs_G by (auto simp: proj_arcs_H_def arcs_H)

  lemma proj_arcs_eq_swap:
    assumes "a \<notin> {uv,vu,wu,wv}"
    shows "proj_arcs_H a = (uw \<rightleftharpoons>\<^sub>F uv o vw \<rightleftharpoons>\<^sub>F vu) a"
    using assms subdiv_distinct_arcs by (cases "a \<in> {uw,vw}") auto

  lemma proj_arcs_G_simps:
      "proj_arcs_G uv = uw"
      "proj_arcs_G vu = vw"
      "a \<notin> {uv,vu} \<Longrightarrow> proj_arcs_G a = a"
    using subdiv_distinct_arcs not_in_arcs_G by (auto simp: swap_id_eq proj_arcs_G_def)

  lemma proj_arcs_G_in_arcs_H:
    assumes "a \<in> arcs G" shows "proj_arcs_G a \<in> arcs H"
    using assms subdiv_distinct_arcs by (auto simp: proj_arcs_G_def arcs_H)

  lemma proj_arcs_HG: "a \<in> arcs G \<Longrightarrow> proj_arcs_H (proj_arcs_G a) = a"
    by (auto simp: proj_arcs_G_def)

  lemma fcs_proj_arcs_GH:
    assumes "a \<in> arcs H" shows "H.face_cycle_set (proj_arcs_G (proj_arcs_H a)) = H.face_cycle_set a"
  proof -
    have "H.face_cycle_set vw = H.face_cycle_set wu" "H.face_cycle_set uw = H.face_cycle_set wv"
      unfolding H.face_cycle_set_def by (auto simp add: H_face_cycle_succ[symmetric]
        self_in_orbit_step H.permutation_face_cycle_succ permutation_self_in_orbit)
    then show ?thesis
      using assms not_in_arcs_H by (cases "a \<in> {uv,vu,uw,wu,vw,wv}") (auto simp: proj_arcs_G_simps)
  qed

  lemma H_face_cycle_succ_neq_uv:
    "a \<notin> {uv,vu} \<Longrightarrow> H.face_cycle_succ a \<notin> {uv,vu}"
    using not_in_arcs_H by (cases "a \<in> arcs H") (auto dest: H.face_cycle_succ_in_arcsI)

  lemma face_cycle_succ_choose_inter:
    "{H.face_cycle_succ uw, H.face_cycle_succ vw, H.face_cycle_succ wu, H.face_cycle_succ wv} \<inter> {uv,vu} = {}"
    using subdiv_distinct_arcs H_face_cycle_succ_neq_uv by safe (simp_all, metis+)

  lemma face_cycle_succ_choose_neq:
      "H.face_cycle_succ wu \<notin> {wu,wv}"
      "H.face_cycle_succ wv \<notin> {wu,wv}"
    using subdiv_distinct_verts0 in_arcs_H
    by (auto simp del: H.edge_rev_in_arcs dest: H.tail_face_cycle_succ)

  lemma H_face_cycle_succ_G_not_in:
    assumes "a \<in> arcs G" shows "H.face_cycle_succ a \<notin> {wu,wv}"
  proof (cases "a \<in> {uv,vu}")
    case True with assms show ?thesis using subdiv_distinct_arcs by (auto simp: arcs_H)
  next
    case False with assms have "a \<in> arcs H" by (auto simp: arcs_H)
    from assms have "head H a \<noteq> w" by (auto simp: head_eq verts_G arcs_H dest: G.head_in_verts)
    then show ?thesis using H.tail_face_cycle_succ[OF \<open>a \<in> arcs H\<close>] by auto
  qed

  lemma
    face_cycle_succ_uv: "GM.face_cycle_succ uv = proj_arcs_H (H.face_cycle_succ wv)" and
    face_cycle_succ_vu: "GM.face_cycle_succ vu = proj_arcs_H (H.face_cycle_succ wu)"
    unfolding GM.face_cycle_succ_def edge_rev_GM edge_succ_GM
    using face_cycle_succ_choose_neq face_cycle_succ_choose_inter subdiv_distinct_arcs
    apply (auto simp: fun_eq_iff perm_swap_def)
    apply (auto simp: perm_rem_def edge_succ_w H.face_cycle_succ_def YYY proj_arcs_H_def)
    done

  lemma face_cycle_succ_not_uv:
    assumes "a \<in> arcs G" "a \<notin> {uv,vu}"
    shows "GM.face_cycle_succ a = proj_arcs_H (H.face_cycle_succ a)"
  proof -
    have "GM.face_cycle_succ a = (uw \<rightleftharpoons>\<^sub>F uv) ((vw \<rightleftharpoons>\<^sub>F rev_G uv) (perm_rem (wv) (perm_rem (wu) (edge_succ HM)) (((vw \<rightleftharpoons>\<^sub>F vu) ((uw \<rightleftharpoons>\<^sub>F uv) (rev_G a))))))"
      by (simp add: GM.face_cycle_succ_def perm_swap_def edge_succ_GM edge_rev_GM)
    also have "(vw \<rightleftharpoons>\<^sub>F vu) ((uw \<rightleftharpoons>\<^sub>F uv) (rev_G a)) = rev_G a"
      using assms not_in_arcs_G by (auto simp: transpose_def G.arev_eq_iff)
    also have "perm_rem (wv) (perm_rem (wu) (edge_succ HM)) (rev_G a) = edge_succ HM (rev_G a)"
    proof -
      have *: "\<And>a. tail H a \<noteq> w \<Longrightarrow> (wu \<rightleftharpoons>\<^sub>F wv) a = a" by (auto simp: transpose_def)
      from assms have "head H a \<noteq> w" "tail H (rev_G a) = head H a"
        by (auto simp: tail_eq head_eq verts_G dest: G.head_in_verts)
      then have "((wu \<rightleftharpoons>\<^sub>F wv) (edge_succ HM (rev_G a))) = edge_succ HM (rev_G a)"
        by (intro *) auto
      then show ?thesis by (auto simp: perm_rem_def edge_succ_w)
    qed
    also have "edge_succ HM (rev_G a) = H.face_cycle_succ a"
      using assms unfolding H.face_cycle_succ_def by (simp add: rev_H_eq_rev_G)
    also have "(uw \<rightleftharpoons>\<^sub>F uv) ((vw \<rightleftharpoons>\<^sub>F rev_G uv) (H.face_cycle_succ a)) = proj_arcs_H (H.face_cycle_succ a)"
    proof -
      from assms have "a \<in> arcs H" by (auto simp: arcs_H)
      then have fcs_not_in: "H.face_cycle_succ a \<notin> {uv, vu, wu, wv}"
        using assms H_face_cycle_succ_G_not_in in_arcs_G not_in_arcs_H
        by (auto simp del: G.arev_in_arcs dest: H.face_cycle_succ_closed[THEN iffD2])
      then show ?thesis by (auto simp add: proj_arcs_eq_swap)
    qed
    finally show ?thesis .
  qed

  lemmas G_face_cycle_succ = face_cycle_succ_uv face_cycle_succ_vu face_cycle_succ_not_uv

  lemma in_G_fcs_in_H_fcs:
    assumes "a \<in> arcs G"
    assumes "x \<in> GM.face_cycle_set a"
    shows "x \<in> proj_arcs_H ` H.face_cycle_set (proj_arcs_G a)"
    using \<open>x \<in> _\<close>
  proof induct
    case base show ?case
      by (rule rev_image_eqI[where x="proj_arcs_G a"]) (auto simp: \<open>a \<in> arcs G\<close> proj_arcs_G_def)
  next
    case (step b)
    { fix x assume "x \<in> H.face_cycle_set (proj_arcs_G a)"
      then have "x \<in> arcs H"
        using \<open>a \<in> arcs G\<close> by (auto dest: H.in_face_cycle_setD simp: proj_arcs_G_in_arcs_H)
      moreover
      then have "x \<notin> {uv,vu}" "x \<notin> {uw,wu,vw,wv} \<Longrightarrow> x \<in> arcs G"
        using \<open>a \<in> arcs G\<close> by (auto simp: arcs_H dest: H.in_face_cycle_setD)
      ultimately
      have "GM.face_cycle_succ (proj_arcs_H x) \<in> {proj_arcs_H (H.face_cycle_succ x),
          proj_arcs_H (H.face_cycle_succ (H.face_cycle_succ x))}"
        by (cases "x \<in> {uw,vw,wu,wv}") (auto simp: G_face_cycle_succ H_face_cycle_succ)
    }
    moreover
    have "b \<in> arcs G"
      using step(1) \<open>a \<in> arcs G\<close> by (simp add: GM.in_face_cycle_setD GM.face_cycle_set_def)
    ultimately
    show ?case using \<open>b \<in> arcs G\<close> step(2) by (auto intro: H.face_cycle_succ_inI)
  qed

  lemma in_H_fcs_in_G_fcs:
    assumes "a \<in> arcs H"
    assumes "x \<in> H.face_cycle_set a"
    shows "x \<in> proj_arcs_H -` GM.face_cycle_set (proj_arcs_H a)"
    using \<open>x \<in> _\<close>
  proof induct
    case base then show ?case by auto
  next
    case (step y)
    then have "y \<in> arcs H" using \<open>a \<in> arcs H\<close> by (auto dest: H.in_face_cycle_setD)
    moreover then have "y \<notin> {uv,vu}" by (fastforce simp: arcs_H)
    ultimately have "proj_arcs_H (H.face_cycle_succ y) = GM.face_cycle_succ (proj_arcs_H y)
        \<or> proj_arcs_H (H.face_cycle_succ y) = proj_arcs_H y"
      by (cases "y \<in> {uw,vw,wv,wu}") (auto simp: H_face_cycle_succ G_face_cycle_succ arcs_G)
    with step show ?case by (auto intro: GM.face_cycle_succ_inI)
  qed

  lemma G_fcs_eq:
    assumes "a \<in> arcs G"
    shows "GM.face_cycle_set a = proj_arcs_H ` H.face_cycle_set (proj_arcs_G a)" (is "?L = ?R")
    using assms by (auto dest: in_H_fcs_in_G_fcs[rotated] in_G_fcs_in_H_fcs[rotated]
      simp: proj_arcs_G_in_arcs_H proj_arcs_HG)

  lemma H_fcs_eq:
    assumes "a \<in> arcs H"
    shows "proj_arcs_H ` H.face_cycle_set a = GM.face_cycle_set (proj_arcs_H a)"
    using assms by (auto dest: in_H_fcs_in_G_fcs[rotated] in_G_fcs_in_H_fcs[rotated]
      simp: proj_arcs_H_in_arcs_G fcs_proj_arcs_GH)

  lemma face_cycle_sets:
    shows "GM.face_cycle_sets = (`) proj_arcs_H ` H.face_cycle_sets" (is "?L = ?R")
    unfolding GM.face_cycle_sets_def H.face_cycle_sets_def
    by (blast intro!: H_fcs_eq G_fcs_eq proj_arcs_G_in_arcs_H proj_arcs_H_in_arcs_G)

  lemma inj_on_proj_arcs_H: "inj_on ((`) proj_arcs_H) H.face_cycle_sets"
  proof (rule inj_onI)
    fix A B assume fcs: "A \<in> H.face_cycle_sets" "B \<in> H.face_cycle_sets"
      and pa_eq: "proj_arcs_H ` A = proj_arcs_H ` B"

    have xw_iff_wy:
      "\<And>X. X \<in> H.face_cycle_sets \<Longrightarrow> uw \<in> X \<longleftrightarrow> wv \<in> X"
      "\<And>X. X \<in> H.face_cycle_sets \<Longrightarrow> vw \<in> X \<longleftrightarrow> wu \<in> X"
      using H_face_cycle_succ by (auto simp: H.face_cycle_sets_def dest: H.face_cycle_succ_inI intro: H.face_cycle_succ_inD)

    have not_in_A: "uv \<notin> A" "vu \<notin> A" and not_in_B: "vu \<notin> B" "uv \<notin> B"
      using fcs not_in_arcs_H by (auto dest: H.in_face_cycle_setsD)

    have "A = proj_arcs_H -` (proj_arcs_H ` A) - {uv,vu}"
      using subdiv_distinct_arcs not_in_A by (auto simp: proj_arcs_H_def xw_iff_wy[OF fcs(1)] split: if_splits)
    also have "\<dots> = proj_arcs_H -` (proj_arcs_H ` B) - {uv,vu}" by (simp add: pa_eq)
    also have "\<dots> = B"
      using subdiv_distinct_arcs not_in_B by (auto simp: proj_arcs_H_def xw_iff_wy[OF fcs(2)] split: if_splits)
    finally show "A = B" .
  qed

  lemma card_face_cycle_sets: "card GM.face_cycle_sets = card H.face_cycle_sets"
    unfolding face_cycle_sets using inj_on_proj_arcs_H by (rule card_image)

  lemma euler_char_eq: "GM.euler_char = H.euler_char"
    by (auto simp: GM.euler_char_def H.euler_char_def card_verts card_arcs card_face_cycle_sets)

  lemma euler_genus_eq: "GM.euler_genus = H.euler_genus"
    by (auto simp: GM.euler_genus_def H.euler_genus_def euler_char_eq card_sccs_eq isolated_verts_eq)

end

lemma subdivision_genus_same_rev:
  assumes "subdivision (G, rev_G) (H, edge_rev HM)" "digraph_map H HM" "pre_digraph_map.euler_genus H HM = m"
  shows "\<exists>GM. digraph_map G GM \<and> pre_digraph_map.euler_genus G GM = m \<and> edge_rev GM = rev_G"
proof -
  from assms show ?thesis
  proof (induction rev_H\<equiv>"edge_rev HM" arbitrary: HM)
    case base then show ?case by auto
  next
    case (divide I rev_I H u v w uv uw vw)
    then interpret subdiv_step I rev_I H "edge_rev HM" u v w uv uw vw
      by unfold_locales simp

    interpret H: digraph_map H HM using \<open>digraph_map H HM\<close> .
    interpret IH: subdiv1_contr I rev_I H "edge_rev HM" u v w uv uw vw HM
      by unfold_locales simp

    have eulerI: "IH.GM.euler_genus = m" by (auto simp: IH.euler_genus_eq divide)
    with _ IH.digraph_map_GM show ?case by (rule divide) (simp add: IH.edge_rev_GM)
  qed
qed

lemma subdivision_genus:
  assumes "subdivision (G, rev_G) (H, rev_H)" "digraph_map H HM" "pre_digraph_map.euler_genus H HM = m"
  shows "\<exists>GM. digraph_map G GM \<and> pre_digraph_map.euler_genus G GM = m"
proof -
  interpret H: digraph_map H HM by fact
  show ?thesis
    using subdivision_genus_same_rev subdivision_choose_rev assms H.bidirected_digraph by metis
qed

lemma subdivision_comb_planar:
  assumes "subdivision (G, rev_G) (H, rev_H)" "comb_planar H" shows "comb_planar G"
  using assms unfolding comb_planar_def by (metis subdivision_genus)

end

author: isabelle-prover

repo: mirror-afp-devel