Theory TheoryExe

section "Executable Signature and Theory"

(* Proofs are ugly, clean up if time *)

theory TheoryExe
  imports SortsExe Theory Instances
begin

datatype exesignature = ExeSignature 
  (execonst_type_of: "(name × typ) list")
  (exetyp_arity_of: "(name × nat) list")
  (exesorts: exeosig)

lemma exe_const_type_of_ok: "
  alist_conds cto ⟹
  (∀ty ∈ Map.ran (map_of cto) . typ_ok_sig (map_of cto, ta, sa) ty)
  ⟷ (∀ty ∈ snd ` set cto  . typ_ok_sig (map_of cto, ta, sa) ty)"
  by (simp add: ran_distinct)

fun exe_wf_sig where
  "exe_wf_sig (ExeSignature cto tao sa) = (exe_wf_osig sa ∧
  fst ` set (exetcsigs sa) = fst ` set tao 
  ∧ (∀type ∈ fst ` set (exetcsigs sa). 
    (∀ars ∈ snd ` set (the (lookup (λk. k=type) (exetcsigs sa))) .
      the (lookup (λk. k=type) tao) = length ars))
  ∧ (∀ty ∈ snd ` set cto . typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty))"

lemma exe_wf_sig_imp_wf_sig:
  assumes "alist_conds cto" "alist_conds tao" "exe_osig_conds sa" "(exe_wf_osig sa
  ∧ fst ` set (exetcsigs sa) = fst ` set tao 
  ∧ (∀type ∈ fst ` set (exetcsigs sa).  
      (∀ars ∈ snd ` set (the (lookup (λk. k=type) (exetcsigs sa))) .
      the (lookup (λk. k=type) tao) = length ars)))
  ∧ (∀ty ∈ snd ` set cto . typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)"
  shows "wf_sig (map_of cto, map_of tao, translate_osig sa)"
proof-
  {
    fix type y
    assume p: "exe_osig_conds sa" "trans (fst (translate_osig sa))" "snd (translate_osig sa) type = Some y"
      hence "exe_ars_conds (exetcsigs sa)"
        using exe_osig_conds_def by blast
    from p have "translate_ars (exetcsigs sa) type = Some y"
      by (metis snd_conv translate_osig.elims)
    hence "(type, y) ∈ set (map (apsnd map_of) (exetcsigs sa))"
      using map_of_SomeD by force
    hence "type ∈ fst ` set (exetcsigs sa)" by force
    from this obtain x where "lookup (λx. x=type) (exetcsigs sa) = Some x" 
      using key_present_imp_eq_lookup_finds_value by metis
    hence "map_of x = y"
      by (metis ‹exe_ars_conds (snd sa)› ‹translate_ars (snd sa) type = Some y› 
          exe_ars_conds_def in_alist_imp_in_map_of lookup_eq_map_of_ap 
          map_of_SomeD option.sel)
    have "∃y. (type, y) ∈ set tao"
      using ‹type ∈ fst ` set (exetcsigs sa)› assms(4) by auto
  }
  note 1 = this

  {
    fix ars type y
    assume p: "exe_osig_conds sa"
      "trans (fst (translate_osig sa))"
      "∀x∈set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) (snd x)"
      "ars ∈ ran y"
      "snd (translate_osig sa) type = Some y"

      hence "exe_ars_conds (exetcsigs sa)"
        using exe_osig_conds_def by blast
      from p(1-2) p(5) have "translate_ars (exetcsigs sa) type = Some y"
        by (metis snd_conv translate_osig.elims)
      hence "(type, y) ∈ set (map (apsnd map_of) (exetcsigs sa))"
        using map_of_SomeD by force
      hence dom: "type ∈ fst ` set (exetcsigs sa)" by force
      from this obtain x where x: "lookup (λx. x=type) (exetcsigs sa) = Some x" 
        using key_present_imp_eq_lookup_finds_value by metis
      hence "map_of x = y"
        by (metis ‹exe_ars_conds (snd sa)› ‹translate_ars (snd sa) type = Some y› 
            exe_ars_conds_def in_alist_imp_in_map_of lookup_eq_map_of_ap map_of_SomeD option.sel)
      have "ars ∈ snd ` set x"
        by (metis ‹map_of x = y› image_iff in_range_if_ex_key map_of_SomeD p(4) snd_conv)

      have "type ∈ fst ` set tao"
        apply (simp add: ‹type ∈ fst ` set (exetcsigs sa)› assms(4))
        using assms(4) dom  by blast
      moreover have 1: "(∀ars ∈ snd ` set (the (lookup (λk. k=type) (exetcsigs sa))) .
        the (lookup (λk. k=type) tao) = length ars)"
        using ‹type ∈ fst ` set (exetcsigs sa)› assms(4) by blast
      
      ultimately have "the (lookup (λk. k = type) tao) = length ars" 
        using ‹lookup (λx. x = type) (exetcsigs sa) = Some x› ‹map_of x = y› 
            in_range_if_ex_key map_of_SomeD option.sel p(3) snd_conv
        by (simp add: 1 ‹ars ∈ snd ` set x›)
      hence "the (map_of tao type) = length ars"
       by (metis ‹the (lookup (λk. k = type) tao) = length ars› lookup_eq_map_of_ap)
  }
  note 2 = this
  {
    fix a b x y
    assume p: "fst ` set b = fst ` set tao"
      "(x, y) ∈ set tao"
      "sa = (a, b)"

    have "x ∈ fst ` set b"
      by (metis fst_conv image_iff p(1) p(2))
    from this obtain ars where "lookup (λk. k=x) b = Some ars"
      by (metis key_present_imp_eq_lookup_finds_value)
    hence "(x,ars) ∈ set b"
      by (simp add: lookup_present_eq_key')
    hence "lookup (λk. k=x) (map (apsnd map_of) b) = Some (map_of ars)"
      by (metis assms(3) exe_ars_conds_def exe_osig_conds_def in_alist_imp_in_map_of
          lookup_eq_map_of_ap p(3) snd_conv translate_ars.simps)
    hence "∃y. map_of (map (apsnd map_of) b) x = Some y"
      by (metis lookup_eq_map_of_ap)
  }
  note 3 = this
  {
    fix a b x
    assume p: "alist_conds cto"
      "x ∈ ran (map_of cto)"
      "sa = (a, b)"
    have "typ_ok_sig (map_of cto, map_of tao, set a,  map_of (map (apsnd map_of) b)) x"
      using assms(4) p(1) p(2) p(3) ran_distinct by fastforce
  }
  note 4 = this
  have "wf_osig (translate_osig sa)"
    using assms(4) wf_osig_iff_exe_wf_osig by simp
  thus ?thesis apply (cases sa)
    using 1 2 3 4 assms by auto
qed

lemma wf_sig_imp_exe_wf_sig:
  assumes "alist_conds cto" "alist_conds tao" "exe_osig_conds sa"
    "wf_sig (map_of cto, map_of tao, translate_osig sa)" 
  shows "(exe_wf_osig sa
    ∧ fst ` set (exetcsigs sa) = fst ` set tao 
    ∧ (∀type ∈ fst ` set (exetcsigs sa). 
        (∀ars ∈ snd ` set (the (lookup (λk. k=type) (exetcsigs sa))) .
        the (lookup (λk. k=type) tao) = length ars)))
    ∧ (∀ty ∈ snd ` set cto . typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)"
proof-
  {
    fix a b x y
    assume p: "alist_conds tao"
      "exe_ars_conds b"
      "dom (map_of (map (apsnd map_of) b)) = dom (map_of tao)"
      "(x, y) ∈ set b"

    hence "x ∈ fst ` set tao"
      by (metis domIff dom_map_of_conv_image_fst exe_ars_conds_def 
          in_alist_imp_in_map_of option.distinct(1) translate_ars.simps)
  }
  note 1 = this
  {
    fix cl n ar and tcs :: "(String.literal × (String.literal × String.literal set list) list) list"
    assume p: "dom (map_of (map (apsnd map_of) tcs)) = dom (map_of tao)"
      "alist_conds tao"
      "(n, ar) ∈ set tao"
    
    obtain mgd where "translate_ars tcs n = Some mgd"
      using p by (metis Some_eq_map_of_iff domI domIff option.exhaust_sel translate_ars.simps)
    hence "map_of (map (apsnd map_of) tcs) n = Some mgd" 
      by (simp add: tcsigs_translate exe_osig_conds_def p)
    hence "n ∈ fst ` set (map (apsnd map_of) tcs)"
      by (meson domI domIff map_of_eq_None_iff)
    then have "n ∈ fst ` set tcs" 
      by force
  }
  note 2 = this
  {
    fix cl tcs n K c Ss 
    assume p: "(n, K) ∈ set tcs"
      "(c, Ss) ∈ set (the (lookup (λk. k = n) tcs))"
      "exe_ars_conds tcs"
      "dom (map_of (map (apsnd map_of) tcs)) = dom (map_of tao)"
      "∀type∈dom (map_of tao). ∀ars∈ran (the (map_of (map (apsnd map_of) tcs) type)).
          the (map_of tao type) = length ars"
    
    have 1: "translate_ars tcs n = Some (map_of K)"
      using exe_ars_conds_def in_alist_imp_in_map_of p(1-3) by blast
    have 2: "map_of K c = Some Ss"
      using p(1-3)
      by (metis Some_eq_map_of_iff exe_ars_conds_def image_iff lookup_eq_map_of_ap
          option.sel snd_conv)
    have "the (lookup (λk. k = n) tao) = length Ss"
      using 1 2 p(4,5)
      by (metis domIff lookup_eq_map_of_ap option.distinct(1) option.sel ranI translate_ars.simps)
  }
  note 3 = this

  have 1: "wf_osig (translate_osig sa)" "dom (tcsigs (translate_osig sa)) = dom (map_of tao)"
    "(∀type ∈ dom (tcsigs (translate_osig sa)). 
    (∀ars ∈ ran (the (tcsigs (translate_osig sa) type)) . the ((map_of tao) type) = length ars))"
    "(∀ty ∈ Map.ran (map_of cto) . wf_type (map_of cto, map_of tao, translate_osig sa) ty)"
    using assms(4) by auto
  note pre = 1
           
  have "exe_wf_osig sa"
    using "1"(1) wf_osig_iff_exe_wf_osig by blast
  moreover have "fst ` set (snd sa) = fst ` set tao"
  proof
    show "fst ` set (snd sa) ⊆ fst ` set tao"
      using assms(3-4)
      by (clarsimp simp add: dom_map_of_conv_image_fst exe_ars_conds_def exe_osig_conds_def)
        (metis tcsigs_translate assms(3) domIff in_alist_imp_in_map_of option.simps(3))
  next
    show "fst ` set (snd sa) ⊇ fst ` set tao" 
      using "1"(2) "2" assms(2-3) tcsigs_translate by auto
  qed
  moreover have "(∀type∈fst ` set (snd sa).  ∀ars∈snd ` set (the (lookup (λk. k = type) (snd sa))).
        the (lookup (λk. k = type) tao) = length ars)"
  proof (standard+, goal_cases)
    case (1 n Ss) 
    obtain c where c: "(c, Ss) ∈ set (the (lookup (λk. k = n) (snd sa)))"
      using "1"(2) by force
    have "dom (map_of (map (apsnd map_of) (snd sa))) = dom (map_of tao)"
      using assms(3) pre(2) tcsigs_translate by fastforce
    show ?case
      using assms(3) pre(2) c tcsigs_translate pre(2-3) domI 
      by (fastforce simp add: exe_osig_conds_def tcsigs_translate[OF assms(3)] 
          "1"(1) key_present_imp_eq_lookup_finds_value lookup_present_eq_key'
          split: option.splits intro!: 3[of _ "the (lookup (λk. k = n) (snd sa))" "snd sa" c])+
  qed
  moreover have "(∀ty ∈ Map.ran (map_of cto) . wf_type (map_of cto, map_of tao, translate_osig sa) ty)"
    using "1"(4) by blast
  ultimately show ?thesis 
    by (simp add: assms(1) ran_distinct)
