CPSUtils.thy

section  ‹Syntax tree helpers›

theory CPSUtils
imports CPSScheme
begin

text ‹
  theory defines the sets ‹lambdas p›, ‹calls p›, ‹calls p›, ‹vars p›, ‹labels p› and ‹prims p› as the subexpressions of the program ‹p›. Finiteness is shown for each of these sets, and some rules about how these sets relate. All these rules are proven more or less the same ways, which is very inelegant due to the nesting of the type and the shape of the derived induction rule.

  would be much nicer to start with these rules and define the set inductively. Unfortunately, that approach would make it very hard to show the finiteness of the sets in question.
 ›


fun lambdas :: "lambda ==> lambda set"
and lambdasC :: "call ==> lambda set"
and lambdasV :: "val ==> lambda set"
where "lambdas (Lambda l vs c) = ({Lambda l vs c} ∪ lambdasC c)"
    | "lambdasC (App l d ds) = lambdasV d ∪ ∪ (lambdasV ` set ds)"
    | "lambdasC (Let l binds c') = (∪(_, y)∈set binds. lambdas y) ∪ lambdasC c'"
    | "lambdasV (L l) = lambdas l"
    | "lambdasV _ = {}"

fun calls :: "lambda ==> call set"
and callsC :: "call ==> call set"
and callsV :: "val ==> call set"
where "calls (Lambda l vs c) = callsC c"
    | "callsC (App l d ds) = {App l d ds} ∪ callsV d ∪ (∪(callsV ` (set ds)))"
    | "callsC (Let l binds c') = {call.Let l binds c'} ∪ ((∪(_, y)∈set binds. calls y) ∪ callsC c')"
    | "callsV (L l) = calls l"
    | "callsV _ = {}"

lemma finite_lambdas[simp]: "finite (lambdas l)" and "finite (lambdasC c)" "finite (lambdasV v)"
by (induct rule: lambdas_lambdasC_lambdasV.induct, auto)

lemma finite_calls[simp]: "finite (calls l)" and "finite (callsC c)" "finite (callsV v)"
by (induct rule: calls_callsC_callsV.induct, auto)

fun vars :: "lambda ==> var set"
and varsC :: "call ==> var set"
and varsV :: "val ==> var set"
where "vars (Lambda _ vs c) = set vs ∪ varsC c"
    | "varsC (App _ a as) = varsV a ∪ ∪(varsV ` (set as))"
    | "varsC (Let _ binds c') = (∪(v, l)∈set binds. {v} ∪ vars l) ∪ varsC c'"
    | "varsV (L l) = vars l"
    | "varsV (R _ v) = {v}"
    | "varsV _ = {}"

lemma finite_vars[simp]: "finite (vars l)" and "finite (varsC c)" "finite (varsV v)"
by (induct rule: vars_varsC_varsV.induct, auto)

fun label :: "lambda + call ==> label"
where "label (Inl (Lambda l _ _)) = l"
    | "label (Inr (App l _ _)) = l"
    | "label (Inr (Let l _ _)) = l"

fun labels :: "lambda ==> label set"
and labelsC :: "call ==> label set"
and labelsV :: "val ==> label set"
where "labels (Lambda l vs c) = {l} ∪ labelsC c"
    | "labelsC (App l a as) = {l} ∪ labelsV a ∪ ∪(labelsV ` (set as))"
    | "labelsC (Let l binds c') = {l} ∪ (∪(v, y)∈set binds. labels y) ∪ labelsC c'"
    | "labelsV (L l) = labels l"
    | "labelsV (R l _) = {l}"
    | "labelsV _ = {}"

lemma finite_labels[simp]: "finite (labels l)" and "finite (labelsC c)" "finite (labelsV v)"
by (induct rule: labels_labelsC_labelsV.induct, auto)

fun prims :: "lambda ==> prim set"
and primsC :: "call ==> prim set"
and primsV :: "val ==> prim set"
where "prims (Lambda _ vs c) = primsC c"
    | "primsC (App _ a as) = primsV a ∪ ∪(primsV ` (set as))"
    | "primsC (Let _ binds c') = (∪(_, y)∈set binds. prims y) ∪ primsC c'"
    | "primsV (L l) = prims l"
    | "primsV (R l v) = {}"
    | "primsV (P prim) = {prim}"
    | "primsV (C l v) = {}"

