text:
(*  Title:      statecharts/HA/HAOps.thy
    Author:     Steffen Helke, Software Engineering Group
    Copyright   2010 Technische Universitaet Berlin
*)

header {* Constructing Hierarchical Automata *}
theory HAOps
imports HA
begin

subsection "Constructing a Composition Function for a PseudoHA"

definition
  EmptyMap :: "'s set => ('s ~=> (('s,'e,'d)seqauto) set)" where
  "EmptyMap S = (\<lambda> a . if a \<in> S then Some {} else None)"

lemma EmptyMap_dom [simp]:
  "dom (EmptyMap S) = S"
by (unfold dom_def EmptyMap_def,auto)

lemma EmptyMap_ran [simp]:
   "S \<noteq> {} \<Longrightarrow> ran (EmptyMap S) = {{}}"
by (unfold ran_def EmptyMap_def, auto)

lemma EmptyMap_the [simp]:
   "x \<in> S \<Longrightarrow> the ((EmptyMap S) x) = {}"
by (unfold ran_def EmptyMap_def, auto)

lemma EmptyMap_ran_override:
  "\<lbrakk> S \<noteq> {}; (S \<inter> (dom G)) = {} \<rbrakk> \<Longrightarrow>
  ran (G ++ EmptyMap S) = insert {} (ran G)"
apply (subst ran_override)
apply (simp add: Int_commute)
apply simp
done

lemma EmptyMap_Union_ran_override:
 "\<lbrakk> S \<noteq> {};
    S \<inter> dom G = {} \<rbrakk> \<Longrightarrow>
  (Union (ran (G ++ (EmptyMap S)))) = (Union (ran G))"
apply (subst EmptyMap_ran_override)
apply auto
done

lemma EmptyMap_Union_ran_override2:
 "\<lbrakk> S \<noteq> {}; S \<inter> dom G1 = {};
    dom G1 \<inter> dom G2 = {} \<rbrakk> \<Longrightarrow>
   \<Union> (ran (G1 ++ EmptyMap S ++ G2)) = (\<Union> (ran G1 \<union> ran G2))"
apply (unfold Union_eq UNION_eq EmptyMap_def Int_def ran_def)
apply (simp add: map_add_Some_iff)
apply (unfold dom_def)
apply simp
apply (rule equalityI)
apply (rule subsetI)
apply simp
apply fast
apply (rule subsetI)
apply (rename_tac t)
apply simp
apply (erule bexE)
apply (rename_tac U)
apply simp
apply (erule disjE)
apply (erule exE)
apply (rename_tac v)
apply (rule_tac x=U in exI)
apply simp
apply (rule_tac x=v in exI)
apply auto
done

lemma EmptyMap_Root [simp]:
 "Root {SA} (EmptyMap (States SA)) = SA";
by (unfold Root_def, auto)

lemma EmptyMap_RootEx [simp]:
  "RootEx {SA} (EmptyMap (States SA))"
by (unfold RootEx_def, auto)

lemma EmptyMap_OneAncestor [simp]:
 "OneAncestor {SA} (EmptyMap (States SA))"
by (unfold OneAncestor_def, auto)

lemma EmptyMap_NoCycles [simp]:
  "NoCycles {SA} (EmptyMap (States SA))"
by (unfold NoCycles_def EmptyMap_def , auto)

lemma EmptyMap_IsCompFun [simp]:
 "IsCompFun {SA} (EmptyMap (States SA))"
by (unfold IsCompFun_def, auto)

lemma EmptyMap_hierauto [simp]:
 "(D,{SA}, SAEvents SA, EmptyMap (States SA)) \<in> hierauto"
by (unfold hierauto_def HierAuto_def, auto)

subsection "Extending a Composition Function by a SA"

definition
  FAddSA :: "[('s ~=> (('s,'e,'d)seqauto) set), 's * ('s,'e,'d)seqauto]
             => ('s ~=> (('s,'e,'d)seqauto) set)"
           ("(_ [f+]/ _)" [10,11]10) where
  "FAddSA G SSA = (let  (S,SA) = SSA
                   in
                     (if ((S \<in> dom G) \<and> (S \<notin> States SA)) then
                        (G ++ (empty(S \<mapsto> (insert SA (the (G S)))))
                         ++ EmptyMap (States SA))
                      else G))"