qed

lemma wf_sig_iff_exe_wf_sig_pre: "alist_conds cto ⟹ alist_conds tao ⟹ exe_osig_conds sa
  ⟹ wf_sig (map_of cto, map_of tao, translate_osig sa) = (exe_wf_osig sa
  ∧ fst ` set (exetcsigs sa) = fst ` set tao  
  ∧ (∀type ∈ fst ` set (exetcsigs sa).
      (∀ars ∈ snd ` set (the (lookup (λk. k=type) (exetcsigs sa))) .
      the (lookup (λk. k=type) tao) = length ars))
  ∧ (∀ty ∈ snd ` set cto . typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty))"
  using exe_wf_sig_imp_wf_sig wf_sig_imp_exe_wf_sig by meson

lemma wf_sig_iff_exe_wf_sig: "alist_conds cto ⟹ alist_conds tao ⟹ exe_osig_conds sa
  ⟹ wf_sig (map_of cto, map_of tao, translate_osig sa)
  ⟷ exe_wf_sig (ExeSignature cto tao sa)"
  unfolding exe_wf_sig.simps
  using wf_sig_iff_exe_wf_sig_pre by presburger

fun translate_signature :: "exesignature ⇒ signature" where
  "translate_signature (ExeSignature cto tao sa) 
    = (map_of cto, map_of tao, translate_osig sa)"

fun exetyp_ok_sig :: "exesignature ⇒ typ ⇒ bool" where
  "exetyp_ok_sig Σ (Ty c Ts) = (case lookup (λk. k=c) (exetyp_arity_of Σ) of
    None ⇒ False
  | Some ar ⇒ length Ts = ar ∧ list_all (exetyp_ok_sig Σ) Ts)"
| "exetyp_ok_sig Σ (Tv _ S) = exewf_sort (execlasses (exesorts Σ)) S"

thm exewf_sort_def
definition [simp]: "exesort_ok_sig Σ S ≡ exesort_ex (execlasses (exesorts Σ)) S 
  ∧ exenormalized_sort (execlasses (exesorts Σ)) S"

lemma typ_arity_lookup_code: "type_arity (translate_signature Σ) n = lookup (λk. k = n) (exetyp_arity_of Σ)"
  by (cases Σ) (simp add: lookup_eq_map_of_ap)

lemma typ_ok_sig_code: 
  assumes "exe_osig_conds (exesorts Σ)"
  shows "typ_ok_sig (translate_signature Σ) ty = exetyp_ok_sig Σ ty"
  using assms apply (induction ty) apply simp
  apply (auto split: option.splits simp add: wf_sort_def list_all_iff typ_arity_lookup_code)[]
  using wf_sort_code by (cases Σ) (simp add: exe_osig_conds_def classes_translate)

fun exe_wf_sig' where
  "exe_wf_sig' (ExeSignature cto tao sa) = (exe_wf_osig sa ∧
  fst ` set (exetcsigs sa) = fst ` set tao 
  ∧ (∀type ∈ fst ` set (exetcsigs sa). 
    (∀ars ∈ snd ` set (the (lookup (λk. k=type) (exetcsigs sa))) .
      the (lookup (λk. k=type) tao) = length ars))
  ∧ (∀ty ∈ snd ` set cto . exetyp_ok_sig (ExeSignature cto tao sa) ty))"

