Quelle  Examples.thy

theory Examples
imports Main "HOL-Library.Predicate_Compile_Alternative_Defs"
begin

declare [[values_timeout = 480.0]]

section ‹Formal Languages›

subsection ‹General Context Free Grammars›

text ‹a contribution by Aditi Barthwal›

datatype ('nts,'ts) symbol = NTS 'nts
                            | TS 'ts

                            
datatype ('nts,'ts) rule = rule 'nts "('nts,'ts) symbol list"

type_synonym ('nts,'ts) grammar = "('nts,'ts) rule set * 'nts"

fun rules :: "('nts,'ts) grammar => ('nts,'ts) rule set"
where
  "rules (r, s) = r"

definition derives 
where
"derives g = { (lsl,rsl). ∃s1 s2 lhs rhs.
                         (s1 @ [NTS lhs] @ s2 = lsl) ∧
                         (s1 @ rhs @ s2) = rsl ∧
                         (rule lhs rhs) ∈ fst g }"

definition derivesp ::
  "(('nts, 'ts) rule => bool) * 'nts => ('nts, 'ts) symbol list => ('nts, 'ts) symbol list => bool"
where
  "derivesp g = (λ lhs rhs. (lhs, rhs) ∈ derives (Collect (fst g), snd g))"
 
lemma [code_pred_def]:
  "derivesp g = (λ lsl rsl. ∃s1 s2 lhs rhs.
                         (s1 @ [NTS lhs] @ s2 = lsl) ∧
                         (s1 @ rhs @ s2) = rsl ∧
                         (fst g) (rule lhs rhs))"
unfolding derivesp_def derives_def by auto

abbreviation "example_grammar ==
({ rule ''S'' [NTS ''A'', NTS ''B''],
   rule ''S'' [TS ''a''],
  rule ''A'' [TS ''b'']}, ''S'')"

definition "example_rules ==
(%x. x = rule ''S'' [NTS ''A'', NTS ''B''] ∨
   x = rule ''S'' [TS ''a''] ∨
  x = rule ''A'' [TS ''b''])"


code_pred [inductify, skip_proof] derivesp .

thm derivesp.equation

definition "testp = (% rhs. derivesp (example_rules, ''S'') [NTS ''S''] rhs)"

code_pred (modes: o ==> bool) [inductify] testp .
thm testp.equation

values "{rhs. testp rhs}"

declare rtranclp.intros(1)[code_pred_def] converse_rtranclp_into_rtranclp[code_pred_def]

code_pred [inductify] rtranclp .

definition "test2 = (λ rhs. rtranclp (derivesp (example_rules, ''S'')) [NTS ''S''] rhs)"

code_pred [inductify, skip_proof] test2 .

values "{rhs. test2 rhs}"

subsection ‹Some concrete Context Free Grammars›

datatype alphabet = a | b

inductive_set S₁ and A₁ and B₁ where
  "[] ∈ S₁"
| "w ∈ A₁ ==> b # w ∈ S₁"
| "w ∈ B₁ ==> a # w ∈ S₁"
| "w ∈ S₁ ==> a # w ∈ A₁"
| "w ∈ S₁ ==> b # w ∈ S₁"
| "[v ∈ B₁; v ∈ B₁] ==> a # v @ w ∈ B₁"

code_pred [inductify] S₁p .
code_pred [random_dseq inductify] S₁p .
thm S₁p.equation
thm S₁p.random_dseq_equation

values [random_dseq 5, 5, 5] 5 "{x. S₁p x}"

inductive_set S₂ and A₂ and B₂ where
  "[] ∈ S₂"
| "w ∈ A₂ ==> b # w ∈ S₂"
| "w ∈ B₂ ==> a # w ∈ S₂"
| "w ∈ S₂ ==> a # w ∈ A₂"
| "w ∈ S₂ ==> b # w ∈ B₂"
| "[v ∈ B₂; v ∈ B₂] ==> a # v @ w ∈ B₂"

code_pred [random_dseq inductify] S₂p .
thm S₂p.random_dseq_equation
thm A₂p.random_dseq_equation
thm B₂p.random_dseq_equation

values [random_dseq 5, 5, 5] 10 "{x. S₂p x}"

inductive_set S₃ and A₃ and B₃ where
  "[] ∈ S₃"
| "w ∈ A₃ ==> b # w ∈ S₃"
| "w ∈ B₃ ==> a # w ∈ S₃"
| "w ∈ S₃ ==> a # w ∈ A₃"
| "w ∈ S₃ ==> b # w ∈ B₃"
| "[v ∈ B₃; w ∈ B₃] ==> a # v @ w ∈ B₃"

