Null program and a few new results
authorpaulson
Wed Aug 05 18:21:37 1998 +0200 (1998-08-05)
changeset 525986d80749453f
parent 5258 d1c0504d6c42
child 5260 1835a591d3a7
Null program and a few new results
src/HOL/UNITY/Union.ML
src/HOL/UNITY/Union.thy
     1.1 --- a/src/HOL/UNITY/Union.ML	Wed Aug 05 18:21:09 1998 +0200
     1.2 +++ b/src/HOL/UNITY/Union.ML	Wed Aug 05 18:21:37 1998 +0200
     1.3 @@ -115,3 +115,37 @@
     1.4  by (asm_simp_tac (simpset() addsimps [Join_def, ensures_stable_Un2]) 1);
     1.5  qed "ensures_stable_Join2";
     1.6  
     1.7 +
     1.8 +(** Theoretical issues **)
     1.9 +
    1.10 +Goalw [Join_def] "Join prgF prgG = Join prgG prgF";
    1.11 +by (simp_tac (simpset() addsimps [Un_commute, Int_commute]) 1);
    1.12 +qed "Join_commute";
    1.13 +
    1.14 +Goalw [Join_def] "Join (Join prgF prgG) prgH = Join prgF (Join prgG prgH)";
    1.15 +by (simp_tac (simpset() addsimps [Un_assoc, Int_assoc]) 1);
    1.16 +qed "Join_assoc";
    1.17 +
    1.18 +(**NOT PROVABLE because no "surjective pairing" for records
    1.19 +Goalw [Join_def, Null_def] "id: Acts prgF ==> Join prgF Null = prgF";
    1.20 +by (asm_simp_tac (simpset() addsimps [insert_absorb]) 1);
    1.21 +qed "Join_Null";
    1.22 +*)
    1.23 +
    1.24 +(**NOT PROVABLE because no "surjective pairing" for records
    1.25 +Goalw [Join_def] "Join prgF prgF = prgF";
    1.26 +auto();
    1.27 +qed "Join_absorb";
    1.28 +*)
    1.29 +
    1.30 +
    1.31 +(*
    1.32 +val field_defs = thms"program.field_defs";
    1.33 +val dest_defs = thms"program.dest_defs";
    1.34 +val dest_convs = thms"program.dest_convs";
    1.35 +
    1.36 +val update_defs = thms"program.update_defs";
    1.37 +val make_defs = thms"program.make_defs";
    1.38 +val update_convs = thms"program.update_convs";
    1.39 +val simps = thms"program.simps";
    1.40 +*)
     2.1 --- a/src/HOL/UNITY/Union.thy	Wed Aug 05 18:21:09 1998 +0200
     2.2 +++ b/src/HOL/UNITY/Union.thy	Wed Aug 05 18:21:37 1998 +0200
     2.3 @@ -12,8 +12,11 @@
     2.4  
     2.5  constdefs
     2.6  
     2.7 -   Join :: "['a program, 'a program] => 'a program"
     2.8 +   Join :: ['a program, 'a program] => 'a program
     2.9      "Join prgF prgG == (|Init = Init prgF Int Init prgG,
    2.10  			 Acts = Acts prgF Un Acts prgG|)"
    2.11  
    2.12 +   Null :: 'a program
    2.13 +    "Null == (|Init = UNIV, Acts = {id}|)"
    2.14 +
    2.15  end