lemma exe_wf_sig_code[code]: "exe_wf_sig Σ = exe_wf_sig' Σ"
  using typ_ok_sig_code by (cases Σ, simp, metis exesignature.sel(3) translate_signature.simps)

fun exeterm_ok' :: "exesignature ⇒ term ⇒ bool" where
  "exeterm_ok' Σ (Fv _ T) = exetyp_ok_sig Σ T"
| "exeterm_ok' Σ (Bv _) = True"
| "exeterm_ok' Σ (Ct s T) = (case lookup (λk. k=s) (execonst_type_of Σ) of
    None ⇒ False
  | Some ty ⇒ exetyp_ok_sig Σ T ∧ tinstT T ty)"
| "exeterm_ok' Σ (t $ u) ⟷ exeterm_ok' Σ t ∧ exeterm_ok' Σ u" 
| "exeterm_ok' Σ (Abs T t) ⟷ exetyp_ok_sig Σ T ∧ exeterm_ok' Σ t"

lemma const_type_of_lookup_code: "const_type (translate_signature Σ) n = lookup (λk. k = n) (execonst_type_of Σ)"
  by (cases Σ) (simp add: lookup_eq_map_of_ap)

lemma wt_term_code: 
  assumes "exe_osig_conds (exesorts Σ)"
  shows "term_ok' (translate_signature Σ) t = exeterm_ok' Σ t"
  by (induction t) (auto simp add: const_type_of_lookup_code assms typ_ok_sig_code split: option.splits)

