Wie zu beweisen, dass die Hinzufügung einer neuen Variablen zu dem Ausdruck seine Semantik nicht ändert?

Question

Hier ist ganz einfach die Sprache aus:

type_synonym vname = "string" 
type_synonym bool3 = "bool option" 
type_synonym env = "vname ⇒ bool3" 

datatype exp = Let vname bool exp | Var vname | And exp exp 

primrec val :: "exp ⇒ env ⇒ bool3" where 
    "val (Let var init body) e = val body (e(var ↦ init))" 
| "val (Var var) e = e var" 
| "val (And a b) e = (case (val a e, val b e) of 
    (Some x, Some y) ⇒ Some (x ∧ y) | _ ⇒ None)" 

Ich versuche zu beweisen, dass, wenn ein Ausdruck keine freien Variablen nicht hat, dann kann ich am Anfang des Ausdrucks jede neue Variable deklariert. Ich habe 3 Ansätze ausprobiert, um es zu beweisen.

1) defined Funktion überprüft, ob der Wert des Ausdrucks gut definiert ist (= alle verwendeten Variablen deklariert):

primrec defined :: "exp ⇒ env ⇒ bool" where 
    "defined (Let var init body) e = defined body (e(var ↦ init))" 
| "defined (Var var) e = (var : dom e)" 
| "defined (And a b) e = (defined a e ∧ defined b e)" 

lemma var_intro: "defined exp env ⟹ defined exp (env(x ↦ init))" 
    apply (induct exp) 
    apply (simp_all split: if_splits) 

2) Der alternative Ansatz ist es, alle freien Variablen aus dem Ausdruck zu sammeln. Und wenn der Ausdruck enthält keine, dann können wir eine neue Variable in die Umwelt hinzuzufügen:

primrec freeVars :: "exp ⇒ vname set ⇒ vname set" where 
    "freeVars (Let var init body) e = freeVars body (insert var e)" 
| "freeVars (Var var) e = (if var ∈ e then {} else {var})" 
| "freeVars (And a b) e = freeVars a e ∪ freeVars b e" 

lemma var_intro2: "freeVars exp {} = {} ⟹ freeVars exp {x} = {}" 
    apply (induct exp) 
    apply (simp_all split: if_splits) 

3) und den letzten Ansatz ist es, alle beschränkten Variablen aus der Umgebung zu beseitigen:

primrec isFree :: "vname ⇒ exp ⇒ bool" where 
    "isFree x (Let var init body) = (if var = x then False else isFree x body)" 
| "isFree x (Var var) = (var = x)" 
| "isFree x (And a b) = (isFree x a ∨ isFree x b)" 

lemma var_elim: "¬ isFree x exp ⟹ val exp (env(x ↦ init)) = val exp (env)" 
    apply (induct exp) 
    apply (simp_all split: if_splits) 

Ich kann keines der Lemmas beweisen. Könnten Sie eine Lösung vorschlagen?

Answer 1

Ihre Beweise werden wahrscheinlich erfordern, dass Sie env auf arbitrary in der Induktion setzen oder die Beweise werden nicht funktionieren. Damit werden Sie wahrscheinlich in der Lage sein, die von Ihnen angegebenen Eigenschaften zu beweisen, aber ich denke, dass es etwas hässlich sein wird, da sowohl Ihre Definitionen als auch Ihre Lemma-Aussagen unnötig spezifisch sind, was Beweisen schmerzhafter machen kann.

Insbesondere Ihre Vorstellung von 'freie Variable w.r.t. eine Umgebung "erscheint mir ein wenig unnötig kompliziert. Ich denke, dass es einfacher ist, die folgende zu verwenden:

primrec freeVars :: "exp ⇒ vname set" where 
    "freeVars (Let var init body) = freeVars body - {var}" 
| "freeVars (Var var) = {var}" 
| "freeVars (And a b) = freeVars a ∪ freeVars b" 

Die Aussage ‚Ausdruck exp wohldefiniert w.r.t. Eine Umgebung env 'ist dann einfach freeVars exp ⊆ dom env.

Dann ist es offensichtlich, dass jeder Ausdruck, der gut definiert ist w.r.t. Einige Umgebungen sind auch in größeren Umgebungen gut definiert.

Answer 2

1) Sie müssen die kommunikative Eigenschaft der Elementeinfügung auf Sets in die Statusaktualisierungen auf Karten aufheben, auf denen Ihr Lemma basiert.

lemma defined_dom: "defined exp env ⟹ dom env = dom env' ⟹ defined exp env'" 
    by (induction exp arbitrary: env env'; auto) 
lemma defined_comm: "defined exp (env(x↦a, y↦b)) ⟹ defined exp (env(y↦b, x↦a))" 
    by (auto elim!: defined_dom) 
lemma var_intro: "defined exp env ⟹ defined exp (env(x ↦ init))" 
    by (induction exp arbitrary: env; simp add: defined_comm) 

2) Wenn Ihr Lemma auf Gruppen basiert, müssen Sie auch die kommunikative Lemma, die bereits in der Bibliothek ist:

lemma var_intro2': "freeVars exp s = {} ⟹ freeVars exp (insert x s) = {}" 
by (induction exp arbitrary: s x; force simp: insert_commute) 
lemma var_intro2: "freeVars exp {} = {} ⟹ freeVars exp {x} = {}" 
    using var_intro2' . 

3) ähnlich:

lemma var_elim: "¬ isFree x exp ⟹ val exp (env(x ↦ init)) = val exp (env)" 
    by (induction exp arbitrary: env; simp add: fun_upd_twist split: if_splits)