Theory NU_Computable

(*<*)
theory NU_Computable
  imports NU_Completeness
begin
(*>*)
section ‹The Computable Algorithm›

text‹Option-typed version of ‹sred_fun›.›

function sred_fun :: "(problem_type × fresh_envs × substs) ⇒ (problem_type × fresh_envs × substs) option" where
"sred_fun (([], ys), nabla, s) = Some (([], ys), nabla, s)" |
"sred_fun (((t1 ≈? t2) # xs, ys), nabla, s) =
  (case t1 of
    Unit ⇒ (case t2 of
               Unit ⇒ sred_fun ((xs, ys), nabla, s)
             | Susp pi X ⇒ sred_fun (apply_subst [(X, swap (rev pi) Unit)] (xs, ys),
                                              nabla, [(X, swap (rev pi) Unit)] ∙ s)
             | _ ⇒ None)
   | Paar u1 u2 ⇒ (case t2 of
                      Paar v1 v2 ⇒ sred_fun (((u1 ≈? v1) # (u2 ≈? v2) # xs, ys), nabla, s)
                    | Susp pi X ⇒
                        if ¬ occurs X (Paar u1 u2)
                        then sred_fun (apply_subst [(X, swap (rev pi) (Paar u1 u2))] (xs, ys),
                                            nabla, [(X, swap (rev pi) (Paar u1 u2))] ∙ s)
                        else None
                    | _ ⇒ None)
   | Func F u ⇒ (case t2 of
                     Func G v ⇒ if F = G
                                  then sred_fun (((u ≈? v) # xs, ys), nabla, s)
                                  else None
                   | Susp pi X ⇒
                       if ¬ occurs X (Func F u)
                       then sred_fun (apply_subst [(X, swap (rev pi) (Func F u))] (xs, ys),
                                           nabla, [(X, swap (rev pi) (Func F u))] ∙ s)
                       else None
                   | _ ⇒ None)
   | Abst a u ⇒ (case t2 of
                    Abst b v ⇒ if a = b
                                 then sred_fun (((u ≈? v) # xs, ys), nabla, s)
                                 else sred_fun (((u ≈? swap [(a, b)] v) # xs, (a ♯? v) # ys), nabla, s)
                  | Susp pi X ⇒
                      if ¬ occurs X (Abst a u)
                      then sred_fun (apply_subst [(X, swap (rev pi) (Abst a u))] (xs, ys),
                                          nabla, [(X, swap (rev pi) (Abst a u))] ∙ s)
                      else None
                  | _ ⇒ None)
   | Atom a ⇒ (case t2 of
                  Atom b ⇒ if a = b then sred_fun ((xs, ys), nabla, s) else None
                | Susp pi X ⇒ sred_fun (apply_subst [(X, swap (rev pi) (Atom a))] (xs, ys),
                                                nabla, [(X, swap (rev pi) (Atom a))] ∙ s)
                | _ ⇒ None)
   | Susp pi X ⇒ (case t2 of
                     Unit ⇒ sred_fun (apply_subst [(X, swap (rev pi) Unit)] (xs, ys),
                                            nabla, [(X, swap (rev pi) Unit)] ∙ s)
                   | Atom a ⇒ sred_fun (apply_subst [(X, swap (rev pi) (Atom a))] (xs, ys),
                                              nabla, [(X, swap (rev pi) (Atom a))] ∙ s)
                   | Paar v1 v2 ⇒
                       if ¬ occurs X (Paar v1 v2)
                       then sred_fun (apply_subst [(X, swap (rev pi) (Paar v1 v2))] (xs, ys),
                                           nabla, [(X, swap (rev pi) (Paar v1 v2))] ∙ s)
                       else None
                   | Func G v ⇒
                       if ¬ occurs X (Func G v)
                       then sred_fun (apply_subst [(X, swap (rev pi) (Func G v))] (xs, ys),
                                           nabla, [(X, swap (rev pi) (Func G v))] ∙ s)
                       else None
                   | Abst a v ⇒
                       if ¬ occurs X (Abst a v)
                       then sred_fun (apply_subst [(X, swap (rev pi) (Abst a v))] (xs, ys),
                                           nabla, [(X, swap (rev pi) (Abst a v))] ∙ s)
                       else None
                   | Susp pi2 Y ⇒
                       if X = Y
                       then sred_fun ((xs, map (λa. a ♯? Susp [] X) (ds_list pi pi2) @ ys), nabla, s)
                       else sred_fun (apply_subst [(X, swap (rev pi) (Susp pi2 Y))] (xs, ys),
                                           nabla, [(X, swap (rev pi) (Susp pi2 Y))] ∙ s)))"
by pat_completeness auto

text‹‹sred_fun› terminates because every recursive call performs an ‹s_red› step on
the problem component, so ‹rank_r› decreases on it.›

termination sred_fun
  by (relation "inv_image rank_r fst")
     (auto simp: wf_rank_r simp del: swap.simps intro!: rank_r_sred)

function  cred_fun :: "(problem_type × fresh_envs × substs) ⇒ (problem_type × fresh_envs × substs) option"
  where
"cred_fun ((xs, (a ♯? Unit)#ys), nabla, s) = cred_fun ((xs, ys), nabla, s)" |
"cred_fun ((xs, (a ♯? Paar t1 t2)#ys), nabla, s) = cred_fun ((xs, (a♯?t1)#(a♯?t2)#ys), nabla, s)" |
"cred_fun ((xs, (a ♯? Func F t)#ys), nabla, s) = cred_fun ((xs, (a♯?t)#ys), nabla, s)" |
"cred_fun ((xs, (a ♯? Abst b t)#ys), nabla, s) = (if a = b then
                                                      cred_fun ((xs, ys), nabla, s)
                                                    else
                                                      cred_fun ((xs, (a♯?t)#ys), nabla, s))" |
"cred_fun ((xs, (a ♯? Atom b)#ys), nabla, s) = (if a = b then
                                                  None
                                                else
                                                  cred_fun ((xs, ys), nabla, s))" |
"cred_fun ((xs, (a ♯? Susp pi X)#ys), nabla, s) = cred_fun ((xs, ys), {((swapas (rev pi) a),X)}∪nabla, s)" |
"cred_fun ((xs, []), nabla, s) = Some ((xs, []), nabla, s)"
  by pat_completeness auto

termination cred_fun
  by (relation "measure (λ((xs, ys), nabla, s). size_fprobs ys)", auto)

text‹Combines ‹sred_fun›  and ‹cred_fun›, mirroring the ‹red_plus› relation: equations are solved first, then freshness constraints.›

fun red_plus_fun :: "(problem_type × fresh_envs × substs) ⇒ (problem_type × fresh_envs × substs) option" where
"red_plus_fun (P, nabla, s) = (case sred_fun (P, nabla, s) of
                                 Some ((xs, ys), nabla', s') ⇒ cred_fun ((xs,ys), nabla', s')
                               | None ⇒ None)"

fun nomu_unify :: "problem_type ⇒ (fresh_envs × substs) option" where
  "nomu_unify P = (case red_plus_fun (P, {}, []) of 
                    Some (_, nabla', s') ⇒ Some (nabla', s')
                    | None ⇒ None)"

text‹In generated SML code, equality on booleans is the native one.›

code_printing constant "HOL.equal :: bool ⇒ bool ⇒ bool" ⇀ (SML) "!((_ : bool) = _)"

text‹Whenever ‹cred_fun› succeeds, the snd (freshness) list of the resulting problem is empty:
all freshness problems have been solved.›

lemma cred_fun_some_snd_empty:
  assumes "cred_fun (P, nabla, s) = Some (P', nabla', s')"
  shows "snd P' = []"
  using assms by (induct "(P, nabla, s)" arbitrary: P nabla s P' nabla' s' rule: cred_fun.induct, auto split: if_splits)


(*<*)
end
(*>*)