Theory Examples

theory Examples
imports Predicate_Compile_Alternative_Defs
theory Examples
imports Main "~~/src/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 S1 and A1 and B1 where
  "[] ∈ S1"
| "w ∈ A1 ==> b # w ∈ S1"
| "w ∈ B1 ==> a # w ∈ S1"
| "w ∈ S1 ==> a # w ∈ A1"
| "w ∈ S1 ==> b # w ∈ S1"
| "[|v ∈ B1; v ∈ B1|] ==> a # v @ w ∈ B1"

code_pred [inductify] S1p .
code_pred [random_dseq inductify] S1p .
thm S1p.equation
thm S1p.random_dseq_equation

values [random_dseq 5, 5, 5] 5 "{x. S1p x}"

inductive_set S2 and A2 and B2 where
  "[] ∈ S2"
| "w ∈ A2 ==> b # w ∈ S2"
| "w ∈ B2 ==> a # w ∈ S2"
| "w ∈ S2 ==> a # w ∈ A2"
| "w ∈ S2 ==> b # w ∈ B2"
| "[|v ∈ B2; v ∈ B2|] ==> a # v @ w ∈ B2"

code_pred [random_dseq inductify] S2p .
thm S2p.random_dseq_equation
thm A2p.random_dseq_equation
thm B2p.random_dseq_equation

values [random_dseq 5, 5, 5] 10 "{x. S2p x}"

inductive_set S3 and A3 and B3 where
  "[] ∈ S3"
| "w ∈ A3 ==> b # w ∈ S3"
| "w ∈ B3 ==> a # w ∈ S3"
| "w ∈ S3 ==> a # w ∈ A3"
| "w ∈ S3 ==> b # w ∈ B3"
| "[|v ∈ B3; w ∈ B3|] ==> a # v @ w ∈ B3"

code_pred [inductify, skip_proof] S3p .
thm S3p.equation

values 10 "{x. S3p x}"

inductive_set S4 and A4 and B4 where
  "[] ∈ S4"
| "w ∈ A4 ==> b # w ∈ S4"
| "w ∈ B4 ==> a # w ∈ S4"
| "w ∈ S4 ==> a # w ∈ A4"
| "[|v ∈ A4; w ∈ A4|] ==> b # v @ w ∈ A4"
| "w ∈ S4 ==> b # w ∈ B4"
| "[|v ∈ B4; w ∈ B4|] ==> a # v @ w ∈ B4"

code_pred (expected_modes: o => bool, i => bool) S4p .

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"  ("_ \<turnstile> _ : _" [50, 50, 50] 50)
  where
    Var [intro!]: "nth_el' env x T ==> env \<turnstile> Var x : T"
  | Abs [intro!]: "T # env \<turnstile> t : U ==> env \<turnstile> Abs T t : (T => U)"
  | App [intro!]: "env \<turnstile> s : T => U ==> env \<turnstile> t : T ==> env \<turnstile> (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 ->β s[t/0]"
  | appL [simp, intro!]: "s ->β t ==> s ° u ->β t ° u"
  | appR [simp, intro!]: "s ->β t ==> u ° s ->β u ° t"
  | abs [simp, intro!]: "s ->β t ==> Abs T s ->β 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) ->β 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). Γ \<turnstile> 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 e1 e2) st = aval e1 st + aval e2 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 a1 a2) st = (aval a1 st < aval a2 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:    "(c1,s1) => s2  ==>  (c2,s2) => s3  ==> (c1;c2, s1) => s3"

| IfTrue:  "bval b s  ==>  (c1,s) => t  ==>  (IF b THEN c1 ELSE c2, s) => t"
| IfFalse: "¬bval b s  ==>  (c2,s) => t  ==>  (IF b THEN c1 ELSE c2, s) => t"

| WhileFalse: "¬bval b s ==> (WHILE b DO c,s) => s"
| WhileTrue:  "bval b s1  ==>  (c,s1) => s2  ==>  (WHILE b DO c, s2) => s3
               ==> (WHILE b DO c, s1) => s3"

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 "{[Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
     (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
     (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)
     )))))))))))))))))))))))))))))))))))))))),
   Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc   (Suc (Suc (Suc (Suc
     (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
     (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)
     )))))))))))))))))))))))))))))))))))))))))]}"] "{list s 2|s. (SKIP, nth [42, 43]) => s}"


subsection {* CCS *}

text{* This example formalizes finite CCS processes without communication or
recursion. 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