lemma finite_prims[simp]: "finite (prims l)" and "finite (primsC c)" "finite (primsV v)"
by (induct rule: labels_labelsC_labelsV.induct, auto)

fun vals :: "lambda ==> val set"
and valsC :: "call ==> val set"
and valsV :: "val ==> val set"
where "vals (Lambda _ vs c) = valsC c"
    | "valsC (App _ a as) = valsV a ∪ ∪(valsV ` (set as))"
    | "valsC (Let _ binds c') = (∪(_, y)∈set binds. vals y) ∪ valsC c'"
    | "valsV (L l) = {L l} ∪ vals l"
    | "valsV (R l v) = {R l v}"
    | "valsV (P prim) = {P prim}"
    | "valsV (C l v) = {C l v}"

lemma
  fixes list2 :: "(var × lambda) list" and t :: "var×lambda"
  shows lambdas1: "Lambda l vs c ∈ lambdas x ==> c ∈ calls x"
  and "Lambda l vs c ∈ lambdasC y ==> c ∈ callsC y"
  and "Lambda l vs c ∈ lambdasV z ==> c ∈ callsV z"
  and "∀z∈ set list. Lambda l vs c ∈ lambdasV z ⟶ c ∈ callsV z"
  and "∀x∈ set list2. Lambda l vs c ∈ lambdas (snd x) ⟶ c ∈ calls (snd x)"
  and "Lambda l vs c ∈ lambdas (snd t) ==> c ∈ calls (snd t)"
apply (induct rule:mutual_lambda_call_var_inducts)
apply auto
apply (case_tac c, auto)[1]
apply (rule_tac x="((a, b), ba)" in bexI, auto)
done

lemma 
  shows lambdas2: "Lambda l vs c ∈ lambdas x ==> l ∈ labels x"
  and "Lambda l vs c ∈ lambdasC y ==> l ∈ labelsC y"
  and "Lambda l vs c ∈ lambdasV z ==> l ∈ labelsV z"
  and "∀z∈ set list. Lambda l vs c ∈ lambdasV z ⟶ l ∈ labelsV z"
  and "∀x∈ set (list2 :: (var × lambda) list) . Lambda l vs c ∈ lambdas (snd x) ⟶ l ∈ labels (snd x)"
  and "Lambda l vs c ∈ lambdas (snd (t:: var×lambda)) ==> l ∈ labels (snd t)"
apply (induct rule:mutual_lambda_call_var_inducts)
apply auto
apply (rule_tac x="((a, b), ba)" in bexI, auto)
done

lemma 
  shows lambdas3: "Lambda l vs c ∈ lambdas x ==> set vs ⊆ vars x"
  and "Lambda l vs c ∈ lambdasC y ==> set vs ⊆ varsC y"
  and "Lambda l vs c ∈ lambdasV z ==> set vs ⊆ varsV z"
  and "∀z∈ set list. Lambda l vs c ∈ lambdasV z ⟶ set vs ⊆ varsV z"
  and "∀x∈ set (list2 :: (var × lambda) list) . Lambda l vs c ∈ lambdas (snd x) ⟶ set vs ⊆ vars (snd x)"
  and "Lambda l vs c ∈ lambdas (snd (t:: var×lambda)) ==> set vs ⊆ vars (snd t)"
apply (induct x and y and z and list and list2 and t rule:mutual_lambda_call_var_inducts)
apply auto
apply (erule_tac x="((aa, ba), bb)" in ballE)
apply (rule_tac x="((aa, ba), bb)" in bexI, auto)
done

lemma 
  shows app1: "App l d ds ∈ calls x ==> d ∈ vals x"
  and "App l d ds ∈ callsC y ==> d ∈ valsC y"
  and "App l d ds ∈ callsV z ==> d ∈ valsV z"
  and "∀z∈ set list. App l d ds ∈ callsV z ⟶ d ∈ valsV z"
  and "∀x∈ set (list2 :: (var × lambda) list) . App l d ds ∈ calls (snd x) ⟶ d ∈ vals (snd x)"
  and "App l d ds ∈ calls (snd (t:: var×lambda)) ==> d ∈ vals (snd t)"
apply (induct x and y and z and list and list2 and t rule:mutual_lambda_call_var_inducts)
apply auto
apply (case_tac d, auto)
apply (erule_tac x="((a, b), ba)" in ballE)
apply (rule_tac x="((a, b), ba)" in bexI, auto)
done

