--- a/src/HOL/Induct/Com.thy Sat Jun 20 15:43:36 2015 +0200
+++ b/src/HOL/Induct/Com.thy Sat Jun 20 15:45:02 2015 +0200
@@ -5,7 +5,7 @@
Example of Mutual Induction via Iteratived Inductive Definitions: Commands
*)
-section{*Mutual Induction via Iteratived Inductive Definitions*}
+section\<open>Mutual Induction via Iteratived Inductive Definitions\<close>
theory Com imports Main begin
@@ -25,15 +25,15 @@
| While exp com ("WHILE _ DO _" 60)
-subsection {* Commands *}
+subsection \<open>Commands\<close>
-text{* Execution of commands *}
+text\<open>Execution of commands\<close>
abbreviation (input)
generic_rel ("_/ -|[_]-> _" [50,0,50] 50) where
"esig -|[eval]-> ns == (esig,ns) \<in> eval"
-text{*Command execution. Natural numbers represent Booleans: 0=True, 1=False*}
+text\<open>Command execution. Natural numbers represent Booleans: 0=True, 1=False\<close>
inductive_set
exec :: "((exp*state) * (nat*state)) set => ((com*state)*state)set"
@@ -74,7 +74,7 @@
and exec_WHILE_case: "(WHILE b DO c,s) -[eval]-> t"
-text{*Justifies using "exec" in the inductive definition of "eval"*}
+text\<open>Justifies using "exec" in the inductive definition of "eval"\<close>
lemma exec_mono: "A<=B ==> exec(A) <= exec(B)"
apply (rule subsetI)
apply (simp add: split_paired_all)
@@ -92,7 +92,7 @@
unfolding subset_eq
by (auto simp add: le_fun_def)
-text{*Command execution is functional (deterministic) provided evaluation is*}
+text\<open>Command execution is functional (deterministic) provided evaluation is\<close>
theorem single_valued_exec: "single_valued ev ==> single_valued(exec ev)"
apply (simp add: single_valued_def)
apply (intro allI)
@@ -102,9 +102,9 @@
done
-subsection {* Expressions *}
+subsection \<open>Expressions\<close>
-text{* Evaluation of arithmetic expressions *}
+text\<open>Evaluation of arithmetic expressions\<close>
inductive_set
eval :: "((exp*state) * (nat*state)) set"
@@ -136,13 +136,13 @@
by (rule fun_upd_same [THEN subst]) fast
-text{* Make the induction rule look nicer -- though @{text eta_contract} makes the new
- version look worse than it is...*}
+text\<open>Make the induction rule look nicer -- though @{text eta_contract} makes the new
+ version look worse than it is...\<close>
lemma split_lemma: "{((e,s),(n,s')). P e s n s'} = Collect (split (%v. split (split P v)))"
by auto
-text{*New induction rule. Note the form of the VALOF induction hypothesis*}
+text\<open>New induction rule. Note the form of the VALOF induction hypothesis\<close>
lemma eval_induct
[case_names N X Op valOf, consumes 1, induct set: eval]:
"[| (e,s) -|-> (n,s');
@@ -167,12 +167,12 @@
done
-text{*Lemma for @{text Function_eval}. The major premise is that @{text "(c,s)"} executes to @{text "s1"}
+text\<open>Lemma for @{text Function_eval}. The major premise is that @{text "(c,s)"} executes to @{text "s1"}
using eval restricted to its functional part. Note that the execution
@{text "(c,s) -[eval]-> s2"} can use unrestricted @{text eval}! The reason is that
the execution @{text "(c,s) -[eval Int {...}]-> s1"} assures us that execution is
functional on the argument @{text "(c,s)"}.
-*}
+\<close>
lemma com_Unique:
"(c,s) -[eval Int {((e,s),(n,t)). \<forall>nt'. (e,s) -|-> nt' --> (n,t)=nt'}]-> s1
==> \<forall>s2. (c,s) -[eval]-> s2 --> s2=s1"
@@ -190,7 +190,7 @@
done
-text{*Expression evaluation is functional, or deterministic*}
+text\<open>Expression evaluation is functional, or deterministic\<close>
theorem single_valued_eval: "single_valued eval"
apply (unfold single_valued_def)
apply (intro allI, rule impI)
@@ -204,14 +204,14 @@
lemma eval_N_E [dest!]: "(N n, s) -|-> (v, s') ==> (v = n & s' = s)"
by (induct e == "N n" s v s' set: eval) simp_all
-text{*This theorem says that "WHILE TRUE DO c" cannot terminate*}
+text\<open>This theorem says that "WHILE TRUE DO c" cannot terminate\<close>
lemma while_true_E:
"(c', s) -[eval]-> t ==> c' = WHILE (N 0) DO c ==> False"
by (induct set: exec) auto
-subsection{* Equivalence of IF e THEN c;;(WHILE e DO c) ELSE SKIP and
- WHILE e DO c *}
+subsection\<open>Equivalence of IF e THEN c;;(WHILE e DO c) ELSE SKIP and
+ WHILE e DO c\<close>
lemma while_if1:
"(c',s) -[eval]-> t
@@ -233,8 +233,8 @@
-subsection{* Equivalence of (IF e THEN c1 ELSE c2);;c
- and IF e THEN (c1;;c) ELSE (c2;;c) *}
+subsection\<open>Equivalence of (IF e THEN c1 ELSE c2);;c
+ and IF e THEN (c1;;c) ELSE (c2;;c)\<close>
lemma if_semi1:
"(c',s) -[eval]-> t
@@ -254,9 +254,9 @@
-subsection{* Equivalence of VALOF c1 RESULTIS (VALOF c2 RESULTIS e)
+subsection\<open>Equivalence of VALOF c1 RESULTIS (VALOF c2 RESULTIS e)
and VALOF c1;;c2 RESULTIS e
- *}
+\<close>
lemma valof_valof1:
"(e',s) -|-> (v,s')
@@ -276,7 +276,7 @@
by (blast intro: valof_valof1 valof_valof2)
-subsection{* Equivalence of VALOF SKIP RESULTIS e and e *}
+subsection\<open>Equivalence of VALOF SKIP RESULTIS e and e\<close>
lemma valof_skip1:
"(e',s) -|-> (v,s')
@@ -293,7 +293,7 @@
by (blast intro: valof_skip1 valof_skip2)
-subsection{* Equivalence of VALOF x:=e RESULTIS x and e *}
+subsection\<open>Equivalence of VALOF x:=e RESULTIS x and e\<close>
lemma valof_assign1:
"(e',s) -|-> (v,s'')