converting ex/If to Isar script
authorpaulson
Fri Aug 15 13:45:39 2003 +0200 (2003-08-15)
changeset 14151b8bb6a6a2c46
parent 14150 9a23e4eb5eb3
child 14152 12f6f18e7afc
converting ex/If to Isar script
src/FOL/IsaMakefile
src/FOL/ex/If.ML
src/FOL/ex/If.thy
     1.1 --- a/src/FOL/IsaMakefile	Fri Aug 15 13:07:01 2003 +0200
     1.2 +++ b/src/FOL/IsaMakefile	Fri Aug 15 13:45:39 2003 +0200
     1.3 @@ -42,7 +42,7 @@
     1.4  
     1.5  FOL-ex: FOL $(LOG)/FOL-ex.gz
     1.6  
     1.7 -$(LOG)/FOL-ex.gz: $(OUT)/FOL ex/First_Order_Logic.thy ex/If.ML		\
     1.8 +$(LOG)/FOL-ex.gz: $(OUT)/FOL ex/First_Order_Logic.thy \
     1.9    ex/If.thy ex/IffOracle.ML ex/IffOracle.thy ex/List.ML ex/List.thy	\
    1.10    ex/Nat.ML ex/Nat.thy ex/Nat2.ML ex/Nat2.thy ex/Natural_Numbers.thy	\
    1.11    ex/Prolog.ML ex/Prolog.thy ex/ROOT.ML ex/cla.ML ex/document/root.tex	\
     2.1 --- a/src/FOL/ex/If.ML	Fri Aug 15 13:07:01 2003 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,59 +0,0 @@
     2.4 -(*  Title:      FOL/ex/If.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 -    Copyright   1991  University of Cambridge
     2.8 -
     2.9 -First-Order Logic: the 'if' example.
    2.10 -*)
    2.11 -
    2.12 -open Cla;    (*in case structure IntPr is open!*)
    2.13 -
    2.14 -val prems = Goalw [if_def]
    2.15 -    "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)";
    2.16 -by (blast_tac (claset() addIs prems) 1);
    2.17 -qed "ifI";
    2.18 -
    2.19 -val major::prems = Goalw [if_def]
    2.20 -   "[| if(P,Q,R);  [| P; Q |] ==> S; [| ~P; R |] ==> S |] ==> S";
    2.21 -by (cut_facts_tac [major] 1);
    2.22 -by (blast_tac (claset() addIs prems) 1);
    2.23 -qed "ifE";
    2.24 -
    2.25 -
    2.26 -Goal "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))";
    2.27 -by (rtac iffI 1);
    2.28 -by (etac ifE 1);
    2.29 -by (etac ifE 1);
    2.30 -by (rtac ifI 1);
    2.31 -by (rtac ifI 1);
    2.32 -
    2.33 -choplev 0;
    2.34 -AddSIs [ifI];
    2.35 -AddSEs [ifE];
    2.36 -by (Blast_tac 1);
    2.37 -qed "if_commute";
    2.38 -
    2.39 -
    2.40 -Goal "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";
    2.41 -by (Blast_tac 1);
    2.42 -qed "nested_ifs";
    2.43 -
    2.44 -choplev 0;
    2.45 -by (rewtac if_def);
    2.46 -by (blast_tac FOL_cs 1);
    2.47 -qed "";
    2.48 -
    2.49 -
    2.50 -(*An invalid formula.  High-level rules permit a simpler diagnosis*)
    2.51 -Goal "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))";
    2.52 -by (Blast_tac 1) handle ERROR => writeln"Failed, as expected";
    2.53 -(*Check that subgoals remain: proof failed.*)
    2.54 -getgoal 1; 
    2.55 -by (REPEAT (Step_tac 1));
    2.56 -
    2.57 -choplev 0;
    2.58 -by (rewtac if_def);
    2.59 -by (blast_tac FOL_cs 1) handle ERROR => writeln"Failed, as expected";
    2.60 -(*Check that subgoals remain: proof failed.*)
    2.61 -getgoal 1; 
    2.62 -by (REPEAT (step_tac FOL_cs 1));
     3.1 --- a/src/FOL/ex/If.thy	Fri Aug 15 13:07:01 2003 +0200
     3.2 +++ b/src/FOL/ex/If.thy	Fri Aug 15 13:45:39 2003 +0200
     3.3 @@ -1,5 +1,64 @@
     3.4 -If = FOL +
     3.5 -consts  if     :: [o,o,o]=>o
     3.6 -rules
     3.7 -        if_def "if(P,Q,R) == P&Q | ~P&R"
     3.8 +(*  Title:      FOL/ex/If.ML
     3.9 +    ID:         $Id$
    3.10 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    3.11 +    Copyright   1991  University of Cambridge
    3.12 +
    3.13 +First-Order Logic: the 'if' example.
    3.14 +*)
    3.15 +
    3.16 +theory If = FOL:
    3.17 +
    3.18 +constdefs
    3.19 +  if :: "[o,o,o]=>o"
    3.20 +   "if(P,Q,R) == P&Q | ~P&R"
    3.21 +
    3.22 +lemma ifI:
    3.23 +    "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)"
    3.24 +apply (simp add: if_def, blast)
    3.25 +done
    3.26 +
    3.27 +lemma ifE:
    3.28 +   "[| if(P,Q,R);  [| P; Q |] ==> S; [| ~P; R |] ==> S |] ==> S"
    3.29 +apply (simp add: if_def, blast)
    3.30 +done
    3.31 +
    3.32 +lemma if_commute: "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
    3.33 +apply (rule iffI)
    3.34 +apply (erule ifE)
    3.35 +apply (erule ifE)
    3.36 +apply (rule ifI)
    3.37 +apply (rule ifI)
    3.38 +oops
    3.39 +
    3.40 +text{*Trying again from the beginning in order to use @{text blast}*}
    3.41 +declare ifI [intro!]
    3.42 +declare ifE [elim!]
    3.43 +
    3.44 +lemma if_commute: "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
    3.45 +by blast
    3.46 +
    3.47 +
    3.48 +lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"
    3.49 +by blast
    3.50 +
    3.51 +text{*Trying again from the beginning in order to prove from the definitions*}
    3.52 +lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"
    3.53 +by (simp add: if_def, blast)
    3.54 +
    3.55 +
    3.56 +text{*An invalid formula.  High-level rules permit a simpler diagnosis*}
    3.57 +lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))"
    3.58 +apply auto
    3.59 +(*The next step will fail unless subgoals remain*)
    3.60 +apply (tactic all_tac)
    3.61 +oops
    3.62 +
    3.63 +text{*Trying again from the beginning in order to prove from the definitions*}
    3.64 +lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))"
    3.65 +apply (simp add: if_def, auto) 
    3.66 +(*The next step will fail unless subgoals remain*)
    3.67 +apply (tactic all_tac)
    3.68 +oops
    3.69 +
    3.70 +
    3.71  end