lemma 
  shows app2: "App l d ds ∈ calls x ==> set ds ⊆ vals x"
  and "App l d ds ∈ callsC y ==> set ds ⊆ valsC y"
  and "App l d ds ∈ callsV z ==> set ds ⊆ valsV z"
  and "∀z∈ set list. App l d ds ∈ callsV z ⟶ set ds ⊆ valsV z"
  and "∀x∈ set (list2 :: (var × lambda) list) . App l d ds ∈ calls (snd x) ⟶ set ds ⊆ vals (snd x)"
  and "App l d ds ∈ calls (snd (t:: var×lambda)) ==> set ds ⊆ vals (snd t)"
apply (induct  x and y and z and list and list2 and t rule:mutual_lambda_call_var_inducts)
apply auto
apply (case_tac x, auto)
apply (erule_tac x="((a, b), ba)" in ballE)
apply (rule_tac x="((a, b), ba)" in bexI, auto)
done

lemma 
  shows let1: "Let l binds c' ∈ calls x ==> l ∈ labels x"
  and "Let l binds c' ∈ callsC y ==> l ∈ labelsC y"
  and "Let l binds c' ∈ callsV z ==> l ∈ labelsV z"
  and "∀z∈ set list. Let l binds c' ∈ callsV z ⟶ l ∈ labelsV z"
  and "∀x∈ set (list2 :: (var × lambda) list) . Let l binds c' ∈ calls (snd x) ⟶ l ∈ labels (snd x)"
  and "Let l binds c' ∈ calls (snd (t:: var×lambda)) ==> l ∈ labels (snd t)"
apply (induct x and y and z and list and list2 and t rule:mutual_lambda_call_var_inducts)
apply auto
apply (erule_tac x="((a, b), ba)" in ballE)
apply (rule_tac x="((a, b), ba)" in bexI, auto)
done

lemma 
  shows let2: "Let l binds c' ∈ calls x ==> c' ∈ calls x"
  and "Let l binds c' ∈ callsC y ==> c' ∈ callsC y"
  and "Let l binds c' ∈ callsV z ==> c' ∈ callsV z"
  and "∀z∈ set list. Let l binds c' ∈ callsV z ⟶ c' ∈ callsV z"
  and "∀x∈ set (list2 :: (var × lambda) list) . Let l binds c' ∈ calls (snd x) ⟶ c' ∈ calls (snd x)"
  and "Let l binds c' ∈ calls (snd (t:: var×lambda)) ==> c' ∈ calls (snd t)"
