# HG changeset patch # User nipkow # Date 778343119 -7200 # Node ID 47be9d22a0d69a2ebaf6b702fe68e672ce8e3301 # Parent 41bf53133ba66b55a6d272df225f228758401836 Renamed a few types and vars diff -r 41bf53133ba6 -r 47be9d22a0d6 IMP/Denotation.thy --- a/IMP/Denotation.thy Wed Aug 31 15:15:54 1994 +0200 +++ b/IMP/Denotation.thy Wed Aug 31 16:25:19 1994 +0200 @@ -1,4 +1,4 @@ -(* Title: ZF/IMP/Denotation.thy +(* Title: HOL/IMP/Denotation.thy ID: $Id$ Author: Heiko Loetzbeyer & Robert Sandner, TUM Copyright 1994 TUM @@ -9,26 +9,26 @@ Denotation = Com + consts - A :: "aexp => env => nat" - B :: "bexp => env => bool" - C :: "com => (env*env)set" - Gamma :: "[bexp,com,(env*env)set] => (env*env)set" + A :: "aexp => state => nat" + B :: "bexp => state => bool" + C :: "com => (state*state)set" + Gamma :: "[bexp,com,(state*state)set] => (state*state)set" rules - A_nat_def "A(N(n)) == (%sigma. n)" - A_loc_def "A(X(x)) == (%sigma. sigma(x))" - A_op1_def "A(Op1(f,a)) == (%sigma. f(A(a,sigma)))" - A_op2_def "A(Op2(f,a0,a1)) == (%sigma. f(A(a0,sigma),A(a1,sigma)))" + A_nat_def "A(N(n)) == (%s. n)" + A_loc_def "A(X(x)) == (%s. s(x))" + A_op1_def "A(Op1(f,a)) == (%s. f(A(a,s)))" + A_op2_def "A(Op2(f,a0,a1)) == (%s. f(A(a0,s),A(a1,s)))" - B_true_def "B(true) == (%sigma. True)" - B_false_def "B(false) == (%sigma. False)" - B_op_def "B(ROp(f,a0,a1)) == (%sigma. f(A(a0,sigma),A(a1,sigma)))" + B_true_def "B(true) == (%s. True)" + B_false_def "B(false) == (%s. False)" + B_op_def "B(ROp(f,a0,a1)) == (%s. f(A(a0,s),A(a1,s)))" - B_not_def "B(noti(b)) == (%sigma. ~B(b,sigma))" - B_and_def "B(b0 andi b1) == (%sigma. B(b0,sigma) & B(b1,sigma))" - B_or_def "B(b0 ori b1) == (%sigma. B(b0,sigma) | B(b1,sigma))" + B_not_def "B(noti(b)) == (%s. ~B(b,s))" + B_and_def "B(b0 andi b1) == (%s. B(b0,s) & B(b1,s))" + B_or_def "B(b0 ori b1) == (%s. B(b0,s) | B(b1,s))" C_skip_def "C(skip) == id" C_assign_def "C(x := a) == {io . snd(io) = fst(io)[A(a,fst(io))/x]}" diff -r 41bf53133ba6 -r 47be9d22a0d6 IMP/Equiv.ML --- a/IMP/Equiv.ML Wed Aug 31 15:15:54 1994 +0200 +++ b/IMP/Equiv.ML Wed Aug 31 16:25:19 1994 +0200 @@ -1,10 +1,10 @@ -(* Title: ZF/IMP/Equiv.ML +(* Title: HOL/IMP/Equiv.ML ID: $Id$ Author: Heiko Loetzbeyer & Robert Sandner, TUM Copyright 1994 TUM *) -goal Equiv.thy "( -a-> n) = (A(a,sigma) = n)"; +goal Equiv.thy "( -a-> n) = (A(a,s) = n)"; by (res_inst_tac [("x","n")] spec 1); (* quantify n *) by (aexp.induct_tac "a" 1); (* struct. ind. *) by (rewrite_goals_tac A_rewrite_rules); (* rewr. Den. *) @@ -16,7 +16,7 @@ val aexp2 = aexp_iff RS iffD2; -goal Equiv.thy "( -b-> w) = (B(b,sigma) = w)"; +goal Equiv.thy "( -b-> w) = (B(b,s) = w)"; by (res_inst_tac [("x","w")] spec 1); (* quantify w *) by (bexp.induct_tac "b" 1); (* struct. ind. *) by (rewrite_goals_tac B_rewrite_rules); (* rewr. Den. *) @@ -34,7 +34,7 @@ val BfstD = read_instantiate_sg (sign_of Equiv.thy) [("P","%x.B(?b,x)")] (fst_conv RS subst); -goal Equiv.thy "!!c. -c-> sigma' ==> : C(c)"; +goal Equiv.thy "!!c. -c-> t ==> : C(c)"; (* start with rule induction *) be (evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1; @@ -60,7 +60,7 @@ val com_cs = comp_cs addSIs [aexp2,bexp2] addIs evalc.intrs; -goal Equiv.thy "!x:C(c). -c-> snd(x)"; +goal Equiv.thy "!io:C(c). -c-> snd(io)"; by (com.induct_tac "c" 1); by (rewrite_tac C_rewrite_rules); by (safe_tac com_cs); diff -r 41bf53133ba6 -r 47be9d22a0d6 IMP/Equiv.thy --- a/IMP/Equiv.thy Wed Aug 31 15:15:54 1994 +0200 +++ b/IMP/Equiv.thy Wed Aug 31 16:25:19 1994 +0200 @@ -1,4 +1,4 @@ -(* Title: ZF/IMP/Equiv.thy +(* Title: HOL/IMP/Equiv.thy ID: $Id$ Author: Heiko Loetzbeyer & Robert Sandner, TUM Copyright 1994 TUM diff -r 41bf53133ba6 -r 47be9d22a0d6 IMP/ROOT.ML --- a/IMP/ROOT.ML Wed Aug 31 15:15:54 1994 +0200 +++ b/IMP/ROOT.ML Wed Aug 31 16:25:19 1994 +0200 @@ -1,4 +1,4 @@ -(* Title: ZF/IMP/ROOT.ML +(* Title: HOL/IMP/ROOT.ML ID: $Id$ Author: Heiko Loetzbeyer & Robert Sandner, TUM Copyright 1994 TUM @@ -12,9 +12,9 @@ *) -ZF_build_completed; (*Make examples fail if ZF did*) +HOL_build_completed; (*Make examples fail if HOL did*) -writeln"Root file for ZF/IMP"; +writeln"Root file for HOL/IMP"; proof_timing := true; loadpath := [".","IMP"]; time_use_thy "Equiv";