datatype exetheory = ExeTheory (exesig: exesignature) (exeaxioms_of: "term list")

lemma exetheory_full_exhaust: "(⋀const_type typ_arity sorts axioms. 
    Θ = (ExeTheory (ExeSignature const_type typ_arity sorts) axioms) ⟹ P)
  ⟹ P"
  apply (cases Θ) subgoal for Σ axioms apply (cases Σ) by auto done

definition "exe_sig_conds Σ ≡ alist_conds (execonst_type_of Σ) ∧ alist_conds (exetyp_arity_of Σ) 
  ∧ exe_osig_conds (exesorts Σ)"

abbreviation "illformed_theory ≡  ((Map.empty, Map.empty, illformed_osig), {})"

lemma illformed_theory_not_wf_theory: "¬ wf_theory illformed_theory" 
  by simp

fun translate_theory :: "exetheory ⇒ theory" where
  "translate_theory (ExeTheory Σ ax) = (if exe_sig_conds Σ then 
    (translate_signature Σ, set ax) else illformed_theory)"

fun exe_wf_theory where "exe_wf_theory (ExeTheory (ExeSignature cto tao sa) ax) ⟷
  exe_sig_conds (ExeSignature cto tao sa) ∧
    (∀p ∈ set ax . term_ok (translate_theory (ExeTheory (ExeSignature cto tao sa) ax)) p ∧ typ_of p = Some propT)
  ∧ is_std_sig (translate_signature (ExeSignature cto tao sa))
  ∧ exe_wf_sig (ExeSignature cto tao sa)
  ∧ eq_axs ⊆ set ax"

