src/HOL/IMP/Star.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45265 521508e85c0d
child 50054 6da283e4497b
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     1
theory Star imports Main
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     2
begin
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     3
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     4
inductive
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     5
  star :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     6
for r where
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     7
refl:  "star r x x" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     8
step:  "r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     9
45265
521508e85c0d tuned names to avoid shadowing
nipkow
parents: 45015
diff changeset
    10
hide_fact (open) refl step  --"names too generic"
521508e85c0d tuned names to avoid shadowing
nipkow
parents: 45015
diff changeset
    11
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    12
lemma star_trans:
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    13
  "star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 43141
diff changeset
    14
proof(induction rule: star.induct)
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    15
  case refl thus ?case .
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    16
next
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    17
  case step thus ?case by (metis star.step)
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    18
qed
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    19
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    20
lemmas star_induct = star.induct[of "r:: 'a*'b \<Rightarrow> 'a*'b \<Rightarrow> bool", split_format(complete)]
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    21
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    22
declare star.refl[simp,intro]
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    23
45265
521508e85c0d tuned names to avoid shadowing
nipkow
parents: 45015
diff changeset
    24
lemma star_step1[simp, intro]: "r x y \<Longrightarrow> star r x y"
521508e85c0d tuned names to avoid shadowing
nipkow
parents: 45015
diff changeset
    25
by(metis star.refl star.step)
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    26
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    27
code_pred star .
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    28
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    29
end