code_pred [inductify, skip_proof] S₃p .
thm S₃p.equation

values 10 "{x. S₃p x}"

inductive_set S₄ and A₄ and B₄ where
  "[] ∈ S₄"
| "w ∈ A₄ ==> b # w ∈ S₄"
| "w ∈ B₄ ==> a # w ∈ S₄"
| "w ∈ S₄ ==> a # w ∈ A₄"
| "[v ∈ A₄; w ∈ A₄] ==> b # v @ w ∈ A₄"
| "w ∈ S₄ ==> b # w ∈ B₄"
| "[v ∈ B₄; w ∈ B₄] ==> a # v @ w ∈ B₄"

code_pred (expected_modes: o => bool, i => bool) S₄p .

hide_const a b

section ‹Semantics of programming languages›

subsection ‹IMP›

type_synonym var = nat
type_synonym state = "int list"

datatype com =
  Skip |
  Ass var "state => int" |
  Seq com com |
  IF "state => bool" com com |
  While "state => bool" com

inductive exec :: "com => state => state => bool" where
"exec Skip s s" |
"exec (Ass x e) s (s[x := e(s)])" |
"exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" |
"b s ==> exec c1 s t ==> exec (IF b c1 c2) s t" |
"~b s ==> exec c2 s t ==> exec (IF b c1 c2) s t" |
"~b s ==> exec (While b c) s s" |
"b s1 ==> exec c s1 s2 ==> exec (While b c) s2 s3 ==> exec (While b c) s1 s3"

code_pred exec .

values "{t. exec
 (While (%s. s!0 > 0) (Seq (Ass 0 (%s. s!0 - 1)) (Ass 1 (%s. s!1 + 1))))
 [3,5] t}"

subsection ‹Lambda›

datatype type =
    Atom nat
  | Fun type type    (infixr ‹==>› 200)

datatype dB =
    Var nat
  | App dB dB (infixl ‹🍋› 200)
  | Abs type dB

primrec
  nth_el :: "'a list ==> nat ==> 'a option" (‹_⟨_⟩› [90, 0] 91)
where
  "[]⟨i⟩ = None"
| "(x # xs)⟨i⟩ = (case i of 0 ==> Some x | Suc j ==> xs ⟨j⟩)"

inductive nth_el' :: "'a list ==> nat ==> 'a ==> bool"
where
  "nth_el' (x # xs) 0 x"
| "nth_el' xs i y ==> nth_el' (x # xs) (Suc i) y"

inductive typing :: "type list ==> dB ==> type ==> bool"  (‹_ ⊨ _ : _› [50, 50, 50] 50)
  where
    Var [intro!]: "nth_el' env x T ==> env ⊨ Var x : T"
  | Abs [intro!]: "T # env ⊨ t : U ==> env ⊨ Abs T t : (T ==> U)"
  | App [intro!]: "env ⊨ s : T ==> U ==> env ⊨ t : T ==> env ⊨ (s 🍋 t) : U"

primrec
  lift :: "[dB, nat] => dB"
where
    "lift (Var i) k = (if i < k then Var i else Var (i + 1))"
  | "lift (s 🍋 t) k = lift s k 🍋 lift t k"
  | "lift (Abs T s) k = Abs T (lift s (k + 1))"

