src/HOL/Isar_examples/ExprCompiler.thy
changeset 11809 c9ffdd63dd93
parent 10007 64bf7da1994a
child 13524 604d0f3622d6
     1.1 --- a/src/HOL/Isar_examples/ExprCompiler.thy	Tue Oct 16 17:56:12 2001 +0200
     1.2 +++ b/src/HOL/Isar_examples/ExprCompiler.thy	Tue Oct 16 17:58:13 2001 +0200
     1.3 @@ -114,15 +114,15 @@
     1.4  lemma exec_append:
     1.5    "ALL stack. exec (xs @ ys) stack env =
     1.6      exec ys (exec xs stack env) env" (is "?P xs")
     1.7 -proof (induct ?P xs type: list)
     1.8 +proof (induct xs)
     1.9    show "?P []" by simp
    1.10 -
    1.11 -  fix x xs assume "?P xs"
    1.12 -  show "?P (x # xs)" (is "?Q x")
    1.13 -  proof (induct ?Q x type: instr)
    1.14 -    show "!!val. ?Q (Const val)" by (simp!)
    1.15 -    show "!!adr. ?Q (Load adr)" by (simp!)
    1.16 -    show "!!fun. ?Q (Apply fun)" by (simp!)
    1.17 +next
    1.18 +  fix x xs assume hyp: "?P xs"
    1.19 +  show "?P (x # xs)"
    1.20 +  proof (induct x)
    1.21 +    from hyp show "!!val. ?P (Const val # xs)" by simp
    1.22 +    from hyp show "!!adr. ?P (Load adr # xs)" by simp
    1.23 +    from hyp show "!!fun. ?P (Apply fun # xs)" by simp
    1.24    qed
    1.25  qed
    1.26  
    1.27 @@ -130,10 +130,10 @@
    1.28  proof -
    1.29    have "ALL stack. exec (compile e) stack env =
    1.30      eval e env # stack" (is "?P e")
    1.31 -  proof (induct ?P e type: expr)
    1.32 +  proof (induct e)
    1.33      show "!!adr. ?P (Variable adr)" by simp
    1.34      show "!!val. ?P (Constant val)" by simp
    1.35 -    show "!!fun e1 e2. (?P e1 ==> ?P e2 ==> ?P (Binop fun e1 e2))"
    1.36 +    show "!!fun e1 e2. ?P e1 ==> ?P e2 ==> ?P (Binop fun e1 e2)"
    1.37        by (simp add: exec_append)
    1.38    qed
    1.39    thus ?thesis by (simp add: execute_def)
    1.40 @@ -151,7 +151,7 @@
    1.41  lemma exec_append:
    1.42    "ALL stack. exec (xs @ ys) stack env
    1.43      = exec ys (exec xs stack env) env" (is "?P xs")
    1.44 -proof (induct ?P xs)
    1.45 +proof (induct xs)
    1.46    show "?P []" (is "ALL s. ?Q s")
    1.47    proof
    1.48      fix s have "exec ([] @ ys) s env = exec ys s env" by simp