src/HOL/Predicate_Compile_Examples/Examples.thy

 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 *}
+section \<open>Formal Languages\<close>
+
+subsection \<open>General Context Free Grammars\<close>
+
+text \<open>a contribution by Aditi Barthwal\<close>
 
 datatype ('nts,'ts) symbol = NTS 'nts
                             | TS 'ts
 
                             

 
 code_pred [inductify, skip_proof] test2 .
 
 values "{rhs. test2 rhs}"
 
-subsection {* Some concrete Context Free Grammars *}
+subsection \<open>Some concrete Context Free Grammars\<close>
 
 datatype alphabet = a | b
 
 inductive_set S\<^sub>1 and A\<^sub>1 and B\<^sub>1 where
   "[] \<in> S\<^sub>1"

 
 code_pred (expected_modes: o => bool, i => bool) S\<^sub>4p .
 
 hide_const a b
 
-section {* Semantics of programming languages *}
-
-subsection {* IMP *}
+section \<open>Semantics of programming languages\<close>
+
+subsection \<open>IMP\<close>
 
 type_synonym var = nat
 type_synonym state = "int list"
 
 datatype com =

 
 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 *}
+subsection \<open>Lambda\<close>
 
 datatype type =
     Atom nat
   | Fun type type    (infixr "\<Rightarrow>" 200)
 

 code_pred [dseq] typing .
 code_pred [random_dseq] typing .
 
 values [random_dseq 1,1,5] 10 "{(\<Gamma>, t, T). \<Gamma> \<turnstile> t : T}"
 
-subsection {* A minimal example of yet another semantics *}
-
-text {* thanks to Elke Salecker *}
+subsection \<open>A minimal example of yet another semantics\<close>
+
+text \<open>thanks to Elke Salecker\<close>
 
 type_synonym vname = nat
 type_synonym vvalue = int
-type_synonym var_assign = "vname \<Rightarrow> vvalue"  --"variable assignment"
+type_synonym var_assign = "vname \<Rightarrow> vvalue"  \<comment>"variable assignment"
 
 datatype ir_expr = 
   IrConst vvalue
 | ObjAddr vname
 | Add ir_expr ir_expr

 code_pred eval_var .
 thm eval_var.equation
 
 values "{val. eval_var (Add (IrConst 1) (IrConst 2)) (| Env = (\<lambda>x. 0)|) val}"
 
-subsection {* Another semantics *}
-
-type_synonym name = nat --"For simplicity in examples"
+subsection \<open>Another semantics\<close>
+
+type_synonym name = nat \<comment>"For simplicity in examples"
 type_synonym state' = "name \<Rightarrow> nat"
 
 datatype aexp = N nat | V name | Plus aexp aexp
 
 fun aval :: "aexp \<Rightarrow> state' \<Rightarrow> nat" where

      (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]) \<Rightarrow> s}"
 
 
-subsection {* CCS *}
-
-text{* This example formalizes finite CCS processes without communication or
-recursion. For simplicity, labels are natural numbers. *}
+subsection \<open>CCS\<close>
+
+text\<open>This example formalizes finite CCS processes without communication or
+recursion. For simplicity, labels are natural numbers.\<close>
 
 datatype proc = nil | pre nat proc | or proc proc | par proc proc
 
 inductive step :: "proc \<Rightarrow> nat \<Rightarrow> proc \<Rightarrow> bool" where
 "step (pre n p) n p" |