lemma FAddSA_dom [simp]:
 "(S \<notin> (dom (A::('a => ('a,'c,'d)seqauto set option)))) \<Longrightarrow>
   ((A [f+] (S,(SA::('a,'c,'d)seqauto))) = A)"
by (unfold FAddSA_def Let_def, auto)

lemma FAddSA_States [simp]:
 "(S \<in> (States (SA::('a,'c,'d)seqauto))) \<Longrightarrow>
   (((A::('a => ('a,'c,'d)seqauto set option)) [f+] (S,SA)) = A)"
by (unfold FAddSA_def Let_def, auto)

lemma FAddSA_dom_insert [simp]:
 "\<lbrakk> S \<in> (dom A); S \<notin>  States SA \<rbrakk> \<Longrightarrow>
   (((A [f+] (S,SA)) S) = Some (insert SA (the (A S))))"
by (unfold FAddSA_def Let_def restrict_def, auto)

lemma FAddSA_States_neq [simp]:
 "\<lbrakk> S' \<notin> States (SA::('a,'c,'d)seqauto); S \<noteq>  S' \<rbrakk> \<Longrightarrow>
  ((((A::('a => ('a,'c,'d)seqauto set option)) [f+] (S,SA)) S') = (A S'))"
apply (case_tac "S \<in> dom A")
apply (case_tac "S \<in> States SA")
apply auto
apply (case_tac "S' \<in> dom A")
apply (unfold FAddSA_def Let_def)
apply auto
apply (simp add: dom_None)
done

lemma FAddSA_dom_emptyset [simp]:
 "\<lbrakk> S \<in> (dom A); S \<notin> States SA; S' \<in> States (SA::('a,'c,'d)seqauto) \<rbrakk> \<Longrightarrow>
    ((((A::('a => ('a,'c,'d)seqauto set option))) [f+] (S,SA)) S') = (Some {})"
apply (unfold FAddSA_def Let_def)
apply auto
apply (unfold EmptyMap_def)
apply auto
done

lemma FAddSA_dom_dom_States [simp]:
  "\<lbrakk> S \<in> (dom F); S \<notin> States SA \<rbrakk> \<Longrightarrow>
    (dom ((F::('a ~=> (('a,'b,'d)seqauto) set)) [f+] (S, SA))) =
    ((dom F) \<union> (States (SA::('a,'b,'d)seqauto)))"
by (unfold FAddSA_def Let_def, auto)

lemma FAddSA_dom_dom [simp]:
  "S \<notin> (dom F) \<Longrightarrow>
   (dom ((F::('a ~=> (('a,'b,'d)seqauto) set)) [f+]
       (S,(SA::('a,'b,'d)seqauto)))) = (dom F)"
by (unfold FAddSA_def Let_def, auto)

lemma FAddSA_States_dom [simp]:
  "S \<in> (States SA) \<Longrightarrow>
   (dom ((F::('a ~=> (('a,'b,'d)seqauto) set)) [f+]
        (S,(SA::('a,'b,'d)seqauto)))) = (dom F)";
by (unfold FAddSA_def Let_def, auto)

lemma FAddSA_dom_insert_dom_disjunct [simp]:
   "\<lbrakk> S \<in> dom G; States SA \<inter> dom G = {} \<rbrakk> \<Longrightarrow> ((G [f+] (S,SA)) S) = Some (insert SA (the (G S)))"
apply (rule  FAddSA_dom_insert)
apply auto
done

lemma FAddSA_Union_ran:
 "\<lbrakk> S \<in> dom G; (States SA) \<inter> (dom G) = {} \<rbrakk> \<Longrightarrow>
   (\<Union> (ran (G [f+] (S,SA)))) = (insert SA (\<Union> (ran G)))"
apply (unfold FAddSA_def Let_def)
apply simp
apply (rule conjI)
prefer 2
apply (rule impI)
apply (unfold Int_def)
apply simp
apply (fold Int_def)
apply (rule impI)
apply (subst EmptyMap_Union_ran_override)
apply auto
done

lemma FAddSA_Union_ran2:
 "\<lbrakk> S \<in> dom G1; (States SA) \<inter> (dom G1) = {}; (dom G1 \<inter> dom G2) = {} \<rbrakk> \<Longrightarrow>
   (\<Union> (ran ((G1 [f+] (S,SA)) ++ G2))) = (insert SA (\<Union> ((ran G1) \<union> (ran G2))))"
apply (unfold FAddSA_def Let_def)
apply (simp (no_asm_simp))
apply (rule conjI)
apply (rule impI)
apply (subst EmptyMap_Union_ran_override2)
apply simp
apply simp
apply simp
apply fast
apply (subst Union_Un_distrib)
apply (subst Union_ran_override2)
apply auto
done

lemma FAddSA_ran:
  "\<lbrakk> \<forall> T \<in> dom G . T \<noteq> S \<longrightarrow> (the (G T) \<inter> the (G S)) = {};
     S \<in> dom G; (States SA) \<inter>  (dom G) = {} \<rbrakk> \<Longrightarrow>
    ran (G [f+] (S,SA)) = insert {} (insert (insert SA (the (G S))) (ran G - {the (G S)}))"
apply (unfold FAddSA_def Let_def)
apply simp
apply (rule conjI)
apply (rule impI)+
prefer 2
apply fast
apply (simp add: EmptyMap_ran_override)
apply (unfold ran_def)
apply auto
apply (rename_tac Y X a xa xb)
apply (erule_tac x=a in allE)
apply simp
apply (erule_tac x=a in allE)
apply simp
done

lemma FAddSA_RootEx_def:
  "\<lbrakk> S \<in> dom G; (States SA) \<inter> (dom G) = {} \<rbrakk> \<Longrightarrow>
    RootEx F (G [f+] (S,SA)) = (\<exists>! A . A \<in> F \<and> A \<notin> insert SA (\<Union> ran G))"
apply (unfold RootEx_def)
apply (simp only: FAddSA_Union_ran Int_commute)
done

lemma FAddSA_RootEx:
  "\<lbrakk> \<Union> (ran G) = F - {Root F G};
     dom G = UNION F States;
     (dom G \<inter> States SA) = {}; S \<in> dom G;
     RootEx F G \<rbrakk> \<Longrightarrow> RootEx (insert SA F) (G [f+] (S,SA))"
apply (simp add: FAddSA_RootEx_def Int_commute cong: rev_conj_cong)
apply (auto cong: conj_cong)
done

lemma FAddSA_Root_def:
  "\<lbrakk> S \<in> dom G; (States SA) \<inter> (dom G) = {} \<rbrakk>  \<Longrightarrow>
   (Root F (G [f+] (S,SA)) = (@ A . A \<in> F \<and> A \<notin> insert SA (\<Union> ran G)))"
apply (unfold Root_def)
apply (simp only: FAddSA_Union_ran Int_commute)
done

lemma FAddSA_RootEx_Root:
  "\<lbrakk> Union (ran G) = F - {Root F G};
     UNION F States = dom G;
     (dom G \<inter> States SA) = {}; S \<in> dom G;
     RootEx F G \<rbrakk> \<Longrightarrow> (Root (insert SA F) (G [f+] (S,SA))) = (Root F G)"
apply (simp add: FAddSA_Root_def Int_commute cong: rev_conj_cong)
apply (simp cong:conj_cong)
done

lemma FAddSA_OneAncestor:
  "\<lbrakk> \<Union> (ran G) = F - {Root F G};
     (dom G \<inter> States SA) = {}; S \<in> dom G;
     UNION F States = dom G; RootEx F G;
     OneAncestor F G \<rbrakk> \<Longrightarrow> OneAncestor (insert SA F) (G [f+] (S,SA))"
apply (subst OneAncestor_def)
apply simp
apply (rule ballI)
apply (rename_tac SAA)
apply (case_tac "SA = SAA")
apply (rule_tac a=S in ex1I)
apply (rule conjI)
apply simp
apply fast
apply (subst FAddSA_dom_insert)
apply simp
apply (simp add:Int_def)
apply simp
apply (rename_tac T)
apply (erule conjE bexE exE disjE)+
apply (rename_tac SAAA)
apply simp
apply (erule conjE)
apply (subst not_not [THEN sym])
apply (rule notI)
apply (case_tac "T \<in> States SAA")
apply blast
apply (drule_tac A=G and S=S and SA=SAA in FAddSA_States_neq)
apply fast
apply simp
apply (case_tac "SAA \<notin> Union (ran G)")
apply (frule ran_dom_the)
prefer 2
apply fast
apply blast
apply simp
apply (erule conjE)
apply (simp add: States_Int_not_mem)
apply (unfold OneAncestor_def)
apply (drule_tac G=G and S=S and SA=SA in FAddSA_RootEx_Root)
apply simp
apply simp
apply simp
apply simp
apply (erule_tac x=SAA in ballE)
prefer 2
apply simp
apply simp
apply (erule conjE bexE ex1E exE disjE)+
apply (rename_tac T SAAA)
apply (rule_tac a=T in ex1I)
apply (rule conjI)
apply fast
apply (case_tac "T = S")
apply simp
apply (case_tac "S \<notin> States SA")
apply simp
apply simp
apply (subst FAddSA_States_neq)
apply blast
apply (rule not_sym)
apply simp
apply simp
apply (rename_tac U)
apply simp
apply (erule conjE bexE)+
apply (rename_tac SAAAA)
apply simp
apply (erule conjE disjE)+
apply (frule FAddSA_dom_emptyset)
prefer 2
apply fast
back
back
apply simp
apply blast
apply simp
apply (erule_tac x=U in allE)
apply (erule impE)
prefer 2
apply simp
apply (rule conjI)
apply fast
apply (case_tac "S \<noteq> U")
apply (subgoal_tac "U \<notin> States SA")
apply (drule_tac A=G in FAddSA_States_neq)
apply fast
apply simp
apply blast
apply (drule_tac A=G and SA=SA in FAddSA_dom_insert)
apply simp
apply blast
apply auto
done

lemma FAddSA_IsCompFun:
 "\<lbrakk> (States SA \<inter> (UNION F States)) = {};
     S \<in> (UNION F States);
     IsCompFun F G \<rbrakk> \<Longrightarrow>  IsCompFun (insert SA F) (G [f+] (S,SA))"
apply (unfold IsCompFun_def)
apply (erule conjE)+
apply (simp add: Int_commute FAddSA_RootEx_Root FAddSA_RootEx FAddSA_OneAncestor FAddSA_NoCycles)
apply (rule conjI)
apply (subst FAddSA_dom_dom_States)
apply simp
apply blast
apply (simp add: Un_commute)
apply (simp add: FAddSA_Union_ran)
apply (case_tac "SA = Root F G")
prefer 2
apply blast
apply (subgoal_tac "States (Root F G) \<subseteq>  UNION F States")
apply simp
apply (frule subset_lemma)
apply auto
done

lemma FAddSA_HierAuto:
  "\<lbrakk> (States SA \<inter> (UNION F States)) = {};
      S \<in> (UNION F States);
      HierAuto D F E G \<rbrakk> \<Longrightarrow> HierAuto D (insert SA F) (E \<union> SAEvents SA) (G [f+] (S,SA))"
apply (unfold HierAuto_def)
apply auto
apply (simp add: MutuallyDistinct_Insert)
apply (rule FAddSA_IsCompFun)
apply auto
done

lemma FAddSA_HierAuto_insert [simp]:
  "\<lbrakk> (States SA \<inter> HAStates HA) = {};
      S \<in> HAStates HA \<rbrakk> \<Longrightarrow>
    HierAuto (HAInitValue HA)
             (insert SA (SAs HA))
             (HAEvents HA \<union> SAEvents SA)
             (CompFun HA [f+] (S,SA))";
apply (unfold HAStates_def)
apply (rule FAddSA_HierAuto)
apply auto
done

subsection "Constructing a PseudoHA";

definition
  PseudoHA :: "[('s,'e,'d)seqauto,'d data] => ('s,'e,'d)hierauto" where
  "PseudoHA SA D = Abs_hierauto(D,{SA}, SAEvents SA ,EmptyMap (States SA))"

lemma PseudoHA_SAs [simp]:
  "SAs (PseudoHA SA D) = {SA}"
by (unfold PseudoHA_def SAs_def, simp add: Abs_hierauto_inverse);

lemma PseudoHA_Events [simp]:
  "HAEvents (PseudoHA SA D) = SAEvents SA"
by (unfold PseudoHA_def HAEvents_def, simp add: Abs_hierauto_inverse);

lemma PseudoHA_CompFun [simp]:
  "CompFun (PseudoHA SA D) = EmptyMap (States SA)"
by (unfold PseudoHA_def CompFun_def, simp add: Abs_hierauto_inverse)

lemma PseudoHA_HAInitValue [simp]:
  "(HAInitValue (PseudoHA SA D)) = D"
by (unfold PseudoHA_def Let_def HAInitValue_def, simp add: Abs_hierauto_inverse)

lemma PseudoHA_CompFun_the [simp]:
 "S \<in> States A \<Longrightarrow> (the (CompFun (PseudoHA A D) S)) = {}"
by simp

lemma PseudoHA_CompFun_ran [simp]:
 "(ran (CompFun (PseudoHA SA D))) = {{}}"
by auto

lemma PseudoHA_HARoot [simp]:
 "(HARoot (PseudoHA SA D)) = SA"
by (unfold HARoot_def, auto)

lemma PseudoHA_HAInitState [simp]:
  "HAInitState (PseudoHA A D) = InitState A"
apply (unfold HAInitState_def)
apply simp
done

lemma PseudoHA_HAInitStates [simp]:
  "HAInitStates (PseudoHA A D) = {InitState A}"
apply (unfold HAInitStates_def)
apply simp
done

lemma PseudoHA_Chi [simp]:
  "S \<in> States A \<Longrightarrow> Chi (PseudoHA A D) S = {}"
apply (unfold Chi_def restrict_def)
apply auto
done

lemma PseudoHA_ChiRel [simp]:
  "ChiRel (PseudoHA A D) = {}"
apply (unfold ChiRel_def)
apply simp
done

lemma PseudoHA_InitConf [simp]:
 "InitConf (PseudoHA A D) = {InitState A}"
apply (unfold InitConf_def)
apply simp
done

subsection {* Extending a HA by a SA (@{text "AddSA"}) *}

definition
  AddSA :: "[('s,'e,'d)hierauto, 's * ('s,'e,'d)seqauto]
             => ('s,'e,'d)hierauto"
           ("(_ [++]/ _)" [10,11]10) where
  "AddSA HA SSA = (let (S,SA) = SSA;
                        DNew = HAInitValue HA;
                        FNew = insert SA (SAs HA);
                        ENew  = HAEvents HA \<union> SAEvents SA;
                        GNew  = CompFun HA [f+] (S,SA)
                   in
                       Abs_hierauto(DNew,FNew,ENew,GNew))"

definition
  AddHA :: "[('s,'e,'d)hierauto, 's * ('s,'e,'d)hierauto]
             => ('s,'e,'d)hierauto"
           ("(_ [**]/ _)" [10,11]10) where
  "AddHA HA1 SHA =
            (let (S,HA2)     = SHA;
                 (D1,F1,E1,G1) = Rep_hierauto (HA1 [++] (S,HARoot HA2));
                 (D2,F2,E2,G2) = Rep_hierauto HA2;
                 FNew       = F1 \<union> F2;
                 ENew       = E1 \<union> E2;
                 GNew       = G1 ++ G2
             in
                 Abs_hierauto(D1,FNew,ENew,GNew))"

lemma AddSA_SAs:
  "\<lbrakk> (States SA \<inter>  HAStates HA) = {};
      S \<in> HAStates HA \<rbrakk> \<Longrightarrow> (SAs (HA [++] (S,SA))) = insert SA (SAs HA)"
apply (unfold Let_def AddSA_def)
apply (subst SAs_def)
apply (simp add: hierauto_def Abs_hierauto_inverse)
done

lemma AddSA_Events:
  "\<lbrakk> (States SA \<inter> HAStates HA) = {};
      S \<in> HAStates HA \<rbrakk> \<Longrightarrow>
     HAEvents (HA [++] (S,SA)) = (HAEvents HA) \<union> (SAEvents SA)"
apply (unfold Let_def AddSA_def)
apply (subst HAEvents_def)
apply (simp add: hierauto_def Abs_hierauto_inverse)
done

lemma AddSA_CompFun:
   "\<lbrakk> (States SA \<inter>  HAStates HA) = {};
      S \<in> HAStates HA \<rbrakk> \<Longrightarrow>
     CompFun (HA [++] (S,SA)) = (CompFun HA [f+] (S,SA))"
apply (unfold Let_def AddSA_def)
apply (subst CompFun_def)
apply (simp add: hierauto_def Abs_hierauto_inverse)
done

lemma AddSA_HAStates:
   "\<lbrakk> (States SA \<inter> HAStates HA) = {};
       S \<in> HAStates HA \<rbrakk> \<Longrightarrow>
      HAStates (HA [++] (S,SA)) = (HAStates HA) \<union> (States SA)"
apply (unfold HAStates_def)
apply (subst AddSA_SAs)
apply (unfold HAStates_def)
apply auto
done

lemma AddSA_HAInitValue:
   "\<lbrakk> (States SA \<inter> HAStates HA) = {};
       S \<in> HAStates HA \<rbrakk> \<Longrightarrow>
      (HAInitValue (HA [++] (S,SA))) = (HAInitValue HA)"
apply (unfold Let_def AddSA_def)
apply (subst HAInitValue_def)
apply (simp add: hierauto_def Abs_hierauto_inverse)
done

lemma AddSA_HARoot:
   "\<lbrakk> (States SA \<inter> HAStates HA) = {};
      S \<in> HAStates HA \<rbrakk> \<Longrightarrow>
      (HARoot (HA [++] (S,SA))) = (HARoot HA)"
apply (unfold HARoot_def)
apply (simp add: AddSA_CompFun AddSA_SAs)
apply (subst FAddSA_RootEx_Root)
apply auto
apply (simp only: HAStates_SA_mem)
apply (unfold HAStates_def)
apply fast
done

lemma AddSA_CompFun_the:
 "\<lbrakk> (States SA \<inter> HAStates A) = {};
    S \<in> HAStates A \<rbrakk> \<Longrightarrow>
  (the ((CompFun (A [++] (S,SA))) S)) = insert SA (the ((CompFun A) S))"
by (simp add: AddSA_CompFun)

lemma AddSA_CompFun_the2:
 "\<lbrakk> S' \<in> States (SA::('a,'c,'d)seqauto);
    (States SA \<inter> HAStates A) = {};
    S \<in> HAStates A \<rbrakk> \<Longrightarrow>
    the ((CompFun (A [++] (S,SA))) S') = {}"
apply (simp add: AddSA_CompFun)
apply (subst FAddSA_dom_emptyset)
apply auto
done

lemma AddSA_CompFun_the3:
 "\<lbrakk> S' \<notin> States (SA::('a,'c,'d)seqauto);
    S \<noteq> S';
    (States SA \<inter> HAStates A) = {};
    S \<in> HAStates A \<rbrakk> \<Longrightarrow>
   (the ((CompFun (A [++] (S,SA))) S')) = (the ((CompFun A) S'))"
by (simp add: AddSA_CompFun)

lemma AddSA_CompFun_ran:
 "\<lbrakk> (States SA \<inter> HAStates A) = {};
     S \<in> HAStates A \<rbrakk> \<Longrightarrow>
   ran (CompFun (A [++] (S,SA))) =
       insert {} (insert (insert SA (the ((CompFun A) S))) (ran (CompFun A) - {the ((CompFun A) S)}))"
apply (simp add: AddSA_CompFun)
apply (subst FAddSA_ran)
apply auto
apply (fast dest: CompFun_Int_disjoint)
done

lemma AddSA_CompFun_ran2:
 "\<lbrakk> (States SA1 \<inter> HAStates A) = {};
    (States SA2 \<inter> (HAStates A \<union> States SA1)) = {};
     S \<in> HAStates A;
     T \<in> States SA1 \<rbrakk> \<Longrightarrow>
   ran (CompFun ((A [++] (S,SA1)) [++] (T,SA2))) =
       insert {} (insert {SA2} (ran (CompFun (A  [++] (S,SA1)))))"
apply (simp add: AddSA_HAStates AddSA_CompFun)
apply (subst FAddSA_ran)
apply (rule ballI)
apply (rule impI)
apply (subst AddSA_CompFun [THEN sym])
apply simp
apply simp
apply (subst AddSA_CompFun [THEN sym])
apply simp
apply simp
apply (rule CompFun_Int_disjoint)
apply simp
apply (simp add: AddSA_HAStates)
apply (simp add: AddSA_HAStates)
apply (case_tac "S \<in> States SA1")
apply simp
apply (simp only: dom_CompFun [THEN sym])
apply (frule FAddSA_dom_dom_States)
apply fast
apply simp
apply (case_tac "S \<in> States SA1")
apply simp
apply fast
apply (subst FAddSA_dom_dom_States)
apply simp
apply simp
apply simp
apply (case_tac "S \<in>  States SA1")
apply simp
apply fast
apply (subst FAddSA_dom_dom_States)
apply simp
apply simp
apply simp
apply (case_tac "S \<in>  States SA1")
apply simp
apply fast
apply simp
apply fast
done

lemma AddSA_CompFun_ran_not_mem:
 "\<lbrakk> States SA2 \<inter> (HAStates A \<union> States SA1) = {};
    States SA1 \<inter> HAStates A = {};
    S \<in> HAStates A \<rbrakk> \<Longrightarrow>
   {SA2} \<notin> ran (CompFun A [f+] (S, SA1))"
apply (cut_tac HA="A [++] (S,SA1)" and Sas="{SA2}" in ran_CompFun_is_not_SA)
apply (simp add: AddSA_HAStates AddSA_CompFun)
apply (simp add: AddSA_HAStates AddSA_SAs)
apply auto
apply (simp add: Int_def)
apply (cut_tac SA=SA2 in EX_State_SA)
apply (erule exE)
apply (frule HAStates_SA_mem)
apply fast
apply (simp only: HAStates_def)
apply fast
apply (simp add: AddSA_HAStates AddSA_CompFun)
done

lemma AddSA_CompFun_ran3:
 "\<lbrakk> (States SA1 \<inter> HAStates A) = {};
    (States SA2 \<inter> (HAStates A \<union> States SA1)) = {};
    (States SA3 \<inter> (HAStates A \<union> States SA1 \<union> States SA2)) = {};
     S \<in> HAStates A;
     T \<in> States SA1 \<rbrakk> \<Longrightarrow>
    ran (CompFun ((A [++] (S,SA1)) [++] (T,SA2) [++] (T,SA3))) =
       insert {} (insert {SA3,SA2} (ran (CompFun (A  [++] (S,SA1)))))"
apply (simp add: AddSA_HAStates AddSA_CompFun)
apply (subst FAddSA_ran)
apply (rule ballI)
apply (rule impI)
apply (subst AddSA_CompFun [THEN sym])
apply simp
apply simp
apply (subst AddSA_CompFun [THEN sym])
apply (simp add: AddSA_HAStates)
apply (simp add: AddSA_HAStates)
apply (subst AddSA_CompFun [THEN sym])
apply simp
apply simp
apply (subst AddSA_CompFun [THEN sym])
apply (simp add: AddSA_HAStates)
apply (simp add: AddSA_HAStates)
apply (rule CompFun_Int_disjoint)
apply simp
apply (simp add: AddSA_HAStates)
apply (simp add: AddSA_HAStates)
apply (simp only: dom_CompFun [THEN sym])
apply (cut_tac F="CompFun A [f+] (S, SA1)" and S=T and SA="SA2" in FAddSA_dom_dom_States)
apply (cut_tac F="CompFun A" and S=S and SA="SA1" in FAddSA_dom_dom_States)
apply fast
apply fast
apply simp
apply fast
apply simp
apply (cut_tac F="CompFun A" and S=S and SA="SA1" in FAddSA_dom_dom_States)
apply simp
apply fast
apply simp
apply (subst FAddSA_dom_dom_States)
apply (subst FAddSA_dom_dom_States)
apply simp
apply fast
apply simp
apply fast
apply (subst FAddSA_dom_dom_States)
apply simp
apply fast
apply simp
apply (subst FAddSA_dom_dom_States)
apply (subst FAddSA_dom_dom_States)
apply simp
apply fast
apply simp
apply fast
apply (subst FAddSA_dom_dom_States)
apply simp
apply fast
apply simp
apply (subst AddSA_CompFun [THEN sym])
back
apply simp
apply simp
apply (subst AddSA_CompFun [THEN sym])
back
apply (simp add: AddSA_HAStates)
apply (simp add: AddSA_HAStates)
apply (subst AddSA_CompFun_ran2)
apply fast
apply fast
apply fast
apply fast
apply (simp add: AddSA_CompFun)
apply (subst  FAddSA_dom_insert)
apply (subst FAddSA_dom_dom_States)
apply simp
apply fast
apply simp
apply fast
apply (subst FAddSA_dom_emptyset)
apply simp
apply fast
apply simp
apply simp
apply (subst  FAddSA_dom_insert)
apply (subst FAddSA_dom_dom_States)
apply simp
apply fast
apply simp
apply fast
apply (subst FAddSA_dom_emptyset)
apply simp
apply fast
apply simp
apply simp
apply (case_tac "{SA2} \<notin> ran (CompFun A [f+] (S,SA1))")
apply fast
apply (simp add:AddSA_CompFun_ran_not_mem)
done

lemma AddSA_CompFun_PseudoHA_ran:
  "\<lbrakk> S \<in> States RootSA;
     States RootSA \<inter> States SA = {} \<rbrakk> \<Longrightarrow>
     (ran (CompFun ((PseudoHA RootSA D) [++] (S,SA)))) = (insert {} {{SA}})"
apply (subst AddSA_CompFun_ran)
apply auto
done

lemma AddSA_CompFun_PseudoHA_ran2:
  "\<lbrakk> States SA1 \<inter> States RootSA = {};
     States SA2 \<inter> (States RootSA \<union> States SA1) = {};
     S \<in> States RootSA \<rbrakk> \<Longrightarrow>
     (ran (CompFun ((PseudoHA RootSA D) [++] (S,SA1) [++] (S,SA2)))) = (insert {} {{SA2,SA1}})"
apply (subst AddSA_CompFun_ran)
prefer 3
apply (subst AddSA_CompFun_the)
apply simp
apply simp
apply (subst AddSA_CompFun_PseudoHA_ran)
apply fast
apply fast
apply (subst AddSA_CompFun_the)
apply simp
apply simp
apply simp
apply fast
apply (simp add: AddSA_HAStates)
apply (simp add: AddSA_HAStates)
done

lemma AddSA_HAInitStates [simp]:
 "\<lbrakk> States SA \<inter> HAStates A = {};
    S \<in> HAStates A \<rbrakk> \<Longrightarrow>
   HAInitStates (A [++] (S,SA)) = insert (InitState SA) (HAInitStates A)"
apply (unfold HAInitStates_def)
apply (simp add: AddSA_SAs)
done

lemma AddSA_HAInitState [simp]:
 "\<lbrakk> States SA \<inter> HAStates A = {};
    S \<in> HAStates A \<rbrakk> \<Longrightarrow>
  HAInitState (A [++] (S,SA)) = (HAInitState A)"
apply (unfold HAInitState_def)
apply (simp add: AddSA_HARoot)
done

lemma AddSA_Chi [simp]:
 "\<lbrakk> States SA \<inter> HAStates A = {};
   S \<in> HAStates A \<rbrakk> \<Longrightarrow>
  Chi (A [++] (S,SA)) S = (States SA) \<union> (Chi A S)"
apply (unfold Chi_def restrict_def)
apply (simp add: AddSA_SAs AddSA_HAStates AddSA_CompFun_the)
apply auto
done

lemma AddSA_Chi2 [simp]:
 "\<lbrakk> States SA \<inter> HAStates A = {};
    S \<in> HAStates A;
    T \<in> States SA \<rbrakk> \<Longrightarrow>
    Chi (A [++] (S,SA)) T = {}"
apply (unfold Chi_def restrict_def)
apply (simp add: AddSA_SAs AddSA_HAStates AddSA_CompFun_the2)
done

lemma AddSA_Chi3 [simp]:
 "\<lbrakk> States SA \<inter> HAStates A = {};
    S \<in> HAStates A;
    T \<notin> States SA; T \<noteq> S \<rbrakk> \<Longrightarrow>
    Chi (A [++] (S,SA)) T = Chi A T"
apply (unfold Chi_def restrict_def)
apply (simp add: AddSA_SAs AddSA_HAStates AddSA_CompFun_the3)
apply auto
done

lemma AddSA_ChiRel [simp]:
 "\<lbrakk> States SA \<inter> HAStates A = {};
    S \<in> HAStates A \<rbrakk> \<Longrightarrow>
   ChiRel (A [++] (S,SA)) = { (T,T') . T = S \<and> T' \<in> States SA } \<union> (ChiRel A)"
apply (unfold ChiRel_def)
apply (simp add: AddSA_HAStates)
apply auto
apply (rename_tac T U)
apply (case_tac "T \<in> States SA")
apply simp
apply simp
apply (rename_tac T U)
apply (case_tac "T \<noteq> S")
apply (case_tac "T \<in>  States SA")
apply simp
apply simp
apply simp
apply (rename_tac T U)
apply (case_tac "T \<in>  States SA")
apply simp
apply simp
apply (cut_tac A=A and T=T in Chi_HAStates)
apply fast
apply (case_tac "T \<in> States SA")
apply simp
apply simp
apply (cut_tac A=A and T=T in Chi_HAStates)
apply fast
apply fast
apply (rename_tac T U)
apply (case_tac "T \<noteq> S")
apply (case_tac "T \<in> States SA")
apply simp
apply simp
apply simp
apply (rename_tac T U)
apply (case_tac "T \<in>  States SA")
apply fast
apply (case_tac "T \<noteq> S")
apply simp
apply simp
done

lemma help_InitConf:
  "\<lbrakk>States SA \<inter> HAStates A = {} \<rbrakk> \<Longrightarrow> {p. fst p \<noteq> InitState SA \<and> snd p \<noteq> InitState SA \<and>
       p \<in>  insert (InitState SA) (HAInitStates A) \<times> insert (InitState SA) (HAInitStates A) \<and>
       (p \<in>  {S} \<times> States SA \<or>  p \<in>  ChiRel A)} =
   (HAInitStates A \<times> HAInitStates A \<inter>  ChiRel A)"
apply auto
apply (cut_tac A=SA in InitState_States)
apply (cut_tac A=A in HAInitStates_HAStates, fast)
apply (cut_tac A=SA in InitState_States)
apply (cut_tac A=A in HAInitStates_HAStates, fast)
done

lemma AddSA_InitConf [simp]:
 "\<lbrakk> States SA \<inter> HAStates A = {};
    S \<in> InitConf A \<rbrakk> \<Longrightarrow>
    InitConf (A [++] (S,SA)) = insert (InitState SA) (InitConf A)"
apply (frule InitConf_HAStates2)
apply (unfold InitConf_def)
apply (simp del: insert_times_insert)
apply auto
apply (rename_tac T)
apply (case_tac "T=S")
apply auto
prefer 3
apply (rule_tac R="(HAInitStates A) \<times> (HAInitStates A) \<inter> ChiRel A" in trancl_subseteq)
apply auto
apply (rotate_tac 3)
apply (frule trancl_collect)
prefer 2
apply fast
apply auto
apply (cut_tac A=SA in InitState_States)
apply (frule ChiRel_HAStates)
apply fast
apply (frule ChiRel_HAStates)
apply (cut_tac A=SA in InitState_States)
apply fast
apply (frule ChiRel_HAStates)
apply (cut_tac A=SA in InitState_States)
apply fast
apply (subst help_InitConf [THEN sym])
apply fast
apply auto
apply (rule_tac b=S in rtrancl_into_rtrancl)
apply auto
prefer 2
apply (erule rtranclE)
apply auto
prefer 2
apply (erule rtranclE)
apply auto
apply (rule_tac R="(HAInitStates A) \<times> (HAInitStates A) \<inter> ChiRel A" in trancl_subseteq)
apply auto
done

lemma AddSA_InitConf2 [simp]:
 "\<lbrakk> States SA \<inter> HAStates A = {};
    S \<notin> InitConf A;
  S \<in> HAStates A \<rbrakk> \<Longrightarrow>
  InitConf (A [++] (S,SA)) = InitConf A"
apply (unfold InitConf_def)
apply simp
apply auto
apply (rename_tac T)
prefer 2
apply (rule_tac R="(HAInitStates A) \<times> (HAInitStates A) \<inter> ChiRel A" in trancl_subseteq)
apply auto
apply (case_tac "T=InitState SA")
apply auto
prefer 2
apply (rotate_tac 3)
apply (frule trancl_collect)
prefer 2
apply fast
apply auto
apply (cut_tac A=SA in InitState_States)
apply (frule ChiRel_HAStates)
apply fast
apply (cut_tac A=SA in InitState_States)
apply (frule ChiRel_HAStates)
apply fast
apply (cut_tac A=SA in InitState_States)
apply (cut_tac A=A in HAInitStates_HAStates)
apply fast
apply (subst help_InitConf [THEN sym])
apply fast
apply auto
apply (rule_tac b="InitState SA" in rtrancl_induct)
apply auto
apply (frule ChiRel_HAStates2)
apply (cut_tac A=SA in InitState_States)
apply fast
prefer 2
apply (frule ChiRel_HAStates)
apply (cut_tac A=SA in InitState_States)
apply fast
apply (rule rtrancl_into_rtrancl)
apply auto
apply (rule rtrancl_into_rtrancl)
apply auto
done

subsection "Theorems for Calculating Wellformedness of HA";

lemma PseudoHA_HAStates_IFF:
 "(States SA) = X  \<Longrightarrow> (HAStates (PseudoHA SA D)) = X";
apply simp
done

lemma AddSA_SAs_IFF:
 "\<lbrakk> States SA \<inter> HAStates HA = {};
    S \<in> HAStates HA;
    (SAs HA) = X \<rbrakk> \<Longrightarrow> (SAs (HA [++] (S, SA))) = (insert SA X)"
apply (subst AddSA_SAs)
apply auto
done

lemma AddSA_Events_IFF:
 "\<lbrakk> States SA \<inter> HAStates HA = {};
    S \<in> HAStates HA;
    (HAEvents HA) = HAE;
    (SAEvents SA) = SAE;
    (HAE \<union> SAE) = X \<rbrakk> \<Longrightarrow> (HAEvents (HA [++] (S, SA))) = X"
apply (subst AddSA_Events)
apply auto
done

lemma AddSA_CompFun_IFF:
 "\<lbrakk> States SA \<inter>  HAStates HA = {};
    S \<in> HAStates HA;
    (CompFun HA) = HAG;
    (HAG [f+] (S, SA)) = X \<rbrakk> \<Longrightarrow> (CompFun (HA [++] (S, SA))) = X"
apply (subst AddSA_CompFun)
apply auto
done

lemma AddSA_HAStates_IFF:
 "\<lbrakk> States SA \<inter> HAStates HA = {};
    S \<in> HAStates HA;
    (HAStates HA) = HAS;
    (States SA) = SAS;
    (HAS \<union> SAS) = X \<rbrakk> \<Longrightarrow> (HAStates (HA [++] (S, SA))) = X"
apply (subst AddSA_HAStates)
apply auto
done

lemma AddSA_HAInitValue_IFF:
 "\<lbrakk> States SA \<inter> HAStates HA = {};
    S \<in> HAStates HA;
    (HAInitValue HA) = X \<rbrakk> \<Longrightarrow> (HAInitValue (HA [++] (S, SA))) = X"
apply (subst AddSA_HAInitValue)
apply auto
done

lemma AddSA_HARoot_IFF:
 "\<lbrakk> States SA \<inter> HAStates HA = {};
    S \<in> HAStates HA;
    (HARoot HA) = X \<rbrakk> \<Longrightarrow> (HARoot (HA [++] (S, SA))) = X"
apply (subst AddSA_HARoot)
apply auto
done

lemma AddSA_InitConf_IFF:
 "\<lbrakk> InitConf A = Y;
    States SA \<inter> HAStates A = {};
    S \<in> HAStates A;
    (if S \<in> Y then insert (InitState SA) Y else Y) = X \<rbrakk> \<Longrightarrow>
    InitConf (A [++] (S,SA)) = X"
apply (case_tac "S \<in> Y")
apply auto
done

lemma AddSA_CompFun_ran_IFF:
  "\<lbrakk> (States SA \<inter> HAStates A) = {};
     S \<in> HAStates A;
     (insert {} (insert (insert SA (the ((CompFun A) S))) (ran (CompFun A) - {the ((CompFun A) S)}))) = X \<rbrakk> \<Longrightarrow>
     ran (CompFun (A [++] (S,SA))) = X"
apply (subst  AddSA_CompFun_ran)
apply auto
done

lemma AddSA_CompFun_ran2_IFF:
 "\<lbrakk> (States SA1 \<inter> HAStates A) = {};
    (States SA2 \<inter> (HAStates A \<union> States SA1)) = {};
    S \<in> HAStates A;
    T \<in> States SA1;
    insert {} (insert {SA2} (ran (CompFun (A  [++] (S,SA1))))) = X \<rbrakk> \<Longrightarrow>
    ran (CompFun ((A [++] (S,SA1)) [++] (T,SA2))) = X"
apply (subst AddSA_CompFun_ran2)
apply auto
done

lemma AddSA_CompFun_ran3_IFF:
 "\<lbrakk> (States SA1 \<inter> HAStates A) = {};
    (States SA2 \<inter> (HAStates A \<union> States SA1)) = {};
    (States SA3 \<inter> (HAStates A \<union> States SA1 \<union> States SA2)) = {};
     S \<in> HAStates A;
     T \<in> States SA1;
     insert {} (insert {SA3,SA2} (ran (CompFun (A  [++] (S,SA1))))) = X \<rbrakk> \<Longrightarrow>
     ran (CompFun ((A [++] (S,SA1)) [++] (T,SA2) [++] (T,SA3))) = X"
apply (subst AddSA_CompFun_ran3)
apply auto
done

lemma AddSA_CompFun_PseudoHA_ran_IFF:
  "\<lbrakk> S \<in> States RootSA;
     States RootSA \<inter> States SA = {};
   (insert {} {{SA}}) = X \<rbrakk> \<Longrightarrow>
   (ran (CompFun ((PseudoHA RootSA D) [++] (S,SA)))) = X"
apply (subst AddSA_CompFun_PseudoHA_ran)
apply auto
done

lemma AddSA_CompFun_PseudoHA_ran2_IFF:
  "\<lbrakk> States SA1 \<inter> States RootSA = {};
     States SA2 \<inter> (States RootSA \<union> States SA1) = {};
     S \<in> States RootSA;
     (insert {} {{SA2,SA1}}) = X \<rbrakk> \<Longrightarrow>
     (ran (CompFun ((PseudoHA RootSA D) [++] (S,SA1) [++] (S,SA2)))) = X"
apply (subst AddSA_CompFun_PseudoHA_ran2)
apply auto
done

ML {*

val AddSA_SAs_IFF = @{thm AddSA_SAs_IFF};
val AddSA_Events_IFF = @{thm AddSA_Events_IFF};
val AddSA_CompFun_IFF = @{thm AddSA_CompFun_IFF};
val AddSA_HAStates_IFF = @{thm AddSA_HAStates_IFF};
val PseudoHA_HAStates_IFF = @{thm PseudoHA_HAStates_IFF};
val AddSA_HAInitValue_IFF = @{thm AddSA_HAInitValue_IFF};
val AddSA_CompFun_ran_IFF = @{thm AddSA_CompFun_ran_IFF};
val AddSA_HARoot_IFF = @{thm AddSA_HARoot_IFF};
val insert_inter = @{thm insert_inter};
val insert_notmem = @{thm insert_notmem};
val PseudoHA_CompFun = @{thm PseudoHA_CompFun};
val PseudoHA_Events = @{thm PseudoHA_Events};
val PseudoHA_SAs = @{thm PseudoHA_SAs};
val PseudoHA_HARoot = @{thm PseudoHA_HARoot};
val PseudoHA_HAInitValue = @{thm PseudoHA_HAInitValue};
val PseudoHA_CompFun_ran = @{thm PseudoHA_CompFun_ran};
val Un_empty_right = @{thm Un_empty_right};
val insert_union = @{thm insert_union};

fun wellformed_tac ctxt L i =
  FIRST[rtac AddSA_SAs_IFF i,
        rtac AddSA_Events_IFF i,
        rtac AddSA_CompFun_IFF i,
        rtac AddSA_HAStates_IFF i,
        rtac PseudoHA_HAStates_IFF i,
        rtac AddSA_HAInitValue_IFF i,
        rtac AddSA_HARoot_IFF i,
        rtac AddSA_CompFun_ran_IFF i,
        rtac insert_inter i,
        rtac insert_notmem i,
        CHANGED (simp_tac (put_simpset HOL_basic_ss ctxt addsimps
           [PseudoHA_HARoot, PseudoHA_CompFun, PseudoHA_CompFun_ran,PseudoHA_Events,PseudoHA_SAs,insert_union,
            PseudoHA_HAInitValue,Un_empty_right]@ L) i),
        fast_tac ctxt i,
        CHANGED (simp_tac ctxt i)];
*}

method_setup wellformed  = {* Attrib.thms >> (fn thms => fn ctxt => (METHOD (fn facts =>
                                       (HEADGOAL (wellformed_tac ctxt (facts @ thms)))))) *}

end

author: Josh-Tilles

repo: AFP

save_path: github-repos/isabelle/Josh-Tilles-AFP


text:
section \<open>Margulis Gabber Galil Construction\label{sec:margulis}\<close>

text \<open>This section formalizes the Margulis-Gabber-Galil expander graph, which is defined on the
product space $\mathbb Z_n \times \mathbb Z_n$. The construction is an adaptation of graph
introduced by Margulis~\cite{margulis1973}, for which he gave a non-constructive proof of its
spectral gap. Later Gabber and Galil~\cite{gabber1981} adapted the graph and derived an explicit
spectral gap, i.e., that the second largest eigenvalue is bounded by $\frac{5}{8} \sqrt{2}$. The
proof was later improved by Jimbo and Marouka~\cite{jimbo1987} using Fourier Analysis.
Hoory et al.~\cite[\S 8]{hoory2006} present a slight simplification of that proof (due to Boppala)
which this formalization is based on.\<close>

theory Expander_Graphs_MGG
  imports
    "HOL-Analysis.Complex_Transcendental"
    "HOL-Decision_Procs.Approximation"
    "Expander_Graphs_Definition"
begin

datatype ('a, 'b) arc = Arc (arc_tail: 'a)  (arc_head: 'a) (arc_label: 'b)

fun mgg_graph_step :: "nat \<Rightarrow> (int \<times> int) \<Rightarrow> (nat \<times> int) \<Rightarrow> (int \<times> int)"
  where "mgg_graph_step n (i,j) (l,\<sigma>) =
  [ ((i+\<sigma>*(2*j+0)) mod int n, j), (i, (j+\<sigma>*(2*i+0)) mod int n)
  , ((i+\<sigma>*(2*j+1)) mod int n, j), (i, (j+\<sigma>*(2*i+1)) mod int n) ] ! l"

definition mgg_graph :: "nat \<Rightarrow> (int \<times> int, (int \<times> int, nat \<times> int) arc) pre_digraph" where
  "mgg_graph n =
    \<lparr> verts = {0..<n} \<times> {0..<n},
      arcs = (\<lambda>(t,l). (Arc t (mgg_graph_step n t l) l))`(({0..<int n}\<times>{0..<int n})\<times>({..<4}\<times>{-1,1})),
      tail = arc_tail,
      head = arc_head \<rparr>"

locale margulis_gaber_galil =
  fixes m :: nat
  assumes m_gt_0: "m > 0"
begin

abbreviation G where "G \<equiv> mgg_graph m"

lemma wf_digraph: "wf_digraph (mgg_graph m)"
proof -
  have
    "tail (mgg_graph m) e \<in> verts (mgg_graph m)" (is "?A")
    "head (mgg_graph m) e \<in> verts (mgg_graph m)" (is "?B")
    if a:"e \<in> arcs (mgg_graph m)" for e
  proof -
    obtain t l \<sigma> where tl_def:
      "t \<in> {0..<int m} \<times> {0..<int m}" "l \<in> {..<4}" "\<sigma> \<in> {-1,1}"
      "e = Arc t (mgg_graph_step m t (l,\<sigma>)) (l,\<sigma>)"
      using a mgg_graph_def by auto
    thus ?A
      unfolding mgg_graph_def by auto
    have "mgg_graph_step m (fst t, snd t) (l,\<sigma>) \<in> {0..<int m} \<times> {0..<int m}"
      unfolding mgg_graph_step.simps using tl_def(1,2) m_gt_0
      by (intro set_mp[OF _ nth_mem])  auto
    hence "arc_head e \<in> {0..<int m} \<times> {0..<int m}"
      unfolding tl_def(4) by simp
    thus ?B
      unfolding mgg_graph_def by simp
  qed
  thus ?thesis
    by unfold_locales auto
qed

lemma mgg_finite: "fin_digraph (mgg_graph m)"
proof -
  have "finite (verts (mgg_graph m))" "finite (arcs (mgg_graph m))"
    unfolding mgg_graph_def by auto
  thus ?thesis
    using wf_digraph
    unfolding fin_digraph_def fin_digraph_axioms_def by auto
qed

interpretation fin_digraph "mgg_graph m"
  using mgg_finite by simp

definition arcs_pos :: "(int \<times> int, nat \<times> int) arc set"
    where "arcs_pos = (\<lambda>(t,l). (Arc t (mgg_graph_step m t (l,1)) (l, 1)))`(verts G\<times>{..<4})"
definition arcs_neg :: "(int \<times> int, nat \<times> int) arc set"
    where "arcs_neg = (\<lambda>(h,l). (Arc (mgg_graph_step m h (l,1)) h (l,-1)))`(verts G\<times>{..<4})"

lemma arcs_sym:
  "arcs G = arcs_pos \<union> arcs_neg"
proof -
  have 0: "x \<in> arcs G" if "x \<in> arcs_pos" for x
    using that unfolding arcs_pos_def mgg_graph_def by auto
  have 1: "a \<in> arcs G" if t:"a \<in> arcs_neg" for a
  proof -
    obtain h l where hl_def: "h \<in> verts G" "l \<in> {..<4}" "a = Arc (mgg_graph_step m h (l,1)) h (l,-1)"
      using t unfolding arcs_neg_def by auto

    define t where "t = mgg_graph_step m h (l,1)"

    have h_ran: "h \<in> {0..<int m} \<times> {0..<int m}"
      using hl_def(1) unfolding mgg_graph_def by simp
    have l_ran: "l \<in> set [0,1,2,3]"
      using hl_def(2) by auto

    have "t \<in> {0..<int m} \<times> {0..<int m}"
      using h_ran l_ran
      unfolding t_def by (cases h, auto simp add:mod_simps)
    hence t_ran: "t \<in> verts G"
      unfolding mgg_graph_def by simp

    have "h = mgg_graph_step m t (l,-1)"
      using h_ran l_ran unfolding t_def by (cases h, auto simp add:mod_simps)
    hence "a = Arc t (mgg_graph_step m t (l,-1)) (l,-1)"
      unfolding t_def hl_def(3) by simp
    thus ?thesis
      using t_ran hl_def(2) mgg_graph_def by (simp add:image_iff)
  qed

  have "card (arcs_pos \<union> arcs_neg) = card arcs_pos + card arcs_neg"
    unfolding arcs_pos_def arcs_neg_def by (intro card_Un_disjoint finite_imageI) auto
  also have "... = card (verts G\<times>{..<4::nat}) + card (verts G\<times>{..<4::nat})"
    unfolding arcs_pos_def arcs_neg_def
    by (intro arg_cong2[where f="(+)"] card_image inj_onI) auto
  also have "... = card (verts G\<times>{..<4::nat}\<times>{-1,1::int})"
    by simp
  also have "... = card ((\<lambda>(t, l). Arc t (mgg_graph_step m t l) l) ` (verts G \<times>{..<4}\<times>{-1,1}))"
    by (intro card_image[symmetric] inj_onI) auto
  also have "... = card (arcs G)"
    unfolding mgg_graph_def by simp
  finally have "card (arcs_pos \<union> arcs_neg) = card (arcs G)"
    by simp
  hence "arcs_pos \<union> arcs_neg = arcs G"
    using 0 1 by (intro card_subset_eq, auto)
  thus ?thesis by simp
qed

lemma sym: "symmetric_multi_graph (mgg_graph m)"
proof -
  define f :: "(int \<times> int, nat \<times> int) arc \<Rightarrow> (int \<times> int, nat \<times> int) arc"
    where "f a = Arc (arc_head a) (arc_tail a) (apsnd (\<lambda>x. (-1) * x) (arc_label a))" for a

  have a: "bij_betw f arcs_pos arcs_neg"
    by (intro bij_betwI[where g="f"])
     (auto simp add:f_def image_iff arcs_pos_def arcs_neg_def)

  have b: "bij_betw f arcs_neg arcs_pos"
    by (intro bij_betwI[where g="f"])
     (auto simp add:f_def image_iff  arcs_pos_def arcs_neg_def)

  have c:"bij_betw f (arcs_pos \<union> arcs_neg) (arcs_neg \<union> arcs_pos)"
    by (intro bij_betw_combine[OF a b])  (auto simp add:arcs_pos_def arcs_neg_def)

  hence c:"bij_betw f (arcs G) (arcs G)"
    unfolding arcs_sym by (subst (2) sup_commute, simp)
  show ?thesis
    by (intro symmetric_multi_graphI[where f="f"] fin_digraph_axioms c)
     (simp add:f_def mgg_graph_def)
qed

lemma out_deg:
  assumes "v \<in> verts G"
  shows "out_degree G v = 8"
proof -
  have "out_degree (mgg_graph m) v = card (out_arcs (mgg_graph m) v)"
    unfolding out_degree_def by simp
  also have "... = card {e. (\<exists>w \<in> verts (mgg_graph m). \<exists>l \<in> {..<4} \<times> {-1,1}.
    e = Arc w (mgg_graph_step m w l) l \<and> arc_tail e = v)}"
    unfolding mgg_graph_def out_arcs_def by (simp add:image_iff)
  also have "... = card {e. (\<exists>l \<in> {..<4} \<times> {-1,1}. e = Arc v (mgg_graph_step m v l) l)}"
    using assms by (intro arg_cong[where f="card"] iffD2[OF set_eq_iff] allI)  auto
  also have "... = card ((\<lambda>l. Arc v (mgg_graph_step m v l) l) ` ({..<4} \<times> {-1,1}))"
    by (intro arg_cong[where f="card"]) (auto simp add:image_iff)
  also have "... = card ({..<4::nat} \<times> {-1,1::int})"
    by (intro card_image inj_onI) simp
  also have "... = 8" by simp
  finally show ?thesis by simp
qed

lemma verts_ne:
  "verts G \<noteq> {}"
  using m_gt_0 unfolding mgg_graph_def by simp

sublocale regular_graph "mgg_graph m"
  using out_deg verts_ne
  by (intro regular_graphI[where d="8"] sym) auto

lemma d_eq_8: "d = 8"
proof -
  obtain v where v_def: "v \<in> verts G"
    using verts_ne by auto
  hence 0:"(SOME v. v \<in> verts G) \<in> verts G"
    by (rule someI[where x="v"])
  show ?thesis
    using out_deg[OF 0]
    unfolding d_def by simp
qed

text \<open>We start by introducing Fourier Analysis on the torus $\mathbb Z_n \times \mathbb Z_n$. The
following is too specialized for a general AFP entry.\<close>

lemma g_inner_sum_left:
  assumes "finite I"
  shows "g_inner (\<lambda>x. (\<Sum>i \<in> I. f i x)) g = (\<Sum>i\<in> I. g_inner (f i) g)"
  using assms by (induction I rule:finite_induct) (auto simp add:g_inner_simps)

lemma g_inner_sum_right:
  assumes "finite I"
  shows "g_inner f (\<lambda>x. (\<Sum>i \<in> I. g i x)) = (\<Sum>i\<in> I. g_inner f (g i))"
  using assms by (induction I rule:finite_induct) (auto simp add:g_inner_simps)

lemma g_inner_reindex:
  assumes "bij_betw h (verts G) (verts G)"
  shows "g_inner f g = g_inner (\<lambda>x. (f (h x))) (\<lambda>x. (g (h x)))"
  unfolding g_inner_def
  by (subst sum.reindex_bij_betw[OF assms,symmetric]) simp

definition \<omega>\<^sub>F :: "real \<Rightarrow> complex" where "\<omega>\<^sub>F x = cis (2*pi*x/m)"

lemma \<omega>\<^sub>F_simps:
  "\<omega>\<^sub>F (x + y) = \<omega>\<^sub>F x * \<omega>\<^sub>F y"
  "\<omega>\<^sub>F (x - y) = \<omega>\<^sub>F x * \<omega>\<^sub>F (-y)"
  "cnj (\<omega>\<^sub>F x) = \<omega>\<^sub>F (-x)"
  unfolding \<omega>\<^sub>F_def by (auto simp add:algebra_simps diff_divide_distrib
      add_divide_distrib cis_mult cis_divide cis_cnj)

lemma \<omega>\<^sub>F_cong:
  fixes x y :: int
  assumes "x mod m = y mod m"
  shows "\<omega>\<^sub>F (of_int x) = \<omega>\<^sub>F (of_int y)"
proof -
  obtain z :: int where "y = x + m*z" using mod_eqE[OF assms] by auto
  hence "\<omega>\<^sub>F (of_int y) = \<omega>\<^sub>F (of_int x + of_int (m*z))"
    by simp
  also have "... = \<omega>\<^sub>F (of_int x) * \<omega>\<^sub>F (of_int (m*z))"
    by (simp add:\<omega>\<^sub>F_simps)
  also have "... = \<omega>\<^sub>F (of_int x) * cis (2 * pi * of_int (z))"
    unfolding \<omega>\<^sub>F_def  using m_gt_0
    by (intro arg_cong2[where f="(*)"] arg_cong[where f="cis"]) auto
  also have "... = \<omega>\<^sub>F (of_int x) * 1"
    by (intro arg_cong2[where f="(*)"] cis_multiple_2pi) auto
  finally show ?thesis by simp
qed

lemma cis_eq_1_imp:
  assumes "cis (2 * pi * x) = 1"
  shows "x \<in> \<int>"
proof -
  have "cos (2 * pi * x) = Re (cis (2*pi*x))"
    using cis.simps by simp
  also have "... = 1"
    unfolding assms by simp
  finally have "cos (2 * pi * x) = 1" by simp
  then obtain y where "2 * pi * x = of_int y * 2 * pi"
    using cos_one_2pi_int by auto
  hence "y = x" by simp
  thus ?thesis by auto
qed

lemma \<omega>\<^sub>F_eq_1_iff:
  fixes x :: int
  shows "\<omega>\<^sub>F x = 1 \<longleftrightarrow> x mod m = 0"
proof
  assume "\<omega>\<^sub>F (real_of_int x) = 1"
  hence "cis (2 * pi * real_of_int x / real m) = 1"
    unfolding \<omega>\<^sub>F_def by simp
  hence "real_of_int x / real m \<in> \<int>"
    using cis_eq_1_imp by simp
  then obtain z :: int where "of_int x / real m = z"
    using Ints_cases by auto
  hence "x = z * real m"
    using m_gt_0 by (simp add: nonzero_divide_eq_eq)
  hence "x = z * m" using of_int_eq_iff by fastforce
  thus "x mod m = 0" by simp
next
  assume "x mod m = 0"
  hence "\<omega>\<^sub>F x = \<omega>\<^sub>F (of_int 0)"
    by (intro \<omega>\<^sub>F_cong) auto
  also have "... = 1" unfolding \<omega>\<^sub>F_def by simp
  finally show "\<omega>\<^sub>F x= 1" by simp
qed

definition FT :: "(int \<times> int \<Rightarrow> complex) \<Rightarrow> (int \<times> int \<Rightarrow> complex)"
  where "FT f v = g_inner f (\<lambda>x. \<omega>\<^sub>F (fst x * fst v + snd x * snd v))"

lemma FT_altdef: "FT f (u,v) = g_inner f (\<lambda>x. \<omega>\<^sub>F (fst x * u + snd x * v))"
  unfolding FT_def by (simp add:case_prod_beta)

lemma FT_add: "FT (\<lambda>x. f x + g x) v = FT f v + FT g v"
  unfolding FT_def by (simp add:g_inner_simps algebra_simps)

lemma FT_zero: "FT (\<lambda>x. 0) v = 0"
  unfolding FT_def g_inner_def by simp

lemma FT_sum:
  assumes "finite I"
  shows "FT (\<lambda>x. (\<Sum>i \<in> I. f i x)) v = (\<Sum>i \<in> I. FT (f i) v)"
  using assms by (induction rule: finite_induct, auto simp add:FT_zero FT_add)

lemma FT_scale: "FT (\<lambda>x. c * f x) v = c * FT f v"
  unfolding FT_def by (simp add: g_inner_simps)

lemma FT_cong:
  assumes "\<And>x. x \<in> verts G \<Longrightarrow> f x = g x"
  shows "FT f = FT g"
  unfolding FT_def by (intro ext g_inner_cong assms refl)

lemma parseval:
  "g_inner f g = g_inner (FT f) (FT g)/m^2" (is "?L = ?R")
proof -
  define \<delta> :: "(int \<times> int) \<Rightarrow> (int \<times> int) \<Rightarrow> complex" where "\<delta> x y = of_bool (x = y)" for x y

  have FT_\<delta>: "FT (\<delta> v) x = \<omega>\<^sub>F (-(fst v *fst x +snd v * snd x))" if "v \<in> verts G" for v x
    using that by (simp add:FT_def g_inner_def \<delta>_def \<omega>\<^sub>F_simps)

  have 1: "(\<Sum>x=0..<int m. \<omega>\<^sub>F (z*x)) = m * of_bool(z mod m = 0)" (is "?L1 = ?R1") for z :: int
  proof (cases "z mod m = 0")
    case True
    have "(\<Sum>x=0..<int m. \<omega>\<^sub>F (z*x)) = (\<Sum>x=0..<int m. \<omega>\<^sub>F (of_int 0))"
      using True by (intro sum.cong \<omega>\<^sub>F_cong refl) auto
    also have "... = m * of_bool(z mod m = 0)"
      unfolding \<omega>\<^sub>F_def True by simp
    finally show ?thesis by simp
  next
    case False
    have "(1-\<omega>\<^sub>F z) * ?L1 = (1-\<omega>\<^sub>F z) * (\<Sum>x \<in> int ` {..<m}. \<omega>\<^sub>F(z*x))"
      by (intro arg_cong2[where f="(*)"] sum.cong refl)
       (simp add: image_atLeastZeroLessThan_int)
    also have "... = (\<Sum>x<m. \<omega>\<^sub>F(z*real x) - \<omega>\<^sub>F(z*(real (Suc x))))"
      by (subst sum.reindex, auto simp add:algebra_simps sum_distrib_left \<omega>\<^sub>F_simps)
    also have "... = \<omega>\<^sub>F (z * 0) - \<omega>\<^sub>F (z * m)"
      by (subst sum_lessThan_telescope') simp
    also have "... = \<omega>\<^sub>F (of_int 0) - \<omega>\<^sub>F (of_int 0)"
      by (intro arg_cong2[where f="(-)"] \<omega>\<^sub>F_cong) auto
    also have "... = 0"
      by simp
    finally have "(1- \<omega>\<^sub>F z) * ?L1 = 0" by simp
    moreover have "\<omega>\<^sub>F z \<noteq> 1" using \<omega>\<^sub>F_eq_1_iff False by simp
    hence "(1- \<omega>\<^sub>F z) \<noteq> 0" by simp
    ultimately have "?L1 = 0" by simp
    then show ?thesis using False by simp
  qed

  have 0:"g_inner (\<delta> v) (\<delta> w) = g_inner (FT (\<delta> v)) (FT (\<delta> w))/m^2" (is "?L1 = ?R1/_")
    if "v \<in> verts G" "w \<in> verts G" for v w
  proof -
    have "?R1=g_inner(\<lambda>x. \<omega>\<^sub>F(-(fst v *fst x +snd v * snd x)))(\<lambda>x. \<omega>\<^sub>F(-(fst w *fst x +snd w * snd x)))"
      using that by (intro g_inner_cong, auto simp add:FT_\<delta>)
    also have "...=(\<Sum>(x,y)\<in>{0..<int m}\<times>{0..<int m}. \<omega>\<^sub>F((fst w-fst v)*x)*\<omega>\<^sub>F((snd w - snd v)* y))"
      unfolding g_inner_def by (simp add:\<omega>\<^sub>F_simps algebra_simps case_prod_beta mgg_graph_def)
    also have "...=(\<Sum>x=0..<int m. \<Sum>y = 0..<int m. \<omega>\<^sub>F((fst w - fst v)*x)*\<omega>\<^sub>F((snd w - snd v) * y))"
      by (subst sum.cartesian_product[symmetric]) simp
    also have "...=(\<Sum>x=0..<int m. \<omega>\<^sub>F((fst w - fst v)*x))*(\<Sum>y = 0..<int m. \<omega>\<^sub>F((snd w - snd v) * y))"
      by (subst sum.swap) (simp add:sum_distrib_left sum_distrib_right)
    also have "... = of_nat (m * of_bool(fst v mod m = fst w mod m)) *
      of_nat (m * of_bool(snd v mod m = snd w mod m))"
      using m_gt_0 unfolding 1
      by (intro arg_cong2[where f="(*)"] arg_cong[where f="of_bool"]
          arg_cong[where f="of_nat"] refl) (auto simp add:algebra_simps cong:mod_diff_cong)
    also have "... = m^2 * of_bool(v = w)"
      using that by (auto simp add:prod_eq_iff mgg_graph_def power2_eq_square)
    also have "... = m^2 * ?L1"
      using that unfolding g_inner_def \<delta>_def by simp
    finally have "?R1 = m^2 * ?L1" by simp
    thus ?thesis using m_gt_0 by simp
  qed

  have "?L = g_inner (\<lambda>x. (\<Sum>v \<in> verts G. (f v) * \<delta> v x)) (\<lambda>x. (\<Sum>v \<in> verts G. (g v) * \<delta> v x))"
    unfolding \<delta>_def by (intro g_inner_cong) auto
  also have "... = (\<Sum>v\<in>verts G. (f v) * (\<Sum>w\<in>verts G. cnj (g w) * g_inner (\<delta> v) (\<delta> w)))"
    by (simp add:g_inner_simps g_inner_sum_left g_inner_sum_right)
  also have "... = (\<Sum>v\<in>verts G. (f v) * (\<Sum>w\<in>verts G. cnj (g w) * g_inner(FT (\<delta> v)) (FT (\<delta> w))))/m^2"
    by (simp add:0 sum_divide_distrib sum_distrib_left algebra_simps)
  also have "...=g_inner(\<lambda>x.(\<Sum>v\<in>verts G. (f v)*FT (\<delta> v) x))(\<lambda>x.(\<Sum>v\<in>verts G. (g v)*FT (\<delta> v) x))/m\<^sup>2"
    by (simp add:g_inner_simps g_inner_sum_left g_inner_sum_right)
  also have "...=g_inner(FT(\<lambda>x.(\<Sum>v\<in>verts G.(f v)*\<delta> v x)))(FT(\<lambda>x.(\<Sum>v\<in>verts G.(g v)*\<delta> v x)))/m\<^sup>2"
    by (intro g_inner_cong arg_cong2[where f="(/)"]) (simp_all add: FT_sum FT_scale)
  also have "... = g_inner (FT f) (FT g)/m^2 "
    unfolding \<delta>_def comp_def
    by (intro g_inner_cong arg_cong2[where f="(/)"] fun_cong[OF FT_cong]) auto
  finally show ?thesis by simp
qed

lemma plancharel:
  "(\<Sum>v \<in> verts G. norm (f v)^2) = (\<Sum>v \<in> verts G. norm (FT f v)^2)/m^2" (is "?L = ?R")
proof -
  have "complex_of_real ?L = g_inner f f"
    by (simp flip:of_real_power add:complex_norm_square g_inner_def algebra_simps)
  also have "... = g_inner (FT f) (FT f) / m^2"
    by (subst parseval) simp
  also have "... = complex_of_real ?R"
    by (simp flip:of_real_power add:complex_norm_square g_inner_def algebra_simps) simp
  finally have "complex_of_real ?L = complex_of_real ?R" by simp
  thus ?thesis
    using of_real_eq_iff by blast
qed

lemma FT_swap:
  "FT (\<lambda>x. f (snd x, fst x)) (u,v) = FT f (v,u)"
proof -
  have 0:"bij_betw (\<lambda>(x::int \<times> int). (snd x, fst x)) (verts G) (verts G)"
    by (intro bij_betwI[where g="(\<lambda>(x::int \<times> int). (snd x, fst x))"])
     (auto simp add:mgg_graph_def)
  show ?thesis
    unfolding FT_def
    by (subst g_inner_reindex[OF 0]) (simp add:algebra_simps)
qed

lemma mod_add_mult_eq:
  fixes a x y :: int
  shows "(a + x * (y mod m)) mod m = (a+x*y) mod m"
  using mod_add_cong mod_mult_right_eq by blast

definition periodic where "periodic f = (\<forall>x y. f (x,y) = f (x mod int m, y mod int m))"

lemma periodicD:
  assumes "periodic f"
  shows "f (x,y) = f (x mod m, y mod m)"
  using assms unfolding periodic_def by simp

lemma periodic_comp:
  assumes "periodic f"
  shows "periodic (\<lambda>x. g (f x))"
  using assms unfolding periodic_def by simp

lemma periodic_cong:
  fixes x y u v :: int
  assumes "periodic f"
  assumes "x mod m = u mod m" "y mod m = v mod m"
  shows "f (x,y) = f (u, v)"
  using periodicD[OF assms(1)] assms(2,3) by metis

lemma periodic_FT: "periodic (FT f)"
proof -
  have "FT f (x,y) = FT f (x mod m,y mod m)" for x y
    unfolding FT_altdef by (intro g_inner_cong \<omega>\<^sub>F_cong ext)
     (auto simp add:mod_simps cong:mod_add_cong)
  thus ?thesis
    unfolding periodic_def by simp
qed

lemma FT_sheer_aux:
  fixes u v c d :: int
  assumes "periodic f"
  shows  "FT (\<lambda>x. f (fst x,snd x+c*fst x+d)) (u,v) = \<omega>\<^sub>F (d* v) * FT f (u-c* v,v)"
    (is "?L = ?R")
proof -
  define s where "s = (\<lambda>(x,y). (x, (y - c * x-d) mod m))"
  define s0 where "s0 = (\<lambda>(x,y). (x, (y-c*x) mod m))"
  define s1 where "s1 = (\<lambda>(x::int,y). (x, (y-d) mod m))"

  have 0:"bij_betw s0 (verts G) (verts G)"
    by (intro bij_betwI[where g="\<lambda>(x,y). (x,(y+c*x) mod m)"])
     (auto simp add:mgg_graph_def s0_def Pi_def mod_simps)
  have 1:"bij_betw s1 (verts G) (verts G)"
    by (intro bij_betwI[where g="\<lambda>(x,y). (x,(y+d) mod m)"])
     (auto simp add:mgg_graph_def s1_def Pi_def mod_simps)
  have 2: "s = (s1 \<circ> s0)"
    by (simp add:s1_def s0_def s_def comp_def mod_simps case_prod_beta ext)
  have 3:"bij_betw s (verts G) (verts G)"
    unfolding 2 using bij_betw_trans[OF 0 1] by simp

  have 4:"(snd (s x) + c * fst x + d) mod int m = snd x mod m" for x
    unfolding s_def by (simp add:case_prod_beta cong:mod_add_cong) (simp add:algebra_simps)
  have 5: "fst (s x) = fst x" for x
    unfolding s_def by (cases x, simp)

  have "?L = g_inner (\<lambda>x. f (fst x, snd x + c*fst x+d)) (\<lambda>x. \<omega>\<^sub>F (fst x*u + snd x* v))"
    unfolding FT_altdef by simp
  also have "... = g_inner (\<lambda>x. f (fst x, (snd x + c*fst x+d) mod m)) (\<lambda>x. \<omega>\<^sub>F (fst x*u + snd x* v))"
    by (intro g_inner_cong  periodic_cong[OF assms]) (auto simp add:algebra_simps)
  also have "... = g_inner (\<lambda>x. f (fst x, snd x mod m)) (\<lambda>x. \<omega>\<^sub>F (fst x*u+ snd (s x)* v))"
    by (subst g_inner_reindex[OF 3]) (simp add:4 5)
  also have "... =
    g_inner (\<lambda>x. f (fst x, snd x mod m)) (\<lambda>x. \<omega>\<^sub>F (fst x*u+ ((snd x-c*fst x-d) mod m)* v))"
    by (simp add:s_def case_prod_beta)
  also have "... = g_inner f (\<lambda>x. \<omega>\<^sub>F (fst x* (u-c * v) + snd x * v-d * v))"
    by (intro g_inner_cong \<omega>\<^sub>F_cong) (auto simp add:mgg_graph_def algebra_simps mod_add_mult_eq)
  also have "... = g_inner f (\<lambda>x. \<omega>\<^sub>F (-d* v)*\<omega>\<^sub>F (fst x*(u-c* v) + snd x * v))"
    by (simp add: \<omega>\<^sub>F_simps   algebra_simps)
  also have "... = \<omega>\<^sub>F (d* v)*g_inner f (\<lambda>x. \<omega>\<^sub>F (fst x*(u-c* v) + snd x * v))"
    by (simp add:g_inner_simps \<omega>\<^sub>F_simps)
  also have "... = ?R"
    unfolding FT_altdef by simp
  finally show ?thesis by simp
qed

lemma FT_sheer:
  fixes u v c d :: int
  assumes "periodic f"
  shows
    "FT (\<lambda>x. f (fst x,snd x+c*fst x+d)) (u,v) = \<omega>\<^sub>F (d* v) * FT f (u-c* v,v)" (is "?A")
    "FT (\<lambda>x. f (fst x,snd x+c*fst x)) (u,v) = FT f (u-c* v,v)" (is "?B")
    "FT (\<lambda>x. f (fst x+c* snd x+d,snd x)) (u,v) = \<omega>\<^sub>F (d* u) * FT f (u,v-c*u)" (is "?C")
    "FT (\<lambda>x. f (fst x+c* snd x,snd x)) (u,v) = FT f (u,v-c*u)" (is "?D")
proof -
  have 1: "periodic (\<lambda>x. f (snd x, fst x))"
    using assms unfolding periodic_def by simp

  have 0:"\<omega>\<^sub>F 0 = 1"
    unfolding \<omega>\<^sub>F_def by simp
  show ?A
    using FT_sheer_aux[OF assms] by simp
  show ?B
    using 0 FT_sheer_aux[OF assms, where d="0"] by simp
  show ?C
    using FT_sheer_aux[OF 1] by (subst (1 2) FT_swap[symmetric], simp)
  show ?D
    using 0 FT_sheer_aux[OF 1, where d="0"] by (subst (1 2) FT_swap[symmetric], simp)
qed

definition T\<^sub>1 :: "int \<times> int \<Rightarrow> int \<times> int" where "T\<^sub>1 x = ((fst x + 2 * snd x) mod m, snd x)"
definition S\<^sub>1 :: "int \<times> int \<Rightarrow> int \<times> int" where "S\<^sub>1 x = ((fst x - 2 * snd x) mod m, snd x)"
definition T\<^sub>2 :: "int \<times> int \<Rightarrow> int \<times> int" where "T\<^sub>2 x = (fst x, (snd x + 2 * fst x) mod m)"
definition S\<^sub>2 :: "int \<times> int \<Rightarrow> int \<times> int" where "S\<^sub>2 x = (fst x, (snd x - 2 * fst x) mod m)"

definition \<gamma>_aux :: "int \<times> int \<Rightarrow> real \<times> real"
    where "\<gamma>_aux x = (\<bar>fst x/m-1/2\<bar>,\<bar>snd x/m-1/2\<bar>)"

definition compare :: "real \<times> real \<Rightarrow> real \<times> real \<Rightarrow> bool"
  where "compare x y = (fst x \<le> fst y \<and> snd x \<le> snd y \<and> x \<noteq> y)"

text \<open>The value here is different from the value in the source material. This is because the proof
in Hoory~\cite[\S 8]{hoory2006} only establishes the bound $\frac{73}{80}$ while this formalization
establishes the improved bound of $\frac{5}{8} \sqrt 2$.\<close>

definition \<alpha> :: real where "\<alpha> = sqrt 2"

lemma \<alpha>_inv: "1/\<alpha> = \<alpha>/2"
  unfolding \<alpha>_def by (simp add: real_div_sqrt)

definition \<gamma> :: "int \<times> int \<Rightarrow> int \<times> int \<Rightarrow> real"
  where "\<gamma> x y = (if compare (\<gamma>_aux x) (\<gamma>_aux y) then \<alpha> else (if compare  (\<gamma>_aux y) (\<gamma>_aux x) then (1 / \<alpha>) else 1))"

lemma \<gamma>_sym: "\<gamma> x y * \<gamma> y x = 1"
  unfolding \<gamma>_def \<alpha>_def compare_def by (auto simp add:prod_eq_iff)

lemma \<gamma>_nonneg: "\<gamma> x y \<ge> 0"
  unfolding \<gamma>_def \<alpha>_def by auto

definition \<tau> :: "int \<Rightarrow> real" where "\<tau> x = \<bar>cos(pi*x/m)\<bar>"

definition \<gamma>' :: "real \<Rightarrow> real \<Rightarrow> real"
  where "\<gamma>' x y = (if abs (x - 1/2) < abs (y - 1/2) then \<alpha> else (if abs (x-1/2) > abs (y-1/2) then (1 / \<alpha>) else 1))"

definition \<phi> :: "real \<Rightarrow> real \<Rightarrow> real"
  where "\<phi> x y = \<gamma>' y (frac(y-2*x))+\<gamma>' y (frac (y+2*x))"

lemma \<gamma>'_cases:
  "abs (x-1/2) = abs (y-1/2) \<Longrightarrow> \<gamma>' x y = 1"
  "abs (x-1/2) > abs (y-1/2) \<Longrightarrow> \<gamma>' x y = 1/\<alpha>"
  "abs (x-1/2) < abs (y-1/2) \<Longrightarrow> \<gamma>' x y = \<alpha>"
  unfolding \<gamma>'_def by auto

lemma if_cong_direct:
  assumes "a = b"
  assumes "c = d'"
  assumes "e = f"
  shows "(if a then c else e) = (if b then d' else f)"
  using assms by (intro if_cong) auto

lemma \<gamma>'_cong:
  assumes "abs (x-1/2) = abs (u-1/2)"
  assumes "abs (y-1/2) = abs (v-1/2)"
  shows "\<gamma>' x y = \<gamma>' u v"
  unfolding \<gamma>'_def
  using assms by (intro if_cong_direct refl) auto

lemma add_swap_cong:
  fixes x y u v :: "'a :: ab_semigroup_add"
  assumes "x = y" "u = v"
  shows "x + u = v + y"
  using assms by (simp add:algebra_simps)

lemma frac_cong:
  fixes x y :: real
  assumes "x - y \<in> \<int>"
  shows "frac x = frac y"
proof -
  obtain k where x_eq: "x = y + of_int k"
    using Ints_cases[OF assms] by (metis add_minus_cancel uminus_add_conv_diff)
  thus ?thesis
    unfolding x_eq  unfolding frac_def by simp
qed

lemma frac_expand:
  fixes x :: real
  shows "frac x = (if x < (-1) then (x-\<lfloor>x\<rfloor>) else (if x < 0 then (x+1) else (if x < 1 then x else (if x < 2 then (x-1) else  (x-\<lfloor>x\<rfloor>)))))"
proof -
  have "real_of_int y = -1 \<longleftrightarrow> y= -1" for y
    by auto
  thus ?thesis
    unfolding frac_def  by (auto simp add:not_less floor_eq_iff)
qed

lemma one_minus_frac:
  fixes x :: real
  shows "1 - frac x = (if x \<in> \<int> then 1 else frac (-x))"
  unfolding frac_neg by simp

lemma abs_rev_cong:
  fixes x y :: real
  assumes "x = - y"
  shows "abs x = abs y"
  using assms by simp

lemma cos_pi_ge_0:
  assumes "x \<in>{-1/2.. 1/2}"
  shows "cos (pi * x) \<ge> 0"
proof -
  have "pi * x \<in> ((*) pi ` {-1/2..1/2})"
    by (intro imageI assms)
  also have "... =  {-pi/2..pi/2}"
    by (subst image_mult_atLeastAtMost[OF pi_gt_zero])  simp
  finally have "pi * x \<in> {-pi/2..pi/2}" by simp
  thus ?thesis
    by (intro cos_ge_zero) auto
qed

text \<open>The following is the first step in establishing Eq. 15 in Hoory et al.~\cite[\S 8]{hoory2006}.
Afterwards using various symmetries (diagonal, x-axis, y-axis) the result will follow for the entire
square $[0,1] \times [0,1]$.\<close>

lemma fun_bound_real_3:
  assumes "0 \<le> x"  "x \<le> y" "y \<le> 1/2" "(x,y) \<noteq> (0,0)"
  shows "\<bar>cos(pi*x)\<bar>*\<phi> x y + \<bar>cos(pi*y)\<bar>*\<phi> y x \<le> 2.5 * sqrt 2" (is "?L \<le> ?R")
proof -
  have apx:"4 \<le> 5 * sqrt (2::real)" "8 * cos (pi / 4) \<le> 5 * sqrt (2::real)"
    by (approximation 5)+

  have "cos (pi * x) \<ge> 0"
    using assms(1,2,3)  by (intro cos_pi_ge_0) simp
  moreover have "cos (pi * y) \<ge> 0"
    using assms(1,2,3)  by (intro cos_pi_ge_0) simp
  ultimately have 0:"?L = cos(pi*x)*\<phi> x y + cos(pi*y)*\<phi> y x"  (is "_ = ?T")
    by simp

  consider (a) "x+y < 1/2" | (b) "y = 1/2- x" | (c) "x+y > 1/2" by argo
  hence "?T \<le> 2.5 * sqrt 2" (is "?T \<le> ?R")
  proof (cases)
    case a
    consider
      (1) "x < y" "x > 0" |
      (2) "x=0" "y < 1/2" |
      (3) "y=x" "x > 0"
      using assms(1,2,3,4) a by fastforce
    thus ?thesis
    proof (cases)
      case 1
      have "\<phi> x y = \<alpha> + 1/\<alpha>"
        unfolding \<phi>_def using 1 a
        by (intro arg_cong2[where f="(+)"] \<gamma>'_cases) (auto simp add:frac_expand)
      moreover have "\<phi> y x = 1/\<alpha> + 1/\<alpha>"
        unfolding \<phi>_def using 1 a
        by (intro arg_cong2[where f="(+)"] \<gamma>'_cases) (auto simp add:frac_expand)
      ultimately have "?T = cos (pi * x) * (\<alpha> + 1/\<alpha>) + cos (pi * y) * (1/\<alpha> + 1/\<alpha>)"
        by simp
      also have "... \<le> 1 * (\<alpha> + 1/\<alpha>) + 1 * (1/\<alpha> + 1/\<alpha>)"
        unfolding \<alpha>_def by (intro add_mono mult_right_mono) auto
      also have "... = ?R"
        unfolding \<alpha>_def by (simp add:divide_simps)
      finally show ?thesis by simp
    next
      case 2
      have y_range: "y \<in> {0<..<1/2}"
        using assms 2 by simp
      have "\<phi> 0 y = 1 + 1"
        unfolding \<phi>_def using y_range
        by (intro arg_cong2[where f="(+)"] \<gamma>'_cases) (auto simp add:frac_expand)
      moreover
      have "\<bar>x\<bar> * 2 < 1 \<longleftrightarrow> x < 1/2 \<and> -x < 1/2" for x :: real by auto
      hence "\<phi> y 0 = 1 / \<alpha> + 1/ \<alpha>"
        unfolding \<phi>_def using y_range
        by (intro arg_cong2[where f="(+)"] \<gamma>'_cases) (simp_all add:frac_expand)
      ultimately have "?T = 2 + cos (pi * y) * (2 / \<alpha>)"
        unfolding 2 by simp
      also have "... \<le> 2 + 1 * (2 / \<alpha>)"
        unfolding \<alpha>_def by (intro add_mono mult_right_mono) auto
      also have "... \<le> ?R"
        unfolding \<alpha>_def by (approximation 10)
      finally show ?thesis by simp
    next
      case 3
      have "\<phi> x y = 1 + 1/\<alpha>"
        unfolding \<phi>_def using 3 a
        by (intro arg_cong2[where f="(+)"] \<gamma>'_cases) (auto simp add:frac_expand)
      moreover have "\<phi> y x = 1 + 1/\<alpha>"
        unfolding \<phi>_def using 3 a
        by (intro arg_cong2[where f="(+)"] \<gamma>'_cases) (auto simp add:frac_expand)
      ultimately have "?T = cos (pi * x) * (2*(1+1/ \<alpha>))"
        unfolding 3 by simp
      also have "... \<le> 1 * (2*(1+1/ \<alpha>))"
        unfolding \<alpha>_def by (intro mult_right_mono) auto
      also have "... \<le> ?R"
        unfolding \<alpha>_def by (approximation 10)
      finally show ?thesis by simp
    qed
  next
    case b
    have x_range: "x \<in> {0..1/4}"
      using assms b by simp
    then consider (1) "x = 0" | (2) "x = 1/4" | (3) "x \<in> {0<..<1/4}" by fastforce
    thus ?thesis
    proof (cases)
      case 1
      hence y_eq: "y = 1/2" using b by simp
      show ?thesis using apx unfolding 1 y_eq \<phi>_def by (simp add:\<gamma>'_def \<alpha>_def frac_def)
    next
      case 2
      hence y_eq: "y = 1/4" using b by simp
      show ?thesis using apx unfolding y_eq 2 \<phi>_def by (simp add:\<gamma>'_def frac_def)
    next
      case 3
      have "\<phi> x y = \<alpha> + 1"
        unfolding \<phi>_def b using 3
        by (intro arg_cong2[where f="(+)"] \<gamma>'_cases) (auto simp add:frac_expand)
      moreover have "\<phi> y x = 1/\<alpha> + 1"
        unfolding \<phi>_def b using 3
        by (intro arg_cong2[where f="(+)"] \<gamma>'_cases) (auto simp add:frac_expand)
      ultimately have "?T = cos (pi * x) * (\<alpha> + 1) + cos (pi * (1 / 2 - x)) * (1/\<alpha> + 1)"
        unfolding b by simp
      also have "... \<le> ?R"
        unfolding \<alpha>_def using x_range
        by (approximation 10 splitting: x=10)
      finally show ?thesis by simp
    qed
  next
    case c
    consider
      (1) "x < y" "y < 1/2" |
      (2) "y=1/2" "x < 1/2" |
      (3) "y=x" "x < 1/2" |
      (4) "x=1/2" "y =1/2"
      using assms(2,3) c  by fastforce
    thus ?thesis
    proof (cases)
      case 1
      define \<theta> :: real where "\<theta> = arcsin (6 / 10)"
      have "cos \<theta> = sqrt (1-0.6^2)"
        unfolding \<theta>_def by (intro cos_arcsin) auto
      also have "... = sqrt ( 0.8^2)"
        by (intro arg_cong[where f="sqrt"]) (simp add:power2_eq_square)
      also have "... = 0.8" by simp
      finally have cos_\<theta>: "cos \<theta> = 0.8" by simp
      have sin_\<theta>: "sin \<theta> = 0.6"
        unfolding \<theta>_def by simp

      have "\<phi> x y = \<alpha> + \<alpha>"
        unfolding \<phi>_def using c 1
        by (intro arg_cong2[where f="(+)"] \<gamma>'_cases) (auto simp add:frac_expand)
      moreover have "\<phi> y x = 1/\<alpha> + \<alpha>"
        unfolding \<phi>_def using c 1
        by (intro arg_cong2[where f="(+)"] \<gamma>'_cases) (auto simp add:frac_expand)
      ultimately have "?T = cos (pi * x) * (2 * \<alpha>) + cos (pi * y) * (\<alpha> + 1 / \<alpha>)"
        by simp
      also have "... \<le> cos (pi * (1/2-y)) * (2*\<alpha>) + cos (pi * y) * (\<alpha>+1 / \<alpha>)"
        unfolding \<alpha>_def using assms(1,2,3) c
        by (intro add_mono mult_right_mono order.refl iffD2[OF cos_mono_le_eq]) auto
      also have "... = (2.5*\<alpha>)* (sin (pi * y) * 0.8 + cos (pi * y) * 0.6)"
        unfolding sin_cos_eq \<alpha>_inv by (simp add:algebra_simps)
      also have "... = (2.5*\<alpha>)* sin(pi*y + \<theta>)"
        unfolding sin_add cos_\<theta> sin_\<theta>
        by (intro arg_cong2[where f="(*)"] arg_cong2[where f="(+)"] refl)
      also have "... \<le> (?R) * 1"
        unfolding \<alpha>_def by (intro mult_left_mono) auto
      finally show ?thesis by simp
    next
      case 2
      have x_range: "x > 0" "x < 1/2"
        using c 2 by auto
      have "\<phi> x y = \<alpha> + \<alpha>"
        unfolding \<phi>_def 2 using x_range
        by (intro arg_cong2[where f="(+)"] \<gamma>'_cases) (auto simp add:frac_expand)
      moreover have "\<phi> y x = 1 + 1"
        unfolding \<phi>_def 2 using x_range
        by (intro arg_cong2[where f="(+)"] \<gamma>'_cases) (auto simp add:frac_expand)
      ultimately have "?T = cos (pi * x) * (2*\<alpha>)"
        unfolding 2 by simp
      also have "... \<le> 1 * (2* sqrt 2)"
        unfolding \<alpha>_def by (intro mult_right_mono) auto
      also have "... \<le> ?R"
        by (approximation 5)
      finally show ?thesis by simp
    next
      case 3
      have x_range: "x \<in> {1/4..1/2}" using 3 c by simp
      hence cos_bound: "cos (pi * x) \<le> 0.71"
        by (approximation 10)
      have "\<phi> x y = 1+\<alpha>"
        unfolding \<phi>_def 3 using 3 c
        by (intro arg_cong2[where f="(+)"] \<gamma>'_cases) (auto simp add:frac_expand)
      moreover have "\<phi> y x = 1+\<alpha>"
        unfolding \<phi>_def 3 using 3 c
        by (intro arg_cong2[where f="(+)"] \<gamma>'_cases) (auto simp add:frac_expand)
      ultimately have "?T = 2 * cos (pi * x) * (1+\<alpha>)"
        unfolding 3 by simp
      also have "... \<le> 2 * 0.71 * (1+sqrt 2)"
        unfolding \<alpha>_def by (intro mult_right_mono mult_left_mono cos_bound) auto
      also have "... \<le> ?R"
        by (approximation 6)
      finally show ?thesis by simp
    next
      case 4
      show ?thesis  unfolding 4 by simp
    qed
  qed
  thus ?thesis using 0 by simp
qed

text \<open>Extend to square $[0, \frac{1}{2}] \times [0,\frac{1}{2}]$ using symmetry around x=y axis.\<close>

lemma fun_bound_real_2:
  assumes "x \<in> {0..1/2}" "y \<in> {0..1/2}" "(x,y) \<noteq> (0,0)"
  shows "\<bar>cos(pi*x)\<bar>*\<phi> x y + \<bar>cos(pi*y)\<bar>*\<phi> y x \<le> 2.5 * sqrt 2"  (is "?L \<le> ?R")
proof (cases "y < x")
  case True
  have "?L = \<bar>cos(pi*y)\<bar>*\<phi> y x + \<bar>cos(pi*x)\<bar>*\<phi> x y"
    by simp
  also have "... \<le> ?R"
    using True assms
    by (intro fun_bound_real_3)  auto
  finally show ?thesis by simp
next
  case False
  then show ?thesis using assms
    by (intro fun_bound_real_3) auto
qed

text \<open>Extend to $x > \frac{1}{2}$ using symmetry around $x=\frac{1}{2}$ axis.\<close>

lemma fun_bound_real_1:
  assumes "x \<in> {0..<1}" "y \<in> {0..1/2}" "(x,y) \<noteq> (0,0)"
  shows "\<bar>cos(pi*x)\<bar>*\<phi> x y + \<bar>cos(pi*y)\<bar>*\<phi> y x \<le> 2.5 * sqrt 2" (is "?L \<le> ?R")
proof (cases "x > 1/2")
  case True
  define x' where "x' = 1-x"

  have "\<bar>frac (x - 2 * y) - 1 / 2\<bar> = \<bar>frac (1 - x + 2 * y) - 1 / 2\<bar>"
  proof (cases "x - 2 * y \<in> \<int>")
    case True
    then obtain k where x_eq: "x = 2*y + of_int k" using Ints_cases[OF True]
      by (metis add_minus_cancel uminus_add_conv_diff)
    show ?thesis unfolding x_eq frac_def by simp
  next
    case False
    hence "1 - x + 2 * y \<notin> \<int>"
      using Ints_1 Ints_diff by fastforce
    thus ?thesis
      by (intro abs_rev_cong) (auto intro:frac_cong simp:one_minus_frac)
  qed

  moreover have "\<bar>frac (x + 2 * y) - 1 / 2\<bar> = \<bar>frac (1 - x - 2 * y) - 1 / 2\<bar>"
  proof (cases "x + 2 * y \<in> \<int>")
    case True
    then obtain k where x_eq: "x = of_int k - 2*y" using Ints_cases[OF True]
      by (metis add.right_neutral add_diff_eq cancel_comm_monoid_add_class.diff_cancel)
    show ?thesis unfolding x_eq frac_def by simp
  next
    case False
    hence "1 - x - 2 * y \<notin> \<int>"
      using Ints_1 Ints_diff by fastforce
    thus ?thesis
      by (intro abs_rev_cong) (auto intro:frac_cong simp:one_minus_frac)
  qed
  ultimately have "\<phi> y x = \<phi> y x'"
    unfolding \<phi>_def  x'_def by (intro \<gamma>'_cong add_swap_cong) simp_all

  moreover have "\<phi> x y = \<phi> x' y"
    unfolding \<phi>_def x'_def
    by (intro \<gamma>'_cong add_swap_cong refl arg_cong[where f="(\<lambda>x. abs (x-1/2))"] frac_cong)
     (simp_all add:algebra_simps)

  moreover have "\<bar>cos(pi*x)\<bar> = \<bar>cos(pi*x')\<bar>"
    unfolding x'_def by (intro abs_rev_cong) (simp add:algebra_simps)

  ultimately have "?L = \<bar>cos(pi*x')\<bar>*\<phi> x' y + \<bar>cos(pi*y)\<bar>*\<phi> y x'"
    by simp
  also have "... \<le> ?R"
    using assms True by (intro fun_bound_real_2) (auto simp add:x'_def)
  finally show ?thesis by simp
next
  case False
  thus ?thesis using assms fun_bound_real_2 by simp
qed

text \<open>Extend to $y > \frac{1}{2}$ using symmetry around $y=\frac{1}{2}$ axis.\<close>

lemma fun_bound_real:
  assumes "x \<in> {0..<1}" "y \<in> {0..<1}" "(x,y) \<noteq> (0,0)"
  shows "\<bar>cos(pi*x)\<bar>*\<phi> x y + \<bar>cos(pi*y)\<bar>*\<phi> y x \<le> 2.5 * sqrt 2"  (is "?L \<le> ?R")
proof (cases "y > 1/2")
  case True
  define y' where "y' = 1-y"

  have "\<bar>frac (y - 2 * x) - 1 / 2\<bar> = \<bar>frac (1 - y + 2 * x) - 1 / 2\<bar>"
  proof (cases "y - 2 * x \<in> \<int>")
    case True
    then obtain k where y_eq: "y = 2*x + of_int k" using Ints_cases[OF True]
      by (metis add_minus_cancel uminus_add_conv_diff)
    show ?thesis unfolding y_eq frac_def by simp
  next
    case False
    hence "1 - y + 2 * x \<notin> \<int>"
      using Ints_1 Ints_diff by fastforce
    thus ?thesis
      by (intro abs_rev_cong) (auto intro:frac_cong simp:one_minus_frac)
  qed

  moreover have "\<bar>frac (y + 2 * x) - 1 / 2\<bar> = \<bar>frac (1 - y - 2 * x) - 1 / 2\<bar>"
  proof (cases "y + 2 * x \<in> \<int>")
    case True
    then obtain k where y_eq: "y = of_int k - 2*x" using Ints_cases[OF True]
      by (metis add.right_neutral add_diff_eq cancel_comm_monoid_add_class.diff_cancel)
    show ?thesis unfolding y_eq frac_def by simp
  next
    case False
    hence "1 - y - 2 * x \<notin> \<int>"
      using Ints_1 Ints_diff by fastforce
    thus ?thesis
      by (intro abs_rev_cong) (auto intro:frac_cong simp:one_minus_frac)
  qed
  ultimately have "\<phi> x y = \<phi> x y'"
    unfolding \<phi>_def  y'_def  by (intro \<gamma>'_cong add_swap_cong) simp_all

  moreover have "\<phi> y x = \<phi> y' x"
    unfolding \<phi>_def y'_def
    by (intro \<gamma>'_cong add_swap_cong refl arg_cong[where f="(\<lambda>x. abs (x-1/2))"] frac_cong)
     (simp_all add:algebra_simps)

  moreover have "\<bar>cos(pi*y)\<bar> = \<bar>cos(pi*y')\<bar>"
    unfolding y'_def by (intro abs_rev_cong) (simp add:algebra_simps)

  ultimately have "?L = \<bar>cos(pi*x)\<bar>*\<phi> x y' + \<bar>cos(pi*y')\<bar>*\<phi> y' x"
    by simp
  also have "... \<le> ?R"
    using assms True by (intro fun_bound_real_1) (auto simp add:y'_def)
  finally show ?thesis by simp
next
  case False
  thus ?thesis using assms fun_bound_real_1 by simp
qed

lemma mod_to_frac:
  fixes x :: int
  shows "real_of_int (x mod m) = m * frac (x/m)" (is "?L = ?R")
proof -
  obtain y where y_def: "x mod m = x + int m* y"
    by (metis mod_eqE mod_mod_trivial)

  have 0: "x mod int m < m" "x mod int m \<ge> 0"
    using m_gt_0 by auto

  have "?L = real m * (of_int (x mod m) / m )"
    using m_gt_0 by (simp add:algebra_simps)
  also have "... = real m * frac (of_int (x mod m) / m)"
    using 0 by (subst iffD2[OF frac_eq]) auto
  also have "... = real m * frac (x / m + y)"
    unfolding y_def using m_gt_0 by (simp add:divide_simps mult.commute)
  also have "... = ?R"
    unfolding frac_def by simp
  finally show ?thesis by simp
qed

lemma fun_bound:
  assumes "v \<in> verts G" "v \<noteq> (0,0)"
  shows "\<tau>(fst v)*(\<gamma> v (S\<^sub>2 v)+\<gamma> v (T\<^sub>2 v))+\<tau>(snd v)*(\<gamma> v (S\<^sub>1 v)+\<gamma> v (T\<^sub>1 v)) \<le> 2.5 * sqrt 2"
    (is "?L \<le> ?R")
proof -
  obtain x y where v_def: "v = (x,y)" by (cases v) auto
  define x' where "x' = x/real m"
  define y' where "y' = y/real m"

  have 0:"\<gamma> v (S\<^sub>1 v) = \<gamma>' x' (frac(x'-2*y'))"
    unfolding \<gamma>_def \<gamma>'_def compare_def v_def \<gamma>_aux_def T\<^sub>1_def S\<^sub>1_def x'_def y'_def using m_gt_0
    by (intro if_cong_direct refl) (auto simp add:case_prod_beta mod_to_frac divide_simps)
  have 1:"\<gamma> v (T\<^sub>1 v) = \<gamma>' x' (frac(x'+2*y'))"
    unfolding \<gamma>_def \<gamma>'_def compare_def v_def \<gamma>_aux_def T\<^sub>1_def x'_def y'_def using m_gt_0
    by (intro if_cong_direct refl) (auto simp add:case_prod_beta mod_to_frac divide_simps)
  have 2:"\<gamma> v (S\<^sub>2 v) = \<gamma>' y' (frac(y'-2*x'))"
    unfolding \<gamma>_def \<gamma>'_def compare_def v_def \<gamma>_aux_def S\<^sub>2_def x'_def y'_def using m_gt_0
    by (intro if_cong_direct refl) (auto simp add:case_prod_beta mod_to_frac divide_simps)
  have 3:"\<gamma> v (T\<^sub>2 v) = \<gamma>' y' (frac(y'+2*x'))"
    unfolding \<gamma>_def \<gamma>'_def compare_def v_def \<gamma>_aux_def T\<^sub>2_def x'_def y'_def using m_gt_0
    by (intro if_cong_direct refl) (auto simp add:case_prod_beta mod_to_frac divide_simps)
  have 4: "\<tau> (fst v)  = \<bar>cos(pi*x')\<bar>" "\<tau> (snd v)  = \<bar>cos(pi*y')\<bar>"
    unfolding \<tau>_def v_def x'_def y'_def by auto

  have "x \<in> {0..<int m}" "y \<in> {0..<int m}" "(x,y) \<noteq> (0,0)"
    using assms  unfolding v_def mgg_graph_def by auto
  hence 5:"x' \<in> {0..<1}" "y' \<in> {0..<1}" "(x',y') \<noteq> (0,0)"
    unfolding x'_def y'_def by auto

  have "?L = \<bar>cos(pi*x')\<bar>*\<phi> x' y' + \<bar>cos(pi*y')\<bar>*\<phi> y' x'"
    unfolding 0 1 2 3 4 \<phi>_def by simp
  also have "... \<le> ?R"
    by (intro fun_bound_real 5)
  finally show ?thesis by simp
qed

text \<open>Equation 15 in Proof of Theorem 8.8\<close>

lemma hoory_8_8:
  fixes f :: "int \<times> int \<Rightarrow> real"
  assumes "\<And>x. f x \<ge> 0"
  assumes "f (0,0) = 0"
  assumes "periodic f"
  shows "g_inner f (\<lambda>x. f(S\<^sub>2 x)*\<tau> (fst x)+f(S\<^sub>1 x)*\<tau> (snd x))\<le>1.25* sqrt 2*g_norm f^2"
    (is "?L \<le> ?R")
proof -
  have 0: "2 * f x * f y \<le> \<gamma> x y * f x^2 + \<gamma> y x * f y^2" (is "?L1 \<le> ?R1") for x y
  proof -
    have "0 \<le> ((sqrt (\<gamma> x y) * f x) - (sqrt (\<gamma> y x) * f y))^2"
      by simp
    also have "... = ?R1 - 2 * (sqrt (\<gamma> x y) * f x) * (sqrt (\<gamma> y x) * f y)"
      unfolding power2_diff using \<gamma>_nonneg assms(1)
      by (intro arg_cong2[where f="(-)"] arg_cong2[where f="(+)"]) (auto simp add: power2_eq_square)
    also have "... = ?R1 -2 * sqrt (\<gamma> x y * \<gamma> y x) * f x * f y"
      unfolding real_sqrt_mult by simp
    also have "... = ?R1 - ?L1"
      unfolding \<gamma>_sym by simp
    finally have "0 \<le> ?R1 - ?L1" by simp
    thus ?thesis by simp
  qed

  have [simp]: "fst (S\<^sub>2 x) = fst x"  "snd (S\<^sub>1 x) = snd x" for x
    unfolding S\<^sub>1_def S\<^sub>2_def by auto

  have S_2_inv [simp]: "T\<^sub>2 (S\<^sub>2 x) = x" if "x \<in> verts G" for x
    using that unfolding T\<^sub>2_def S\<^sub>2_def mgg_graph_def
    by (cases x,simp add:mod_simps)
  have S_1_inv [simp]: "T\<^sub>1 (S\<^sub>1 x) = x" if "x \<in> verts G" for x
    using that unfolding T\<^sub>1_def S\<^sub>1_def mgg_graph_def
    by (cases x,simp add:mod_simps)

  have S2_inj: "inj_on S\<^sub>2 (verts G)"
    using S_2_inv by (intro inj_on_inverseI[where g="T\<^sub>2"])
  have S1_inj: "inj_on S\<^sub>1 (verts G)"
    using S_1_inv by (intro inj_on_inverseI[where g="T\<^sub>1"])

  have "S\<^sub>2 ` verts G \<subseteq> verts G"
    unfolding mgg_graph_def S\<^sub>2_def
    by (intro image_subsetI)  auto
  hence S2_ran: "S\<^sub>2 ` verts G = verts G"
    by (intro card_subset_eq card_image S2_inj) auto

  have "S\<^sub>1 ` verts G \<subseteq> verts G"
    unfolding mgg_graph_def S\<^sub>1_def
    by (intro image_subsetI)  auto
  hence S1_ran: "S\<^sub>1 ` verts G = verts G"
    by (intro card_subset_eq card_image S1_inj) auto

  have 2: "g v * f v^2 \<le> 2.5 * sqrt 2 * f v^2" if "g v \<le> 2.5 * sqrt 2 \<or> v = (0,0)" for v g
  proof (cases "v=(0,0)")
    case True
    then show ?thesis using assms(2) by simp
  next
    case False
    then show ?thesis using that by (intro mult_right_mono) auto
  qed

  have "2*?L=(\<Sum>v\<in>verts G. \<tau>(fst v)*(2*f v *f(S\<^sub>2 v)))+(\<Sum>v\<in>verts G. \<tau>(snd v) * (2 * f v * f (S\<^sub>1 v)))"
    unfolding g_inner_def by (simp add: algebra_simps sum_distrib_left sum.distrib)
  also have "... \<le>
    (\<Sum>v\<in>verts G. \<tau>(fst v)*(\<gamma> v (S\<^sub>2 v) * f v^2 + \<gamma> (S\<^sub>2 v) v * f(S\<^sub>2 v)^2))+
    (\<Sum>v\<in>verts G. \<tau>(snd v)*(\<gamma> v (S\<^sub>1 v) * f v^2 + \<gamma> (S\<^sub>1 v) v * f(S\<^sub>1 v)^2))"
    unfolding \<tau>_def by (intro add_mono sum_mono mult_left_mono 0) auto
  also have "... =
    (\<Sum>v\<in>verts G. \<tau>(fst v)*\<gamma> v (S\<^sub>2 v)*f v^2)+(\<Sum>v\<in>verts G. \<tau>(fst v) * \<gamma> (S\<^sub>2 v) v * f(S\<^sub>2 v)^2)+
    (\<Sum>v\<in>verts G. \<tau>(snd v)*\<gamma> v (S\<^sub>1 v)*f v^2)+(\<Sum>v\<in>verts G. \<tau>(snd v) * \<gamma> (S\<^sub>1 v) v * f(S\<^sub>1 v)^2)"
    by (simp add:sum.distrib algebra_simps)
  also have "... =
    (\<Sum>v\<in>verts G. \<tau>(fst v)*\<gamma> v (S\<^sub>2 v)*f v^2)+
    (\<Sum>v\<in>verts G. \<tau>(fst (S\<^sub>2 v)) * \<gamma> (S\<^sub>2 v) (T\<^sub>2 (S\<^sub>2 v)) * f(S\<^sub>2 v)^2)+
    (\<Sum>v\<in>verts G. \<tau>(snd v)*\<gamma> v (S\<^sub>1 v)*f v^2)+
    (\<Sum>v\<in>verts G. \<tau>(snd (S\<^sub>1 v)) * \<gamma> (S\<^sub>1 v) (T\<^sub>1 (S\<^sub>1 v)) * f(S\<^sub>1 v)^2)"
    by (intro arg_cong2[where f="(+)"] sum.cong refl) simp_all
  also have "... =
    (\<Sum>v\<in>verts G. \<tau>(fst v)*\<gamma> v (S\<^sub>2 v)*f v^2)+ (\<Sum>v\<in>S\<^sub>2 ` verts G. \<tau>(fst v) * \<gamma> v (T\<^sub>2 v) * f v^2)+
    (\<Sum>v\<in>verts G. \<tau>(snd v)*\<gamma> v (S\<^sub>1 v)*f v^2)+ (\<Sum>v\<in>S\<^sub>1 ` verts G. \<tau>(snd v) * \<gamma> v (T\<^sub>1 v) * f v^2)"
    using S1_inj S2_inj by (simp add:sum.reindex)
  also have "... =
    (\<Sum>v\<in>verts G. (\<tau>(fst v)*(\<gamma> v (S\<^sub>2 v)+\<gamma> v (T\<^sub>2 v))+\<tau>(snd v)*(\<gamma> v (S\<^sub>1 v)+\<gamma> v (T\<^sub>1 v))) *f v^2)"
    unfolding S1_ran S2_ran by (simp add:algebra_simps sum.distrib)
  also have "... \<le> (\<Sum>v\<in>verts G. 2.5 * sqrt 2 * f v^2)"
    using fun_bound by (intro sum_mono 2) auto
  also have "... \<le>  2.5 * sqrt 2 * g_norm f^2"
    unfolding g_norm_sq g_inner_def
    by (simp add:algebra_simps power2_eq_square sum_distrib_left)
  finally have "2 * ?L \<le> 2.5 * sqrt 2 * g_norm f^2" by simp
  thus ?thesis by simp
qed

lemma hoory_8_7:
  fixes f :: "int\<times>int \<Rightarrow> complex"
  assumes "f (0,0) = 0"
  assumes "periodic f"
  shows "norm(g_inner f (\<lambda>x. f (S\<^sub>2 x) * (1+\<omega>\<^sub>F (fst x)) + f (S\<^sub>1 x) * (1+\<omega>\<^sub>F (snd x))))
    \<le> (2.5 * sqrt 2) * (\<Sum>v \<in> verts G. norm (f v)^2)" (is "?L \<le> ?R")
proof -
  define g :: "int\<times>int \<Rightarrow> real" where "g x = norm (f x)" for x

  have g_zero: "g (0,0) = 0"
    using assms(1) unfolding g_def by simp
  have g_nonneg: "g x \<ge> 0" for x
    unfolding g_def by simp
  have g_periodic: "periodic g"
    unfolding g_def by (intro periodic_comp[OF assms(2)])

  have 0: "norm(1+\<omega>\<^sub>F x) = 2*\<tau> x" for x :: int
  proof -
    have "norm(1+\<omega>\<^sub>F x) = norm(\<omega>\<^sub>F (-x/2)*(\<omega>\<^sub>F 0 + \<omega>\<^sub>F x))"
      unfolding \<omega>\<^sub>F_def norm_mult by simp
    also have "... = norm (\<omega>\<^sub>F (0-x/2) + \<omega>\<^sub>F (x-x/2))"
      unfolding \<omega>\<^sub>F_simps by (simp add: algebra_simps)
    also have "... = norm (\<omega>\<^sub>F (x/2) + cnj (\<omega>\<^sub>F (x/2)))"
      unfolding \<omega>\<^sub>F_simps(3) by (simp add:algebra_simps)
    also have "... = \<bar>2*Re (\<omega>\<^sub>F (x/2))\<bar>"
      unfolding complex_add_cnj norm_of_real by simp
    also have "... =  2*\<bar>cos(pi*x/m)\<bar>"
      unfolding \<omega>\<^sub>F_def cis.simps by simp
    also have "... = 2*\<tau> x" unfolding \<tau>_def by simp
    finally show ?thesis by simp
  qed

  have "?L\<le>norm(\<Sum>v\<in>verts G. f v * cnj(f(S\<^sub>2 v)*(1+\<omega>\<^sub>F (fst v))+f(S\<^sub>1 v )*(1+\<omega>\<^sub>F (snd v))))"
    unfolding g_inner_def by (simp add:case_prod_beta)
  also have "...\<le>(\<Sum>v\<in>verts G. norm(f v * cnj(f (S\<^sub>2 v) *(1+\<omega>\<^sub>F (fst v))+f (S\<^sub>1 v)*(1+\<omega>\<^sub>F (snd v)))))"
    by (intro norm_sum)
  also have "...=(\<Sum>v\<in>verts G. g v * norm(f (S\<^sub>2 v) *(1+\<omega>\<^sub>F (fst v))+f (S\<^sub>1 v)*(1+\<omega>\<^sub>F (snd v))))"
    unfolding norm_mult g_def complex_mod_cnj by simp
  also have "...\<le>(\<Sum>v\<in>verts G. g v * (norm (f(S\<^sub>2 v)*(1+\<omega>\<^sub>F (fst v)))+norm(f(S\<^sub>1 v)*(1+\<omega>\<^sub>F(snd v)))))"
    by (intro sum_mono norm_triangle_ineq mult_left_mono g_nonneg)
  also have "...=2*g_inner g (\<lambda>x. g (S\<^sub>2 x)*\<tau> (fst x)+g(S\<^sub>1 x)*\<tau> (snd x))"
    unfolding g_def g_inner_def norm_mult 0
    by (simp add:sum_distrib_left algebra_simps case_prod_beta)
  also have "... \<le>2*(1.25* sqrt 2*g_norm g^2)"
    by (intro mult_left_mono hoory_8_8 g_nonneg g_zero g_periodic) auto
  also have "... = ?R"
    unfolding g_norm_sq g_def g_inner_def by (simp add:power2_eq_square)
  finally show ?thesis by simp
qed

lemma hoory_8_3:
  assumes "g_inner f (\<lambda>_. 1) = 0"
  assumes "periodic f"
  shows "\<bar>(\<Sum>(x,y)\<in>verts G. f(x,y)*(f(x+2*y,y)+f(x+2*y+1,y)+f(x,y+2*x)+f(x,y+2*x+1)))\<bar>
    \<le> (2.5 * sqrt 2) * g_norm f^2" (is "\<bar>?L\<bar> \<le> ?R")
proof -
  let ?f = "(\<lambda>x. complex_of_real (f x))"

  define Ts :: "(int \<times> int \<Rightarrow> int \<times> int) list" where
    "Ts = [(\<lambda>(x,y).(x+2*y,y)),(\<lambda>(x,y).(x+2*y+1,y)),(\<lambda>(x,y).(x,y+2*x)),(\<lambda>(x,y).(x,y+2*x+1))]"
  have p: "periodic ?f"
    by (intro periodic_comp[OF assms(2)])

  have 0: "(\<Sum>T\<leftarrow>Ts. FT (?f\<circ>T) v) = FT ?f (S\<^sub>2 v)*(1+\<omega>\<^sub>F (fst v))+FT ?f (S\<^sub>1 v)*(1+\<omega>\<^sub>F (snd v))"
    (is "?L1 = ?R1") for v :: "int \<times> int"
  proof -
    obtain x y where v_def: "v = (x,y)" by (cases v, auto)
    have "?L1 = (\<Sum>T\<leftarrow>Ts. FT (?f\<circ>T) (x,y))"
      unfolding v_def by simp
    also have "... = FT ?f (x,y-2*x)*(1+\<omega>\<^sub>F x) + FT ?f (x-2*y,y)*(1+\<omega>\<^sub>F y)"
      unfolding Ts_def by (simp add:FT_sheer[OF p] case_prod_beta comp_def) (simp add:algebra_simps)
    also have "... = ?R1"
      unfolding v_def S\<^sub>2_def S\<^sub>1_def
      by (intro arg_cong2[where f="(+)"] arg_cong2[where f="(*)"] periodic_cong[OF periodic_FT]) auto
    finally show ?thesis by simp
  qed

  have "cmod ((of_nat m)^2) = cmod (of_real (of_nat m^2))" by simp
  also have "... = abs (of_nat m^2)" by (intro norm_of_real)
  also have "... = real m^2" by simp
  finally have 1: "cmod ((of_nat m)\<^sup>2) = (real m)\<^sup>2" by simp

  have "FT (\<lambda>x. complex_of_real (f x)) (0, 0) = complex_of_real (g_inner f (\<lambda>_ . 1))"
    unfolding FT_def g_inner_def g_inner_def \<omega>\<^sub>F_def by simp
  also have "... = 0"
    unfolding assms by simp
  finally have 2: "FT (\<lambda>x. complex_of_real (f x)) (0, 0) = 0"
    by simp

  have "abs ?L = norm (complex_of_real ?L)"
    unfolding norm_of_real by simp
  also have "... = norm (\<Sum>T \<leftarrow> Ts. (g_inner ?f (?f \<circ> T)))"
    unfolding Ts_def by (simp add:algebra_simps g_inner_def  sum.distrib comp_def case_prod_beta)
  also have "... = norm (\<Sum>T \<leftarrow> Ts. (g_inner (FT ?f) (FT (?f \<circ> T)))/m^2)"
    by (subst parseval) simp
  also have "... = norm (g_inner (FT ?f) (\<lambda>x. (\<Sum>T \<leftarrow> Ts. (FT (?f \<circ> T) x)))/m^2)"
    unfolding Ts_def by (simp add:g_inner_simps case_prod_beta add_divide_distrib)
  also have "...=norm(g_inner(FT ?f)(\<lambda>x.(FT ?f(S\<^sub>2 x)*(1+\<omega>\<^sub>F (fst x))+FT f(S\<^sub>1 x)*(1+\<omega>\<^sub>F (snd x)))))/m^2"
    by (subst 0) (simp add:norm_divide 1)
  also have "... \<le> (2.5 * sqrt 2) * (\<Sum>v \<in> verts G. norm (FT f v)^2) / m^2"
    by (intro divide_right_mono hoory_8_7[where f="FT f"] 2 periodic_FT) auto
  also have "... = (2.5 * sqrt 2) * (\<Sum>v \<in> verts G. cmod (f v)^2)"
    by (subst (2) plancharel) simp
  also have "... = (2.5 * sqrt 2) * (g_inner f f)"
    unfolding g_inner_def norm_of_real by (simp add: power2_eq_square)
  also have "... = ?R"
    using g_norm_sq by auto
  finally show ?thesis by simp
qed

text \<open>Inequality stated before Theorem 8.3 in Hoory.\<close>

lemma mgg_numerical_radius_aux:
  assumes "g_inner f (\<lambda>_. 1) = 0"
  shows "\<bar>(\<Sum>a \<in> arcs G. f (head G a) * f (tail G a))\<bar> \<le> (5 * sqrt 2) * g_norm f^2"  (is "?L \<le> ?R")
proof -
  define g where "g x = f (fst x mod m, snd x mod m)" for x :: "int \<times> int"
  have 0:"g x = f x" if "x \<in> verts G" for x
    unfolding g_def using that
    by (auto simp add:mgg_graph_def mem_Times_iff)

  have g_mod_simps[simp]: "g (x, y mod m) = g (x, y)" "g (x mod m, y) = g (x, y)" for x y :: int
    unfolding g_def by auto

  have periodic_g: "periodic g"
    unfolding periodic_def by simp

  have "g_inner g (\<lambda>_. 1) = g_inner f (\<lambda>_. 1)"
    by (intro g_inner_cong 0) auto
  also have "... = 0"
    using assms by simp
  finally have 1:"g_inner g (\<lambda>_. 1) = 0" by simp

  have 2:"g_norm g = g_norm f"
    by (intro g_norm_cong 0) (auto)

  have "?L = \<bar>(\<Sum>a \<in> arcs G. g (head G a) * g (tail G a))\<bar>"
    using wellformed
    by (intro arg_cong[where f="abs"] sum.cong arg_cong2[where f="(*)"] 0[symmetric]) auto
  also have "...=\<bar>(\<Sum>a\<in>arcs_pos. g(head G a)*g(tail G a))+(\<Sum>a\<in>arcs_neg. g(head G a)*g(tail G a))\<bar>"
    unfolding arcs_sym arcs_pos_def arcs_neg_def
    by (intro arg_cong[where f="abs"] sum.union_disjoint) auto
  also have "... = \<bar>2 * (\<Sum>(v,l)\<in>verts G \<times> {..<4}. g v * g (mgg_graph_step m v (l, 1)))\<bar>"
    unfolding arcs_pos_def arcs_neg_def
    by (simp add:inj_on_def sum.reindex case_prod_beta mgg_graph_def algebra_simps)
  also have "... = 2 * \<bar>(\<Sum>v \<in> verts G. (\<Sum>l \<in> {..<4}. g v * g (mgg_graph_step m v (l, 1))))\<bar>"
    by (subst sum.cartesian_product)  (simp add:abs_mult)
  also have "... = 2*\<bar>(\<Sum>(x,y)\<in>verts G. (\<Sum>l\<leftarrow>[0..<4]. g(x,y)* g (mgg_graph_step m (x,y) (l,1))))\<bar>"
    by (subst interv_sum_list_conv_sum_set_nat)
      (auto simp add:atLeast0LessThan case_prod_beta simp del:mgg_graph_step.simps)
  also have "... =2*\<bar>\<Sum>(x,y)\<in>verts G. g (x,y)* (g(x+2*y,y)+g(x+2*y+1,y)+g(x,y+2*x)+g(x,y+2*x+1))\<bar>"
    by (simp add:case_prod_beta numeral_eq_Suc algebra_simps)
  also have "... \<le> 2* ((2.5 * sqrt 2) * g_norm g^2)"
    by (intro mult_left_mono hoory_8_3 1 periodic_g) auto
  also have "... \<le> ?R" unfolding 2 by simp
  finally show ?thesis by simp
qed

definition MGG_bound :: real
  where "MGG_bound = 5 * sqrt 2 / 8"

text \<open>Main result: Theorem 8.2 in Hoory.\<close>

lemma mgg_numerical_radius: "\<Lambda>\<^sub>a \<le> MGG_bound"
proof -
  have "\<Lambda>\<^sub>a \<le> (5 * sqrt 2)/real d"
    by (intro expander_intro mgg_numerical_radius_aux) auto
  also have "... = MGG_bound"
    unfolding MGG_bound_def d_eq_8 by simp
  finally show ?thesis by simp
qed

end

end

author: ekarayel


text:
(*  Title:      CCL/Lfp.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1992  University of Cambridge
*)

section {* The Knaster-Tarski Theorem *}

theory Lfp
imports Set
begin

definition
  lfp :: "['a set\<Rightarrow>'a set] \<Rightarrow> 'a set" where -- "least fixed point"
  "lfp(f) == Inter({u. f(u) <= u})"

(* lfp(f) is the greatest lower bound of {u. f(u) <= u} *)

lemma lfp_lowerbound: "f(A) <= A \<Longrightarrow> lfp(f) <= A"
  unfolding lfp_def by blast

lemma lfp_greatest: "(\<And>u. f(u) <= u \<Longrightarrow> A<=u) \<Longrightarrow> A <= lfp(f)"
  unfolding lfp_def by blast

lemma lfp_lemma2: "mono(f) \<Longrightarrow> f(lfp(f)) <= lfp(f)"
  by (rule lfp_greatest, rule subset_trans, drule monoD, rule lfp_lowerbound, assumption+)

lemma lfp_lemma3: "mono(f) \<Longrightarrow> lfp(f) <= f(lfp(f))"
  by (rule lfp_lowerbound, frule monoD, drule lfp_lemma2, assumption+)

lemma lfp_Tarski: "mono(f) \<Longrightarrow> lfp(f) = f(lfp(f))"
  by (rule equalityI lfp_lemma2 lfp_lemma3 | assumption)+

(*** General induction rule for least fixed points ***)

lemma induct:
  assumes lfp: "a: lfp(f)"
    and mono: "mono(f)"
    and indhyp: "\<And>x. \<lbrakk>x: f(lfp(f) Int {x. P(x)})\<rbrakk> \<Longrightarrow> P(x)"
  shows "P(a)"
  apply (rule_tac a = a in Int_lower2 [THEN subsetD, THEN CollectD])
  apply (rule lfp [THEN [2] lfp_lowerbound [THEN subsetD]])
  apply (rule Int_greatest, rule subset_trans, rule Int_lower1 [THEN mono [THEN monoD]],
    rule mono [THEN lfp_lemma2], rule CollectI [THEN subsetI], rule indhyp, assumption)
  done

(** Definition forms of lfp_Tarski and induct, to control unfolding **)

lemma def_lfp_Tarski: "\<lbrakk>h == lfp(f); mono(f)\<rbrakk> \<Longrightarrow> h = f(h)"
  apply unfold
  apply (drule lfp_Tarski)
  apply assumption
  done

lemma def_induct: "\<lbrakk>A == lfp(f);  a:A;  mono(f); \<And>x. x: f(A Int {x. P(x)}) \<Longrightarrow> P(x)\<rbrakk> \<Longrightarrow> P(a)"
  apply (rule induct [of concl: P a])
    apply simp
   apply assumption
  apply blast
  done

(*Monotonicity of lfp!*)
lemma lfp_mono: "\<lbrakk>mono(g); \<And>Z. f(Z) <= g(Z)\<rbrakk> \<Longrightarrow> lfp(f) <= lfp(g)"
  apply (rule lfp_lowerbound)
  apply (rule subset_trans)
   apply (erule meta_spec)
  apply (erule lfp_lemma2)
  done

end

repo: isabelle