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 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" ("_ ⊢ _ : _" [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 →⇩β 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). Γ ⊢ 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 "{[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