src/HOLCF/IOA/ex/TrivEx.ML
author wenzelm
Thu Nov 15 23:25:46 2001 +0100 (2001-11-15)
changeset 12218 6597093b77e7
parent 8600 a466c687c726
child 13524 604d0f3622d6
permissions -rw-r--r--
GPLed;
mueller@6470
     1
(*  Title:      HOLCF/IOA/TrivEx.thy
mueller@6470
     2
    ID:         $Id$
wenzelm@12218
     3
    Author:     Olaf Müller
wenzelm@12218
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
mueller@6470
     5
wenzelm@12218
     6
Trivial Abstraction Example.
mueller@6470
     7
*)
mueller@6470
     8
mueller@6470
     9
val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
mueller@6470
    10
  by (fast_tac (claset() addDs prems) 1);
mueller@6470
    11
qed "imp_conj_lemma";
mueller@6470
    12
mueller@6470
    13
mueller@6470
    14
Goalw [is_abstraction_def] 
mueller@6470
    15
"is_abstraction h_abs C_ioa A_ioa";
mueller@6470
    16
by (rtac conjI 1);
mueller@6470
    17
(* ------------- start states ------------ *)
mueller@6470
    18
by (simp_tac (simpset() addsimps 
mueller@6470
    19
    [h_abs_def,starts_of_def,C_ioa_def,A_ioa_def]) 1);
mueller@6470
    20
(* -------------- step case ---------------- *)
mueller@6470
    21
by (REPEAT (rtac allI 1));
mueller@6470
    22
by (rtac imp_conj_lemma 1);
mueller@6470
    23
by (simp_tac (simpset() addsimps [trans_of_def,
mueller@6470
    24
        C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1);
nipkow@8600
    25
by (induct_tac "a" 1);
mueller@6470
    26
by (simp_tac (simpset() addsimps [h_abs_def]) 1);
mueller@6470
    27
qed"h_abs_is_abstraction";
mueller@6470
    28
mueller@6470
    29
mueller@6470
    30
Goal "validIOA C_ioa (<>[] <%(n,a,m). n~=0>)";
mueller@6470
    31
by (rtac AbsRuleT1 1);
mueller@6470
    32
by (rtac h_abs_is_abstraction 1);
mueller@6470
    33
by (rtac MC_result 1);
mueller@6470
    34
by (abstraction_tac 1);
mueller@6470
    35
by (asm_full_simp_tac (simpset() addsimps [h_abs_def]) 1);
mueller@6470
    36
qed"TrivEx_abstraction";
mueller@6470
    37
mueller@6470
    38