primrec
  subst :: "[dB, dB, nat] => dB"  (‹_[_'/_]› [300, 0, 0] 300)
where
    subst_Var: "(Var i)[s/k] =
      (if k < i then Var (i - 1) else if i = k then s else Var i)"
  | subst_App: "(t 🍋 u)[s/k] = t[s/k] 🍋 u[s/k]"
  | subst_Abs: "(Abs T t)[s/k] = Abs T (t[lift s 0 / k+1])"

inductive beta :: "[dB, dB] => bool"  (infixl ‹→_\β› 50)
  where
    beta [simp, intro!]: "Abs T s 🍋 t →_\<beta> s[t/0]"
  | appL [simp, intro!]: "s →_\<beta> t ==> s 🍋 u →_\<beta> t 🍋 u"
  | appR [simp, intro!]: "s →_\<beta> t ==> u 🍋 s →_\<beta> u 🍋 t"
  | abs [simp, intro!]: "s →_\<beta> t ==> Abs T s →_\<beta> Abs T t"

code_pred (expected_modes: i => i => o => bool, i => i => i => bool) typing .
thm typing.equation

code_pred (modes: i => i => bool,  i => o => bool as reduce') beta .
thm beta.equation

values "{x. App (Abs (Atom 0) (Var 0)) (Var 1) →_\<beta> x}"

definition "reduce t = Predicate.the (reduce' t)"

value "reduce (App (Abs (Atom 0) (Var 0)) (Var 1))"

code_pred [dseq] typing .
code_pred [random_dseq] typing .

values [random_dseq 1,1,5] 10 "{(Γ, t, T). Γ ⊨ t : T}"

subsection ‹A minimal example of yet another semantics›

text ‹thanks to Elke Salecker›

type_synonym vname = nat
type_synonym vvalue = int
type_synonym var_assign = "vname ==> vvalue"  ― ‹variable assignment›

datatype ir_expr = 
  IrConst vvalue
| ObjAddr vname
| Add ir_expr ir_expr

datatype val =
  IntVal  vvalue

record  configuration =
  Env :: var_assign

inductive eval_var ::
  "ir_expr ==> configuration ==> val ==> bool"
where
  irconst: "eval_var (IrConst i) conf (IntVal i)"
| objaddr: "[ Env conf n = i ] ==> eval_var (ObjAddr n) conf (IntVal i)"
| plus: "[ eval_var l conf (IntVal vl); eval_var r conf (IntVal vr) ] ==>
    eval_var (Add l r) conf (IntVal (vl+vr))"


code_pred eval_var .
thm eval_var.equation

values "{val. eval_var (Add (IrConst 1) (IrConst 2)) (| Env = (λx. 0)|) val}"

subsection ‹Another semantics›

type_synonym name = nat ― ‹For simplicity in examples›
type_synonym state' = "name ==> nat"

datatype aexp = N nat | V name | Plus aexp aexp

fun aval :: "aexp ==> state' ==> nat" where
"aval (N n) _ = n" |
"aval (V x) st = st x" |
"aval (Plus e₁ e₂) st = aval e₁ st + aval e₂ st"

datatype bexp = B bool | Not bexp | And bexp bexp | Less aexp aexp

primrec bval :: "bexp ==> state' ==> bool" where
"bval (B b) _ = b" |
"bval (Not b) st = (¬ bval b st)" |
"bval (And b1 b2) st = (bval b1 st ∧ bval b2 st)" |
"bval (Less a₁ a₂) st = (aval a₁ st < aval a₂ st)"

datatype
  com' = SKIP 
      | Assign name aexp         (‹_ ::= _› [1000, 61] 61)
      | Semi   com'  com'          (‹_; _›  [60, 61] 60)
      | If     bexp com' com'     (‹IF _ THEN _ ELSE _›  [0, 0, 61] 61)
      | While  bexp com'         (‹WHILE _ DO _›  [0, 61] 61)

inductive
  big_step :: "com' * state' ==> state' ==> bool" (infix ‹==>› 55)
where
  Skip:    "(SKIP,s) ==> s"
| Assign:  "(x ::= a,s) ==> s(x := aval a s)"

| Semi:    "(c₁,s₁) ==> s₂ ==> (c₂,s₂) ==> s₃ ==> (c₁;c₂, s₁) ==> s₃"

| IfTrue:  "bval b s ==> (c₁,s) ==> t ==> (IF b THEN c₁ ELSE c₂, s) ==> t"
| IfFalse: "¬bval b s ==> (c₂,s) ==> t ==> (IF b THEN c₁ ELSE c₂, s) ==> t"

| WhileFalse: "¬bval b s ==> (WHILE b DO c,s) ==> s"
| WhileTrue:  "bval b s₁ ==> (c,s₁) ==> s₂ ==> (WHILE b DO c, s₂) ==> s₃
               ==> (WHILE b DO c, s₁) ==> s₃"

code_pred big_step .

thm big_step.equation

definition list :: "(nat ==> 'a) ==> nat ==> 'a list" where
  "list s n = map s [0 ..< n]"

values [expected "{[42::nat, 43]}"] "{list s 2|s. (SKIP, nth [42, 43]) ==> s}"


subsection ‹CCS›

text‹This example formalizes finite CCS processes without communication or
 . For simplicity, labels are natural numbers.›

datatype proc = nil | pre nat proc | or proc proc | par proc proc

inductive step :: "proc ==> nat ==> proc ==> bool" where
"step (pre n p) n p" |
"step p1 a q ==> step (or p1 p2) a q" |
"step p2 a q ==> step (or p1 p2) a q" |
"step p1 a q ==> step (par p1 p2) a (par q p2)" |
"step p2 a q ==> step (par p1 p2) a (par p1 q)"

code_pred step .

inductive steps where
"steps p [] p" |
"step p a q ==> steps q as r ==> steps p (a#as) r"

code_pred steps .

values 3 
 "{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}"

values 5
 "{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}"

values 3 "{(a,q). step (par nil nil) a q}"


end