apply (induct x and y and z and list and list2 and t rule:mutual_lambda_call_var_inducts)
apply auto
apply (case_tac c', auto)
apply (erule_tac x="((a, b), ba)" in ballE)
apply (rule_tac x="((a, b), ba)" in bexI, auto)
done

lemma 
  shows let3: "Let l binds c' ∈ calls x ==> fst ` set binds ⊆ vars x"
  and "Let l binds c' ∈ callsC y ==> fst ` set binds ⊆ varsC y"
  and "Let l binds c' ∈ callsV z ==> fst ` set binds ⊆ varsV z"
  and "∀z∈ set list. Let l binds c' ∈ callsV z ⟶ fst ` set binds ⊆ varsV z"
  and "∀x∈ set (list2 :: (var × lambda) list) . Let l binds c' ∈ calls (snd x) ⟶ fst ` set binds ⊆ vars (snd x)"
  and "Let l binds c' ∈ calls (snd (t:: var×lambda)) ==> fst ` set binds ⊆ vars (snd t)"
       apply (induct x and y and z and list and list2 and t rule:mutual_lambda_call_var_inducts)
             apply auto
  apply fastforce
  done

lemma
  shows let4: "Let l binds c' ∈ calls x ==> snd ` set binds ⊆ lambdas x"
  and "Let l binds c' ∈ callsC y ==> snd ` set binds ⊆ lambdasC y"
  and "Let l binds c' ∈ callsV z ==> snd ` set binds ⊆ lambdasV z"
  and "∀z∈ set list. Let l binds c' ∈ callsV z ⟶ snd ` set binds ⊆ lambdasV z"
  and "∀x∈ set (list2 :: (var × lambda) list) . Let l binds c' ∈ calls (snd x) ⟶ snd ` set binds ⊆ lambdas (snd x)"
  and "Let l binds c' ∈ calls (snd (t:: var×lambda)) ==> snd ` set binds ⊆ lambdas (snd t)"
apply (induct x and y and z and list and list2 and t rule:mutual_lambda_call_var_inducts)
apply auto
apply (rule_tac x="((a, b), ba)" in bexI, auto)
apply (case_tac ba, auto)
apply (erule_tac x="((aa, bb), bc)" in ballE)
apply (rule_tac x="((aa, bb), bc)" in bexI, auto)
done

lemma
shows vals1: "P prim ∈ vals p ==> prim ∈ prims p"
  and "P prim ∈ valsC y ==> prim ∈ primsC y"
  and "P prim ∈ valsV z ==> prim ∈ primsV z"
  and "∀z∈ set list. P prim ∈ valsV z ⟶ prim ∈ primsV z"
  and "∀x∈ set (list2 :: (var × lambda) list) . P prim ∈ vals (snd x) ⟶ prim ∈ prims (snd x)"
  and "P prim ∈ vals (snd (t:: var×lambda)) ==> prim ∈ prims (snd t)"
apply (induct rule:mutual_lambda_call_var_inducts)
apply auto
apply (erule_tac x="((a, b), ba)" in ballE)
apply (rule_tac x="((a, b), ba)" in bexI, auto)
done

lemma
shows vals2: "R l var ∈ vals p ==> var ∈ vars p"
  and "R l var ∈ valsC y ==> var ∈ varsC y"
  and "R l var ∈ valsV z ==> var ∈ varsV z"
  and "∀z∈ set list. R l var ∈ valsV z ⟶ var ∈ varsV z"
  and "∀x∈ set (list2 :: (var × lambda) list) . R l var ∈ vals (snd x) ⟶ var ∈ vars (snd x)"
  and "R l var ∈ vals (snd (t:: var×lambda)) ==> var ∈ vars (snd t)"
apply (induct rule:mutual_lambda_call_var_inducts)
apply auto
apply (erule_tac x="((a, b), ba)" in ballE)
apply (rule_tac x="((a, b), ba)" in bexI, auto)
done

lemma
shows vals3: "L l ∈ vals p ==> l ∈ lambdas p"
  and "L l ∈ valsC y ==> l ∈ lambdasC y"
  and "L l ∈ valsV z ==> l ∈ lambdasV z"
  and "∀z∈ set list. L l ∈ valsV z ⟶ l ∈ lambdasV z"
  and "∀x∈ set (list2 :: (var × lambda) list) . L l ∈ vals (snd x) ⟶ l ∈ lambdas (snd x)"
  and "L l ∈ vals (snd (t:: var×lambda)) ==> l ∈ lambdas (snd t)"
apply (induct rule:mutual_lambda_call_var_inducts)
apply auto
apply (erule_tac x="((a, b), ba)" in ballE)
apply (rule_tac x="((a, b), ba)" in bexI, auto)
apply (case_tac l, auto)
done


definition nList :: "'a set => nat => 'a list set"
where "nList A n ≡ {l. set l ≤ A ∧ length l = n}"

lemma finite_nList[intro]:
  assumes finA: "finite A"
  shows "finite (nList A n)"
proof(induct n)
case 0 thus ?case by (simp add:nList_def) next
case (Suc n) hence finn: "finite (nList (A) n)" by simp
  have "nList A (Suc n) = (case_prod (#)) ` (A × nList A n)" (is "?lhs = ?rhs")
  proof(rule subset_antisym[OF subsetI subsetI])
  fix l assume "l ∈ ?lhs" thus "l ∈ ?rhs"
    by (cases l, auto simp add:nList_def)
  next
  fix l assume "l ∈ ?rhs" thus "l ∈ ?lhs"
    by (auto simp add:nList_def)
  qed
  thus "finite ?lhs" using finA and finn
    by auto
qed

definition NList :: "'a set => nat set => 'a list set"
where "NList A N ≡ ∪ n ∈ N. nList A n"

lemma finite_Nlist[intro]:
  "[ finite A; finite N ] ==> finite (NList A N)"
unfolding NList_def by auto

definition call_list_lengths
  where "call_list_lengths p = {0,1,2,3} ∪ (λc. case c of (App _ _ ds) ==> length ds | _ ==> 0) ` calls p"

lemma finite_call_list_lengths[simp]: "finite (call_list_lengths p)"
  unfolding call_list_lengths_def by auto

end