Theory TTreeImplCardinality

theory TTreeImplCardinality
imports TTreeAnalysisSig CardinalityAnalysisSig "Cardinality-Domain-Lists"
begin

hide_const Multiset.single

context TTreeAnalysis
begin

fun unstack :: "stack ⇒ exp ⇒ exp" where
  "unstack [] e = e"
| "unstack (Alts e1 e2 # S) e = unstack S e"
| "unstack (Upd x # S) e = unstack S e"
| "unstack (Arg x # S) e = unstack S (App e x)"
| "unstack (Dummy x # S) e = unstack S e"

fun Fstack :: "Arity list ⇒ stack ⇒ var ttree"
  where "Fstack _ [] = ⊥"
  | "Fstack (a#as) (Alts e1 e2 # S) = (Texp e1⋅a ⊕⊕ Texp e2⋅a) ⊗⊗ Fstack as S"
  | "Fstack as (Arg x # S) = many_calls x ⊗⊗ Fstack as S"
  | "Fstack as (_ # S) = Fstack as S"



(*
lemma carrier_Fstack[simp]: "carrier (Fstack S) = ap S"
  by (induction S rule: Fstack.induct) (auto simp add: empty_is_bottom[symmetric])
*)

fun prognosis :: "AEnv ⇒ Arity list ⇒ Arity ⇒ conf ⇒ var ⇒ two"
   where "prognosis ae as a (Γ, e, S) = pathsCard (paths (substitute (FBinds Γ⋅ae) (thunks Γ) (Texp e⋅a ⊗⊗ Fstack as S)))"
end

end