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.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.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'')
```