lemma wf_sig_iff_exe_wf_sig': "exe_sig_conds Σ ⟹
    wf_sig (translate_signature Σ) ⟷
    exe_wf_sig Σ" 
  by (metis exe_sig_conds_def exesignature.exhaust_sel wf_sig_iff_exe_wf_sig translate_signature.simps)

lemma wf_sig_imp_exe_wf_sig': "exe_sig_conds Σ ⟹
    wf_sig (translate_signature Σ) ⟹
    exe_wf_sig Σ" 
  by (metis exe_sig_conds_def exesignature.exhaust_sel wf_sig_iff_exe_wf_sig translate_signature.simps)

lemma exe_wf_sig_imp_wf_sig': "exe_sig_conds Σ ⟹
    exe_wf_sig Σ
    ⟹ wf_sig (translate_signature Σ)" 
  by (metis exe_sig_conds_def exesignature.exhaust_sel wf_sig_iff_exe_wf_sig translate_signature.simps)

lemma wf_theory_translate_imp_exe_wf_theory:
  assumes "wf_theory (translate_theory a)" shows "exe_wf_theory a" 
proof-
  have "exe_sig_conds (exesig a)" using assms
    by (metis exetheory.collapse illformed_theory_not_wf_theory translate_theory.simps)
  moreover have "wf_sig (translate_signature (exesig a))
    ⟷ exe_wf_sig (exesig a)"
    by (simp add: calculation(1) wf_sig_iff_exe_wf_sig')
  ultimately show ?thesis using assms
    by (cases a rule: exe_wf_theory.cases) (fastforce simp add: image_iff eq_fst_iff)
qed

lemma exe_wf_theory_translate_imp_wf_theory:
  assumes "exe_wf_theory a" shows "wf_theory (translate_theory a)"
proof-
  have "exe_sig_conds (exesig a)" using assms
    by (metis (full_types) exe_wf_theory.simps exesignature.exhaust_sel exetheory.sel(1) translate_theory.cases)
  moreover hence "
  (∀ty ∈ Map.ran (map_of (execonst_type_of (exesig a))) . typ_ok_sig (translate_signature (exesig a)) ty)
  ⟷ (∀ty ∈ snd ` set (execonst_type_of (exesig a)) . typ_ok_sig (translate_signature (exesig a)) ty)"
    by (simp add: exe_sig_conds_def ran_distinct)
  moreover have "wf_sig (translate_signature (exesig a))
    ⟷ exe_wf_sig (exesig a)"
    by (simp add: calculation(1) wf_sig_iff_exe_wf_sig')
  ultimately show ?thesis
    using assms by (cases a rule: exe_wf_theory.cases) auto 
qed

lemma wf_theory_translate_iff_exe_wf_theory:
  "wf_theory (translate_theory a) ⟷ exe_wf_theory a"
  using exe_wf_theory_translate_imp_wf_theory wf_theory_translate_imp_exe_wf_theory by blast

fun exeis_std_sig where "exeis_std_sig (ExeSignature cto tao sorts) ⟷
    lookup (λk. k = STR ''fun'') tao = Some 2 ∧ lookup (λk. k = STR ''prop'') tao  = Some 0 
  ∧ lookup (λk. k = STR ''itself'') tao = Some 1
  ∧ lookup (λk. k = STR ''Pure.eq'') cto 
    = Some ((Tv (Var (STR '''a'', 0)) full_sort) → ((Tv (Var (STR '''a'', 0)) full_sort) → propT))
  ∧ lookup (λk. k = STR ''Pure.all'') cto = Some ((Tv (Var  (STR '''a'', 0)) full_sort → propT) → propT)
  ∧ lookup (λk. k = STR ''Pure.imp'') cto = Some (propT → (propT → propT))
  ∧ lookup (λk. k = STR ''Pure.type'') cto = Some (itselfT (Tv (Var (STR '''a'', 0)) full_sort))"

lemma is_std_sig_code: "is_std_sig (translate_signature Σ) = exeis_std_sig Σ"
  by (cases Σ) (auto simp add: lookup_eq_map_of_ap)

fun exe_wf_theory' where "exe_wf_theory' (ExeTheory (ExeSignature cto tao sa) ax) ⟷
  exe_sig_conds (ExeSignature cto tao sa) ∧
    (∀p ∈ set ax . exeterm_ok' (ExeSignature cto tao sa) p ∧ typ_of p = Some propT)
  ∧ exeis_std_sig (ExeSignature cto tao sa)
  ∧ exe_wf_sig (ExeSignature cto tao sa)
  ∧ eq_axs ⊆ set ax"

lemma term_ok'_code: 
  assumes "exe_osig_conds (exesorts (ExeSignature cto tao sa))"
  shows "(term_ok' (translate_signature (ExeSignature cto tao sa)) p ∧ typ_of p = Some propT)
    = (exeterm_ok' (ExeSignature cto tao sa) p ∧ typ_of p = Some propT)"
  using wt_term_code[OF assms] by force

lemma term_ok_translate_code_step:
  assumes "exe_sig_conds (ExeSignature cto tao sa)"
  shows "(term_ok (translate_theory (ExeTheory (ExeSignature cto tao sa) ax)) p ∧ typ_of p = Some propT)
    = (term_ok' (translate_signature (ExeSignature cto tao sa)) p ∧ typ_of p = Some propT)"
  using assms by (auto simp add: wt_term_def split: if_splits)
  
lemma term_ok_theory_cond_code:
  assumes "exe_sig_conds (ExeSignature cto tao sa)"
  shows"(∀p ∈ set ax . term_ok (translate_theory (ExeTheory (ExeSignature cto tao sa) ax)) p ∧ typ_of p = Some propT)
    = (∀p ∈ set ax . exeterm_ok' (ExeSignature cto tao sa) p ∧ typ_of p = Some propT)"
  using assms wf_term_imp_term_ok' exe_sig_conds_def wt_term_code
  by (fastforce simp add: term_ok_translate_code_step wt_term_code wt_term_def)
  
lemma exe_wf_theory_code[code]: "exe_wf_theory Θ = exe_wf_theory' Θ"
  apply (cases Θ rule: exetheory_full_exhaust)
  apply (simp only: exe_wf_theory.simps exe_wf_theory'.simps)
  using term_ok_theory_cond_code is_std_sig_code by meson

end