src/HOL/Induct/Com.thy
changeset 60530 44f9873d6f6f
parent 59807 22bc39064290
child 61424 c3658c18b7bc
     1.1 --- a/src/HOL/Induct/Com.thy	Sat Jun 20 15:43:36 2015 +0200
     1.2 +++ b/src/HOL/Induct/Com.thy	Sat Jun 20 15:45:02 2015 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  Example of Mutual Induction via Iteratived Inductive Definitions: Commands
     1.5  *)
     1.6  
     1.7 -section{*Mutual Induction via Iteratived Inductive Definitions*}
     1.8 +section\<open>Mutual Induction via Iteratived Inductive Definitions\<close>
     1.9  
    1.10  theory Com imports Main begin
    1.11  
    1.12 @@ -25,15 +25,15 @@
    1.13        | While exp com          ("WHILE _ DO _"  60)
    1.14  
    1.15  
    1.16 -subsection {* Commands *}
    1.17 +subsection \<open>Commands\<close>
    1.18  
    1.19 -text{* Execution of commands *}
    1.20 +text\<open>Execution of commands\<close>
    1.21  
    1.22  abbreviation (input)
    1.23    generic_rel  ("_/ -|[_]-> _" [50,0,50] 50)  where
    1.24    "esig -|[eval]-> ns == (esig,ns) \<in> eval"
    1.25  
    1.26 -text{*Command execution.  Natural numbers represent Booleans: 0=True, 1=False*}
    1.27 +text\<open>Command execution.  Natural numbers represent Booleans: 0=True, 1=False\<close>
    1.28  
    1.29  inductive_set
    1.30    exec :: "((exp*state) * (nat*state)) set => ((com*state)*state)set"
    1.31 @@ -74,7 +74,7 @@
    1.32      and exec_WHILE_case: "(WHILE b DO c,s) -[eval]-> t"
    1.33  
    1.34  
    1.35 -text{*Justifies using "exec" in the inductive definition of "eval"*}
    1.36 +text\<open>Justifies using "exec" in the inductive definition of "eval"\<close>
    1.37  lemma exec_mono: "A<=B ==> exec(A) <= exec(B)"
    1.38  apply (rule subsetI)
    1.39  apply (simp add: split_paired_all)
    1.40 @@ -92,7 +92,7 @@
    1.41    unfolding subset_eq
    1.42    by (auto simp add: le_fun_def)
    1.43  
    1.44 -text{*Command execution is functional (deterministic) provided evaluation is*}
    1.45 +text\<open>Command execution is functional (deterministic) provided evaluation is\<close>
    1.46  theorem single_valued_exec: "single_valued ev ==> single_valued(exec ev)"
    1.47  apply (simp add: single_valued_def)
    1.48  apply (intro allI)
    1.49 @@ -102,9 +102,9 @@
    1.50  done
    1.51  
    1.52  
    1.53 -subsection {* Expressions *}
    1.54 +subsection \<open>Expressions\<close>
    1.55  
    1.56 -text{* Evaluation of arithmetic expressions *}
    1.57 +text\<open>Evaluation of arithmetic expressions\<close>
    1.58  
    1.59  inductive_set
    1.60    eval    :: "((exp*state) * (nat*state)) set"
    1.61 @@ -136,13 +136,13 @@
    1.62    by (rule fun_upd_same [THEN subst]) fast
    1.63  
    1.64  
    1.65 -text{* Make the induction rule look nicer -- though @{text eta_contract} makes the new
    1.66 -    version look worse than it is...*}
    1.67 +text\<open>Make the induction rule look nicer -- though @{text eta_contract} makes the new
    1.68 +    version look worse than it is...\<close>
    1.69  
    1.70  lemma split_lemma: "{((e,s),(n,s')). P e s n s'} = Collect (split (%v. split (split P v)))"
    1.71    by auto
    1.72  
    1.73 -text{*New induction rule.  Note the form of the VALOF induction hypothesis*}
    1.74 +text\<open>New induction rule.  Note the form of the VALOF induction hypothesis\<close>
    1.75  lemma eval_induct
    1.76    [case_names N X Op valOf, consumes 1, induct set: eval]:
    1.77    "[| (e,s) -|-> (n,s');
    1.78 @@ -167,12 +167,12 @@
    1.79  done
    1.80  
    1.81  
    1.82 -text{*Lemma for @{text Function_eval}.  The major premise is that @{text "(c,s)"} executes to @{text "s1"}
    1.83 +text\<open>Lemma for @{text Function_eval}.  The major premise is that @{text "(c,s)"} executes to @{text "s1"}
    1.84    using eval restricted to its functional part.  Note that the execution
    1.85    @{text "(c,s) -[eval]-> s2"} can use unrestricted @{text eval}!  The reason is that
    1.86    the execution @{text "(c,s) -[eval Int {...}]-> s1"} assures us that execution is
    1.87    functional on the argument @{text "(c,s)"}.
    1.88 -*}
    1.89 +\<close>
    1.90  lemma com_Unique:
    1.91   "(c,s) -[eval Int {((e,s),(n,t)). \<forall>nt'. (e,s) -|-> nt' --> (n,t)=nt'}]-> s1
    1.92    ==> \<forall>s2. (c,s) -[eval]-> s2 --> s2=s1"
    1.93 @@ -190,7 +190,7 @@
    1.94  done
    1.95  
    1.96  
    1.97 -text{*Expression evaluation is functional, or deterministic*}
    1.98 +text\<open>Expression evaluation is functional, or deterministic\<close>
    1.99  theorem single_valued_eval: "single_valued eval"
   1.100  apply (unfold single_valued_def)
   1.101  apply (intro allI, rule impI)
   1.102 @@ -204,14 +204,14 @@
   1.103  lemma eval_N_E [dest!]: "(N n, s) -|-> (v, s') ==> (v = n & s' = s)"
   1.104    by (induct e == "N n" s v s' set: eval) simp_all
   1.105  
   1.106 -text{*This theorem says that "WHILE TRUE DO c" cannot terminate*}
   1.107 +text\<open>This theorem says that "WHILE TRUE DO c" cannot terminate\<close>
   1.108  lemma while_true_E:
   1.109      "(c', s) -[eval]-> t ==> c' = WHILE (N 0) DO c ==> False"
   1.110    by (induct set: exec) auto
   1.111  
   1.112  
   1.113 -subsection{* Equivalence of IF e THEN c;;(WHILE e DO c) ELSE SKIP  and
   1.114 -       WHILE e DO c *}
   1.115 +subsection\<open>Equivalence of IF e THEN c;;(WHILE e DO c) ELSE SKIP  and
   1.116 +       WHILE e DO c\<close>
   1.117  
   1.118  lemma while_if1:
   1.119       "(c',s) -[eval]-> t
   1.120 @@ -233,8 +233,8 @@
   1.121  
   1.122  
   1.123  
   1.124 -subsection{* Equivalence of  (IF e THEN c1 ELSE c2);;c
   1.125 -                         and  IF e THEN (c1;;c) ELSE (c2;;c)   *}
   1.126 +subsection\<open>Equivalence of  (IF e THEN c1 ELSE c2);;c
   1.127 +                         and  IF e THEN (c1;;c) ELSE (c2;;c)\<close>
   1.128  
   1.129  lemma if_semi1:
   1.130       "(c',s) -[eval]-> t
   1.131 @@ -254,9 +254,9 @@
   1.132  
   1.133  
   1.134  
   1.135 -subsection{* Equivalence of  VALOF c1 RESULTIS (VALOF c2 RESULTIS e)
   1.136 +subsection\<open>Equivalence of  VALOF c1 RESULTIS (VALOF c2 RESULTIS e)
   1.137                    and  VALOF c1;;c2 RESULTIS e
   1.138 - *}
   1.139 +\<close>
   1.140  
   1.141  lemma valof_valof1:
   1.142       "(e',s) -|-> (v,s')
   1.143 @@ -276,7 +276,7 @@
   1.144    by (blast intro: valof_valof1 valof_valof2)
   1.145  
   1.146  
   1.147 -subsection{* Equivalence of  VALOF SKIP RESULTIS e  and  e *}
   1.148 +subsection\<open>Equivalence of  VALOF SKIP RESULTIS e  and  e\<close>
   1.149  
   1.150  lemma valof_skip1:
   1.151       "(e',s) -|-> (v,s')
   1.152 @@ -293,7 +293,7 @@
   1.153    by (blast intro: valof_skip1 valof_skip2)
   1.154  
   1.155  
   1.156 -subsection{* Equivalence of  VALOF x:=e RESULTIS x  and  e *}
   1.157 +subsection\<open>Equivalence of  VALOF x:=e RESULTIS x  and  e\<close>
   1.158  
   1.159  lemma valof_assign1:
   1.160       "(e',s) -|-> (v,s'')