Up to index of Isabelle/HOL/HOL-Predicate_Compile_Examples
theory Examplestheory 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 S⇣1 and A⇣1 and B⇣1 where
"[] ∈ S⇣1"
| "w ∈ A⇣1 ==> b # w ∈ S⇣1"
| "w ∈ B⇣1 ==> a # w ∈ S⇣1"
| "w ∈ S⇣1 ==> a # w ∈ A⇣1"
| "w ∈ S⇣1 ==> b # w ∈ S⇣1"
| "[|v ∈ B⇣1; v ∈ B⇣1|] ==> a # v @ w ∈ B⇣1"
code_pred [inductify] S⇣1p .
code_pred [random_dseq inductify] S⇣1p .
thm S⇣1p.equation
thm S⇣1p.random_dseq_equation
values [random_dseq 5, 5, 5] 5 "{x. S⇣1p x}"
inductive_set S⇣2 and A⇣2 and B⇣2 where
"[] ∈ S⇣2"
| "w ∈ A⇣2 ==> b # w ∈ S⇣2"
| "w ∈ B⇣2 ==> a # w ∈ S⇣2"
| "w ∈ S⇣2 ==> a # w ∈ A⇣2"
| "w ∈ S⇣2 ==> b # w ∈ B⇣2"
| "[|v ∈ B⇣2; v ∈ B⇣2|] ==> a # v @ w ∈ B⇣2"
code_pred [random_dseq inductify] S⇣2p .
thm S⇣2p.random_dseq_equation
thm A⇣2p.random_dseq_equation
thm B⇣2p.random_dseq_equation
values [random_dseq 5, 5, 5] 10 "{x. S⇣2p x}"
inductive_set S⇣3 and A⇣3 and B⇣3 where
"[] ∈ S⇣3"
| "w ∈ A⇣3 ==> b # w ∈ S⇣3"
| "w ∈ B⇣3 ==> a # w ∈ S⇣3"
| "w ∈ S⇣3 ==> a # w ∈ A⇣3"
| "w ∈ S⇣3 ==> b # w ∈ B⇣3"
| "[|v ∈ B⇣3; w ∈ B⇣3|] ==> a # v @ w ∈ B⇣3"
code_pred [inductify, skip_proof] S⇣3p .
thm S⇣3p.equation
values 10 "{x. S⇣3p x}"
inductive_set S⇣4 and A⇣4 and B⇣4 where
"[] ∈ S⇣4"
| "w ∈ A⇣4 ==> b # w ∈ S⇣4"
| "w ∈ B⇣4 ==> a # w ∈ S⇣4"
| "w ∈ S⇣4 ==> a # w ∈ A⇣4"
| "[|v ∈ A⇣4; w ∈ A⇣4|] ==> b # v @ w ∈ A⇣4"
| "w ∈ S⇣4 ==> b # w ∈ B⇣4"
| "[|v ∈ B⇣4; w ∈ B⇣4|] ==> a # v @ w ∈ B⇣4"
code_pred (expected_modes: o => bool, i => bool) S⇣4p .
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 e⇣1 e⇣2) st = aval e⇣1 st + aval e⇣2 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⇣1 a⇣2) st = (aval a⇣1 st < aval a⇣2 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⇣1,s⇣1) => s⇣2 ==> (c⇣2,s⇣2) => s⇣3 ==> (c⇣1;c⇣2, s⇣1) => s⇣3"
| IfTrue: "bval b s ==> (c⇣1,s) => t ==> (IF b THEN c⇣1 ELSE c⇣2, s) => t"
| IfFalse: "¬bval b s ==> (c⇣2,s) => t ==> (IF b THEN c⇣1 ELSE c⇣2, s) => t"
| WhileFalse: "¬bval b s ==> (WHILE b DO c,s) => s"
| WhileTrue: "bval b s⇣1 ==> (c,s⇣1) => s⇣2 ==> (WHILE b DO c, s⇣2) => s⇣3
==> (WHILE b DO c, s⇣1) => s⇣3"
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, (43 :: nat)]}"] "{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